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?

8

335Ṁ793

2027

1.7%

simp

7%

aesop

1.7%

rw_search

1.6%

sorry

4%

duper

40%

grind

44%

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.

Market context

The Lean Theorem Prover

Get

1,000

to start trading!

People are also trading

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 theorems will be officially formally proven in Lean by the end of 2028?

Will reinforcement learning overtake LMs on math before 2028?

ZK tool for demonstrating one has proved math theorem (in Lean) created by EOY2026?

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

Will Lean mathlib contain more than 10 million lines of code by 2030?

Status of the Wentworth-Lorell conjecture in 2026

Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?

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

Biggest formal math library in 2040 HoTT-based?

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

People are also trading

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 theorems will be officially formally proven in Lean by the end of 2028?

Will reinforcement learning overtake LMs on math before 2028?

ZK tool for demonstrating one has proved math theorem (in Lean) created by EOY2026?

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

Will Lean mathlib contain more than 10 million lines of code by 2030?

Status of the Wentworth-Lorell conjecture in 2026

Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?

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

Biggest formal math library in 2040 HoTT-based?

Related questions

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 theorems will be officially formally proven in Lean by the end of 2028?

Will reinforcement learning overtake LMs on math before 2028?

ZK tool for demonstrating one has proved math theorem (in Lean) created by EOY2026?

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

Will Lean mathlib contain more than 10 million lines of code by 2030?

Status of the Wentworth-Lorell conjecture in 2026

Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?

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

Biggest formal math library in 2040 HoTT-based?

© Manifold Markets, Inc.•Terms•Privacy