Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?
Standard
17
Ṁ4932025
40%
chance
1D
1W
1M
ALL
Sometime around the resolution date, I will write a script that samples random tactic-mode lemmas from mathlib, and replaces the proof of those lemmas with an invocation of aesop.
Resolves YES if aesop successfully proves >50% of the lemmas.
Get
1,000and
1.00
1,0001.00Sort by:
You will use aesop without any arguments or additional configuration (besides what is given in mathlib)?
Related questions
Related questions
Will rw_search be able to replace >50% of mathlib proofs by 2025-11-26?
19% chance
Will an AI get bronze or silver on any International Math Olympiad by end of 2025?
79% chance
Will any AI be able to explain formal language proofs to >=50% of IMO problems by the start of 2025?
48% chance
Will AIs be widely recognized as having developed a new, innovative, foundational mathematical theory before 2030?
31% chance
Will an AI solve any important mathematical conjecture before January 1st, 2030?
76% chance
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)
71% chance
Will an AI model write the proof to the Riemann Hypothesis by the end of 2025?
10% chance
Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?
69% chance
Will reinforcement learning overtake LMs on math before 2028?
63% chance
Will AIs be widely recognized as having developed a new, innovative, foundational mathematical theory before 2035?
41% chance