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

3

50

Ṁ83Ṁ110

Dec 31

68%

chance

1D

1W

1M

ALL

Amount

Ṁ1

Ṁ10

Ṁ100

Payout if YES

Ṁ14 +45%

New probability

70% +3%

There's a pumping lemma but Myhill–Nerode is conspicuously missing.

Resolves YES if it's available in master before market close.

Get Ṁ1,000 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

How many digits of pi will be calculated by in February 2024 at City of London School?

Greatest Mathematician of all time

Will we have a formalized proof of Fermat's last theorem by 2029-05-01?

55% chance

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

54% chance