Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?
Plus
21
Ṁ3828resolved Nov 27
Resolved
NO1D
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,000 play money
🏅 Top traders
| # | Name | Total profit |
|---|---|---|
| 1 | Ṁ543 | |
| 2 | Ṁ84 | |
| 3 | Ṁ66 | |
| 4 | Ṁ49 | |
| 5 | Ṁ32 |
Sort by:
You will use aesop without any arguments or additional configuration (besides what is given in mathlib)?
Related questions
Related questions
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)
75% chance
AI outperforms humans in all mathematical research areas by 2028?
10% chance
Will Alphaproof achieve >30% performance on the FrontierMath benchmark before 2026?
8% chance
Will an AI model write the proof to the Riemann Hypothesis by the end of 2025?
1% chance
What tactic will prove the most mathlib lemmas at the end of 2026?
Will the best public LLM at the end of 2025 solve more than 5 of the first 10 Project Euler problems published in 2026?
66% chance
Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?
60% chance
Will AIs be widely recognized as having developed a new, innovative, foundational mathematical theory before 2035?
37% chance
Will an AI achieve >80% performance on the FrontierMath benchmark before 2027?
44% chance
Will an AI achieve >85% performance on the FrontierMath benchmark before 2027?
38% chance