Will the Myhill–Nerode theorem be formalized in Lean mathlib by the end of 2024?
8
130Ṁ961
resolved Dec 31
Resolved
NO

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.

Math
The Lean Theorem Prover
Get
Ṁ1,000
to start trading!

🏅 Top traders

#NameTotal profit
1Ṁ277
2Ṁ255
3Ṁ2

People are also trading

Will rw_search be able to replace >50% of mathlib proofs by 2025-11-26?
19% chance
Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?
14% chance
Which theorems will be formally proven in Lean by the end of 2028?
Will reinforcement learning overtake LMs on math before 2028?
63% chance
What tactic will prove the most mathlib lemmas at the end of 2026?
Will LLMs be able to formally verify non-trivial programs by the end of 2025?
21% chance
Which theorem prover will have proved the most theorems on Freek's list by end of 2025?
Will fermats last theorem be formalized in lean down to the axiom in 5 years.
54% chance
Will a standardized category theory language for ML models emerge by end of 2025?
3% chance
Will we have a formalized proof of the Modularity theorem by 2029-05-01?
74% chance
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 rw_search be able to replace >50% of mathlib proofs by 2025-11-26?
19% chance
Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?
14% chance
Which theorems will be formally proven in Lean by the end of 2028?
Will reinforcement learning overtake LMs on math before 2028?
63% chance
What tactic will prove the most mathlib lemmas at the end of 2026?
Will LLMs be able to formally verify non-trivial programs by the end of 2025?
21% chance
Which theorem prover will have proved the most theorems on Freek's list by end of 2025?
Will fermats last theorem be formalized in lean down to the axiom in 5 years.
54% chance
Will a standardized category theory language for ML models emerge by end of 2025?
3% chance
Will we have a formalized proof of the Modularity theorem by 2029-05-01?
74% chance
© Manifold Markets, Inc.•Terms•Privacy