Will rw_search be able to replace >50% of mathlib proofs by 2025-11-26?
Basic
9
Ṁ280Nov 26
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 achieve >85% performance on the FrontierMath benchmark before 2027?
65% chance
Will an AI achieve >30% performance on the FrontierMath benchmark before 2026?
88% chance
Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?
41% chance
Will Alphaproof achieve >30% performance on the FrontierMath benchmark before 2026?
35% chance
Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?
66% chance
Will Complexity theory in mathlib be mostly lambda-calculus based on 2025-02-17?
63% chance
Will reinforcement learning overtake LMs on math before 2028?
70% chance
Will ZFC no longer be the standard foundation for mathematics by 2050?
33% chance
Will we have a formalized proof of Fermat's last theorem by 2029-05-01?
74% chance
Will AI contribute as much as a co-author would today to a real research mathematics paper before Jan 1 2026?
58% chance