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.
Blog
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.
Purple Square Atlas: a visual application of Burnside’s lemma
Six geometric tiles, 336 rotation classes, and a next step toward musical composition.
The Ouroboros Problem
Why circular reasoning quietly erases the predictive value of AI agents that do science, how the same loop turns a proof into a null result, and how to build agents that cannot cheat.
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.
Mathematics Is Larger Than Its Current Culture
A response to “A Severe Misalignment of AI in Mathematics”: solving problems fast and understanding deeply are not opposites.
First transmission
A signal test from the space between code and cosmos.