In late 2025, I stopped reviewing every line of code proposed by Claude Code; I switched my focus to planning, scaffolding and guardrails instead. I was amused by stories of vibe coders overwhelmed by thousands of lines of code.

Fast forward a year later, and I find myself in the same position.

I read about efforts to formalize mathematics in Lean this summer, and thought it was a noble cause worthy of my tokens. I contributed to Tau Ceti and registered a few theorems on Palomar. Formalizing Clark-Ocone felt like coming full circle; I first came across the theorem while writing my Master’s dissertation.

Inspiration to tackle unsolved problems came when Dr. Shanmu Jin, a neurosurgery resident, proved Crouzeix’s conjecture. Amusingly, this was around the time Jarred Sumner made progress on the Riemann hypothesis by telling the model “believe in yourself”. I enjoyed Hilbert spaces as an undergraduate, so I started looking for problems in the area.

The problem I settled on was the Hlawka inequality for Schatten p-norms. Think of it as a cousin of the triangle inequality, but with three matrices instead of two vectors and the Schatten p-norm instead of lengths.

Working with Astra and Fable, I was able to prove the existence of a bound. With considerably more effort and a lot more hand-holding, we got to an elegant proof of the exact bound. The cyclic family attains the bound for diagonal matrices and all p ≥ 256.

I’m now creating resources to help myself and others understand the 9,000-line proof. As I do this, I think about professional and hobbyist mathematicians working on similar projects, their lines of Lean code ever growing.

How does one keep up when we can produce proofs faster than we can understand them?

human-written Mathlib vs AI-written Tau Ceti