Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?
Plus
18
Ṁ4982025
41%
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.
This question is managed and resolved by Manifold.
Get
1,000and
3.00
1,0003.00Sort by:
You will use aesop without any arguments or additional configuration (besides what is given in mathlib)?
Related questions
Related questions
Will an AI achieve >85% performance on the FrontierMath benchmark before 2028?
70% chance
Will any AI be able to explain formal language proofs to >=50% of IMO problems by the start of 2025?
48% chance
Will the Myhill–Nerode theorem be formalized in Lean mathlib by the end of 2024?
69% chance
Will rw_search be able to replace >50% of mathlib proofs by 2025-11-26?
19% chance
Will an AI achieve >85% performance on the FrontierMath benchmark before 2027?
62% chance
Will AIs be widely recognized as having developed a new, innovative, foundational mathematical theory before 2030?
32% chance
Will any AI be able to formalize >=90% of IMO problems by the start of 2025?
17% 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?
5% chance
Will an AI solve any important mathematical conjecture before January 1st, 2030?
78% chance
Will Alphaproof achieve >30% performance on the FrontierMath benchmark before 2026?
34% chance