What tactic will prove the most mathlib lemmas at the end of 2026? | Manifold

What tactic will prove the most mathlib lemmas at the end of 2026?

Basic

7

Ṁ702

2027

2%

simp

38%

aesop

2%

rw_search

1.7%

sorry

4%

duper

52%

Other

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.

#️ Technology

#The Lean Theorem Prover

Get

1,000

and

3.00

Sort by:

Depending on the setup exact? will get a 100% success rate. How will you prevent that?

By "prove", is it ok if there are warnings? Because I know of a tactic that has a 100% success rate 😉

@tfae screw the innuendo, I'm going all in on sorry

@tfae Lol.

But no. Feel free to ask more questions about what counts as proof, but sorry does not count.

@BoltonBailey it was still worth it for the meme

Related questions

Will the Myhill–Nerode theorem be formalized in Lean mathlib by the end of 2024?

Will any AI be able to explain formal language proofs to >=50% of IMO problems by the start of 2025?

Will reinforcement learning overtake LMs on math before 2028?

Will the best public LLM at the end of 2025 solve more than 5 of the first 10 Project Euler problems published in 2026?

Will a Large Language Model prove an important math theorem by end of 2024?

Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?

Will an LLM be able to solve confusing but elementary geometric reasoning problems in 2024? (strict LLM version)

Will any AI be able to formalize >=90% of IMO problems by the start of 2025?

Which theorem prover will have proved the most theorems on Freek's list by end of 2025?

Will an AI solve any important mathematical conjecture before January 1st, 2030?

Related questions

Will the Myhill–Nerode theorem be formalized in Lean mathlib by the end of 2024?

Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?

Will any AI be able to explain formal language proofs to >=50% of IMO problems by the start of 2025?

Will an LLM be able to solve confusing but elementary geometric reasoning problems in 2024? (strict LLM version)

Will reinforcement learning overtake LMs on math before 2028?

Will any AI be able to formalize >=90% of IMO problems by the start of 2025?

Will the best public LLM at the end of 2025 solve more than 5 of the first 10 Project Euler problems published in 2026?

Which theorem prover will have proved the most theorems on Freek's list by end of 2025?

Will a Large Language Model prove an important math theorem by end of 2024?

Will an AI solve any important mathematical conjecture before January 1st, 2030?

© Manifold Markets, Inc.•Terms + Mana-only Terms•Privacy•Rules