Büchi's problem

Exercise · buchi_false_M0

The case $M = 0$ fails: the hypothesis is vacuous, so $a = 0$ cannot be concluded.

Formal statement · Lean 4.lean

theorem buchi_false_M0 : ¬ IsBuchi 0 := by
  sorry

Proof. sorry

Nobody has tried yet.