Lean formalizations and related articles
More projects are on GitHub. During my studies, I have often encountered errors and missing details in the literature and textbooks. As something of a perfectionist, I find this especially frustrating: I care deeply about complete, rigorous, and logically sound arguments. This is what led me to begin using formal verification tools such as Lean. I use LLMs and Lean formalization extensively in all of the repositories below. I do not claim to fully understand all of the mathematical content they contain, and I am acutely aware that verification in Lean is not the same as human understanding. I value mathematics that humans can understand, and at present, LLM-generated proofs are generally not readable mathematics. For each repository, I therefore try to digest the result myself and write an article that presents the proof—or at least summarizes the main idea of the AI-generated argument—in a form that a human can readily follow. This takes time, so I appreciate your patience if you are interested in any of the results below.
partial-balayage-lean
Formalizes fifteen weak-type bounds using two partial balayage principles, covering Riesz and Beurling transforms, full and traceless Hessians, Leray and gradient projections, centred intervals and Euclidean balls, and Poisson and heat maximal operators.
Two partial balayage principles for weak-type estimates
· PDF
FluidSingularSets
Studies the interior singular set of unforced three-dimensional suitable weak Navier–Stokes solutions. Proves Hausdorff nullity for logarithmic gauges at every finite iteration depth and the local upper parabolic box-dimension bound 25/23.
odd-zeta-irrationality
Apéry proved $$\zeta(3)$$ irrational in 1979. For larger odd arguments no single value is known to be irrational; what can be proved is that some member of a finite list must be. Formalizes two such statements, following Zudilin's higher-derivative hypergeometric construction: at least one of $$\zeta(7),\zeta(9),\dots,\zeta(21)$$ is irrational, and at least one of $$\zeta(9),\zeta(11),\dots,\zeta(33)$$.
erdos455-convex-primes
Erdős Problem #455 asks whether a convex sequence of primes $$q_0\lt q_1\lt\cdots$$, one with non-decreasing gaps, must satisfy $$q_n/n^2\to\infty$$. Richter (1976) proved $$\liminf q_n/n^2\ge 0.352$$. Proves $$\liminf q_n/n^2 \gt 0.864289$$, from a max-plus certificate whose roughly $$5\cdot 10^{10}$$ elementary operations are evaluated by the Lean kernel.
erdos5-limit-points
Erdős Problem #5 asks whether every positive real is a limit point of the normalised prime gaps $$(p_{n+1}-p_n)/\log n$$. Merikoski (2020) showed that this limit-point set has the four-point property, which forces lower density $$\ge 1/3$$. Proves that every set with the four-point property has lower density $$\ge 25/74 = 1/3 + 1/222$$, so $$1/3$$ is not asymptotically sharp.
FavardLength
The Favard length of a planar set is its average projection length. For the four-corner Cantor approximants $$K_n$$ it tends to $$0$$, and $$\alpha_{\mathrm{Fav}}$$ is the decay exponent: the supremum of the $$a$$ with $$\mathrm{Fav}(K_n)\le C n^{-a}$$. Nazarov–Peres–Volberg (2010) proved $$\alpha_{\mathrm{Fav}}\ge 1/6$$ and C. Marshall (2026) $$\ge 1/5$$; Bateman–Volberg (2010) give $$\alpha_{\mathrm{Fav}}\le 1$$. Proves $$\alpha_{\mathrm{Fav}}\ge 1/4$$, from Marshall's combinatorics in endpoint form plus a joint negative moment of the low-frequency product.
falconer-packing
For a planar Borel set $$E$$, write $$d=\dim_H E$$ and let $$\Delta_y(E)$$ be the set of distances from $$y$$ to points of $$E$$. Proves $$|\Delta_y(E)|\gt0$$ for some $$y\in E$$ when $$1\lt d\le5/4$$ and $$\dim_P E\lt B_{\mathrm H}(d)$$, using only standard axioms.
centered-maximal-constant
$$c_2$$ is the least $$C$$ with $$\alpha\,\lvert\{Mf\gt\alpha\}\rvert\le C\lVert f\rVert_1$$ for the centred Hardy–Littlewood maximal operator over squares in the plane. The best known bounds were $$1.6212\le c_2\le 4$$, from Aldaz (2000) and the covering argument. Proves $$1.6855\le c_2\le 3.879$$. For Euclidean balls, also proves $$c_2^{\mathrm{ball}}\le e$$ and $$c_n^{\mathrm{ball}}\le(n/2)^{n/(n-2)}$$ for $$n\ge3$$.
expository note
c2 < 4 (PDF)
BerryEsseen
$$C$$ is the least constant with $$\sup_x\lvert F_n(x)-\Phi(x)\rvert\le C\beta/\sqrt n$$ for the
distribution function $$F_n$$ of a normalized sum of $$n$$ i.i.d. variables with third absolute
moment $$\beta$$. Esseen (1956): $$C\ge 0.4097$$; best published upper bound $$0.4690$$ (Shevtsova, 2013).
Proves $$0.4\le C\le 0.423$$ in Lean, with the help of native_decide.
NKBesicovitch
An $$(n,k)$$-Besicovitch set contains a unit $$k$$-disk in every $$k$$-direction of $$\mathbb{R}^n$$; conjecturally it has positive volume when $$2\le k\lt n$$. Oberlin (2010): positive volume when $$n\lt(1+\sqrt2)^{k-1}+k$$, and $$\dim_H E\ge n-(n-k)/(1+\sqrt2)^k$$. Proves both with $$1+\sqrt2\approx 2.4142$$ replaced by $$p_c\approx 2.4812$$, the root in $$(2,3)$$ of $$p^3-2p^2-2p+2$$.
Besicovitchs-1-2
$$\sigma_1(X)$$ is the least $$\beta$$ forcing every set of finite length in $$X$$ with lower density $$\ge\beta$$ a.e. to be countably $$1$$-rectifiable; Besicovitch conjectured $$\sigma_1(\mathbb{R}^2)=\tfrac12$$. In the plane the upper bound fell from $$1-10^{-2576}$$ (Besicovitch, 1928) to $$3/4$$ (Besicovitch, 1938), then $$(2+\sqrt{46})/12=0.73186$$ (Preiss–Tišer, 1992), $$0.72655$$ (Schechter, 1998) and $$0.7$$ (De Lellis et al., 2024). Proves $$\sigma_1(H)\le 0.6934$$ for every real Hilbert space $$H$$, and $$\tfrac12\le\sigma_1(\mathbb{R}^2)$$.
progress report
New Progress on Besicovitch’s 1/2 Problem (PDF)
Papers and preprints
Optimal Sparse Bounds and Commutator Characterizations Without Doubling
preprint arXiv:2510.26505