Will the Myhill–Nerode theorem be formalized in Lean mathlib by the end of 2024?
Basic
6
Ṁ254Dec 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.
This question is managed and resolved by Manifold.
Get
1,000and
3.00
1,0003.00Sort 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
Related questions
Will Lean mathlib have a definition of graph minors by the end of 2024?
80% chance
Will Complexity theory in mathlib be mostly lambda-calculus based on 2025-02-17?
63% chance
Will we have a formalized proof of the Modularity theorem by 2029-05-01?
59% chance
Will we have a formalized proof of Fermat's last theorem by 2029-05-01?
65% chance
Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?
40% chance
Will fermats last theorem be formalized in lean down to the axiom in 5 years.
39% chance
Will any AI be able to explain formal language proofs to >=50% of IMO problems by the start of 2025?
60% chance
What tactic will prove the most mathlib lemmas at the end of 2026?
Will reinforcement learning overtake LMs on math before 2028?
63% chance
Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?
69% chance