All missions

Motivation

How densely can equal disks be packed in the plane? The hexagonal arrangement, with centers on the triangular lattice, covers a fraction $\pi/(2\sqrt3)\approx0.9069$ of the plane, and Thue's theorem says no packing does better. In 2003 Cohn and Elkies introduced a linear programming bound for sphere packing: a single auxiliary function whose values are nonpositive outside a ball and whose Fourier transform is nonnegative certifies an upper bound on packing density. Viazovska (dimension 8) and Cohn, Kumar, Miller, Radchenko and Viazovska (dimension 24) found auxiliary functions for which the bound is sharp, solving sphere packing in those dimensions. Cohn and Elkies conjectured that a sharp function exists also in dimension 2 (Conjecture 7.3 of their paper). The planar packing problem itself is classical; the question here is whether the Fourier method certifies it exactly.

Timeline

• 1890s–1940s. Thue's theorem on optimality of the hexagonal circle packing; an elementary proof based on an idea of Rogers is presented by Hales (2000).
• 2003. Cohn and Elkies introduce the linear programming bound and conjecture sharp auxiliary functions in dimensions 2, 8 and 24 (doi:10.4007/annals.2003.157.689).
• 2017. Viazovska constructs the sharp function in dimension 8 (doi:10.4007/annals.2017.185.3.7); Cohn, Kumar, Miller, Radchenko and Viazovska do so in dimension 24 (doi:10.4007/annals.2017.185.3.8).
• 2019. Radchenko and Viazovska prove Fourier interpolation on the real line (doi:10.1007/s10240-018-0101-z).
• 2021. Sardari shows that values and first derivatives on triangular-lattice shells do not determine a planar radial Schwartz function (arXiv:2102.08753).
• 2022. Cohn, Kumar, Miller, Radchenko and Viazovska prove universal optimality in dimensions 8 and 24 via interpolation formulas (doi:10.4007/annals.2022.196.3.3).

The source of this mission, an OpenAI preprint dated September 23, 2026, claims an explicit sharp planar certificate.

Setting

Scale disks to radius $1/2$, so a packing is a set of centers $\mathcal C\subset\mathbb R^2$ with $|x-y|\ge1$ for distinct centers. The Fourier transform is

$$\widehat f(\xi)=\int_{\mathbb R^2}f(x)\,e^{-2\pi i\,x\cdot\xi}\,dx.$$

A Schwartz function is smooth with all derivatives decaying faster than any inverse power of $|x|$. A function is radial if $f(x)$ depends only on $|x|$; for real radial integrable $f$, $\widehat f$ is real and radial. The Cohn–Elkies theorem says that if $f$ is admissible, $f(x)\le0$ for $|x|\ge1$ and $\widehat f\ge0$, then every packing of radius-$1/2$ disks has density at most $\operatorname{vol}B(0,1/2)\cdot f(0)/\widehat f(0)$.

Formalization targets

Goal: Theorem 1.1 (sharp Fourier certificate)

There is a real radial Schwartz function $f:\mathbb R^2\to\mathbb R$ with

$$\widehat f(0)=1,\qquad f(0)=\frac{2}{\sqrt3},\qquad \widehat f(\xi)\ge0\ \ (\xi\in\mathbb R^2),\qquad f(x)\le0\ \ (|x|\ge1).$$

Lean: OAI.sharp_fourier_certificate, open on the platform.

Significance

With $f(0)/\widehat f(0)=2/\sqrt3$ the Cohn–Elkies bound equals $\frac{\pi}{4}\cdot\frac{2}{\sqrt3}=\frac{\pi}{2\sqrt3}$, the hexagonal density, so the theorem answers the two-dimensional case of Cohn–Elkies Conjecture 7.3 affirmatively and gives a Fourier-analytic proof of Thue's theorem for arbitrary (not only periodic) packings. Its zero structure also recovers uniqueness of the triangular lattice among periodic optimal packings. The certificate does not satisfy the additional zero-set requirement of Cohn–Elkies Conjecture 8.1, which remains a separate question. The construction methods feed into the companion work on universal optimality of the triangular lattice in the same family. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists. By contrast, Viazovska's dimension-8 theorem has been the subject of formalization efforts, so a planar certificate would be a natural low-dimensional companion.

Difficulty

In dimensions 8 and 24 the magic functions come from modular forms, whose symmetries control a function and its Fourier transform at once. No such modular construction is known to produce the planar certificate, and Sardari's nonuniqueness theorem shows that prescribing values and derivatives on the lattice shells does not pin a function down. Numerical Laguerre–Gaussian searches (Cohn–Elkies) approach the bound but do not attain it. The hard part is an exact construction together with rigorous sign control of both $f$ (for $|x|\ge1$) and $\widehat f$ (everywhere), including between interpolation nodes and in the tails.

Formalization scope

• The plane is EuclideanSpace ℝ (Fin 2); the function is a SchwartzMap Plane ℝ.
• SharpPlanar.fourier f ξ is the Bochner integral of $f(x)\exp(-2\pi i\langle x,\xi\rangle)$; for a Schwartz function it is the usual transform.
• SharpCertificate f: Radial f, fourier f 0 = 1, f 0 = 2 / √3, for every ξ the transform has zero imaginary part and nonnegative real part, and f x ≤ 0 when 1 ≤ ‖x‖.
• The goal is pure existence; any certificate, explicit or not, proves it.

A complete development needs Fourier transforms of radial functions in the plane (Hankel transforms, Gaussian pairings) and rigorous interval or Bernstein-polynomial sign certification. Formalizing the Cohn–Elkies bound itself (certificate implies density bound) would be a valuable reusable companion. Contributions formalizing Proposition 2.2, Proposition 3.4 or Proposition 4.3 are welcome.

Selected references

• OpenAI, A sharp Fourier certificate for planar circle packing, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-sharp-Fourier-certificate-for-planar-circle-packing-September-23-2026/paper.pdf
• H. Cohn, N. Elkies, New upper bounds on sphere packings I, Ann. of Math., 2003. https://doi.org/10.4007/annals.2003.157.689
• T. C. Hales, Cannonballs and honeycombs, Notices Amer. Math. Soc., 2000.
• M. S. Viazovska, The sphere packing problem in dimension 8, Ann. of Math., 2017. https://doi.org/10.4007/annals.2017.185.3.7
• H. Cohn, A. Kumar, S. D. Miller, D. Radchenko, M. Viazovska, The sphere packing problem in dimension 24, Ann. of Math., 2017. https://doi.org/10.4007/annals.2017.185.3.8
• D. Radchenko, M. Viazovska, Fourier interpolation on the real line, Publ. Math. IHÉS, 2019. https://doi.org/10.1007/s10240-018-0101-z
• H. Cohn, A. Kumar, S. D. Miller, D. Radchenko, M. Viazovska, Universal optimality of the E8 and Leech lattices and interpolation formulas, Ann. of Math., 2022. https://doi.org/10.4007/annals.2022.196.3.3
• N. Talebizadeh Sardari, Higher Fourier interpolation on the plane, preprint, 2021. https://arxiv.org/abs/2102.08753

Motivation

Which arrangement of points in the plane minimizes interaction energy? For many repulsive interactions the expected answer is the triangular (hexagonal) lattice. Universal optimality, formulated by Cohn and Kumar (2007, doi:10.1090/S0894-0347-06-00546-7), asks for a single configuration that minimizes energy simultaneously for every completely monotone potential of squared distance, which includes all Gaussians and all inverse powers. It was proved in dimensions 8 and 24 for $E_8$ and the Leech lattice; in dimension two it was a conjecture. The question matters in mathematical physics (crystallization, vortex lattices, Coulomb and Riesz gases) and in the theory of Fourier interpolation.

Timeline

• 1953–1964. Rankin, Cassels, Ennola and Diananda show that the triangular lattice minimizes the Epstein zeta function among planar lattices (doi:10.1017/S2040618500035668, doi:10.1017/S2040618500033906).
• 1988. Montgomery proves the Gaussian (theta-function) minimum among planar lattices of fixed covolume for every parameter (doi:10.1017/S0017089500007047).
• 2003. Cohn and Elkies introduce Fourier linear-programming bounds for sphere packing (doi:10.4007/annals.2003.157.689).
• 2007. Cohn and Kumar formulate the Euclidean universal-optimality program (Conjecture 9.4).
• 2018. Cohn and de Courcy-Ireland extend the Fourier comparison to density-based competitor classes (doi:10.1215/00127094-2018-0018).
• 2019. Radchenko and Viazovska develop Fourier interpolation on the line (doi:10.1007/s10240-018-0101-z).
• 2022. Cohn, Kumar, Miller, Radchenko and Viazovska prove universal optimality of $E_8$ and the Leech lattice (doi:10.4007/annals.2022.196.3.3).
• 2024–2025. Partial planar results: comparisons with periodic classes (Faulhuber–Shafkulovska–Zlotnikov, doi:10.1090/bproc/247), small periodic configurations (Hardin–Tenpas, doi:10.19086/da.144978), and local optimality under small displacements (Leblé, arXiv:2511.03353).

The source of this mission, an OpenAI preprint dated September 26, 2026, claims the full planar statement against all locally finite configurations of density one. A companion OpenAI preprint reaches the same energy conclusion by a different (modulo-12) interpolation construction.

Setting

Let $b=\sqrt3/2$ and $A=b^{-1/2}\{m(1,0)+n(1/2,b):m,n\in\mathbb Z\}$, the triangular lattice of covolume one. Let $B_R$ be the closed disk of radius $R$ about the origin. A set $\mathcal C\subset\mathbb R^2$ is locally finite if each $\mathcal C\cap B_R$ is finite, and has centered disk density one if $N_R/(\pi R^2)\to1$, where $N_R=\#(\mathcal C\cap B_R)$.

A smooth $g:(0,\infty)\to[0,\infty)$ is completely monotone if $(-1)^jg^{(j)}(t)\ge0$ for all $j\ge0$, $t>0$. The lower energy per particle is

$$E_g(\mathcal C)=\liminf_{R\to\infty}\frac1{N_R}\sum_{\substack{x,y\in\mathcal C\cap B_R\\ x\ne y}}g(|x-y|^2)\in[0,\infty],$$

summing over ordered pairs. The Fourier transform is $\widehat f(\xi)=\int f(x)e^{-2\pi i x\cdot\xi}\,dx$ and $A^*=\{\xi:\xi\cdot a\in\mathbb Z\ \forall a\in A\}$ is the dual lattice.

Formalization targets

Milestone: Theorem 1.2 (sharp Gaussian minorants)

For every $\alpha>0$ there is a real radial Schwartz $f_\alpha$ with

$$f_\alpha\le e^{-\pi\alpha|x|^2},\quad \widehat f_\alpha\ge0,\quad f_\alpha(a)=e^{-\pi\alpha|a|^2}\ (a\in A\setminus\{0\}),\quad \widehat f_\alpha(w)=0\ (w\in A^*\setminus\{0\}),$$

given for $\alpha\ge1$ by the paper's explicit atomic interpolation construction.

Goal: Theorem 1.1 (universal energy minimum)

For every smooth nonnegative completely monotone $g$ and every locally finite $\mathcal C$ of centered disk density one,

$$E_g(\mathcal C)\ \ge\ \sum_{a\in A\setminus\{0\}}g(|a|^2)\ =\ E_g(A)\qquad\text{in }[0,\infty].$$

Lean: OAI.AtomicTriangular.universal_energy_minimum, open on the platform.

Significance

Theorem 1.1 would settle the planar case of the Cohn–Kumar universal-optimality conjecture in a density-based competitor class with no periodicity or perturbation assumption, for every completely monotone potential including those (such as $t^{-p}$ with $p\le1$) whose lattice sums diverge. By Bernstein's theorem such potentials are mixtures of Gaussians, so the sharp Gaussian certificates of Theorem 1.2 are the analytic core. The theorem identifies the minimum value; it does not classify minimizers. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists. A formalization would also produce reusable Fourier-analytic tools in Lean (Poisson summation for lattices, linear-programming energy bounds).

Difficulty

Lattice-restricted results (Rankin, Montgomery) compare only lattices; a competitor here may be nonperiodic, have arbitrarily close pairs, and have large local clustering. The Fourier linear-programming method handles general competitors but needs, for each Gaussian, an auxiliary function that is simultaneously a pointwise minorant, has nonnegative Fourier transform, and is sharp: it must touch the Gaussian on every lattice shell and its transform must vanish on every dual shell. Constructing such functions for all $\alpha>0$ at once, with rigorous sign control between the interpolation nodes, is the central obstacle. A second issue is passing from the density hypothesis alone (no averaging over translates) to the energy inequality.

Formalization scope

• Points live in EuclideanSpace ℝ (Fin 2); A is Set.range triangularPoint.
• AdmissiblePotential g: ContDiffOn ℝ ⊤ g (Ioi 0), $g\ge0$ and $(-1)^r$ iteratedDeriv r g t $\ge0$ for $t>0$.
• energy g C is the liminf over $R\to\infty$ of diskEnergy, valued in ℝ≥0∞; latticeEnergy g is a tsum in ℝ≥0∞, so divergent sums are allowed and no summability hypothesis is needed.
• The goal returns both the inequality for every admissible C and the equality latticeEnergy g = energy g A.
• For Theorem 1.2, realFourier is Mathlib's 𝓕 (kernel $e^{-2\pi i\langle x,\xi\rangle}$) applied to the complexified function; the $\alpha\ge1$ clause names the paper's explicit coefficients (R, R0, Yf, Uplus, Uminus) and error bounds.

Contributions formalizing Lemma 2.1 (reciprocal Gaussian parameters), Proposition 2.3 (density-only linear programming), Lemma 4.1 (finite certificate) and Proposition 5.1 (exact interpolation and approximation) are welcome.

Selected references

• OpenAI, An atomic certificate for triangular-lattice universal optimality, preprint, September 26, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-atomic-certificate-for-triangular-lattice-universal-optimality-September-26-2026/paper.pdf
• H. Cohn, A. Kumar, Universally optimal distribution of points on spheres, J. Amer. Math. Soc., 2007. https://doi.org/10.1090/S0894-0347-06-00546-7
• H. Cohn, A. Kumar, S. D. Miller, D. Radchenko, M. Viazovska, Universal optimality of the E8 and Leech lattices and interpolation formulas, Ann. of Math., 2022. https://doi.org/10.4007/annals.2022.196.3.3
• H. Cohn, N. Elkies, New upper bounds on sphere packings I, Ann. of Math., 2003. https://doi.org/10.4007/annals.2003.157.689
• H. Cohn, M. de Courcy-Ireland, The Gaussian core model in high dimensions, Duke Math. J., 2018. https://doi.org/10.1215/00127094-2018-0018
• H. L. Montgomery, Minimal theta functions, Glasgow Math. J., 1988. https://doi.org/10.1017/S0017089500007047
• R. A. Rankin, A minimum problem for the Epstein zeta-function, 1953. https://doi.org/10.1017/S2040618500035668
• D. Radchenko, M. Viazovska, Fourier interpolation on the real line, Publ. Math. IHÉS, 2019. https://doi.org/10.1007/s10240-018-0101-z
• T. Leblé, The hexagonal lattice is universally locally optimal, preprint, 2025. https://arxiv.org/abs/2511.03353

Motivation: Nagata's conjecture beyond the plane

Seshadri constants measure the local positivity of a line bundle at a point or a configuration of points: how much of an ample class survives after blowing up the points and subtracting equal multiples of the exceptional curves. For $r$ points on a surface with ample $L$, a dimension count gives the universal upper bound $\sqrt{L^2/r}$. Nagata's 1959 conjecture, which came out of his counterexample to Hilbert's fourteenth problem, says that this bound is attained at $r\ge10$ very general points of the projective plane. On an arbitrary polarized surface, the qualitative Nagata–Biran(–Szemberg) conjecture predicts that the bound is attained at $r$ very general points for every sufficiently large $r$. On the symplectic side, the conjecture corresponds to packing stability: large numbers of equal balls fill a four-manifold.

Timeline

• 1959 — Nagata formulates his plane conjecture and proves the strict multiplicity inequality when $r\ge16$ is a perfect square (Amer. J. Math. 81).
• 1999 — Biran proves symplectic packing stability for rational symplectic classes on closed four-manifolds (Invent. Math. 136).
• 2003 — Harbourne proves maximality for all sufficiently large $r$ with $rL^2$ a perfect square, and asymptotic lower bounds (J. reine angew. Math.).
• 2004 — Roé relates one-point and multipoint Seshadri constants (J. Algebra); Strycharz-Szemberg and Szemberg formulate a stronger prediction with an explicit threshold (Serdica Math. J. 30).
• 2009 — Roé and Ross prove a multipoint product inequality that propagates maximality (Geom. Dedicata).
• 2010 — Syzdek and Szemberg state the qualitative conjecture for arbitrary polarized surfaces (Math. Nachr. 283, Conjecture 4.3; arXiv:0709.2592).
• 2016 — Buse, Hind and Opshtein prove strong packing stability for all closed symplectic four-manifolds (Trans. AMS). Symplectic stability alone does not fix the complex structure needed for the algebraic statement (Eckl 2017, Differential Geom. Appl.).
• 2026 — An OpenAI preprint, Maximal Seshadri constants on arbitrary polarized surfaces (OpenAI Math Release, September 23, 2026), claims the qualitative conjecture for every smooth complex projective surface and every ample line bundle. It has not been peer reviewed, and its proof is not formally verified.

Setting

Let $S$ be a smooth integral complex projective surface and $L$ an ample line bundle, with self-intersection $H=L^2$. For a tuple $\mathbf p=(p_1,\dots,p_r)$ of distinct points, the multipoint Seshadri constant is

$$\varepsilon(S,L;\mathbf p)=\inf_C\frac{L\cdot C}{\sum_{i=1}^r\operatorname{mult}_{p_i}C},$$

the infimum over integral curves $C$ through at least one $p_i$. If $\pi:Y\to S$ is the blow-up at $\mathbf p$ with exceptional curves $E_1,\dots,E_r$, then $\varepsilon$ is the largest $\lambda\ge0$ such that $\pi^*L-\lambda\sum E_i$ is nef (nonnegative on every integral curve), and always $\varepsilon\le\sqrt{H/r}$. Let $U_r\subset S^r$ be the set of tuples of distinct points. A property holds at very general tuples if it fails only on a countable union of proper Zariski-closed subsets of $U_r$.

Formalization targets

Goal: eventual maximality of multipoint Seshadri constants (Theorem 1.1)

For every such $(S,L)$ there is $r_0\ge1$ such that for each $r\ge r_0$ there is a countable union $Z_r$ of proper Zariski-closed subsets of $U_r$, with $U_r\setminus Z_r\neq\varnothing$, such that for every $\mathbf p\in U_r\setminus Z_r$

$$\pi^*L-\sqrt{\tfrac{L^2}{r}}\sum_{i=1}^rE_i\ \text{ is nef on the blow-up at }\mathbf p, \qquad\text{and}\qquad \varepsilon(S,L;\mathbf p)=\sqrt{\tfrac{L^2}{r}} .$$

The threshold $r_0$ may depend on $(S,L)$ and is not explicit. The goal statement is published on the platform with status Open.

Significance

The result itself. Theorem 1.1 settles the qualitative Nagata–Biran conjecture for all polarized complex surfaces, with no assumption that $rL^2$ is a square or that a plane constant is maximal (the hypotheses needed by Harbourne, Roé and Roé–Ross). Because the conclusion is nefness of the square-zero boundary class, it rules out every curve whose degree-to-multiplicity ratio is below $\sqrt{L^2/r}$, including curves with unequal multiplicities. Via Eckl's Kähler packing correspondence, it gives the algebraic counterpart of packing stability. The sharp plane case ($r\ge10$ in $\mathbb P^2$) is a separate companion result.

Formalizing it. The statement is built from scheme-theoretic foundations: projective surfaces, line bundles, sheaf cohomology, blow-ups by universal property, intersection numbers through Euler characteristics. A complete proof would be among the first machine-checked results about the birational geometry of surfaces. Much of the required infrastructure, such as Riemann–Roch on surfaces, finite-dimensionality of coherent cohomology and the existence of blow-ups, is not yet in Mathlib.

Difficulty

The upper bound $\varepsilon\le\sqrt{H/r}$ is an elementary jet count. Equality requires showing that no curve on the surface has too large multiplicity at the chosen points, for all multiplicity orders simultaneously. Degenerating the points to a special configuration, the usual approach in the plane, fails because the threshold in $r$ must be uniform in the jet order: the asymptotic interpolation theorems (Alexander–Hirschowitz) give thresholds depending on a fixed multiplicity bound. Arbitrary surfaces also lack the toric coordinates available on $\mathbb P^2$. The source transfers the problem to finite interpolation on an algebraic torus through a nodal divisor in $|dL|$.

Formalization scope

• Surface: an integral scheme, smooth of relative dimension $2$ over $\operatorname{Spec}\mathbb C$, with a closed immersion into some $\mathbb P^N_{\mathbb C}$ compatible with the structure maps. LineBundle: a locally free sheaf of rank one. IsAmple: the nonvanishing loci of sections of positive powers that are affine form a neighbourhood basis.
• Cohomology is Ext^n(𝒪, M) in the category of sheaves of modules, and dimensions are finrank ℂ. Then $L^2=\chi(2L)-2\chi(L)+\chi(\mathcal O)$ and $L\cdot C=\chi(L|_C)-\chi(\mathcal O_C)$, by Riemann–Roch. If cohomology were infinite-dimensional, finrank would return $0$; finite-dimensionality for projective schemes is part of what a solver must prove.
• Points are $\mathbb C$-points, the configuration space carries the Zariski topology induced from $S^r$, and very general sets are indexed by $\mathbb N$ (IsClosed, ≠ univ, with a point outside all of them).
• The multiplicity is the order of the local equation of $C$ in the local ring at $p$. The Seshadri constant is the real sInf over integral curves with positive total multiplicity.
• Nefness is expressed through a blow-up PointBlowup, characterized by its universal property, and the exceptional ideal sheaves $\mathcal O(-E_i)$. The inequality is $\pi^*L\cdot C+\sqrt{H/r}\sum_i \deg(\mathcal O(-E_i)|_C)\ge0$ for every integral curve $C$ on the blow-up.
• Needed infrastructure: coherent cohomology of projective schemes, Riemann–Roch on curves and surfaces, blow-ups of points, jets and principal parts. Contributions building any of these layers are welcome and reusable.

Selected references

• M. Nagata, On the 14-th problem of Hilbert, Amer. J. Math. 81 (1959), 766–772. https://doi.org/10.2307/2372927
• P. Biran, A stability property of symplectic packing, Invent. Math. 136 (1999), 123–155. https://doi.org/10.1007/s002220050306
• B. Harbourne, Seshadri constants and very ample divisors on algebraic surfaces, J. reine angew. Math. (2003). https://doi.org/10.1515/crll.2003.044
• J. Roé, A relation between one-point and multi-point Seshadri constants, J. Algebra (2004). https://doi.org/10.1016/j.jalgebra.2003.10.009
• B. Strycharz-Szemberg and T. Szemberg, Remarks on the Nagata conjecture, Serdica Math. J. 30 (2004), 405–430. https://www.math.bas.bg/serdica/2004/2004-405-430.pdf
• J. Roé and J. Ross, An inequality between multipoint Seshadri constants, Geom. Dedicata (2009). https://doi.org/10.1007/s10711-008-9315-4
• W. Syzdek and T. Szemberg, Seshadri fibrations of algebraic surfaces, Math. Nachr. 283 (2010), 902–908. https://arxiv.org/abs/0709.2592v1
• O. Buse, R. Hind and E. Opshtein, Packing stability for symplectic 4-manifolds, Trans. Amer. Math. Soc. (2016). https://doi.org/10.1090/tran/6802
• T. Eckl, Kähler packings and Seshadri constants on projective complex surfaces, Differential Geom. Appl. (2017). https://doi.org/10.1016/j.difgeo.2017.03.007
• OpenAI, Maximal Seshadri constants on arbitrary polarized surfaces, OpenAI Math Release preprint, September 23, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Maximal-Seshadri-Constants-on-Arbitrary-Polarized-Surfaces-September-23-2026/main.pdf

Motivation

Euler's totient $\varphi(n)$ counts the integers in $\{1,\dots,n\}$ coprime to $n$. Many integers share a totient, and most integers are not totients at all, so counting the distinct values of $\varphi$ is much harder than counting integers with a given factorization. Let

$$\mathcal V=\{\varphi(n):n\ge1\},\qquad V(x)=\#\{v\in\mathcal V: v\le x\}.$$

The size of $V(x)$ was studied by Pillai, Erdős, Hall, Pomerance, Maier and Ford over most of the twentieth century; Ford's 1998 estimate determines $V(x)$ up to a bounded multiplicative factor but leaves open whether $V(x)$ has an asymptotic equivalent, and Erdős and Hall's question whether $V(cx)/V(x)\to c$.

This mission asks for a formal proof of the explicit asymptotic formula and the Erdős–Hall regular-variation property, as stated in an OpenAI preprint dated September 25, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1929 — Pillai proves that totients have density zero (Bull. AMS 35, 1929).
• 1935 — Erdős shows $V(x)\ll_\varepsilon x/(\log x)^{1-\varepsilon}$ via the normal number of prime factors of $p-1$ (Q. J. Math. 1935); later lower bounds use semiprimes (1945).
• 1976 — Erdős and Hall obtain a lower factor $\exp\{a(\log_3x)^2\}$ and ask whether $V(cx)/V(x)\to c$ (Mathematika 1976).
• 1986–1988 — Pomerance brings the upper bound to the same scale (Acta Arith. 1986); Maier and Pomerance determine the leading constant $C_0=0.8178\ldots$ in $V(x)=\frac{x}{\log x}\exp\{(C_0+o(1))(\log_3x)^2\}$ (Acta Arith. 1988).
• 1998 — Ford determines $V(x)$ up to a bounded factor and proves $V(cx)-V(x)\asymp_cV(x)$ (Ramanujan J. 1998).
• September 2026 — The OpenAI preprint claims an explicit asymptotic equivalent and $V(cx)/V(x)\to c$ (Theorem 2.1, p. 4).

Setting

Logarithms are natural and $\log_j$ is the $j$-fold iterate. For $j\ge1$ let $a_j=(j+1)\log(j+1)-j\log j-1$, let $\rho\in(0,1)$ be the unique root of $\sum_{j\ge1}a_j\rho^j=1$, and set

$$\lambda=\log(1/\rho),\qquad \gamma=\Bigl(\sum_{j\ge1}ja_j\rho^j\Bigr)^{-1},\qquad g_0=1,\ \ g_j=\sum_{d=1}^ja_dg_{j-d}.$$

For large $x$ put $B=\log_2x$, $m=\lfloor(\log B-\log_2B)/\lambda\rfloor$, the phase $\theta=(\log B-\log_2B)/\lambda-m\in[0,1)$, and $G_m=B^m/(m!\prod_{i\le m}g_i)$; the factor $\frac{x}{\log x}G_m$ is Ford's counting scale.

For each $H$ the preprint defines an explicit arithmetic coefficient $A_H(f;s)$, $s\in[0,1)$, from a finite set of "tail witnesses" (tuples of primes $Q_h$, $P\le h<H$, and a cofactor $a$, subject to explicit size and recurrence constraints, $P=\lfloor\log\log H\rfloor$) by inclusion–exclusion over witnesses with a common totient $d$, weighted by $f(\ell(d)/d)/d$ (formula (2.8), p. 5). Here $\ell(v)=\min\{n\ge1:\varphi(n)=v\}$ is the least preimage, and $A(f;s)=\lim_{H\to\infty}A_H(f;s)$ when the limit exists. The coefficient is defined without reference to $V$.

Formalization targets

Milestone: nonnegativity of the approximants (Theorem 2.1, p. 4)

$A_H(1;s)\ge0$ for $s\in[0,1)$.

Goal: Theorem 2.1 (p. 4)

$A_H(1;\cdot)\to A(1;\cdot)$ uniformly on $[0,1)$, with $0<\inf_sA(1;s)\le\sup_sA(1;s)<\infty$, and

$$V(x)\sim\frac{x}{\log x}\,G_m\,A(1;\theta),\qquad \frac{V(cx)}{V(x)}\longrightarrow c\quad(c>0\ \text{fixed}).$$

Further milestones: least preimages (Theorem 2.2, p. 6)

For $k\ge1$ let $N_k(x)=\#\{v\in\mathcal V:v\le x,\ kx<\ell(v)\le(k+1)x\}$ and $f_k(r)=\min\{1,\tfrac{k+1}r\}-\min\{1,\tfrac kr\}$. Then $A_H(f_k;\cdot)$ converges uniformly and $N_k(x)=\frac{x}{\log x}G_m(A(f_k;\theta)+o(1))$; if some totient $d$ has $\ell(d)>kd$ then $\inf_sA(f_k;s)>0$ and $N_k(x)\asymp V(x)$, and otherwise $N_k\equiv0$ and $A(f_k;\cdot)\equiv0$. The positive alternative holds for $k=1,2$.

Significance

The result itself. The formula replaces Ford's bounded uncertainty by an explicit function of the phase $\theta$, built from finite arithmetic data, and answers the Erdős–Hall question: $V$ is regularly varying of index $1$. Theorem 2.2 answers, in weighted form, Erdős's question on how least preimages are distributed in intervals $(kx,(k+1)x]$, reducing it to the existence of a "seed" totient with $\ell(d)>kd$. Whether such seeds exist for every $k$ (equivalently, whether $\ell(d)/d$ is unbounded) is not settled by the preprint.

Formalizing it. This is analytic number theory at full strength: Ford's structure theorems for totient preimages, sieve bounds for two or three linear forms in shifted primes, simplex volume computations and an inclusion–exclusion limit. Mathlib has the totient and the prime number theorem in some forms but not these sieve and distribution results. The definitions in this mission (the renewal root $\rho$, the witnesses, $A_H$) are explicit and can be checked independently of any proof.

Difficulty

Counting integers $n$ with a typical factorization is a volume computation, but $V(x)$ counts values, and different $n$ can have the same totient. The preprint must show that, outside a negligible set, distinct long prime prefixes give distinct values (Proposition 5.1, p. 22, and Proposition 5.3, p. 27), which needs a uniform comparison estimate for products of shifted primes (Proposition 4.2, p. 17), while short discrete tails that may collide are kept exactly and handled by inclusion–exclusion (Lemma 6.4, p. 30). The limits are taken in a specific order ($x\to\infty$ with $H$ fixed, then $H\to\infty$), and no continuity of $s\mapsto A(1;s)$ is available, so all errors must be uniform in the phase.

Formalization scope

• IsTotient v means $v=\varphi(n)$ for some $n\ge1$; V x counts totients in $\{1,\dots,\lfloor x\rfloor\}$; ell v is Nat.find of the least preimage (junk value $0$ for non-totients, never used on them).
• rho is the sInf of roots in $(0,1)$ of $\sum_{j\ge0}a_{j+1}z^{j+1}=1$; the root is unique, so this is the source's $\rho$.
• AH H f s is formula (2.8) with finsum over totients $d$ and over nonempty finite sets $T$ of witnesses with $\varphi(w)=d$; the witness set is finite for each $H$, so the finsums are genuine finite sums. A f s is limUnder atTop; the goal asserts uniform convergence, so the junk value is never used.
• mainTerm x = x / log x * G x (m x) * A 1 (theta x); asymptotic equivalence is Tendsto (V x / mainTerm x) atTop (𝓝 1).
• The milestone coefficient_nonnegative is stated for every $H$, while the source states it for sufficiently large $H$; for small $H$ the witness set is empty or the inclusion–exclusion is still a probability, so this is a harmless strengthening.
• companion_zero_case restates alternative (ii) of Theorem 2.2 in a separate definition file (TotientCompanionZero) with identical definitions.

Selected references

• OpenAI, An asymptotic formula for the number of totients, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-asymptotic-formula-for-the-number-of-totients-September-25-2026/An-asymptotic-formula-for-the-number-of-totients-September-25-2026.pdf
• S. S. Pillai, On some functions connected with φ(n), Bull. Amer. Math. Soc. 35 (1929), 832–836. https://www.ams.org/journals/bull/1929-35-06/S0002-9904-1929-04799-2/S0002-9904-1929-04799-2.pdf
• P. Erdős, On the normal number of prime factors of p−1 and some related problems concerning Euler's φ-function, Q. J. Math. 6 (1935). https://doi.org/10.1093/qmath/os-6.1.205
• P. Erdős, R. R. Hall, Distinct values of Euler's φ-function, Mathematika 23 (1976). https://doi.org/10.1112/S0025579300006100
• C. Pomerance, On the distribution of the values of Euler's function, Acta Arith. 47 (1986). https://doi.org/10.4064/aa-47-1-63-70
• H. Maier, C. Pomerance, On the number of distinct values of Euler's φ-function, Acta Arith. 49 (1988). https://doi.org/10.4064/aa-49-3-263-275
• K. Ford, The distribution of totients, Ramanujan J. 2 (1998), 67–151; revised arXiv:1104.3264. https://arxiv.org/abs/1104.3264v2

Motivation

For a positive integer $n$, Jacobsthal's function $j(n)$ is the least $m$ such that every run of $m$ consecutive integers contains an integer coprime to $n$. Equivalently, $j(n)-1$ is the longest interval that can be covered by choosing one residue class modulo each prime divisor of $n$ (the classes $0\bmod p$ shifted by the interval's start). Its maximum over integers with at most $k$ prime divisors,

$$h(k)=\max\{j(n):\ \omega(n)\le k\},$$

governs how long a stretch can be sieved out by $k$ primes. It is linked to gaps between consecutive primes (long covered intervals produce large prime gaps, as in the Erdős–Rankin and Ford–Green–Konyagin–Maynard–Tao constructions) and to the limits of the linear sieve. Jacobsthal asked, and Erdős recorded, whether $h(k)\ll k^2$.

Background

• 1960. Jacobsthal begins a series of papers on this function.
• 1962. Erdős records Jacobsthal's question $h(k)\ll k^2$ and notes Brun's bound $h(k)\ll k^{C_0}$ (doi:10.7146/math.scand.a-10523).
• 1971. Iwaniec's error-term estimate for the linear sieve gives order $k^2\log^2k$ for the first $k$ primes (doi:10.4064/aa-19-1-1-30).
• 1977. Vaughan proves the uniform bound $j(n)\ll\omega(n)^2\log(2\omega(n))$ and explains the exponent 2 by the linear sieve's square-root restriction (doi:10.1017/S0013091500026560).
• 1978. Iwaniec proves $h(k)\ll k^2\log^2k$ for arbitrary prime sets (doi:10.1515/dema-1978-0121).
• 2012. Hajdu and Saradha disprove Jacobsthal's primorial-extremality conjecture: $j(P_{24})=234<236=h(24)$ (doi:10.1090/S0025-5718-2012-02581-6).
• 2015, 2019. Costello–Watts and Ziller compute bounds and exact values for small $k$ (doi:10.1090/S0025-5718-2014-02896-2).
• 2018. Ford, Green, Konyagin, Maynard and Tao give the lower bound $j(P_k)\gg k(\log k)^2\frac{\log\log\log k}{\log\log k}$ (doi:10.1090/jams/876).

The source of this mission is an OpenAI preprint dated September 25, 2026.

Setting

• $\omega(n)$ is the number of distinct prime divisors of $n$, with $\omega(1)=0$.
• For $n\ge1$, $j(n)$ is the least $m\ge1$ such that for every integer $a$, one of $a,a+1,\dots,a+m-1$ is coprime to $n$ (note $\gcd(0,n)=n$).
• $h(k)=\sup\{j(n):n\ge1,\ \omega(n)\le k\}$ for $k\ge1$. All logarithms are natural.

Formalization targets

Milestone: quadratic bound (Jacobsthal's question)

$$\exists C>0\ \forall k\ge1:\quad h(k)\le C\,k^2.$$

Goal: Theorem 1.1

$$\exists C>0\ \forall k\ge1:\quad h(k)\le C\,\frac{k^2}{(\log\log(3k))^2}.$$

Both are stated in Lean as the existence, for each $k$, of a length $m$ satisfying IsJacobsthalBound k m with the displayed size bound. The goal OAI.Erdos970.Erdos970Final.erdos_970_iterated_log is open on the platform.

Significance

Theorem 1.1 answers Jacobsthal's question affirmatively, uniformly over all prime sets and interval positions, and removes the logarithmic losses in the bounds of Vaughan and Iwaniec, going slightly below the quadratic scale. It shows that the linear sieve can be pushed to its limiting parameter $s=2$, where the lower sieve function vanishes, by retaining a boundary contribution. The gap to the best lower bound (roughly $k(\log k)^2$) remains large; Vaughan suggested $j(n)\ll_\varepsilon\omega(n)^{1+\varepsilon}$.

The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists. The constant $C$ is not made explicit.

Difficulty

The linear sieve gives a lower bound for the number of uncovered integers only when the sieving range is below the square root of the interval length, which is exactly where the exponent 2 comes from; at the critical parameter the main term of the lower-bound sieve vanishes, so the standard argument yields nothing and a $\log^2k$ loss appears. One must keep the boundary term that the leading linear-sieve calculation discards, and then show that the actual prescribed residue classes do not deviate much from a reference calculation. Positivity of the reference calculation alone does not suffice: the comparison requires an inverse estimate for a witnessing edge of a decreasing-prime tree, variance bounds, and stopping-time counts for hard endpoints.

Formalization scope

• IsJacobsthalBound k m: for every n : ℕ with 0 < n and n.primeFactors.card ≤ k, and every a : ℤ, some i < m has (a + i).natAbs.Coprime n.
• JacobsthalQuadratic: ∃ C > 0, ∀ k > 0, ∃ m, IsJacobsthalBound k m ∧ m ≤ C k^2.
• JacobsthalIteratedLog: the same with bound C k^2 / (log (log (3k)))^2; for $k\ge1$ the denominator is positive.
• The two targets live in separate definition files that both define IsJacobsthalBound identically.

A complete development needs the fundamental lemma of the sieve, Buchstab-type functions of the linear sieve, prime number theorem estimates in short ranges and progressions, the additive large sieve, a lattice-point count on plane curves, and renewal-type arguments for a continuous path process. Contributions formalizing Theorem 1.2 (the quantitative covering estimate), Lemma 2.1 (fundamental lemma of the sieve), Proposition 6.3 (positive reference margin), Proposition 8.2 (inverse estimate for an edge) and Corollary 9.3 are welcome.

Selected references

• OpenAI, A quadratic bound for Jacobsthal's function, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-quadratic-bound-for-Jacobsthals-function-September-25-2026/paper.pdf
• P. Erdős, On the integers relatively prime to n and on a number-theoretic function considered by Jacobsthal, Math. Scand., 1962. https://doi.org/10.7146/math.scand.a-10523
• R. C. Vaughan, On the order of magnitude of Jacobsthal's function, Proc. Edinburgh Math. Soc., 1977. https://doi.org/10.1017/S0013091500026560
• H. Iwaniec, On the problem of Jacobsthal, Demonstratio Math., 1978. https://doi.org/10.1515/dema-1978-0121
• H. Iwaniec, On the error term in the linear sieve, Acta Arith., 1971. https://doi.org/10.4064/aa-19-1-1-30
• L. Hajdu, N. Saradha, Disproof of a conjecture of Jacobsthal, Math. Comp., 2012. https://doi.org/10.1090/S0025-5718-2012-02581-6
• K. Ford, B. Green, S. Konyagin, J. Maynard, T. Tao, Long gaps between primes, J. Amer. Math. Soc., 2018. https://doi.org/10.1090/jams/876
• F. Costello, P. Watts, An upper bound on Jacobsthal's function, Math. Comp., 2015. https://doi.org/10.1090/S0025-5718-2014-02896-2
• J. Friedlander, H. Iwaniec, Opera de Cribro, AMS, 2010. https://doi.org/10.1090/coll/057

Motivation

A random conductance model puts a random conductivity on every edge of the lattice $\mathbb Z^d$. It is the simplest discrete model of diffusion in a heterogeneous medium, and its generator is the generator of a random walk in a random environment. Classical stochastic homogenization shows that on large scales the random operator behaves like a constant-coefficient elliptic operator whose homogenized coefficient $A_{\mathrm{hom}}$ is deterministic. The characterization of $A_{\mathrm{hom}}$, however, involves an equation on the whole lattice for every realization of the coefficients. In practice one computes a spatial average over a box of size $L$ of the energy density of an approximate corrector, as in Gloria and Otto (arXiv:1104.1291, §1). The random part of the error of this procedure is a variance. Its size as a function of $L$ determines how large a computational box must be.

Timeline:

• 1979–1981: Kozlov (MR542557) and Papanicolaou–Varadhan (MR712714) prove qualitative homogenization for continuum elliptic equations with random coefficients.
• 1983: Künnemann (MR714611) proves the discrete version, the diffusion limit of reversible jump processes on $\mathbb Z^d$ with ergodic bond conductivities. It provides the corrector and the approximate corrector used here.
• 1986: Yurinskii (MR867870) gives the first quantitative rates, far from optimal.
• 1998: Naddaf and Spencer (preprint, Estimates on the variance of some homogenization problems) introduce the spectral-gap approach and obtain optimal variance bounds under a small-contrast assumption on the conductivities.
• 2011: Gloria and Otto (DOI 10.1214/10-AOP571) prove the optimal variance estimate without any small-contrast assumption, with a logarithmic loss in $d = 2$. This mission formalizes that estimate.

Setting

Fix $d \ge 2$ and $0 < \alpha \le \beta$. Sites are $x \in \mathbb Z^d$ and $e_1,\dots,e_d$ is the canonical basis. An edge $[z, z+e_i]$ carries a conductivity $a(z,i) \in [\alpha,\beta]$; such a field $a$ belongs to the class $\mathcal A_{\alpha\beta}$. The discrete gradients are $\nabla_i u(x) = u(x+e_i) - u(x)$ and $\nabla^*_i u(x) = u(x) - u(x-e_i)$, and $A(x) = \mathrm{diag}[a(x,1),\dots,a(x,d)]$.

The conductivities are i.i.d.: they are distributed according to the product $\nu^{\otimes E}$ over all edges of one probability law $\nu$ on $[\alpha,\beta]$. No density is assumed, so atomic laws are allowed. $\langle\cdot\rangle$ is the expectation and $\operatorname{var}$ the variance.

For a direction $\xi \in \mathbb R^d$ with $|\xi| = 1$ and a cut-off $T > 0$, the approximate corrector $\phi_T$ solves

$$T^{-1}\phi_T(x) - \nabla^*\cdot A(x)\big(\nabla\phi_T(x) + \xi\big) = 0 \qquad (x \in \mathbb Z^d).$$

The zero-order term introduces the length scale $\sqrt T$. The Green's function $G_T(x,y;a)$ is the $\ell^2$ solution of $(T^{-1} - \nabla^*\cdot A\nabla)G_T(\cdot,y) = \delta_y$ in weak form.

A mask $\eta_L : \mathbb Z^d \to [0,1]$ is supported in the box $(-L,L)^d$, sums to $1$ and satisfies $|\nabla\eta_L| \le C_\eta L^{-d-1}$. The averaged energy density is

$$\xi\cdot A_{L,T}\xi = \sum_{x\in\mathbb Z^d}\Big(T^{-1}\phi_T(x)^2 + \big(\nabla\phi_T(x)+\xi\big)\cdot A(x)\big(\nabla\phi_T(x)+\xi\big)\Big)\eta_L(x).$$

Formalization targets

Goal: Theorem 2.1, estimate (2.5)

There are an exponent $q > 0$ and a threshold $T_0$, depending only on $d, \alpha, \beta$, and for each mask constant $C_\eta$ a constant $C$, such that for every law $\nu$ on $[\alpha,\beta]$, every unit $\xi$, every $T \ge T_0$, every $L > 0$ and every mask $\eta_L$:

$$\operatorname{var}[\xi\cdot A_{L,T}\xi] \le \begin{cases} C\,L^{-2}(\ln T)^q, & d = 2,\\ C\,L^{-d}, & d > 2.\end{cases}$$

The statement fixes the shape of the bound, not the value of $q$ or $C$, which is why it is the goal.

Milestones

The milestones follow the paper's proof:

• well-posedness: the Green's function (Definition 2.7) and the approximate corrector (Lemma 2.2, pathwise form);
• the variance estimate Lemma 2.3 for functions of countably many i.i.d. variables;
• deterministic Green's-function bounds: Lemma 2.8 (BMO and decay on dyadic annuli), Lemma 2.9 (Meyers-type higher integrability), Corollaries 2.2 and 2.3;
• susceptibility formulas: Lemmas 2.4 and 2.5, which give $\partial\phi_T/\partial a(e)$ and $\partial G_T/\partial a(e)$;
• measurability: Lemma 2.6;
• a Caccioppoli inequality in probability: Lemma 2.7;
• a convolution estimate: Lemma 2.10;
• moment bounds: Proposition 2.1, which gives $\langle|\phi_T(0)|^q\rangle \lesssim 1$ for $d > 2$ and $\lesssim(\ln T)^{\gamma(q)}$ for $d = 2$;
• the two steps of §3.2: the derivative formula (3.17) and its uniform bound (3.22).

Significance

The result. The estimate says that smooth averages of the energy density fluctuate as if the density were independent from site to site, at the rate $L^{-d/2}$. That rate is the best possible, since the coefficients themselves are independent. In the error analysis of approximations of $A_{\mathrm{hom}}$, this controls the random error and separates it from the systematic error caused by the cut-off $T$. Proposition 2.1, a byproduct, shows that the approximate corrector has all moments bounded uniformly in $T$ when $d > 2$, which yields a stationary corrector (Corollary 2.1 of the paper).

Formalizing it. The theorem has been proved since 2011, and no machine-checked version is known. A formal proof would combine three components that are reusable well beyond this paper:

• a variance inequality for functions of countably many independent variables, in the infinite product measure;
• quantitative regularity of discrete elliptic Green's functions, uniform in the coefficients;
• the sensitivity calculus of solutions with respect to a single coefficient.

Difficulty

The obvious argument fails because the energy density is not independent from site to site: the corrector couples all conductivities through the inverse of a random elliptic operator. Bounding the variance needs the sensitivity of $\xi\cdot A_{L,T}\xi$ to each single conductivity, and that sensitivity is expressed through gradients of the Green's function. Pointwise bounds on $\nabla G_T$ that are uniform in the coefficients do not exist: the continuum counterpart fails, by examples from quasi-conformal mappings. Only averaged decay on dyadic annuli and a small gain of integrability are available, which is why the proof needs the moment bounds of Proposition 2.1. In $d = 2$ the Green's function does not decay, so only BMO-type control is available, and a logarithm of $T$ is lost.

Formalization scope

Statements follow the arXiv v1 reprint (arXiv:1104.1291v1) of the Annals of Probability article; theorem and page numbers refer to it.

• The lattice is Fin d → ℤ. An edge $[z,z+e_i]$ is the pair (z, i), and a coefficient field is a real function on edges; the theorems assume it takes values in $[\alpha,\beta]$.
• The i.i.d. law is Measure.infinitePi of one probability measure $\nu$ on $\mathbb R$ with $\nu([\alpha,\beta]^c) = 0$.
• $\phi_T$ is the unique bounded solution of (2.3) and $G_T(\cdot,y)$ the unique $\ell^2$ solution of (2.11). The definitions file explains why the bounded solution is the paper's stationary $\phi_T$.
• Norms are Euclidean. The mask's gradient bound is componentwise with an explicit constant $C_\eta$.
• Every $\lesssim$ becomes an explicit constant chosen before the law, the coefficients and the spatial variables, and every $\gg 1$ becomes an explicit threshold.
• Variances, lower integrals and infinite sums that could otherwise default to $0$ are either taken in $[0,\infty]$ or come with square-integrability in the conclusion.

Ruling out a trivial formalization. If the constant $C$ were allowed to depend on the law $\nu$ or on the mask, the goal would follow from the boundedness of the energy average alone. If the variance were taken of a function that is not square-integrable, it would be $0$ by convention. The goal fixes $C$ before $\nu$ and $\eta_L$ and requires square-integrability as part of the conclusion.

Not formalized:

• the last sentence of Theorem 2.1, the variance estimate for the corrector $\phi$ itself when $d > 2$. It needs the stationary corrector of Lemma 2.1, whose existence is quoted from Künnemann;
• Lemma 2.8 (ii);
• the stochastic part of Lemma 2.2 (stationarity and zero mean of $\phi_T$), which follows from the pathwise statement as explained in the definitions file.

Welcome contributions are proofs of any milestone and reusable infrastructure: infinite-product variance inequalities, discrete integration by parts, and discrete maximum principles.

Selected references

• A. Gloria, F. Otto, An optimal variance estimate in stochastic homogenization of discrete elliptic equations, Ann. Probab. 39(3) (2011) 779–856. arXiv:1104.1291, DOI 10.1214/10-AOP571
• R. Künnemann, The diffusion limit for reversible jump processes on $\mathbb Z^d$ with ergodic random bond conductivities, Comm. Math. Phys. 90 (1983) 27–68. MR714611
• S. M. Kozlov, The averaging of random operators, Mat. Sb. 109(151) (1979) 188–202. MR542557
• G. C. Papanicolaou, S. R. S. Varadhan, Boundary value problems with rapidly oscillating random coefficients, Colloq. Math. Soc. János Bolyai 27 (1981) 835–873. MR712714
• V. V. Yurinskii, Averaging of symmetric diffusion in a random medium, Sibirsk. Mat. Zh. 27 (1986) 167–180. MR867870
• N. G. Meyers, An $L^p$ estimate for the gradient of solutions of second order elliptic divergence equations, Ann. Scuola Norm. Sup. Pisa 17 (1963) 189–206. MR0159110

Motivation

A degree sequence records how many neighbours each vertex of a graph has. In network statistics it is often the only summary of a graph that is observed or trusted, and the natural probability models for graphs in which "the degree sequence captures the information" are exponential families whose sufficient statistic is the degree sequence. Chatterjee, Diaconis and Sly (arXiv:1005.1136, Ann. Appl. Probab. 2011) call the resulting model the β-model and study its maximum likelihood theory and its use for sampling random graphs with a prescribed degree sequence.

For any exponential family, the first question about estimation is which values of the sufficient statistic can be matched by a parameter: the maximum likelihood equations say exactly "the expected statistic equals the observed one". Theorem 1.4 of the paper answers this for the β-model. Up to taking a closure, the expected degree sequences of the β-model fill the whole convex hull of the degree sequences. The paper notes that the result can also be derived from classical results on the mean space of exponential families (Barndorff-Nielsen 1978; Brown 1986; Wainwright and Jordan 2008, Theorem 3.3), and gives a self-contained proof in §3. Lemma 4.1 of the same paper uses Theorem 1.4 to show that the maximum likelihood estimator exists.

Setting

Fix $n\ge 0$ and the vertex set $\{1,\dots,n\}$. A graph $G$ is undirected and simple: no loops and no multiple edges. Its degree sequence is $d(G)=(d_1,\dots,d_n)\in\mathbb R^n$, and

$$\mathcal D=\{d(G):\ G\text{ a simple graph on }n\text{ vertices}\}$$

is the finite set of all degree sequences. Its convex hull $\operatorname{conv}(\mathcal D)$ is a polytope in $\mathbb R^n$.

For $\beta\in\mathbb R^n$, the β-model $\mathbb P_\beta$ is the law of the random graph in which each pair $\{i,j\}$, $i\neq j$, is an edge with probability

$$p_{ij}=\frac{e^{\beta_i+\beta_j}}{1+e^{\beta_i+\beta_j}},$$

independently of all other pairs. The expected degree sequences form the set

$$\mathcal R=\big\{\big(\mathbb E_\beta[d_1],\dots,\mathbb E_\beta[d_n]\big):\ \beta\in\mathbb R^n\big\}.$$

Two functions on $\mathbb R^n$ appear in the proof. The first is $g=(g_1,\dots,g_n)$ with

$$g_i(x)=\sum_{j\neq i}\frac{e^{x_i+x_j}}{1+e^{x_i+x_j}}.$$

The second is, for each $y\in\mathbb R^n$,

$$f_y(x)=\sum_{i=1}^n x_iy_i-\log\prod_{1\le i<j\le n}\big(1+e^{x_i+x_j}\big).$$

The Lean development names these objects betaModel, D, R, g and fy in the namespace GivenDegreeSeq.MeanPolytope.

Formalization targets

Goal: Theorem 1.4 (p. 8)

$$\operatorname{conv}(\mathcal D)=\overline{\mathcal R}\qquad\text{for every }n.$$

The statement fixes no constants. The closure cannot be dropped: for $n\ge2$ the degree sequence $0$ of the empty graph lies in $\mathcal D$ but not in $\mathcal R$, because every expected degree is positive.

Milestones, in the order the proof uses them

1. The probability formula (p. 6): $\mathbb P_\beta$ is a probability measure, and

$$\mathbb P_\beta(\{G\})=\frac{e^{\sum_i\beta_id_i}}{\prod_{i<j}(1+e^{\beta_i+\beta_j})}.$$

2. Expected degrees (p. 15): $\mathbb E_x[d_i]=g_i(x)$, so $\mathcal R=g(\mathbb R^n)$.
3. The easy inclusion (p. 15): $\overline{\mathcal R}\subseteq\operatorname{conv}(\mathcal D)$.
4. A uniform bound (p. 16): $f_y(x)\le 0$ for all $y\in\operatorname{conv}(\mathcal D)$ and $x\in\mathbb R^n$.
5. Smoothness (p. 16): $f_y$ is twice differentiable and $\nabla^2 f_y$ is uniformly bounded.
6. Lemma 3.1 (pp. 14–15): if $f$ is twice differentiable, $M=\sup f<\infty$ and $\|\nabla^2 f\|_{\mathrm{op}}\le C$, then

$$|\nabla f(x)|^2\le 2C\big(M-f(x)\big),$$

and $\nabla f(x_k)\to0$ along some sequence. 7. The gradient (p. 16): $\nabla f_y(x)=y-g(x)$.

Significance

The theorem describes the mean space of the β-model. Its interior contains every degree sequence that lies strictly inside the polytope, and for these sequences maximum likelihood estimation is well posed. The paper's consistency result (Theorem 1.3) and the existence part of Lemma 4.1 start from this description. The polytope $\operatorname{conv}(\mathcal D)$ is studied in its own right; its extreme points are the degree sequences of threshold graphs (Mahadev and Peled 1995).

Theorem 1.4 is proved, and as far as this mission's authors know it is not machine-checked anywhere. Formalizing it means turning the paper's short proof into a complete argument. That includes the steps the page dismisses as easy: the exponential-family formula for the independent-edge law, the expectation computation, the Hessian bound for $f_y$, and the passage from a sequence of approximate critical points to the closure. Lemma 3.1, a descent-type gradient bound for a function bounded above, is a general fact of real analysis and is independent of graphs.

Difficulty

The inclusion $\overline{\mathcal R}\subseteq\operatorname{conv}(\mathcal D)$ is direct: an expectation is an average. The reverse inclusion is the content. For $y$ in the interior of the polytope, one would like to find $x$ with $g(x)=y$ by maximizing the concave function $f_y$. For $y$ on the boundary of the polytope, however, $f_y$ need not attain its supremum. So the argument cannot rely on the existence of a maximizer, and it has to produce points $x_k$ with $g(x_k)\to y$ without ever solving $g(x)=y$. Compactness arguments on $\beta$ fail for the same reason: the relevant sequences $x_k$ are unbounded.

Formalization scope

• Graphs and measure. Vertices are Fin n, so the paper's vertex $i$ is the index $i-1$. Graphs are SimpleGraph (Fin n), a finite type. Its σ-algebra is Mathlib's SimpleGraph.instMeasurableSpace, under which every set of graphs on Fin n is measurable.
• The law and its expectations. $\mathbb P_\beta$ is the finite sum of Dirac masses weighted by the independent-edge product over pairs $i<j$. $\mathcal R$ is defined through Bochner expectations under $\mathbb P_\beta$, not as the range of $g$. Defining $\mathcal R$ as $g(\mathbb R^n)$ would erase the link to the probability model and is ruled out.
• Vector spaces. $\mathcal D$ and $\mathcal R$ are subsets of Fin n → ℝ, whose product topology is the Euclidean topology, so the closure is unambiguous. Gradients and Hessians are taken on EuclideanSpace ℝ (Fin n). There "twice differentiable" means that $f$ and its Fréchet derivative are differentiable, and the Hessian norm is the norm of the second Fréchet derivative, which equals the $L^2$ operator norm of the Hessian matrix.
• No size hypothesis. The goal holds for every $n$; for $n\le1$ both sides are $\{0\}$.
• Readings of the page.
  • On p. 15 the paper prints $\log\sum_{1\le i<j\le n}(1+e^{x_i+x_j})$ in $f_y$. The formalization uses $\log\prod$, the only reading under which "taking logs, we get $f_d(x)\le0$" and $\nabla f_y=y-g$ hold. The milestone text keeps the printed version.
  • The "Lemma 11" of p. 16 is Lemma 3.1.
  • The probability-measure property of $\mathbb P_\beta$ is stated as a conjunct of milestone 1.
  • The differentiability of $f_y$ is stated alongside the Hessian bound in milestone 5.

Contributions of any milestone are welcome. Lemma 3.1 and the gradient identity are self-contained calculus. The probability formula and the expected-degree identity are finite computations on graphs.

Selected references

• S. Chatterjee, P. Diaconis, A. Sly, Random graphs with a given degree sequence, Ann. Appl. Probab. 21(4) (2011), 1400–1435. https://arxiv.org/abs/1005.1136 (v5), https://doi.org/10.1214/10-AAP728
• O. Barndorff-Nielsen, Information and Exponential Families in Statistical Theory, Wiley, Chichester, 1978. MR0489333, https://mathscinet.ams.org/mathscinet-getitem?mr=0489333
• L. D. Brown, Fundamentals of Statistical Exponential Families with Applications in Statistical Decision Theory, IMS Lecture Notes–Monograph Series 9, 1986. MR0882001, https://mathscinet.ams.org/mathscinet-getitem?mr=0882001
• M. J. Wainwright, M. I. Jordan, Graphical models, exponential families, and variational inference, Found. Trends Mach. Learn. 1 (2008), 1–305. https://doi.org/10.1561/2200000001
• N. V. R. Mahadev, U. N. Peled, Threshold Graphs and Related Topics, Ann. Discrete Math. 56, North-Holland, 1995. MR1417258, https://mathscinet.ams.org/mathscinet-getitem?mr=1417258

Motivation

The eigenvalues of a large non-Hermitian random matrix are hard to study directly. For Hermitian matrices, the empirical spectral distribution (ESD) is controlled by the resolvent and the Stieltjes transform, both stable under small perturbations. For non-Hermitian matrices no such tool exists: eigenvalues can move a long way under tiny perturbations, and the moment method fails because moments do not determine a measure on $\mathbb C$. The route that works, going back to Girko (1984) and used by Bai (1997), Götze–Tikhomirov (2007), Pan–Zhou (2007) and Tao–Vu (2008), passes through logarithmic determinants. The identity $\frac1n\log|\det(A-zI)|=\int\log|w-z|\,d\mu_A(w)$ links the ESD $\mu_A$ to a scalar quantity. That scalar is computable from the singular values of $A-zI$, which are eigenvalues of a Hermitian matrix.

Tao and Vu, with an appendix by Krishnapur (Ann. Probab. 38 (2010) 2023–2065), turn this link into an exact criterion. Theorem 1.15 of that paper states that the ESD of a normalized i.i.d. random matrix converges to a measure $\mu$ if and only if the normalized log-determinants converge to the logarithmic potential of $\mu$ for almost every $z$. The same holds for a regularized version built from the singular values. This mission formalizes Theorem 1.15 and the main steps of its proof (§8 and Appendix A of the published article).

Setting

Let $x$ be a complex random variable with $\mathbf E x=0$ and $\mathbf E|x|^2=1$, and let $(x_{ij})_{i,j\ge1}$ be independent copies of $x$ on a probability space $(\Omega,\mathbf P)$. For each $n$, $X_n=(x_{ij})_{1\le i,j\le n}$. Let $M_n$ be deterministic $n\times n$ complex matrices with

$$\text{(1.3)}\qquad\sup_n\frac1{n^2}\|M_n\|_2^2<\infty,\qquad\|M\|_2^2=\sum_{i,j}|m_{ij}|^2,$$

and put $A_n=M_n+X_n$.

For $A\in M_n(\mathbb C)$ with eigenvalues $\lambda_1,\dots,\lambda_n$, counted with algebraic multiplicity, the ESD is $\mu_A=\frac1n\sum_i\delta_{\lambda_i}$. Its singular values are $\sigma_1(A)\ge\dots\ge\sigma_n(A)\ge0$. A sequence of random measures $\mu_n$ converges in probability to a deterministic $\mu$ if, for every continuous compactly supported $f:\mathbb C\to\mathbb R$, $\int f\,d\mu_n-\int f\,d\mu$ tends to $0$ in probability. It converges almost surely if, with probability one, $\int f\,d\mu_n\to\int f\,d\mu$ for all such $f$ at once. The logarithmic potential of a measure $\mu$ is $z\mapsto\int\log|w-z|\,d\mu(w)$.

Hypothesis (1.4) states that, for almost every $z$, the ESDs of the deterministic matrices $(\frac1{\sqrt n}M_n-zI)(\frac1{\sqrt n}M_n-zI)^*$ converge to a limit.

In Lean everything lives in the namespace UnivESD.LogDet. The ESD is esd, the one-based singular value is sv, logPotential is the logarithmic potential, and ConvInProb/ConvAS/ESDConvInProb/ESDConvAS are the modes of convergence. IIDArray is the entry model, HSBound is (1.3), shiftA M xs z n ω is $\frac1{\sqrt n}A_n-zI$, and Cond14 is (1.4).

Formalization targets

Goal: Theorem 1.15

Let $\mu$ be a probability measure on $\mathbb C$ with $\int|z|^2\,d\mu<\infty$. The following are equivalent:

1. $\mu_{\frac1{\sqrt n}A_n}\to\mu$ in probability;
2. for a.e. $z$, $\displaystyle\frac1n\log\Big|\det\big(\tfrac1{\sqrt n}A_n-zI\big)\Big|\to\int_{\mathbb C}\log|w-z|\,d\mu(w)$ in probability;
3. for a.e. $z$ there are $\varepsilon_n>0$, $\varepsilon_n\to0$, with

$$\frac1n\log\det\Big(\big(\tfrac1{\sqrt n}A_n-zI\big)\big(\tfrac1{\sqrt n}A_n-zI\big)^*+\varepsilon_nI\Big)\to2\int_{\mathbb C}\log|w-z|\,d\mu(w)$$

in probability.

Under (1.4) the same equivalence holds with almost sure convergence throughout.

Milestones, in the order the proof uses them

• (8.1): for a.e. $z$, $w\mapsto\log|w-z|$ is $\mu$-integrable.
• Lemma A.3 (Weyl's comparison for products): $\prod_{j\le J}|\lambda_j|\le\prod_{j\le J}\sigma_j(A)$ and $\prod_{j\ge J}\sigma_j(A)\le\prod_{j\ge J}|\lambda_j|$.
• (8.3): $\mathbf P(\sigma_{n-i}\le ci/n)=O(\exp(-n^{0.01}))$ for $2n^{0.99}\le i\le n-1$.
• (8.2): $\frac1n\sum_{i=1}^n\big(\log\sqrt{\sigma_i^2+\varepsilon_n}-\log\sigma_i\big)\to0$ almost surely.
• p. 2057: almost surely, eventually, $\frac1n\sum_{(1-\kappa)n<i\le n}\log\frac1{\sigma_i}\le O(\kappa\log\frac1\kappa)$, and the same bound for $\log\frac1{|\lambda_i|}$.

Significance

Theorem 1.15 reduces convergence of a non-Hermitian ESD to a family of scalar limit statements. Each of these can be attacked through Hermitian tools, because the regularized log-determinant in (iii) is a smooth functional of the singular values. Corollary 1.16 of the paper derives from it a practical criterion: the ESD converges to $\mu$ once the singular value distributions of $\frac1{\sqrt n}A_n-zI$ converge for a.e. $z$ to laws $\eta_z$ with $\int\log t\,d\eta_z=2\int\log|w-z|\,d\mu$. With the universality principle (Theorem 1.5, the companion mission) and Mehta's computation for complex Gaussian matrices, this yields the circular law for i.i.d. matrices with finite variance.

The theorem is proved in the source. To our knowledge neither it nor any of its milestones has a machine-checked proof. Mathlib has the ingredients for the objects (characteristic polynomials and their roots, LinearMap.singularValues, the strong law of large numbers) but not the results. A formal proof would give the platform its first verified bridge between eigenvalue and singular value asymptotics. Lemma A.3 alone, Weyl's multiplicative majorization, is a standard linear-algebra fact absent from Mathlib.

Difficulty

Two things make the obvious argument fail. First, $\log$ is unbounded at $0$. Vague convergence of $\mu_{\frac1{\sqrt n}A_n}$ controls $\int f\,d\mu_n$ only for continuous compactly supported $f$, while $\log|w-z|$ has a singularity at $w=z$ and grows at infinity. Passing between (i) and (ii) therefore requires uniform control of the eigenvalues (and singular values) near $0$ after the shift: the contribution of the smallest ones must vanish. Second, eigenvalues are not stable under perturbation, so this control cannot be read off the eigenvalues. It has to come from the singular values, through a lower-tail bound on $\sigma_{n-i}$ that is exponentially small in a power of $n$, and through a deterministic inequality transferring bounds from singular values to eigenvalues. The smallest singular values ($i$ below $n^{0.99}$) need a separate polynomial lower bound (the paper's Lemma 4.1, posed in the companion mission). The tail bound in its printed form is false at that end of the range.

Formalization scope

Conventions committed to in Lean:

• The ESD is $n^{-1}$ times the sum of Dirac masses over the root multiset of the characteristic polynomial, so multiplicities are kept. Test functions are real-valued, continuous and compactly supported. Almost sure ESD convergence uses one null set for all test functions.
• The matrices $X_n$ are the top-left corners of one infinite i.i.d. array. In-probability statements do not depend on how the $X_n$ are coupled across $n$, but almost-sure statements do, and the paper's proof applies the strong law to this array. The limit in (1.4) is required to be a probability measure, which is equivalent under (1.3).
• The second-moment condition on $\mu$ is Integrable (‖w‖²) μ. The logarithmic potential is a Bochner integral, which is $0$ when not integrable; by (8.1) this happens only for a null set of $z$, which "for a.e. $z$" ignores.
• Real.log 0 = 0. In (ii), a singular matrix would contribute $0$ instead of $-\infty$; for this model the determinant is almost surely nonzero eventually. Every milestone with $\log\sigma_i$ or $\log|\lambda_i|$ carries positivity of those quantities in its conclusion.
• Singular values are one-based (sv A i is Mathlib's singularValues (i-1)). Eigenvalue enumerations are Fin n-indexed, and the paper's $\lambda_i$ is index $i-1$.
• The paper's $O(\cdot)$ constants are existential and fixed before $n$. In the $\kappa\log(1/\kappa)$ bounds the constant is fixed before $\kappa$; a $\kappa$-dependent constant would make the bounds empty.

Disclosed corrections to the printed text:

1. (iii)'s matrix. Theorem 1.15 prints a mis-bracketed product, and (1.8) prints $(C+\varepsilon_nI)(C^*+\varepsilon_nI)$. The Lean uses $CC^*+\varepsilon_nI$ with $C=\frac1{\sqrt n}A_n-zI$, the matrix of (8.2) and of the proof of Corollary 1.16.
2. (8.3)'s range. It is printed for $1\le i\le n-n^{0.99}$, which is false for small $i$: for Gaussian entries and $M_n=0$, $n\sigma_{n-1}$ has a non-degenerate limit law. It is posed on $2n^{0.99}\le i\le n-1$, the range the proof covers and the use needs.
3. Lemma A.3, second inequality. It is posed for $1\le J\le n$, since $\sigma_0$ is undefined. The eigenvalues are ordered $|\lambda_1|\ge\dots\ge|\lambda_n|$, not $|\lambda_1|\le\dots\le|\lambda_n|$ as printed: the printed order is a slip. With it, both inequalities are weaker than Weyl's and cannot support the use on p. 2057, which orders the eigenvalues decreasingly. The decreasing order implies the printed form.
4. (8.2) and (8.1). (8.2) is stated for every deterministic $\varepsilon_n>0$ with $\varepsilon_n\to0$; the proof uses nothing else. (8.1) is stated as $\mu$-integrability plus local integrability of $z\mapsto\int|\log|w-z||\,d\mu(w)$.

A trivializing formalization is ruled out by construction. The goal mentions only $A_n$ and $\mu$. The proof's comparison ensemble $B_n=\sqrt n\,\mathrm{diag}(\lambda_i)$ is not a hypothesis. No statement takes a log-potential or a log-determinant as an input that could be fixed to make it hold.

The companion mission (Theorem 1.5, universality) poses Theorem 2.1 (the replacement principle), Lemma 1.7 (tightness) and Lemma 4.1 (least singular value), which the proof here also uses. They are not restated here. Once that mission is published they belong here as references. Contributions are welcome on the linear-algebra layer (Lemma A.3, multiplicative Weyl majorization), the Fubini argument of (8.1), and the singular-value tail bound (8.3). These are reusable well beyond this paper.

Selected references

• T. Tao, V. Vu (appendix by M. Krishnapur), Random matrices: Universality of ESDs and the circular law, Ann. Probab. 38(5) (2010) 2023–2065. https://doi.org/10.1214/10-AOP534 (source of this mission; published version).
• V. L. Girko, The circular law, Teor. Veroyatnost. i Primenen. 29 (1984) 669–679. https://doi.org/10.1137/1129095
• Z. D. Bai, Circular law, Ann. Probab. 25(1) (1997) 494–529. https://doi.org/10.1214/aop/1024404298
• F. Götze, A. Tikhomirov, The circular law for random matrices, Ann. Probab. 38(4) (2010) 1444–1491. https://doi.org/10.1214/09-AOP522
• T. Tao, V. Vu, Random matrices: the circular law, Commun. Contemp. Math. 10(2) (2008) 261–307. https://doi.org/10.1142/S0219199708002788
• H. Weyl, Inequalities between the two kinds of eigenvalues of a linear transformation, Proc. Natl. Acad. Sci. USA 35 (1949) 408–411. https://doi.org/10.1073/pnas.35.7.408