Will the Myhill–Nerode theorem be formalized in Lean mathlib by the end of 2024?
8
130Ṁ961
resolved Dec 31
Resolved
NO

There's a pumping lemma but Myhill–Nerode is conspicuously missing.

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Computability/DFA.html#DFA.pumping_lemma

Resolves YES if it's available in master before market close.

Math
The Lean Theorem Prover
Get
Ṁ1,000
to start trading!

🏅 Top traders

#NameTotal profit
1Ṁ277
2Ṁ255
3Ṁ2

People are also trading

Which theorems will be formally proven in Lean by the end of 2028?
What tactic will prove the most mathlib lemmas at the end of 2026?
Will rw_search be able to replace >50% of mathlib proofs by 2025-11-26?
19% chance
Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?
41% chance
Will LLMs be able to formally verify non-trivial programs by the end of 2025?
30% chance
Will fermats last theorem be formalized in lean down to the axiom in 5 years.
49% chance
Will we have a formalized proof of the Modularity theorem by 2029-05-01?
65% chance
Will we have a formalized proof of Fermat's last theorem by 2029-05-01?
70% chance
Will Kevin Buzzard successfully fulfill his grant specs of formalizing Fermat's Last Theorem in Lean within 5 years?
56% chance
Will Terence Tao write a paper with Lean code in it during the 2026 calendar year?
79% chance
Sort by:

You can follow along here: https://github.com/leanprover-community/mathlib4/pull/11311

bought Ṁ200 YES

@tfae planning to go on vacation? 😉

@kiudee No, but there are only a handful of maintainers that can merge the PR, and they might.

bought Ṁ8 YES

Interestingly, someone was working on a proof of the theorem here:
https://github.com/atarnoam/lean-automata/blob/main/src/regular_languages.lean

People are also trading

Which theorems will be formally proven in Lean by the end of 2028?
What tactic will prove the most mathlib lemmas at the end of 2026?
Will rw_search be able to replace >50% of mathlib proofs by 2025-11-26?
19% chance
Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?
41% chance
Will LLMs be able to formally verify non-trivial programs by the end of 2025?
30% chance
Will fermats last theorem be formalized in lean down to the axiom in 5 years.
49% chance
Will we have a formalized proof of the Modularity theorem by 2029-05-01?
65% chance
Will we have a formalized proof of Fermat's last theorem by 2029-05-01?
70% chance
Will Kevin Buzzard successfully fulfill his grant specs of formalizing Fermat's Last Theorem in Lean within 5 years?
56% chance
Will Terence Tao write a paper with Lean code in it during the 2026 calendar year?
79% chance
© Manifold Markets, Inc.•Terms•Privacy