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.
#News
The beauty of cancellation
Colored beads, disappearing tableaux, and a visual journey into the Lean-checked height-two theorem of Cho and Huh.
Two new papers on Parikh matrices, and a theorem checked in Lean
Four diagonals determine the Parikh matrix of a word whose letters occur at most twice; plus rigidity, ranges and a golden-ratio threshold for words with repeated letters.
A new preprint on ternary Parikh matrices
Exact counting formulas for words with repeated letters, connecting Parikh matrices, integer partitions and numerical semigroups.
Counting Melodies revision 2: from rhythms to Young diagrams
A revised manuscript, an interactive rhythm laboratory, and preserved editions of my 2005 and 2006 mathematical work.