Will the Myhill–Nerode theorem be formalized in Lean mathlib by the end of 2024?
6
63
Ṁ254Ṁ130
Dec 31
89%
chance
1D
1W
1M
ALL
There's a pumping lemma but Myhill–Nerode is conspicuously missing.
Resolves YES if it's available in master before market close.
Get Ṁ200 play money
Sort by:
Interestingly, someone was working on a proof of the theorem here:
https://github.com/atarnoam/lean-automata/blob/main/src/regular_languages.lean
Related questions
Will we have a formalized proof of the Modularity theorem by 2029-05-01?
60% chance
Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?
65% chance
Will Kevin Buzzard successfully formalize Fermat's Last Theorem in Lean within his 5 year grant?
66% chance
Will a Millenium problem be formally stated in a theorem prover by 2025
59% chance
When will we have a fully formalized proof of the Poincare Conjecture?
Will we have a formalized proof of Fermat's last theorem by 2029-05-01?
59% chance
Will a Large Language Model prove an important math theorem by end of 2024?
9% chance
Will Terence Tao write a paper with Lean code in it during the 2026 calendar year?
74% chance
Will Complexity theory in mathlib be mostly lambda-calculus based on 2025-02-17?
63% chance
Will Lean mathlib have a definition of graph minors by the end of 2024?
80% chance