What tactic will prove the most mathlib lemmas at the end of 2026?
Mini
7
Ṁ7022027
1D
1W
1M
ALL
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.
Get
1,000and
1.00
1,0001.00Sort 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 we have a formalized proof of Fermat's last theorem by 2029-05-01?
72% chance
Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?
41% chance
Will the Myhill–Nerode theorem be formalized in Lean mathlib by the end of 2024?
87% chance
Will an LLM be able to solve confusing but elementary geometric reasoning problems in 2024? (strict LLM version)
25% chance
Will any AI be able to explain formal language proofs to >=50% of IMO problems by the start of 2025?
60% chance
Will reinforcement learning overtake LMs on math before 2028?
63% chance
Will Lean mathlib have a definition of graph minors by the end of 2024?
58% 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?
58% chance
Will any AI be able to formalize >=90% of IMO problems by the start of 2025?
17% chance
Will an AI solve any important mathematical conjecture before January 1st, 2030?
78% chance