Harmonic Analysis

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

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

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

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

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,

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

The Hardy–Littlewood maximal function replaces a function by the largest of its averages around each point. It is the basic tool for differentiation theorems and singular integrals, and it is bounded on $L^p$ for $p>1$ but not on $L^1$. Kinnunen showed that it also preserves first-order Sobolev regularity: it is bounded on $W^{1,p}(\mathbb R^n)$ for $1<p<\infty$, because $|\nabla Mf|\le M|\nabla f|$ pointwise (Kinnunen 1997). At $p=1$ this argument breaks, since $M$ is unbounded on $L^1$. Hajłasz and Onninen asked whether the gradient estimate $\|\nabla Mf\|_1\le C\|\nabla f\|_1$ nevertheless holds (Question 1 in Ann. Acad. Sci. Fenn. Math. 2004). The question is a test of whether maximal operators improve or destroy regularity at the endpoint, where the usual $L^p$ machinery is unavailable.

This mission asks for a formal proof of the planar centered-disk case, as stated in an OpenAI preprint dated September 26, 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

• 1997 — Kinnunen: $M$ is bounded on $W^{1,p}$, $1<p<\infty$ (Israel J. Math. 1997).
• 2002–2007 — In one dimension, Tanaka proves an $L^1$ derivative bound for the uncentered operator (Bull. Austral. Math. Soc. 2002); Aldaz and Pérez Lázaro obtain the sharp variation constant and absolute continuity (Trans. AMS 2007).
• 2004 — Hajłasz and Onninen pose the endpoint question.
• 2009 — Aldaz and Pérez Lázaro treat block-decreasing inputs in higher dimensions (Studia Math. 2009).
• 2015 — Kurka proves a variation bound for the one-dimensional centered operator (Ann. Acad. Sci. Fenn. Math. 2015).
• 2018 — Luiro proves the $L^1$ gradient estimate for radial inputs and the uncentered ball operator (Ark. Mat. 2018).
• 2020–2025 — Beltran–Madrid and Weigt treat fractional centered operators (JFA 2020; Math. Z. 2022); Weigt proves variation bounds for dyadic and uncentered-cube maximal operators (IMRN 2023; JEMS 2025); Lahti and Weigt show that a variation bound for the centered operator upgrades to Sobolev regularity (arXiv:2510.01936).
• September 2026 — The OpenAI preprint claims the planar centered-disk endpoint bound (Theorem 1.1, p. 1).

Setting

Identify $\mathbb R^2$ with the Euclidean plane and write $B(x,r)$ for the open disk of radius $r$ centered at $x$. For a locally integrable real function $f$, the centered disk maximal function is

The space $W^{1,1}(\mathbb R^2)$ consists of integrable $f$ whose distributional gradient is represented by an integrable vector field $\nabla f$, i.e. $\int f\,\partial_i\varphi=-\int(\nabla f)_i\varphi$ for all $\varphi\in C_c^\infty$. Norms of gradients are Euclidean: $\|\nabla f\|_1=\int|\nabla f|$. For the signed estimate, put $A_tg(x)=\frac1{\pi t^2}\int_{B(x,t)}g$ and $S_{a,b}g(x)=\sup_{a\le t\le b}A_tg(x)$.

Formalization targets

Milestone: Proposition 1.2 (signed finite-band estimate, p. 2)

There is an absolute constant $C$ such that for every real $g\in C_c^\infty(\mathbb R^2)$ and $0<a\le b$ with $b/a$ a power of two (including $1$),

with $C$ independent of $a$, $b$ and the number of dyadic scales.

Goal: Theorem 1.1 (p. 1)

There is an absolute constant $C<\infty$ such that for every real $f\in W^{1,1}(\mathbb R^2)$, $Mf$ is finite almost everywhere, locally integrable, belongs to $W^{1,1}_{\mathrm{loc}}(\mathbb R^2)$, and has a globally integrable weak gradient with

Significance

The result itself. It resolves the planar centered-disk case of the Hajłasz–Onninen question with no radiality or support assumption. As a consequence (Corollary 6.3, p. 39) the bound extends to $BV(\mathbb R^2)$ inputs and yields a co-area type perimeter bound for level sets of $M\mathbf 1_E$. The constant is absolute but not optimized. Higher dimensions, other centered maximal operators, and continuity of $f\mapsto\nabla Mf$ in $W^{1,1}$ remain separate questions.

Formalizing it. Mathlib has Lebesgue integration, weak derivatives only in limited form, and no maximal-function regularity theory. A formal proof would need distributional gradients, Poincaré inequalities on squares, dyadic multiscale decompositions and a vector-measure representation of bounded distributional derivatives (the preprint's Appendix A). These pieces are reusable across harmonic analysis.

Difficulty

For $p>1$ one bounds $|\nabla Mf|\le M|\nabla f|$ and uses the strong maximal inequality, which fails for $p=1$. One-dimensional proofs order the optimizing intervals, and that ordering has no analogue for families of centered disks. Fractional-order proofs use that optimizing balls overlap little, a mechanism that degenerates at order zero. The preprint (Sections 2–5) instead proves the signed finite-band estimate uniformly in the number of scales: it uses a vanishing first moment at interior maximizing radii, a concentration-in-a-thin-shell lemma (Lemma 2.4, p. 8), and two multiscale constructions that pay for direction changes in scale and space. A variation bound alone would leave a possibly singular derivative measure; removing the singular part needs the signed form of Proposition 1.2 applied to locally mean-subtracted inputs (Section 6).

Formalization scope

• The plane is EuclideanSpace ℝ (Fin 2). maximal f x is an ℝ≥0∞-valued supremum over all real $r>0$ of lower Lebesgue integrals of $|f|$ over Metric.ball x r divided by $\pi r^2$; the goal asserts it is finite a.e. before passing to maximalReal = toReal.
• HasWeakGradient f g is the integration-by-parts identity against every $C^\infty$ compactly supported test function, coordinatewise; the input is Integrable f, Integrable g, HasWeakGradient f g, which is exactly $W^{1,1}$ with weak gradient g. The bound is stated against this g, so it does not depend on a choice of representative.
• InW11Loc asks for local integrability and a locally integrable weak gradient; the goal also asks for one integrable weak gradient G with ∫ ‖G‖ ≤ C * ∫ ‖g‖, C ≥ 0 chosen before f.
• The milestone uses signed averages (Bochner integrals) and sSup over the closed radius band $[a,2^ma]$; the band envelope is continuous in $r$, so the supremum is finite. Inputs are ContDiff ℝ ∞ with compact support.
• The BV extension (Corollary 6.3) is not part of either target.

Selected references

• OpenAI, An Endpoint Gradient Bound for the Centered Disk Maximal Operator, OpenAI Math Release preprint, September 26, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-Endpoint-Gradient-Bound-for-the-Centered-Disk-Maximal-Operator-September-26-2026/article.pdf
• J. Kinnunen, The Hardy–Littlewood maximal function of a Sobolev function, Israel J. Math. (1997). https://doi.org/10.1007/BF02773636
• P. Hajłasz, J. Onninen, On boundedness of maximal functions in Sobolev spaces, Ann. Acad. Sci. Fenn. Math. (2004). https://afm.journal.fi/article/view/135096
• H. Tanaka, A remark on the derivative of the one-dimensional Hardy–Littlewood maximal function, Bull. Austral. Math. Soc. (2002). https://doi.org/10.1017/S0004972700020293
• J. M. Aldaz, J. Pérez Lázaro, Functions of bounded variation, the derivative of the one dimensional maximal function, and applications to inequalities, Trans. AMS (2007). https://doi.org/10.1090/S0002-9947-06-04347-9
• O. Kurka, On the variation of the Hardy–Littlewood maximal function, Ann. Acad. Sci. Fenn. Math. (2015). https://doi.org/10.5186/aasfm.2015.4003
• H. Luiro, The variation of the maximal function of a radial function, Ark. Mat. (2018). https://doi.org/10.4310/ARKIV.2018.v56.n1.a9
• J. Weigt, The variation of the uncentered maximal operator with respect to cubes, J. Eur. Math. Soc. (2025). https://doi.org/10.4171/JEMS/1575
• P. Lahti, J. Weigt, The centered maximal operator removes the non-concave Cantor part from the gradient, arXiv:2510.01936 (2025). https://arxiv.org/abs/2510.01936v1

Motivation

The Hilbert transform $Hf(x)=\mathrm{p.v.}\int f(x-t)\,\frac{dt}{t}$ is the basic singular integral of harmonic analysis. In the plane one can take it along a line through each point, with the direction of the line allowed to depend on the point: given a unit vector field $v:\mathbb R^2\to S^1$, integrate $f$ along the segment through $x$ in direction $v(x)$. Whether such directional Hilbert transforms are bounded on $L^2$ is one of the central problems connecting singular integrals, Kakeya-type geometry and time–frequency analysis. If $v$ depends on only one coordinate, the $L^2$ problem already contains Carleson's theorem on almost-everywhere convergence of Fourier series. For general fields some regularity of $v$ is necessary, and some truncation of the integration length is necessary because a field can turn.

Stein asked whether a Lipschitz field suffices when the integration length is at most a small multiple of $1/\mathrm{Lip}(v)$. In the formulation of Lacey and Li, this is a uniform weak-$(2,2)$ conjecture. A parallel conjecture of Zygmund concerns the corresponding maximal averages.

Timeline

• 1966. Carleson proves almost-everywhere convergence of Fourier series of $L^2$ functions (doi:10.1007/BF02392815); the one-variable-field $L^2$ case of the directional problem reduces to this.
• 1987. Stein lists the Lipschitz directional Hilbert transform among problems in harmonic analysis in his ICM address (Problems in harmonic analysis related to curvature and oscillatory integrals).
• 1989. Bourgain proves an $L^2$ bound for the maximal averaging operator along analytic vector fields (doi:10.1017/CBO9780511662294.006).
• 2006. Lacey and Li prove annular weak-$(2,2)$ and strong $L^p$, $p>2$, bounds for directional Hilbert transforms with measurable directions (doi:10.1090/S0002-9947-06-03869-4), and a Lipschitz Kakeya maximal theorem.
• 2010. Lacey and Li's memoir develops the relation between maximal operators and the Hilbert-transform problem, with conditional results requiring stronger maximal estimates or $C^{1+\eta}$ fields (doi:10.1090/S0065-9266-10-00572-7).
• 2012. Stein and Street prove local $L^p$ bounds for singular Radon transforms associated with real-analytic maps (doi:10.1016/j.aim.2011.11.016).
• 2013. Bateman proves single-annulus $L^p$ estimates for fields depending on one coordinate (doi:10.4171/RMI/748); Bateman and Thiele prove strong $L^p$ bounds, $3/2<p<\infty$, for the full transform along one-variable fields (doi:10.2140/apde.2013.6.1577).
• 2015–2017. Guo extends the one-variable setting to fields constant along Lipschitz curves (doi:10.2140/apde.2015.8.1263, doi:10.1090/tran/6750) and proves single-annulus variation-norm bounds for Lipschitz fields; Guo and Thiele treat a lacunary model of Lipschitz fields (doi:10.1112/S0025579316000280).
• 2018. Di Plinio and Parissis extend the lacunary framework (doi:10.1007/s11856-018-1724-y); Di Plinio, Guo, Thiele and Zorin-Kranich show that uniform $L^2$ bounds on vertical frequency bands imply the full short principal-value bound under a small Lipschitz condition (doi:10.1016/j.jfa.2018.07.005).

The source of this mission, an OpenAI preprint dated September 25, 2026, claims the uniform strong $L^2$ bound at short scale for every Lipschitz field.

Setting

Let $v:\mathbb R^2\to S^1$ be Lipschitz with $\mathrm{Lip}(v)\le1$. For $0<\varepsilon<a$ the short directional Hilbert transform is

The direction is frozen at the output point $x$. For a Schwartz function $f$ the principal value $H_{v,a}f=\lim_{\varepsilon\downarrow0}H^\varepsilon_{v,a}f$ exists at every point, since $f(x-tv(x))-f(x+tv(x))=O_x(|t|)$.

Formalization targets

Goal: Theorem 1.1

There are absolute constants $a_*\in(0,1/2)$ and $C_*<\infty$ such that every unit field $v$ with $\mathrm{Lip}(v)\le1$ satisfies, for all $f\in\mathcal S(\mathbb R^2)$,

and the truncations and the principal value extend to bounded operators on $L^2$ with norm at most $C_*$. The constants $a_*$ and $C_*$ are existential; no numerical value is fixed. The Lean statement OAI.LipschitzHilbert.main is open on the platform.

The proposal also contains OAI.LipschitzHilbert.uniform_truncation, the rescaled form for $K$-Lipschitz fields at every outer length $R\le 1/(10^6K)$. By the dilation $x\mapsto Kx$ it is the same estimate at the reciprocal-Lipschitz scale; its explicit constant $10^{-6}$ is a convention of the formalization, not of the paper.

Significance

The theorem answers the short-scale form of Stein's question affirmatively and with a strong (not only weak-type) $L^2$ bound, for fields depending on both coordinates and with no regularity beyond Lipschitz. Earlier unconditional results required the field to depend on one variable, to be constant along a foliation, to be analytic, to take lacunary directions, or restricted the frequency to one annulus. The uniformity in the inner truncation is an operator bound for each truncation, which is what the principal value and the weak-type bound are derived from.

The result is claimed in an OpenAI preprint of 87 pages; it has not been peer reviewed and no machine-checked proof exists. The Lean goal records the complete short-scale conclusion; a formal proof would certify a long chain of time–frequency arguments (wave-packet decompositions, size and density selection, a Lipschitz Kakeya input, and a phase-gain iteration).

Difficulty

Restricting to short scales limits how far the field turns but does not make the operator a Fourier multiplier: the line of integration still varies with the output point. Positive (maximal) operator bounds lose all oscillation, while the one-variable reduction to Carleson's theorem is unavailable when $v$ depends on both coordinates. The known band-to-full reassembly reduces matters to one vertical frequency band, but on a band one needs a restricted estimate with a logarithmic gain in the ratio of the measures of the input and test sets; the Lacey–Li Kakeya estimate only provides a polynomial loss in that ratio, so an additional oscillatory saving is required.

Formalization scope

• The plane is EuclideanSpace ℝ (Fin 2); inputs are SchwartzMap Plane ℂ, norms are eLpNorm _ 2 volume in ℝ≥0∞.
• The field is v : Plane → Plane with LipschitzWith 1 v and ‖v x‖ = 1 for all x.
• twoSidedTruncation v ε a f x is the sum of interval integrals over $[-a,-\varepsilon]$ and $[\varepsilon,a]$ of $t^{-1}f(x-tv(x))$; smoothPrincipalValue integrates the symmetric quotient over $(0,a)$, with the removable value at $t=0$ filled by the derivative.
• ShortHilbertConclusion a C bundles the five clauses (truncation bound for $0<\varepsilon<a$, principal-value bound, weak-(2,2) bound at every finite nonzero level, and bounded Lp extensions agreeing a.e. on Schwartz inputs). The goal asks for $a\in(0,1/2)$ and $C>0$.

A complete development needs singular-integral and Littlewood–Paley machinery on $\mathbb R^2$, wave-packet analysis and a Lipschitz Kakeya maximal estimate; much of this is reusable for other time–frequency problems. Contributions formalizing the band-restricted estimate, the band-to-full reassembly, or the one-dimensional inputs (the maximal truncated Hilbert transform) are welcome.

Selected references

• OpenAI, A uniform Hilbert transform estimate for Lipschitz directions, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-uniform-Hilbert-transform-estimate-for-Lipschitz-directions-September-25-2026/main.pdf
• M. Lacey, X. Li, On a conjecture of E. M. Stein on the Hilbert transform on vector fields, Mem. Amer. Math. Soc., 2010. https://doi.org/10.1090/S0065-9266-10-00572-7
• M. T. Lacey, X. Li, Maximal theorems for the directional Hilbert transform on the plane, Trans. Amer. Math. Soc., 2006. https://doi.org/10.1090/S0002-9947-06-03869-4
• M. Bateman, C. Thiele, $L^p$ estimates for the Hilbert transforms along a one-variable vector field, Anal. PDE, 2013. https://doi.org/10.2140/apde.2013.6.1577
• F. Di Plinio, S. Guo, C. Thiele, P. Zorin-Kranich, Square functions for bi-Lipschitz maps and directional operators, J. Funct. Anal., 2018. https://doi.org/10.1016/j.jfa.2018.07.005
• S. Guo, C. Thiele, Hilbert transforms along Lipschitz direction fields: a lacunary model, Mathematika, 2017. https://doi.org/10.1112/S0025579316000280
• E. M. Stein, B. Street, Multi-parameter singular Radon transforms III: real analytic surfaces, Adv. Math., 2012. https://doi.org/10.1016/j.aim.2011.11.016
• L. Carleson, On convergence and growth of partial sums of Fourier series, Acta Math., 1966. https://doi.org/10.1007/BF02392815

Motivation

For a set $E\subset\mathbb R^d$ the distance set is $\Delta(E)=\{|x-y|:x,y\in E\}$. Falconer (1985) asked how large a set must be, measured by Hausdorff dimension, to force $\Delta(E)$ to have positive length. Examples built from lattices show that dimension $d/2$ is not enough in general, and Falconer conjectured that any compact set of dimension strictly greater than $d/2$ suffices. The question is the continuous analogue of Erdős's distinct-distances problem and has been a driving problem for geometric measure theory and Fourier restriction theory: progress on it has repeatedly come from, and fed back into, spherical averages, restriction estimates, decoupling and radial projections.

Background

• 1985. Falconer proves the threshold $(d+1)/2$ and introduces the conjecture (doi:10.1112/S0025579300010998).
• 1987. Mattila's spherical-average criterion makes Fourier $L^2$ estimates the central approach (doi:10.1112/S0025579300013462).
• 1994. Bourgain connects improvements in dimensions two and three to restriction phenomena (doi:10.1007/BF02772994).
• 1999, 2005. Wolff reaches $4/3$ in the plane; Erdoğan reaches $d/2+1/3$ for $d\ge3$ (doi:10.1155/S1073792899000288, doi:10.1155/imrn.2005.1411).
• 2019–2021. Du, Guth, Ou, Wang, Wilson and Zhang reach $9/5$ in $\mathbb R^3$; Du and Zhang reach $d/2+1/4+1/(8d-4)$; Guth, Iosevich, Ou and Wang reach $5/4$ in the plane, with a pinned conclusion (arXiv:1802.10186, doi:10.4007/annals.2019.189.3.4, doi:10.1007/s00222-019-00917-x).
• 2019. Keleti and Shmerkin develop multiscale profile methods for planar distance sets (doi:10.1007/s00039-019-00500-9).
• 2023–2024. Orponen and Shmerkin prove the planar Furstenberg-set/projection estimates; Orponen, Shmerkin and Wang prove radial projection theorems; Du, Ou, Ren and Zhang improve higher-dimensional thresholds (arXiv:2106.03338, doi:10.1007/s00039-024-00660-3, arXiv:2309.04103).
• 2025. Shmerkin and Wang show $\dim_H\Delta(E)=1$ when the Hausdorff and packing dimensions both equal $d/2$ (doi:10.1007/s00039-024-00696-5).
• 2026. Liu proves the planar conclusion for sets with equal Hausdorff and packing dimension above one (arXiv:2603.15328).

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

Setting

• $\mathbb R^d$ carries the Euclidean distance $|x-y|$.
• For $E\subset\mathbb R^d$, the Hausdorff dimension $\dim_HE$ is the infimum of $s\ge0$ for which the $s$-dimensional Hausdorff measure of $E$ vanishes.
• $\Delta(E)=\{|x-y|:x,y\in E\}\subset[0,\infty)$, and $\mathcal L^1$ is Lebesgue measure on $\mathbb R$.

Formalization targets

Milestone: the planar case

Goal: Theorem 1.1

The goal OAI.Falconer.falconer_distance_conjecture is open on the platform.

Significance

Theorem 1.1 resolves Falconer's distance conjecture in every dimension, with no regularity assumption beyond the strict dimension bound: no equality of Hausdorff and packing dimension, no Ahlfors regularity, no product structure. The threshold $d/2$ is sharp by Falconer's lattice examples, and no endpoint assertion is made. The result is unpinned: it does not assert that a single point $y\in E$ has $\mathcal L^1(\{|x-y|:x\in E\})>0$ at the threshold. Positive measure is stronger than $\dim_H\Delta(E)=1$.

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

Difficulty

The classical route bounds the $L^2$ norm of a distance measure via spherical averages of Fourier transforms (Mattila), and every improvement so far has come from finer restriction or decoupling estimates, which stall above $d/2$. In higher dimensions there is a structural obstacle: radial projections of an $s$-dimensional source cannot gain dimension above $s$, so for $d/2<s<d-1$ one cannot assume radial projections have densities, and the angular input the Fourier argument needs must be built as cap bounds on directional fibres with arbitrarily small losses. Converting such fractal angular laws into a distance estimate requires a belt (rather than cap) estimate whose annular power is exactly balanced at $S=d/2$, and a recursive multiscale accounting whose costs must be paid by a potential across two separated depths.

Formalization scope

• Points live in EuclideanSpace ℝ (Fin d), so dist is the Euclidean distance.
• dimH E : ℝ≥0∞ is Mathlib's Hausdorff dimension; the hypothesis is (d : ℝ≥0∞) / 2 < dimH E, strict.
• The conclusion is 0 < volume {r : ℝ | ∃ x ∈ E, ∃ y ∈ E, dist x y = r} with Lebesgue volume on ℝ; compactness of $E$ makes this set compact.
• The planar milestone uses PlanarFalconer.distanceSet on EuclideanSpace ℝ (Fin 2) with 1 < dimH E.

A complete development needs Frostman's lemma, energy and Fourier characterizations of dimension, Mattila's spherical-average criterion, stationary phase for spherical oscillatory integrals, and the Orponen–Shmerkin planar incidence theorem (used as an external input). Contributions formalizing Lemma 5.5 (the classical distance threshold $(d+1)/2$), Theorem 4.1 (linear projection gain), Theorem 4.2 (planar discretized Furstenberg estimate), Proposition 5.10 (starting pair measures), Proposition 8.1 (graph estimate) and Theorem 10.4 (single-profile angular bound) are welcome.

Selected references

• OpenAI, The Falconer distance conjecture in all dimensions, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Falconer-distance-conjecture-in-all-dimensions-September-23-2026/paper.pdf
• K. J. Falconer, On the Hausdorff dimensions of distance sets, Mathematika, 1985. https://doi.org/10.1112/S0025579300010998
• P. Mattila, Spherical averages of Fourier transforms of measures with finite energy; dimensions of intersections and distance sets, Mathematika, 1987. https://doi.org/10.1112/S0025579300013462
• T. Wolff, Decay of circular means of Fourier transforms of measures, IMRN, 1999. https://doi.org/10.1155/S1073792899000288
• L. Guth, A. Iosevich, Y. Ou, H. Wang, On Falconer's distance set problem in the plane, Invent. Math., 2020. https://doi.org/10.1007/s00222-019-00917-x
• X. Du, L. Guth, Y. Ou, H. Wang, B. Wilson, R. Zhang, Weighted restriction estimates and application to Falconer distance set problem, Amer. J. Math., 2021. https://doi.org/10.1353/ajm.2021.0005
• T. Orponen, P. Shmerkin, On the Hausdorff dimension of Furstenberg sets and orthogonal projections in the plane, Duke Math. J., 2023. https://arxiv.org/abs/2106.03338
• T. Orponen, P. Shmerkin, H. Wang, Kaufman and Falconer estimates for radial projections and a continuum version of Beck's theorem, Geom. Funct. Anal., 2024. https://doi.org/10.1007/s00039-024-00660-3
• P. Shmerkin, H. Wang, On the distance sets spanned by sets of dimension d/2 in $\mathbb R^d$, Geom. Funct. Anal., 2025. https://doi.org/10.1007/s00039-024-00696-5
• X. Du, Y. Ou, K. Ren, R. Zhang, New improvement to Falconer distance set problem in higher dimensions, preprint, 2024. https://arxiv.org/abs/2309.04103

Motivation

Reaction–diffusion equations $u_t = \Delta u + f(u)$ are the standard model for the interplay of diffusion with local growth or decay: chemical kinetics, population dynamics, and the bifurcation of equilibria of partial differential equations. The special case

(the Chafee–Infante equation on bounded domains, Chafee and Infante 1974) is the model equation for loss of stability: $u = 0$ is linearly stable for $\lambda < 0$ and unstable for $\lambda > 0$, and for $m = 3$, $\gamma > 0$ the reaction term produces a supercritical pitchfork bifurcation. Before any of that dynamics can be studied, one needs solutions to exist. §5.5 of J. K. Hunter's Notes on Partial Differential Equations (UC Davis, revised 6/18/2014) proves local existence by rewriting the equation as an integral equation and applying the contraction mapping theorem. This argument, the "mild solution" method of Kato and Segal, is the template for local well-posedness of semilinear parabolic and dispersive equations (Pazy 1983, Henry 1981).

Setting

Write $\mathbb{R}^n$ for Euclidean space with Lebesgue measure. For $f \in L^2(\mathbb{R}^n)$ the Fourier transform is $\hat f(k) = (2\pi)^{-n}\int f(x)e^{-ik\cdot x}\,dx$, defined by this formula on Schwartz functions and extended to $L^2$ by Plancherel's theorem. For $s \ge 0$, the Sobolev space $H^s(\mathbb{R}^n)$ consists of the $f \in L^2$ with finite norm

The heat semigroup $e^{-tA}$, $A = -\Delta$, is the Fourier multiplier $\widehat{e^{-tA}h}(k) = e^{-t|k|^2}\hat h(k)$. For $t > 0$ it is convolution with the heat kernel $\Gamma_t(x) = (4\pi t)^{-n/2}e^{-|x|^2/4t}$.

Fix $\lambda, \gamma \in \mathbb{R}$ and an integer $m \ge 1$, and let $F(h) = \lambda h - \gamma h^m$ act pointwise on functions. The initial value problem is

Write $C([0,T];H^s)$ for the curves $t \mapsto u(t) \in H^s$ that are continuous on $[0,T]$ in the $H^s$ norm, normed by $\sup_{0\le t\le T}\|u(t)\|_{H^s}$. A mild solution on $[0,T]$ with values in $H^{2\alpha}$ is a curve $u \in C([0,T];H^{2\alpha})$ satisfying the Duhamel formula

The right-hand side, viewed as a function of $u$, is the map $\Phi(u)$.

Formalization targets

Goal: local existence and uniqueness (Theorem 5.49)

Let $1 \le n \le 3$ and $n/4 < \alpha < 1$. For every $R > 0$ there is $T > 0$, depending only on $\alpha, n, R, \lambda, \gamma, m$, such that for every $g$ with $\|g\|_{H^{2\alpha}} \le R$, (5.34) has a mild solution $u \in C([0,T];H^{2\alpha})$, and any two mild solutions on $[0,T]$ coincide.

Milestones

• Smoothing (Lemma 5.50). For $\alpha > 0$ there is $C = C(\alpha,n)$ with

• Fractional Sobolev embedding (Theorem 5.79). If $0 < s < n/2$ and $1/q = 1/2 - s/n$, then $\|f\|_{L^q} \le C\|f\|_{H^s}$. If $s > n/2$, then every $f \in H^s$ is a.e. equal to a continuous function vanishing at infinity, and $\|f\|_{L^\infty} \le C\|f\|_{H^s}$.
• Local Lipschitz bound for $\Phi$ (Lemma 5.51). For $n/4 < \alpha < 1$, $\Phi$ maps $C([0,T];H^{2\alpha})$ to itself, and for $0 < T \le T_0$

where all norms are in $C([0,T];H^{2\alpha})$ and $C$ depends on $\alpha, m, n, \lambda, \gamma, T_0$.

Significance

The theorem is the base case of the semigroup approach to nonlinear evolution equations. The existence time depends only on the size of the data, so an a priori bound on $\|u(t)\|_{H^{2\alpha}}$ upgrades local existence to global existence. The same scheme, with $X = \mathcal D(A^\alpha)$ for a sectorial operator $A$, covers general semilinear parabolic problems. The smoothing estimate and the fractional Sobolev embedding are also used separately, in parabolic regularity theory and in the analysis of dispersive equations.

The results are classical and proved in the notes. None of them has a machine-checked proof on this platform. Mathlib has the $L^2$ Fourier transform and Plancherel's theorem, tempered distributions, and a Bessel-potential definition of Sobolev spaces, but no fractional Sobolev embedding on $\mathbb{R}^n$ and no mild-solution theory for semilinear heat equations. The mission asks for complete formal proofs of the three milestones and the goal, stated for the concrete objects above.

Difficulty

The obvious fixed-point argument needs three separate analytic inputs. The first is that the $L^2 \to H^{2\alpha}$ operator norm of $e^{-tA}$ blows up like $t^{-\alpha}$, which is integrable only because $\alpha < 1$. The second is that $F$ is locally Lipschitz from $H^{2\alpha}$ to $L^2$, which needs the embedding $H^{2\alpha} \hookrightarrow L^\infty$ and fails for $\alpha \le n/4$. The third is that the Duhamel integral defines a continuous $H^{2\alpha}$-valued curve even though its integrand is singular at $s = t$. With these in hand, the contraction must be run on a ball whose radius is fixed by the data, with $T$ chosen uniformly over that ball. Uniqueness is claimed in all of $C([0,T];H^{2\alpha})$, not only in the ball where the contraction runs, so an extra argument is needed to exclude solutions that leave the ball.

Formalization scope

• $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) with volume. The solution and the data are real-valued. Theorem 5.79 and Lemma 5.50 are stated for complex-valued functions. A curve is a map ℝ → (ℝⁿ → ℝ), and only its values on $[0,T]$ matter.
• Fourier normalization. The book's $\hat f(k) = (2\pi)^{-n}\int f e^{-ik\cdot x}$ is obtained from Mathlib's $L^2$ transform Lp.fourierTransformₗᵢ (kernel $e^{-2\pi i\langle x,\xi\rangle}$, no prefactor) as $\hat f(k) = (2\pi)^{-n}\mathcal F f(k/2\pi)$. Mathlib's constants are never used for the book's.
• $H^s$ norm. hsNorm is valued in $[0,\infty]$ and is $\infty$ off $L^2$, so $f \in H^s$ means hsNorm n s f < ⊤. The factor $(2\pi)^n$ is inside the square root, as in the book's inner product and in its proof of Lemma 5.50. Definition 5.74 prints it outside, which is inconsistent with both. With this choice $\|f\|_{H^0} = \|f\|_{L^2}$.
• Semigroup. $e^{-tA}$ is convolution with the heat kernel for $t > 0$, which agrees with the multiplier (5.37) on $L^2$, and the identity at $t = 0$. No abstract semigroup theory is used.
• Duhamel integral. It is taken pointwise in $x$, and (5.39) is required for almost every $x$ at each $t \in [0,T]$. For curves in $C([0,T];H^{2\alpha})$ with $\alpha > n/4$, the integrand is bounded, so this is the book's $L^2$-valued integral.
• Constants and corrections. The data dependence of $T$ is read as uniform over the ball $\|g\|_{H^{2\alpha}} \le R$. In Lemma 5.51 the constant, announced as $C(\alpha,m,n)$, is allowed to depend on $\lambda, \gamma$ and on an upper bound $T_0$ for $T$. The hypothesis $\alpha < 1$ is added. Both corrections are used by the notes' own proof, and without them the printed inequality fails for large $T$. Theorem 5.79 prints its inequalities without the constant $C$ it announces, and the constant is restored. Throughout, $m \ge 1$.
• Trivializing readings excluded. The norms are $[0,\infty]$-valued and $\infty$ off $L^2$, so no bound holds through a junk value $0$. A mild solution must satisfy the Duhamel identity and be continuous in $H^{2\alpha}$, so existence cannot be met by an unconstrained curve. Uniqueness is stated over all mild solutions on $[0,T]$, not over a ball.
• Infrastructure. A complete development needs Plancherel in the book's normalization, the heat-kernel/multiplier identity on $L^2$, Bochner or pointwise integration of $L^2$-valued curves, the Banach fixed-point theorem on a closed ball of $C([0,T];H^{2\alpha})$, and the fractional Sobolev embedding. The embedding and the smoothing estimate can be reused beyond this mission. Contributions of the $H^s$ theory as a normed space are welcome.

Selected references

• J. K. Hunter, Notes on Partial Differential Equations, UC Davis lecture notes, revised 6/18/2014, §5.5 and Appendices 5.C–5.D. https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf
• N. Chafee and E. F. Infante, A bifurcation problem for a nonlinear partial differential equation of parabolic type, Applicable Analysis 4 (1974), 17–37. https://doi.org/10.1080/00036817408839081
• A. Pazy, Semigroups of Linear Operators and Applications to Partial Differential Equations, Springer, 1983. https://doi.org/10.1007/978-1-4612-5561-1
• D. Henry, Geometric Theory of Semilinear Parabolic Equations, Lecture Notes in Mathematics 840, Springer, 1981. https://doi.org/10.1007/BFb0089647