Will an AI be able to convert recent mathematical results into a fully formal proofs that can be verified by a mainstream proof assistant by 2025?

39

1kṀ8327

resolved Jan 2

Resolved

NO

1H

6H

1D

1W

1M

ALL

Definitions used:

Under "AI" I consider any fully autonomous computer program that is not given any human input other than the mathematic
Under "recent mathematical results" I consider novel mathematical results that have been published during or after 2010.
Under "fully formal proof" I consider a sequence of proof steps written in a formal mathematical logic such as CIC or ZFC.
Under "mainstream proof assistant" I consider languages such as Isabelle/HOL, Coq, or Lean.

This question will resolve to YES if such an AI can translate and verify at least five recent mathematical results that had not previously been verified in a proof assistant before the start of 2025, and will otherwise resolve to NO.

Get

1,000

to start trading!

🏅 Top traders

#	Name	Total profit
1		Ṁ460
2		Ṁ264
3		Ṁ244
4		Ṁ173
5		Ṁ112

People are also trading

Will AI be capable of producing an Annals-quality math paper for $100k by March 2030?

Will an AI achieve >85% performance on the FrontierMath benchmark before 2028?

In 2029, will any AI be able to take an arbitrary proof in the mathematical literature and translate it into a form suitable for symbolic verification? (Gary Marcus benchmark #5)

Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?

Will an AI model write the proof to the Riemann Hypothesis by the end of 2025?

Will natural language based proof assistants be in common use by 2026?

By 2030, AI can autonomously prove mathematical theorems that are publishable in mathematics journals today?

Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?

Will an AI implement a full infinity-topos mathematical framework by end of 2025?

Will AIs be widely recognized as having developed a new, innovative, foundational mathematical theory before 2035?

Related questions

Will AI be capable of producing an Annals-quality math paper for $100k by March 2030?

Will an AI achieve >85% performance on the FrontierMath benchmark before 2028?

In 2029, will any AI be able to take an arbitrary proof in the mathematical literature and translate it into a form suitable for symbolic verification? (Gary Marcus benchmark #5)

Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?

Will an AI model write the proof to the Riemann Hypothesis by the end of 2025?

Will natural language based proof assistants be in common use by 2026?

By 2030, AI can autonomously prove mathematical theorems that are publishable in mathematics journals today?

Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?

Will an AI implement a full infinity-topos mathematical framework by end of 2025?

Will AIs be widely recognized as having developed a new, innovative, foundational mathematical theory before 2035?

© Manifold Markets, Inc.•Terms•Privacy