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.

Market context

The Lean Theorem Prover

Get

1,000

to start trading!

🏅 Top traders

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

People are also trading

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

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

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

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

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 Kevin Buzzard successfully fulfill his grant specs of formalizing Fermat's Last Theorem in Lean within 5 years?

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

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

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

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

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

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

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

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

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 Kevin Buzzard successfully fulfill his grant specs of formalizing Fermat's Last Theorem in Lean within 5 years?

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

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

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

Related questions

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

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

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

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

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 Kevin Buzzard successfully fulfill his grant specs of formalizing Fermat's Last Theorem in Lean within 5 years?

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

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

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

© Manifold Markets, Inc.•Terms•Privacy