What tactic will prove the most mathlib lemmas at the end of 2026?
Basic
7
Ṁ7022027
2%
simp
38%
aesop
2%
rw_search
1.7%
sorry
4%
duper
52%
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 a single tactic. This market resolves to whichever tactic of the ones provided as answers proves the biggest fraction of lemmas.
This question is managed and resolved by Manifold.
Get
1,000
and3.00
Sort by:
By "prove", is it ok if there are warnings? Because I know of a tactic that has a 100% success rate 😉
@tfae Lol.
But no. Feel free to ask more questions about what counts as proof, but sorry does not count.
Related questions
Related questions
Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?
40% chance
Will reinforcement learning overtake LMs on math before 2028?
63% 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 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 an AI solve any important mathematical conjecture before January 1st, 2030?
76% chance
Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?
69% chance
Will we have a formalized proof of Fermat's last theorem by 2029-05-01?
65% chance
Will an LLM be able to solve confusing but elementary geometric reasoning problems in 2024? (strict LLM version)
14% chance
Will the Myhill–Nerode theorem be formalized in Lean mathlib by the end of 2024?
89% chance
Will rw_search be able to replace >50% of mathlib proofs by 2025-11-26?
19% chance