Will the Myhill–Nerode theorem be formalized in Lean mathlib by the end of 2024?
3
50
110
Dec 31
68%
chance

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.

Get Ṁ1,000 play money
Sort by:
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