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

7

Ṁ813

Dec 31

87%

chance

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 we have a formalized proof of Fermat's last theorem by 2029-05-01?

Will Lean mathlib have a definition of graph minors by the end of 2024?

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.

Will any AI be able to formalize >=90% of IMO problems by the start of 2025?

Will any AI be able to explain formal language proofs to >=50% of IMO problems by the start of 2025?

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?

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

Will reinforcement learning overtake LMs on math before 2028?

Related questions

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

Will any AI be able to explain formal language proofs to >=50% of IMO problems by the start of 2025?

Will Lean mathlib have a definition of graph minors by the end of 2024?

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.

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

Will any AI be able to formalize >=90% of IMO problems by the start of 2025?

Will reinforcement learning overtake LMs on math before 2028?

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