Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?
16
48
Ṁ444Ṁ310
2025
42%
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 Ṁ200 play money
Sort by:
bought Ṁ40 of NO
You will use aesop without any arguments or additional configuration (besides what is given in mathlib)?
More related questions
Related questions
Will any AI be able to explain formal language proofs to >=50% of IMO problems by the start of 2025?
63% chance
Will an AI solve any important mathematical conjecture before January 1st, 2030?
68% chance
Will natural language based proof assistants be in common use by 2026?
35% chance
Will AIs be widely recognized as having developed a new, innovative, foundational mathematical theory before 2030?
42% chance
Will any AI be able to formalize >=90% of IMO problems by the start of 2025?
32% chance
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?
23% 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)
39% chance
Will we have a formalized proof of Fermat's last theorem by 2029-05-01?
59% chance
Will any language model trained without large number arithmetic be able to generalize to large number arithmetic by 2026?
69% chance
Will an AI co-author a mathematics research paper published in a reputable journal before the end of 2026?
59% chance