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?
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?
39% chance
What tactic will prove the most mathlib lemmas at the end of 2026?
Will LLMs be able to formally verify non-trivial programs by the end of 2025?
27% 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?
74% chance
Will we have a formalized proof of Fermat's last theorem by 2029-05-01?
72% 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?
82% 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?
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?
39% chance
What tactic will prove the most mathlib lemmas at the end of 2026?
Will LLMs be able to formally verify non-trivial programs by the end of 2025?
27% 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?
74% chance
Will we have a formalized proof of Fermat's last theorem by 2029-05-01?
72% 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?
82% chance
© Manifold Markets, Inc.•Terms•Privacy