Will rw_search be able to replace >50% of mathlib proofs by 2025-11-26?
Basic
9
Ṁ2802025
19%
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 rw_search.
Resolves YES if rw_search successfully proves >50% of the lemmas.
This question is managed and resolved by Manifold.
Get
1,000and
3.00
1,0003.00Related questions
Related questions
Will an AI model write the proof to the Riemann Hypothesis by the end of 2025?
8% chance
Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?
40% 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 majority of mathematicians rely on formal computer proof assistants before the end of 2040?
69% 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 we have a formalized proof of Fermat's last theorem by 2029-05-01?
65% chance
Will reinforcement learning overtake LMs on math before 2028?
63% 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?
10% chance
Will the best public LLM at the end of 2025 solve more than 5 of the first 10 Project Euler problems published in 2026?
42% chance
Will ZFC no longer be the standard foundation for mathematics by 2050?
33% chance