All of the lean code was written by LLMs under my watch. 

My skill files for lean projects are available here and I have written a blog post explaining how to do it. My current setup (as of Oct 5 2026) is to use Opus 5.5 (xhigh) as orchestrator, and have the code mostly written by Sonnet, Luna-xhigh and Sol-low subagents.

Github repositories of Lean formalizations

 

Formalizations of my own papers:

 

  • AVAnomalousDiffusion (with Vlad Vicol). A formalization of our paper on anomalous diffusion by iterative quantitative homogenization. Github | Palomar 
  • CoarseGraining (with Tuomo Kuusi). A formalization, based on this paper, of coarse-graining theory for elliptic equations, including quenched homogenization estimates for isotropic random media. (There is also a decent amount of elliptic regularity theory formalized in this repo: Schauder & Calderon-Zygmund estimates, etc). Github | Palomar
  • CoarseDeGiorgi (with B. Avelin, T. Kuusi and A. Turpeinen). A complete formalization of our joint paper which extends the theory of De Giorgi-Nash-Moser to elliptic equations with symmetric coefficients which are possibly degenerate and unbounded but satisfy a coarse ellipticity condition. This applies to coefficients with possibly negative Besov regularity, under conditions on the exponents which are shown to be sharp. Github | Palomar
  • GMCExplicitDelta (with Ahmed Bou-Rabee and Tuomo Kuusi). Built on top of subdiffusive-process. The arguments of our paper are perturbative in disorder strength \delta and the results hold only when this \delta is small enough. The paper and its lean formalization prove that such a threshold exists without computing it. This repository computes this \delta explicitly for the coarse-graining cascade estimate at the heart of the renormalization argument: it holds for \delta \leq 0.366 in d=2, \delta \leq 0.188 in d=3 and \delta \leq 0.156 in d=4, with explicit constants. The numerical inequalities are checked by the Lean kernel. (The thresholds in the main theorems of the paper use further steps and are not yet explicit.) Github
  • HighContrastHomogenization (with Tuomo Kuusi and Amélie Loher). A formalization of our paper proving that the scale at which homogenization occurs is at most a power of the ellipticity ratio for stationary random coefficient fields with a finite range of dependence. Github | Palomar
  • subdiffusive-process (with A. Bou-Rabee and Tuomo Kuusi). A complete formalization of our joint paper proving an anomalous scaling limit of a Brownian particle in a log-correlated potential. Github | Palomar
  • Superdiffusion (with Tuomo Kuusi). A complete formalization of our paper (joint with Ahmed Bou-Rabee) on power-law superdiffusion and anomalous elliptic regularity for a diffusion process in a random, multiscale divergence-free drift. Github | Palomar
  • SuperdiffusionCLT. A complete formalization of our paper (joint with Tuomo Kuusi and Ahmed Bou-Rabee) proving a \sqrt{\log t}-type superdiffusion and superdiffusive central limit theorem for a Brownian motion in a critically-correlated random divergence-free drift. Github | Palomar
PDE & Fluids:
  •  
  • A-free-measures. A complete formalization of the paper of De Philippis and Rindler (Ann. of Math. 2016) on the structure of \mathcal{A}-free measures: if \mathcal{A}\mu = 0, then at almost every point of the singular part of \mu, the polar of \mu lies in the wave cone of \mathcal{A}. This is proved for operators of every order, with variable coefficients and with a measure on the right-hand side, together with all the applications in the paper: Alberti’s rank-one theorem, the structure of BD functions, the dimensional structure of normal currents, the converse of Rademacher’s theorem and the absolute continuity of top-dimensional metric currents. The results the paper cites from Alberti–Marchese, Schioppa and the Ambrosio–Kirchheim theory of metric currents are proved here, as far as the proofs need them, rather than assumed. Github
  • CaffarelliKohnNirenberg (with Vlad Vicol). Formalizes the Caffarelli–Kohn–Nirenberg partial regularity theorem for the three-dimensional incompressible Navier–Stokes equations: the singular set of a suitable weak solution has zero one-dimensional parabolic Hausdorff measure. Includes two \varepsilon-regularity criteria and allows forcing locally in L^q for q > 5/2. An accompanying manuscript presents the proof. Github | Palomar
  • CIVAxisymmetric (with Vlad Vicol). A formalization of the paper by Constantin, Ignatova and Vicol on the regularity of asymptotically axisymmetric solutions to the 3D Navier-Stokes equations with analytic forcing. This paper shows that the blow-up solution with smooth forcing term constructed by OpenAI cannot be improved to an analytic forcing term. Github | Palomar  
  • DeGiorgi (with Julia Kempe). Formalizes De Giorgi–Nash–Moser theory for uniformly elliptic divergence-form equations with bounded measurable coefficients: local boundedness, weak and strong Harnack inequalities, and Hölder regularity. Includes supporting developments in Sobolev spaces and weak derivatives. This was the first major PDE theorem formalized so I keep this repo in the list for historical reasons, but the code is not pretty and I do not suggest building on top of it. In particular a much better formulation of De Giorgi-Nash-Moser is found in the repo EllipticRegularityLean below.  Github
  • EllipticRegularityLean (with Tuomo Kuusi and Amélie Loher). A formalization of regularity theory of divergence-form elliptic and parabolic equations with measurable coefficients. It covers the isoperimetric, Sobolev and trace inequalities; harmonic functions and the monotonicity formulas of Almgren and Alt–Caffarelli–Friedman; Schauder and Calderón–Zygmund estimates, with an application to Yudovich uniqueness for the 2D Euler equations; the Meyers estimate, De Giorgi–Nash–Moser theory and the Harnack inequality, with sharp exponents and Green function bounds; and the parabolic Harnack inequality and Nash–Aronson bounds. Github
  • EscauriazaSereginSverak. Formalizes the Escauriaza-Seregin-Šverák and Ladyzhenskaya-Prodi-Serrin regularity theorems for the three-dimensional incompressible Navier–Stokes equations: Leray–Hopf solutions satisfying the critical space-time integrability conditions are smooth at positive times and unique. Includes the supporting Carleman inequalities, unique continuation and backward uniqueness. An accompanying manuscript presents the proofs. Github | Palomar
  • hoermander-rothschild-stein (with Amélie Loher). Hörmander’s theory of hypoellipticity, and the Rothschild–Stein theory: lifting to homogeneous groups, fundamental solutions, and sharp Sobolev and Hölder estimates for sums of squares of vector fields, with Baker-Campbell-Hausdorff, Chow-Rashevskii and the Nagel-Stein-Wainger ball-box theorem. We also prove sharp Gaussian heat kernel bounds on Carnot groups. Github | Palomar
Mathematical Physics & Probability:

 

  • BKARForestFormula. Formalizes the Brydges–Kennedy–Abdesselam–Rivasseau forest interpolation formula for smooth functions, expressing a fully coupled quantity as a sum of integrals indexed by forests, as stated for example in Abdesselam and Rivasseau. This is a fundamental tool for cluster expansions used in constructive field theory. Github | Palomar
  • balaban-lean (in progress). An attempted formalization, not yet finished, of Balaban’s renormalization group analysis of the classical O(N) spin model at low temperature in dimensions d \geq 3, which includes the classical Heisenberg model. It follows Balaban’s papers from 1995–1999, the last two with O’Carroll. The two main theorems, a multiscale expansion of the generating function and the low-temperature correlation functions of Balaban and O’Carroll, are stated in Lean but not yet proved. The repository keeps a progress page and a list of the open mathematical issues. Github
  • Critical2DKPZ. A formalization of this paper by Berger, Caravenna, Clark, Dunlap, Gu, Liu, Nakajima, Sun, Tsai, Xie and Zygouras. The centered logarithms of the partition functions of directed polymers on \mathbb{Z}^2 at critical disorder converge to a random distribution, which they call the critical 2D KPZ process. The paper proves a comparison principle and shows that, for flat initial data, the process is Gaussian at small scales, has a covariance kernel behaving like \log\log(1/|z|), is neither a signed measure nor Gaussian, is invariant under translations and rotations and covariant under scaling, and that its tested laws are of Ehrhard type. The results from the literature that the proofs use, on the critical 2D stochastic heat flow and elsewhere, are formalized as well. The repository also proves four new properties of the process, written up in a short note: strict skewness, twice differentiable dependence on the initial condition, Brownian motion across scales, and a Gaussian free field tangent. Github | Palomar
  • DOZZ (with Amélie Loher). Formalization of the theorem of Kupiainen, Rhodes and Vargas that the three-point structure constants of Liouville conformal field theory on the Riemann sphere, defined probabilistically through the Gaussian free field and Gaussian multiplicative chaos, are given by the formula conjectured by Dorn and Otto and by Zamolodchikov and Zamolodchikov (DOZZ). Github | Palomar
  • Frohlich-Spencer (with Amélie Loher). Formalization of three papers of Fröhlich & Spencer on phase transitions in lattice systems with an abelian symmetry and on localization: the Kosterlitz–Thouless transition (1981), massless phases of lattice gauge theories and spin systems (1982), and the absence of diffusion in the Anderson model (1983). The two-dimensional multiscale analysis follows the finite-volume presentation of Kharash and Peled. Github | Palomar
  • LiebThirring (with Amélie Loher). Formalization of non-relativistic Coulomb matter in three dimensions: stability of matter, Lieb’s ionization bound, the thermodynamic limit and the Thomas–Fermi limit. Github | Palomar
  • MarkovProcess. Constructs continuous-path strong Markov processes from conservative Feller semigroups satisfying a Kolmogorov moment condition, with existence and uniqueness for every starting point. Includes killed processes, exit laws, Dynkin’s formula, optional stopping, and Feynman–Kac semigroups for bounded potentials.  Github | Palomar
  • RegularityStructures. Formalization of Hairer’s convergence theorem for the dynamical \Phi^4_3 model (A theory of regularity structures, Theorem 1.15). For smooth initial data, the solutions of \partial_t u = \Delta u - u^3 + au + \xi on the three-dimensional torus, with the space-time white noise \xi mollified and the mass suitably renormalized, converge in probability up to the maximal existence time of the limit, and the limit does not depend on the mollifier. The general theory is formalized along the way, in the semigroup formulation of Hoshino: the reconstruction theorem, the multilevel Schauder estimate, and maximal solutions with the blow-up alternative. Github | Palomar