![](/_next/image?url=https%3A%2F%2Fstorage.googleapis.com%2Fmantic-markets.appspot.com%2Fcontract-images%2Ftfae%252Fc3cad8bfbca6.jpg&w=3840&q=75)
Will the Myhill–Nerode theorem be formalized in Lean mathlib by the end of 2024?
Mini
6
Ṁ254Dec 31
89%
chance
1D
1W
1M
ALL
There's a pumping lemma but Myhill–Nerode is conspicuously missing.
Resolves YES if it's available in master before market close.
Get Ṁ600 play money
Sort by:
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
Related questions
Will an AI be able to convert recent mathematical results into a fully formal proofs that can be verified by a mainstream proof assistant by 2025?
24% chance
Will we have a formalized proof of Fermat's last theorem by 2029-05-01?
71% chance
In 2029, will any AI be able to take an arbitrary proof in the mathematical literature and translate it into a form suitable for symbolic verification? (Gary Marcus benchmark #5)
55% chance
Will Lean mathlib have a definition of graph minors by the end of 2024?
80% chance
Will we have a formalized proof of the Modularity theorem by 2029-05-01?
59% chance
Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?
40% chance
Will Kevin Buzzard successfully formalize Fermat's Last Theorem in Lean within his 5 year grant?
81% chance
Will Fermat's last theorem be formalized before AI gets IMO gold?
25% chance
What tactic will prove the most mathlib lemmas at the end of 2026?
Will Complexity theory in mathlib be mostly lambda-calculus based on 2025-02-17?
63% chance