Full technical article: a verified tableau injection
Download the illustrated 11-page PDF explaining our Lean formalization of Cho–Huh’s established height-two theorem, with counterexamples and exact proof scope.
#Formal verification
The beauty of cancellation
Colored beads, disappearing tableaux, and a visual journey into the Lean-checked height-two theorem of Cho and Huh.