Will the Myhill–Nerode theorem be formalized in Lean mathlib by the end of 2024? | Manifold

Will the Myhill–Nerode theorem be formalized in Lean mathlib by the end of 2024?

Basic

8

Ṁ961

resolved Dec 31

Resolved

NO

1D

1W

1M

ALL

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.

This question is managed and resolved by Manifold.

#The Lean Theorem Prover

Get

1,000

and

3.00

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

Related questions

Will Complexity theory in mathlib be mostly lambda-calculus based on 2025-02-17?

Will we have a formalized proof of the Modularity theorem by 2029-05-01?

Will we have a formalized proof of Fermat's last theorem by 2029-05-01?

Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?

Will Kevin Buzzard successfully fulfill his grant specs of formalizing Fermat's Last Theorem in Lean within 5 years?

Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?

Will fermats last theorem be formalized in lean down to the axiom in 5 years.

What tactic will prove the most mathlib lemmas at the end of 2026?

Will reinforcement learning overtake LMs on math before 2028?

Will rw_search be able to replace >50% of mathlib proofs by 2025-11-26?

Related questions

Will Complexity theory in mathlib be mostly lambda-calculus based on 2025-02-17?

Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?

Will we have a formalized proof of the Modularity theorem by 2029-05-01?

Will fermats last theorem be formalized in lean down to the axiom in 5 years.

Will we have a formalized proof of Fermat's last theorem by 2029-05-01?

What tactic will prove the most mathlib lemmas at the end of 2026?

Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?

Will reinforcement learning overtake LMs on math before 2028?

Will Kevin Buzzard successfully fulfill his grant specs of formalizing Fermat's Last Theorem in Lean within 5 years?

Will rw_search be able to replace >50% of mathlib proofs by 2025-11-26?

© Manifold Markets, Inc.•Terms + Mana-only Terms•Privacy•Rules