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

8

Ṁ130Ṁ961

resolved Dec 31

Resolved

NO

1H

6H

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.

The Lean Theorem Prover

Get

1,000

to start trading!

🏅 Top traders

#	Trader	Total profit
1		Ṁ277
2		Ṁ255
3		Ṁ2

People are also trading

Which theorems will be officially formally proven in Lean by the end of 2028?

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

Will Lean mathlib contain more than 10 million lines of code by 2030?

Will any of Levent Alpöge’s mathematical results with Claude be proven flawed by the end of the year?

ZK tool for demonstrating one has proved math theorem (in Lean) created by EOY2026?

Will Terence Tao write a paper with Lean code in it during the 2026 calendar year?

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

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

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?

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

People are also trading

Which theorems will be officially formally proven in Lean by the end of 2028?

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

Will Lean mathlib contain more than 10 million lines of code by 2030?

Will any of Levent Alpöge’s mathematical results with Claude be proven flawed by the end of the year?

ZK tool for demonstrating one has proved math theorem (in Lean) created by EOY2026?

Will Terence Tao write a paper with Lean code in it during the 2026 calendar year?

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

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

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?

Related questions

Which theorems will be officially formally proven in Lean by the end of 2028?

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

Will Lean mathlib contain more than 10 million lines of code by 2030?

Will any of Levent Alpöge’s mathematical results with Claude be proven flawed by the end of the year?

ZK tool for demonstrating one has proved math theorem (in Lean) created by EOY2026?

Will Terence Tao write a paper with Lean code in it during the 2026 calendar year?

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

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

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?