What tactic will prove the most mathlib lemmas at the end of 2026?
7
310Ṁ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.

Get
Ṁ1,000
to start trading!
© Manifold Markets, Inc.TermsPrivacy