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

Ṁ893

Dec 31

69%

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 any AI be able to explain formal language proofs to >=50% of IMO problems by the start of 2025?

-12% 1d48% chance

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 any AI be able to formalize >=90% of IMO problems by the start of 2025?

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.

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 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.

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 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