Research notes, visual explanations, and ideas in progress.
KLS history, recent breakthroughs, and a Lean formalization, from the earlier bound 500 to an October 9 release with a universal Poincaré constant at most 15.
On Proof, Understanding, and Artificial Intelligence
From photon interference and the permanent to hafnians, including my results on both uniform hiding and local anticoncentration.
From chess and AI coding to scientific discovery: why verification matters, what Lean checks, and how I would organize research with AI and formal proofs.
A PDF, an overnight argument, and two days learning the geometry behind a problem that had resisted me for months.
From the lowest-hanging Erdős problems to research at machine speed—and the question of what theoretical researchers should value next.