Lean formalization
I have been working on formalizing mathematics in the Lean 4 proof assistant, building on Mathlib. Each project below comes with a blueprint: a self-contained mathematical document in which every definition and result is linked to its Lean counterpart. In both projects every proof is checked by Lean, no declaration uses sorry, and the main theorems depend only on Lean’s three standard axioms.
Projects:
Short-time existence for higher-order parabolic equations on manifolds
Repository : here
Companion paper / blueprint : here
Description: A formalization, with a companion paper, of a theorem that geometric analysis uses constantly and rarely proves. Let (M, g) be a closed Riemannian manifold, V a tensor bundle over M, and consider a fully nonlinear equation ∂tu = F(t, u, ∇u, ..., ∇2pu) of any even order 2p which is parabolic at a smooth initial datum u0, in the sense of the Legendre condition on its linearization. Then (A) there is a smooth solution on M × [0,T] for some T > 0, (B) it is unique among parabolic solutions, and (C) it depends continuously on u0 in C∞. All three are proved in Lean, along with the existence of maximal solutions.
This covers the quasilinear equations of Mantegazza–Martinazzi (Ann. SNS Pisa, 2012), whose result is also formalized as a corollary, as well as polyharmonic map flows of every order, the Ricci–DeTurck flow, and parabolic Monge–Ampère equations. The proof is arranged for formalization: it avoids trace, interpolation and fractional Sobolev spaces, Fourier analysis, and linear theory with non-smooth coefficients, obtaining regularity from the implicit function theorem via Angenent’s parameter trick.
The Complete Mathematical Works of Theodore J. Kaczynski, formalized in Lean 4
Repository : here
Blueprint : here
Errata : here
Description: A formalization of every published mathematical paper of Theodore J. Kaczynski (1964–1969), together with his doctoral dissertation Boundary Functions (Michigan, 1967). Most of these works concern the boundary behavior of functions in the disk and the half-plane; the first is a new group-theoretic proof of Wedderburn’s theorem. The project has about 22,400 lines of Lean, and all 21 pinned headline theorems are proved. These include McMillan’s Fσδ theorem and its generalization to cluster sets, the realization of every Fσδ subset of the line as a set of curvilinear convergence (answering a problem of McMillan), Baire class results for boundary functions, a bounded harmonic function whose boundary function is not of Baire class 1 (answering a problem of Bagemihl and Piranian), a non-Borel set of curvilinear convergence in a cube, and Sutcliffe’s digit-reversal conjecture.
Results the papers quote from the literature (the crosscut theorem, Tietze’s arc theorem, Banach’s theorem on Baire classes, Bagemihl’s ambiguous-point theorem, and others) are proved in the project as well, while the full Jordan curve theorem and Kierst’s theorem are avoided by direct arguments. The errata record the places where the published proofs needed a correction. The blueprint and the formalization were written by Claude, Anthropic’s AI model, orchestrating Lean-writing agents under my direction.