Analysis

Motivation: from weak Hessian bounds to every geodesic

On a smooth Riemannian manifold, an upper bound $\nabla^2F\le G\,g$ on the Hessian of a function $F$ immediately bounds the second derivative of $F$ along every geodesic: $(F\circ\sigma)''\le|\dot\sigma|^2\,G\circ\sigma$. In non-smooth geometry this step breaks down. On metric measure spaces with Ricci curvature bounded below in the synthetic sense — the $\mathrm{RCD}(K,N)$ spaces — Hessians exist only weakly: inequalities are tested against the reference measure $m$, whereas a single prescribed geodesic can lie in a set of measure zero. Passing from a distributional Hessian bound to a statement about every individual geodesic is a recurring need, for example in characterizing lower bounds on sectional curvature synthetically (in the same release the preprint accompanies an OpenAI preprint on Gigli's distributional-curvature characterization of Alexandrov spaces). Earlier results get this passage only under extra regularity.

Timeline

• 2014 — Savaré's self-improvement of the Bakry–Émery condition gives a measure-valued Bochner calculus on $\mathrm{RCD}(K,\infty)$ spaces (Savaré 2014).
• 2015 — Ambrosio, Gigli and Savaré identify Bakry–Émery bounds with Riemannian curvature-dimension bounds (Ann. Probab. 2015). Ketterer uses an exponential change of measure under a Hessian assumption with Sobolev regularity (Ketterer 2015, Thm 7.1).
• 2018 — Gigli's second-order calculus on $\mathrm{RCD}$ spaces: Hessians of test functions and $\nabla_{\nabla g}\nabla g=\nabla(\Gamma(g)/2)$ (Gigli, Mem. AMS 2018). Han passes from infinitesimal to weak convexity by entropy convexity for $e^{-au}m$, assuming second-order Sobolev regularity (Han 2018); Sturm treats semiconvex functions by vanishing entropy (Sturm 2018).
• 2020 — Kapovitch and Ketterer derive geodesic convexity from an $L^2$-Hessian bound for Laplacian-domain functions (J. reine angew. Math. 2020, Thm 4.7).
• 2021 — Braun, Habermann and Sturm develop variable-curvature equivalences (J. Math. Pures Appl. 2021).
• 2024–2025 — Brena and Gigli discuss the passage from weak Hessian bounds to geodesic convexity and propose a change-of-measure route, identifying the regularity it needs (Potential Anal. 2025, Remarks 2.3–2.4). Deng proves that finite-dimensional $\mathrm{RCD}(K,N)$ spaces are non-branching (Geom. Topol. 2025, Thm 1.3).
• 2026 — An OpenAI preprint, Weak Hessian bounds along every geodesic in RCD spaces (OpenAI Math Release, September 24, 2026), claims the passage under only bounded Lipschitz regularity of $F$ and bounded continuous $G$. It has not been peer reviewed, and the claim has not been formally verified.

Setting

$(M,d,m)$ is a complete separable metric space with a Borel measure $m$ that charges every nonempty open set and is finite on bounded sets. $\mathrm{RCD}(K,N)$, for $K\in\mathbb R$ and $1<N<\infty$, means the (unreduced) Lott–Sturm–Villani curvature-dimension condition $\mathrm{CD}(K,N)$ for optimal transport between absolutely continuous probability measures with finite second moment, together with a quadratic Cheeger energy (infinitesimal Hilbertianity).

The minimal weak upper gradient $|\nabla f|$ is defined through test plans (probability measures on absolutely continuous curves with bounded compression and finite kinetic energy). Polarization gives $\Gamma(u,v)=\langle\nabla u,\nabla v\rangle$, and the Laplacian is the nonpositive generator, $\int\Gamma(u,v)\,dm=-\int(\Delta u)v\,dm$. The test class consists of bounded, globally Lipschitz $g$ in the domain of $\Delta$ with $\Delta g\in W^{1,2}$. For such compactly supported $g$ and nonnegative compactly supported Lipschitz $h$, the weak Hessian evaluation of $F$ is

$$H_F(\nabla g,\nabla g)(h)= -\int_M\big(\Gamma(h,g)+h\,\Delta g\big)\,\Gamma(F,g)\,dm-\int_M h\,\Gamma\!\big(F,\tfrac12\Gamma(g)\big)\,dm .$$

A constant-speed minimizing geodesic is a curve $\sigma:[0,1]\to M$ with $d(\sigma_s,\sigma_t)=|s-t|\,\ell$, where $\ell=d(\sigma_0,\sigma_1)$. All of these notions are defined from scratch in the Lean development (IsTestPlan, weakGradient, gamma, IsLaplacian, IsTestFunction, weakHessian, CurvatureDimension, RCD).

Formalization targets

Goal: weak Hessian bounds along every geodesic (Theorem 1.1)

Let $(M,d,m)$ be a full-support $\mathrm{RCD}(K,N)$ space with $1<N<\infty$. Let $F$ be bounded and globally Lipschitz and $G$ bounded and continuous, and assume

$$H_F(\nabla g,\nabla g)(h)\le\int_M h\,G\,\Gamma(g)\,dm$$

for all compactly supported test functions $g$ and all nonnegative $h\in\mathrm{Lip}_c(M)$. Then every constant-speed minimizing geodesic $\sigma$ of length $\ell$ satisfies $(F\circ\sigma)''\le\ell^2\,G\circ\sigma$ in distributions on $(0,1)$:

$$\int_0^1F(\sigma_t)\,\varphi''(t)\,dt\le\ell^2\int_0^1G(\sigma_t)\,\varphi(t)\,dt\qquad\text{for all } 0\le\varphi\in C_c^\infty(0,1).$$

The goal is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. If the source's proof is correct, the theorem makes a measure-theoretic Hessian inequality usable on every prescribed geodesic, including geodesics that are invisible to almost-everywhere statements. For constant $G=c$ it says that $t\mapsto F(\sigma_t)-c\ell^2t^2/2$ is concave on every geodesic. Compared with earlier results, $F$ needs only to be bounded and Lipschitz (no second-order Sobolev or Laplacian-domain regularity), $G$ may vary in space, and $m$ may have infinite total mass. Such geodesic convexity statements feed into synthetic characterizations of sectional-curvature lower bounds and into rigidity arguments on $\mathrm{RCD}$ spaces.

Formalizing it. The statement depends on a large definitional layer: test plans, weak upper gradients, Cheeger energy, the Laplacian, Lott–Sturm–Villani $\mathrm{CD}(K,N)$ and the weak Hessian. None of these is in Mathlib. Formalizing them faithfully is reusable infrastructure for the whole theory of metric measure spaces with Ricci bounds. The proof itself relies on deep inputs (Savaré's self-improvement, the Ambrosio–Gigli–Savaré and Braun–Habermann–Sturm equivalences, Deng's non-branching theorem), so the realistic path is to state those inputs as milestones.

Difficulty

A weak Hessian bound holds only after integration against $m$. A naive argument would average the bound over a family of geodesics and then localize, but a fixed geodesic can carry zero measure, and almost-everywhere statements about transport geodesics say nothing about it. The natural fix — change the measure to $e^{\lambda F}m$ and use entropy convexity — requires the weighted Bochner inequality on the weighted test class. A Lipschitz weight does not preserve that class: the drift term $\Gamma(V,u)$ need not be Sobolev, as an explicit Euclidean example in the source shows (Remark 4.2). Localizing to one geodesic also needs uniqueness of geodesics between nearby endpoints, which in this generality comes from non-branching of finite-dimensional $\mathrm{RCD}$ spaces.

Formalization scope

• $X$ is a MetricSpace with Borel σ-algebra, CompleteSpace and SeparableSpace; $m$ is a Measure X with FullSupport and FiniteOnBoundedSets. RCD m K N is the unreduced CurvatureDimension with the $\tau$ coefficients for all $N'\ge N$, plus QuadraticCheegerEnergy (the parallelogram law for Cheeger energy).
• IsTestFunction requires the function itself (not merely a representative) to be bounded and globally Lipschitz, in the Laplacian domain, with Sobolev Laplacian. WeakHessianUpperBound m F G quantifies over compactly supported test functions $g$ and compactly supported nonnegative Lipschitz $h$.
• Geodesics are continuous maps Set.Icc 0 1 → X with $d(\sigma_s,\sigma_t)=|s-t|\,d(\sigma_0,\sigma_1)$, so constant curves are included (the conclusion is then trivial). The conclusion CurveSecondDerivativeBound integrates over $[0,1]$ against smooth nonnegative $\varphi$ with tsupport φ ⊆ Ioo 0 1.
• Choice-based definitions (weakGradient, laplacian) return $0$ when the object does not exist. The hypotheses on $F$ (bounded Lipschitz) and the test-function requirements ensure that the relevant gradients and Laplacians exist, so the hypothesis is not vacuous.
• Contributions welcome: a faithful library of test plans, minimal weak upper gradients and the Laplacian on metric measure spaces; the Lott–Sturm–Villani $\mathrm{CD}(K,N)$ condition; entropy and Wasserstein geodesics.

Selected references

• N. Gigli, Nonsmooth differential geometry — an approach tailored for spaces with Ricci curvature bounded from below, Mem. Amer. Math. Soc. 251 (2018). https://doi.org/10.1090/memo/1196
• G. Savaré, Self-improvement of the Bakry–Émery condition and Wasserstein contraction of the heat flow in $\mathrm{RCD}(K,\infty)$ metric measure spaces, Discrete Contin. Dyn. Syst. 34 (2014), 1641–1661. https://doi.org/10.3934/dcds.2014.34.1641
• L. Ambrosio, N. Gigli and G. Savaré, Bakry–Émery curvature-dimension condition and Riemannian Ricci curvature bounds, Ann. Probab. 43 (2015), 339–404. https://doi.org/10.1214/14-AOP907
• M. Braun, K. Habermann and K.-T. Sturm, Optimal transport, gradient estimates, and pathwise Brownian coupling on spaces with variable Ricci bounds, J. Math. Pures Appl. 147 (2021), 60–97. https://doi.org/10.1016/j.matpur.2021.01.002
• C. Ketterer, Obata's rigidity theorem for metric measure spaces, Anal. Geom. Metr. Spaces 3 (2015), 278–295. https://doi.org/10.1515/agms-2015-0016
• K.-T. Sturm, Gradient flows for semiconvex functions on metric measure spaces — existence, uniqueness and Lipschitz continuity, Proc. Amer. Math. Soc. 146 (2018), 3985–3994. https://doi.org/10.1090/proc/14061
• B.-X. Han, Characterizations of monotonicity of vector fields on metric measure spaces, Calc. Var. PDE 57 (2018). https://doi.org/10.1007/s00526-018-1388-9
• V. Kapovitch and C. Ketterer, CD meets CAT, J. reine angew. Math. 766 (2020), 1–44. https://arxiv.org/abs/1712.02839
• C. Brena and N. Gigli, Fine representation of Hessian of convex functions and Ricci tensor on RCD spaces, Potential Anal. 62 (2025), 703–737. https://doi.org/10.1007/s11118-024-10153-5
• Q. Deng, Hölder continuity of tangent cones in $\mathrm{RCD}(K,N)$ spaces and applications to non-branching, Geom. Topol. 29 (2025), 1037–1114. https://doi.org/10.2140/gt.2025.29.1037
• OpenAI, Weak Hessian bounds along every geodesic in RCD spaces, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Weak-Hessian-bounds-along-every-geodesic-in-RCD-spaces-September-24-2026/weak-hessian-geodesics.pdf

Motivation

The nodal set of a Laplace eigenfunction is the set where it vanishes. In 1982 Yau asked whether, on a fixed smooth closed Riemannian manifold of dimension $d$, the $(d-1)$-dimensional measure of the nodal set of every eigenfunction with eigenvalue $\lambda$ is comparable to $\sqrt\lambda$ from above and below (Yau, Problem section, Annals of Math. Studies 102, 1982). The conjectured two-sided bound

$$c_g\sqrt\lambda\le\mathcal H^{d-1}_g(Z_u)\le C_g\sqrt\lambda,$$

with constants depending only on the metric, has organized several decades of work on unique continuation and quantitative zero sets of elliptic equations. The lower and upper inequalities are logically separate, and a fixed metric must be distinguished from a metric chosen anew for each eigenvalue.

Timeline

• 1978. Brüning proves the sharp lower bound on smooth surfaces (doi:10.1007/BF01214561).
• 1982. Yau states the conjecture.
• 1988. Donnelly and Fefferman prove both bounds for real-analytic metrics (doi:10.1007/BF01393691).
• 1989. Hardt and Simon give a general non-polynomial upper estimate for smooth metrics (doi:10.4310/jdg/1214443599).
• 1990. Donnelly and Fefferman prove the surface upper bound $C\lambda^{3/4}$ (doi:10.1090/S0894-0347-1990-1035413-2).
• 2015–2017. Enciso and Peralta-Salas, then with Steinerberger, prescribe the nodal set of a first eigenfunction by choosing the metric (doi:10.4310/jdg/1442364650, doi:10.1093/imrn/rnw126).
• 2018. Logunov proves a polynomial upper estimate in dimension $\ge3$ (doi:10.4007/annals.2018.187.1.4) and the sharp lower estimate in every dimension (doi:10.4007/annals.2018.187.1.5); Logunov and Malinnikova improve the surface exponent to $3/4-\beta$ (doi:10.1007/978-3-319-59078-3_17).
• 2023. Hezari proves upper bounds for Gevrey and certain quasianalytic metrics (doi:10.1007/s00220-023-04853-z).

After Logunov, the smooth upper bound was known to be polynomial in $\lambda$ but not of order $\sqrt\lambda$. The source of this mission, an OpenAI preprint dated September 23, 2026, claims that the upper bound fails for fixed smooth metrics in dimensions three and four.

Setting

Let $(M,g)$ be a closed connected smooth Riemannian manifold of dimension $d$. In local coordinates, with $|g|=\det(g_{ij})$ and $(g^{ij})$ the inverse matrix, the Laplace–Beltrami operator is $\Delta_g u=|g|^{-1/2}\partial_i(|g|^{1/2}g^{ij}\partial_j u)$. An eigenfunction with eigenvalue $\lambda>0$ is a nonzero real $u$ with $-\Delta_g u=\lambda u$; its nodal set is $Z_u=\{u=0\}$, measured by $\mathcal H^{d-1}_g$, Hausdorff measure for the Riemannian distance of $g$.

The round metric $g_*$ on $S^3\subset\mathbb R^4$ is the pullback of the Euclidean inner product. A $C^\infty$ neighborhood of $g_*$ is any set of metrics containing all $g$ whose coefficient functions, in finitely many charts and on compact subsets, have derivatives up to some order within $\varepsilon$ of those of $g_*$.

Formalization targets

Goal: Theorem 1.1 (three-sphere)

For every $C^\infty$ neighborhood $\mathcal N$ of $g_*$ there are $g_\infty\in\mathcal N$, nonzero smooth $u_j$ and $\lambda_j>0$ with

$$-\Delta_{g_\infty}u_j=\lambda_ju_j,\qquad \lambda_j\to\infty,\qquad \frac{\mathcal H^2_{g_\infty}(Z_{u_j})}{\sqrt{\lambda_j}}\to\infty.$$

Lean: OAI.YauCounterexamples.sphere_three, open on the platform.

Milestone: Theorem 1.2 (four-manifold)

There are a smooth metric $g_\infty$ on $S^2\times\mathbb T^2$, nonzero smooth $u_j$ and $\lambda_j\to\infty$ with $-\Delta_{g_\infty}u_j=\lambda_ju_j$ and $\mathcal H^3_{g_\infty}(Z_{u_j})/\sqrt{\lambda_j}\to\infty$.

Significance

Theorem 1.1 disproves the upper-bound half of Yau's conjecture for smooth metrics already in dimension three, with metrics arbitrarily close to the round sphere, where the bound does hold. Neither theorem asserts a power-law excess, and neither contradicts the lower bound. Together with the companion preprints of this family (a sharp $\sqrt\lambda$ upper bound on smooth surfaces, and power-law violations in dimension at least five) it would locate the boundary of validity of the upper bound by dimension. The result is claimed in an OpenAI preprint that has not been peer reviewed, and no machine-checked proof exists.

Difficulty

Approximate eigenfunctions (quasimodes) with large nodal sets are comparatively easy to build locally. The obstacle is to replace each quasimode by an exact eigenfunction of an ordinary Laplace–Beltrami operator of one fixed metric, while keeping every sign change that witnesses nodal measure, and to do this for infinitely many eigenvalues at once with corrections that converge in $C^\infty$. A scalar potential or conductivity correction would be easy, but the operator must be a genuine metric Laplacian, which imposes a determinant identity between conductivity and density; the paper uses different, dimension-specific repairs in dimensions three and four. Also, the nodal set is not assumed regular, so its measure must be bounded below by a stable, lower semicontinuous count of sign changes.

Formalization scope

• SmoothMetric E M is Mathlib's ContMDiffRiemannianMetric on the tangent bundle. Sphere 3 is the unit sphere of EuclideanSpace ℝ (Fin 4) with its standard charts; the four-manifold is Sphere 2 × (Circle × Circle).
• laplaceBeltrami g u x is the coordinate formula above, in the chart at x with coordinates from Module.finBasis; only values in the open chart target are used.
• IsSmoothNeighborhood g₀ N: some finite list of compact-chart derivative tests and one $\varepsilon>0$ such that every metric passing them lies in N. Quantifying over all such N is the $C^\infty$ topology.
• nodalMeasure g d u is Measure.hausdorffMeasure d of $\{u=0\}$ for the path distance of g itself (EMetricSpace.ofRiemannianMetric), not the distance inherited from $\mathbb R^4$.
• HasUnboundedNodalRatio g d asks for smooth nonzero eigenfunctions with positive eigenvalues tending to $\infty$, finite nodal measures, and ratio $\mathcal H^{d-1}/\sqrt\lambda\to\infty$. Finiteness rules out the degenerate reading where an infinite measure would become $0$ under toReal; it holds for every eigenfunction of a smooth metric on a compact manifold (Hardt–Simon).

A complete development needs elliptic regularity and perturbation theory for simple eigenvalues of metric Laplacians, WKB-type quasimode constructions, and Hausdorff-measure lower bounds from sign changes along segments. Contributions formalizing the named propositions (Proposition 2.6 spherical profiles, Proposition 3.6 simultaneous wave realization, Proposition 4.4 exactification, Proposition 6.2 one construction step) are welcome.

Selected references

• OpenAI, Smooth counterexamples to Yau's nodal upper bound in dimensions three and four, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Smooth-counterexamples-to-Yaus-nodal-upper-bound-in-dimensions-three-and-four-September-23-2026/paper.pdf
• S.-T. Yau, Problem section, Seminar on Differential Geometry, Annals of Mathematics Studies 102, 1982.
• H. Donnelly, C. Fefferman, Nodal sets of eigenfunctions on Riemannian manifolds, Invent. Math., 1988. https://doi.org/10.1007/BF01393691
• R. Hardt, L. Simon, Nodal sets for solutions of elliptic equations, J. Differential Geom., 1989. https://doi.org/10.4310/jdg/1214443599
• A. Logunov, Nodal sets of Laplace eigenfunctions: polynomial upper estimates of the Hausdorff measure, Ann. of Math., 2018. https://doi.org/10.4007/annals.2018.187.1.4
• A. Logunov, Nodal sets of Laplace eigenfunctions: proof of Nadirashvili's conjecture and of the lower bound in Yau's conjecture, Ann. of Math., 2018. https://doi.org/10.4007/annals.2018.187.1.5
• A. Logunov, E. Malinnikova, Nodal sets of Laplace eigenfunctions: estimates of the Hausdorff measure in dimensions two and three, 2018. https://doi.org/10.1007/978-3-319-59078-3_17
• H. Hezari, Upper bounds on the size of nodal sets for Gevrey and quasianalytic Riemannian manifolds, Commun. Math. Phys., 2023. https://doi.org/10.1007/s00220-023-04853-z
• A. Enciso, D. Peralta-Salas, Eigenfunctions with prescribed nodal sets, J. Differential Geom., 2015. https://doi.org/10.4310/jdg/1442364650

Motivation

The nodal set of a Laplace eigenfunction is the set where it vanishes. On a vibrating membrane these are the curves that stay at rest (Chladni patterns), and in quantum mechanics they are the points where a stationary wave function has zero amplitude. A basic question is how large the nodal set is as the frequency grows. Yau conjectured in 1982 that on a smooth closed $n$-dimensional Riemannian manifold the $(n-1)$-dimensional measure of the nodal set of an eigenfunction with eigenvalue $\lambda$ is comparable to $\sqrt\lambda$, from above and below, with constants depending only on the manifold (Yau, Problem section, Annals of Math. Studies 102, 1982). The question is a test case for unique continuation and quantitative control of the zeros of solutions to elliptic equations.

Timeline

• 1978. Brüning proves the lower bound $\mathcal H^1(Z_u)\ge c\sqrt\lambda$ on smooth surfaces (doi:10.1007/BF01214561).
• 1982. Yau states the conjecture (upper and lower bounds of order $\sqrt\lambda$ in every dimension).
• 1988. Donnelly and Fefferman prove both bounds for real-analytic manifolds and metrics (doi:10.1007/BF01393691).
• 1990. Donnelly and Fefferman prove the upper bound $C\lambda^{3/4}$ for smooth surfaces (doi:10.1090/S0894-0347-1990-1035413-2); Dong gives a different proof of the same order in 1992 (doi:10.4310/JDG/1214448750).
• 2005. Nazarov, Polterovich and Sodin propose a statistical approach to local doubling and relate it to nodal length (doi:10.1353/ajm.2005.0030).
• 2015. Roy-Fortin establishes comparisons between local growth exponents and nodal length on surfaces (doi:10.2140/apde.2015.8.223, arXiv:1510.02376).
• 2018. Logunov proves the lower bound in every dimension (doi:10.4007/annals.2018.187.1.5); Logunov and Malinnikova improve the surface upper bound to $C\lambda^{3/4-\beta}$ for a universal $\beta\in(0,1/4)$ (doi:10.1007/978-3-319-59078-3_17).

The source of this mission, an OpenAI preprint dated September 23, 2026, claims the sharp upper bound $C\sqrt\lambda$ on every smooth closed surface, which together with Brüning's lower bound would settle Yau's conjecture in dimension two.

Setting

Let $(M,g)$ be a closed (compact, without boundary) connected smooth Riemannian surface. In local coordinates write $g=(g_{ij})$, $|g|=\det(g_{ij})$ and $(g^{ij})$ for the inverse matrix. The Laplace–Beltrami operator is

$$\Delta_g u=|g|^{-1/2}\sum_{i,j}\partial_i\bigl(|g|^{1/2}g^{ij}\partial_j u\bigr).$$

A Laplace eigenfunction with eigenvalue $\lambda>0$ is a nonzero real function $u$ with $-\Delta_g u=\lambda u$. Its nodal set is $Z_u=\{x\in M: u(x)=0\}$, and its nodal length is $\mathcal H^1_g(Z_u)$, the one-dimensional Hausdorff measure for the Riemannian distance $d_g$.

Formalization targets

Goal: Theorem 1.1

$$\exists\,C=C(M,g)<\infty\ \ \forall\lambda>0\ \ \forall u\not\equiv0:\quad -\Delta_g u=\lambda u\ \Longrightarrow\ \mathcal H^1_g(Z_u)\le C\sqrt\lambda.$$

The constant depends only on the surface and its metric and is the same for every eigenfunction in every positive eigenspace. The Lean statement OAI.SharpNodal.Main asserts MainStatement M; it is open on the platform.

Significance

The order $\sqrt\lambda$ is optimal: Brüning's lower bound shows it cannot be improved, and on the round sphere spherical harmonics attain it. Before this work the best smooth-surface upper bound was $C\lambda^{3/4-\beta}$. A sharp upper bound on every smooth surface, combined with the known lower bounds, would resolve Yau's conjecture for smooth closed surfaces; in dimensions three and higher the smooth upper bound remains a separate question (the companion missions in this family address it).

The theorem is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists. A formal proof would certify a long chain of quantitative estimates (Carleman inequalities, multiscale subdivision, packing), each of which is a natural target for reuse in other unique-continuation problems.

Difficulty

For a real-analytic metric, an eigenfunction extends holomorphically and its zeros can be counted by complex-analytic methods; this is how Donnelly and Fefferman obtain $\sqrt\lambda$. For a merely smooth metric no such extension exists. The standard route bounds nodal length on each wavelength-sized square by the local doubling exponent (growth of the $L^2$ norm from a disk to a larger disk). The known bounds on individual doubling exponents are too weak: a square can have growth much larger than average, and summing worst-case local bounds loses a power of $\lambda$. What is needed is control of the average growth over all wavelength-scale squares, while allowing large values on individual squares.

Formalization scope

• The surface is a type M with [MetricSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 2)) M] [IsManifold 𝓘(ℝ, Plane) ∞ M], a smooth RiemannianBundle on the tangent bundle, and [IsRiemannianManifold 𝓘(ℝ,Plane) M], so the metric-space distance is the Riemannian distance. CompactSpace and ConnectedSpace encode closed and connected; the model space has no boundary.
• laplaceBeltrami is the coordinate formula above, computed through chartAt with the metric matrix obtained from mfderiv of the inverse chart. No orientability is assumed.
• Eigenfunctions are assumed ContMDiff … ∞ and nonzero, with $-\Delta_g u=\lambda u$ at every point; smoothness is automatic by elliptic regularity, so this does not weaken the statement.
• nodalLength u is Measure.hausdorffMeasure 1 of $\{u=0\}$ for the Borel structure of the metric, valued in ℝ≥0∞; the bound is ≤ ENNReal.ofReal (C * Real.sqrt lam) with $C\ge0$ fixed before $\lambda$ and $u$.

A complete development needs local isothermal coordinates or a coordinate-free substitute, Carleman estimates, $L^2$ growth bounds, and a planar comparison between growth and nodal length (Roy-Fortin's theorem). Much of this, especially Hausdorff-measure estimates for zero sets of solutions of planar elliptic equations, is reusable. Contributions formalizing the paper's intermediate results (Theorem 2.2, Proposition 3.4, Theorem 5.5, Lemma 6.2) or Roy-Fortin's planar theorem are welcome.

Selected references

• OpenAI, Sharp nodal length on smooth surfaces, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Sharp-nodal-length-on-smooth-surfaces-September-23-2026/paper.pdf
• S.-T. Yau, Problem section, in Seminar on Differential Geometry, Annals of Mathematics Studies 102, Princeton University Press, 1982.
• J. Brüning, Über Knoten von Eigenfunktionen des Laplace–Beltrami-Operators, Math. Z., 1978. https://doi.org/10.1007/BF01214561
• H. Donnelly, C. Fefferman, Nodal sets of eigenfunctions on Riemannian manifolds, Invent. Math., 1988. https://doi.org/10.1007/BF01393691
• H. Donnelly, C. Fefferman, Nodal sets for eigenfunctions of the Laplacian on surfaces, J. Amer. Math. Soc., 1990. https://doi.org/10.1090/S0894-0347-1990-1035413-2
• R.-T. Dong, Nodal sets of eigenfunctions on Riemann surfaces, J. Differential Geom., 1992. https://doi.org/10.4310/JDG/1214448750
• F. Nazarov, L. Polterovich, M. Sodin, Sign and area in nodal geometry of Laplace eigenfunctions, Amer. J. Math., 2005. https://doi.org/10.1353/ajm.2005.0030
• G. Roy-Fortin, Nodal sets and growth exponents of Laplace eigenfunctions on surfaces, Anal. PDE, 2015. https://doi.org/10.2140/apde.2015.8.223
• A. Logunov, Nodal sets of Laplace eigenfunctions: proof of Nadirashvili's conjecture and of the lower bound in Yau's conjecture, Ann. of Math., 2018. https://doi.org/10.4007/annals.2018.187.1.5
• A. Logunov, E. Malinnikova, Nodal sets of Laplace eigenfunctions: estimates of the Hausdorff measure in dimensions two and three, Oper. Theory Adv. Appl. 261, 2018. https://doi.org/10.1007/978-3-319-59078-3_17

Motivation

How rigid is a von Neumann algebra inside $B(H)$? If two algebras $M,N\subseteq B(H)$ have unit balls that are uniformly close, must they be the same algebra up to a small change of coordinates? Kadison and Kastler introduced the distance between the unit balls in 1972 (Amer. J. Math. 1972) and asked whether sufficiently close algebras are spatially isomorphic, implemented by a unitary close to the identity. The positive answer for a class of algebras is called (strong) Kadison–Kastler stability. The problem connects perturbation theory, Hochschild cohomology, and Kadison's similarity problem, and it was settled previously only for injective (amenable) algebras, type I algebras, and specific nonamenable examples.

This mission asks for a formal proof of the uniform strong Kadison–Kastler stability theorem stated in an OpenAI preprint dated September 23, 2026 (source): a single tolerance works for all von Neumann algebras on all Hilbert spaces. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1972 — Kadison and Kastler introduce the metric and prove stability results for type I algebras (Amer. J. Math. 1972).
• 1974–1975 — Phillips proves spatial isomorphism for close type I algebras (Pacific J. Math. 1974); Christensen obtains a conjugating unitary near the identity (J. LMS 1975).
• 1977 — Christensen (Invent. Math. 1977), Johnson (Proc. LMS 1977) and Raeburn–Taylor (JFA 1977) settle the injective case.
• 1980 — Christensen's theory of near inclusions (Acta Math. 1980).
• 1982 — Johnson's examples show that for C*-algebras the implementing unitary cannot always be chosen near the identity in a uniform way (Canad. Math. Bull. 1982).
• 1983 — Haagerup's cyclic similarity estimate (Ann. of Math. 1983).
• 2010–2012 — Christensen, Sinclair, Smith, White and Winter prove spatial isomorphism for close separable nuclear C*-algebras (PNAS 2010; Acta Math. 2012).
• 2012–2014 — Cameron, Christensen, Sinclair, Smith, White and Wiggins construct the first nonamenable Kadison–Kastler stable factors, $(L^\infty(X)\rtimes SL_n(\mathbb Z))\bar\otimes R$ for $n\ge3$ (PNAS 2012; Duke 2014).
• September 2026 — The OpenAI preprint claims uniform stability for all von Neumann algebras (Theorem 1.1, p. 2).

Setting

Let $H$ be a complex Hilbert space and $B(H)$ the bounded operators with the operator norm. A von Neumann algebra $M\subseteq B(H)$ is a unital $*$-subalgebra equal to its double commutant (in particular it contains the identity $I_H$). Write $M_1=\{x\in M:\|x\|\le1\}$ for its unit ball. The Kadison–Kastler distance is the Hausdorff distance of unit balls,

$$d(M,N)=\max\Bigl(\sup_{x\in M_1}\inf_{y\in N_1}\|x-y\|,\ \sup_{y\in N_1}\inf_{x\in M_1}\|x-y\|\Bigr).$$

A unitary $u\in B(H)$ conjugates $M$ to $N$ if $uMu^*=N$.

Formalization targets

Goal: Theorem 1.1 (p. 2)

For every $\varepsilon>0$ there is $\delta>0$ such that for every complex Hilbert space $H$ and all von Neumann algebras $M,N\subseteq B(H)$ with $d(M,N)<\delta$, there is a unitary $u\in B(H)$ with

$$uMu^*=N\qquad\text{and}\qquad\|u-I_H\|<\varepsilon .$$

The tolerance $\delta$ depends only on $\varepsilon$: not on the algebras, their type, their representations, or the size of $H$.

Significance

The result itself. It answers the Kadison–Kastler perturbation question in its strongest uniform form for von Neumann algebras, including all nonamenable and type III cases and non-separable Hilbert spaces. Consequences include that every algebraic or analytic invariant preserved by unitary conjugacy (type, factoriality, property $\Gamma$, Cartan subalgebras) is locally constant in the Kadison–Kastler metric. The analogous C*-algebra statement fails in its uniform-unitary form by Johnson's examples, so the theorem is specific to von Neumann algebras.

Formalizing it. The statement uses only Mathlib's VonNeumannAlgebra, unitary operators and Hausdorff distance, so it is fully expressible today. The proof, however, draws on free probability, tracial ultraproducts, Tomita–Takesaki theory, crossed products, Poisson boundaries and measurable cocycles, most of which are absent from Mathlib. Formalizing even the amenable (injective) case would be a substantial reusable contribution.

Difficulty

Closeness of unit balls supplies nearby elements but no linear or multiplicative correspondence between the algebras, and it gives no control at matrix levels, where perturbation arguments naturally live. For nonamenable algebras the classical route through vanishing Hochschild cohomology is unavailable. The preprint proceeds by cases. For finite factors it proves a uniform bound on all matrix amplifications of commutator maps (Theorem 3.1, p. 11) and corrects nearby unitaries to a measurable cocycle over an amenable boundary action (Section 4). Infinite factors require comparing modular groups through Tomita graphs (Proposition 6.5, p. 41) and aligning the modular action (Proposition 7.1, p. 45) before passing to crossed products (Theorem 8.4, p. 59). General algebras then require aligning centers and passing from separable to arbitrary Hilbert spaces (Section 9) without losing uniformity.

Formalization scope

• $H$ ranges over complex Hilbert spaces (NormedAddCommGroup, InnerProductSpace ℂ, CompleteSpace) in a fixed universe u; $\delta$ is chosen before $H$, so the uniformity over Hilbert spaces is part of the statement.
• VonNeumannAlgebra H is Mathlib's notion; these algebras contain the identity, so "unital with identity $I_H$" is built in.
• kkDistance M N is Metric.hausdorffDist of the closed unit balls. Both balls contain $0$ and are bounded, so the Hausdorff distance is finite and the definition is exactly (1.1).
• NearConjugacy M N ε asks for a unitary $v$ with $v\,M\,v^*=N$ as sets and $\|v-1\|<\varepsilon$.
• There is no trivializing reading: the hypotheses are satisfied by $M=N$, and the conclusion is nontrivial for $M\neq N$.

Selected references

• OpenAI, Universal strong Kadison–Kastler stability, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Universal-strong-Kadison-Kastler-stability-September-23-2026/paper.pdf
• R. V. Kadison, D. Kastler, Perturbations of von Neumann algebras. I. Stability of type, Amer. J. Math. 94 (1972). https://doi.org/10.2307/2373592
• E. Christensen, Perturbations of type I von Neumann algebras, J. London Math. Soc. (1975). https://doi.org/10.1112/jlms/s2-9.3.395
• E. Christensen, Perturbation of operator algebras, Invent. Math. 43 (1977). https://doi.org/10.1007/BF01390201
• B. E. Johnson, Perturbations of Banach algebras, Proc. London Math. Soc. (1977). https://doi.org/10.1112/plms/s3-34.3.439
• I. Raeburn, J. L. Taylor, Hochschild cohomology and perturbations of Banach algebras, J. Funct. Anal. (1977). https://doi.org/10.1016/0022-1236(77)90072-6
• E. Christensen, Near inclusions of C-algebras*, Acta Math. 144 (1980). https://doi.org/10.1007/BF02392125
• B. E. Johnson, A counterexample in the perturbation theory of C-algebras*, Canad. Math. Bull. 25 (1982). https://doi.org/10.4153/CMB-1982-043-4
• U. Haagerup, Solution of the similarity problem for cyclic representations of C-algebras*, Ann. of Math. 118 (1983). https://doi.org/10.2307/2007028
• E. Christensen, A. M. Sinclair, R. R. Smith, S. A. White, W. Winter, Perturbations of nuclear C-algebras*, Acta Math. 208 (2012). https://doi.org/10.1007/s11511-012-0075-5
• J. Cameron, E. Christensen, A. M. Sinclair, R. R. Smith, S. A. White, A. D. Wiggins, Kadison–Kastler stable factors, Duke Math. J. 163 (2014). https://doi.org/10.1215/00127094-2819736

Motivation

Lieb–Thirring inequalities bound the negative eigenvalues of a Schrödinger operator $-\Delta-W$ by an integral of the potential. Lieb and Thirring introduced them in 1975 to give a short proof of the stability of matter, and they remain basic tools in mathematical physics, spectral theory and the analysis of many-fermion systems. The sharp constants are known only in a few cases. In one dimension, the Lieb–Thirring conjecture predicts the sharp constant for every exponent $\gamma$: for $1/2<\gamma<3/2$ it should be the constant of the best potential with a single bound state, given by an explicit $\operatorname{sech}^2$ profile.

Timeline

• 1961. Keller solves the one-bound-state variational problem (doi:10.1063/1.1703708).
• 1971, 1974. Inverse-scattering trace identities for the KdV equation give the sharp value $L_{3/2,1}=3/16$ (Zakharov–Faddeev, doi:10.1007/BF01086739; Gardner–Greene–Kruskal–Miura, doi:10.1002/cpa.3160270108).
• 1975–1976. Lieb and Thirring prove their inequalities and state the one-dimensional conjecture (doi:10.1103/PhysRevLett.35.687).
• 1978. Aizenman and Lieb extend semiclassical equality to all $\gamma\ge3/2$ (doi:10.1016/0375-9601(78)90385-7).
• 1996, 1998. Weidl proves finiteness of $L_{1/2,1}$ (doi:10.1007/BF02104912); Hundertmark, Lieb and Thomas obtain its sharp value $1/2$ (doi:10.4310/ATMP.1998.v2.n4.a2).
• 2000. Laptev and Weidl prove sharp semiclassical constants in all dimensions for $\gamma\ge3/2$ (doi:10.1007/BF02392782); Hundertmark, Laptev and Weidl prove $L_{\gamma,1}\le2L^{\rm cl}_{\gamma,1}$ for $1/2\le\gamma<3/2$ (doi:10.1007/s002220000077).
• 2008–2025. Improved constants at $\gamma=1$ by Dolbeault–Laptev–Loss (doi:10.4171/JEMS/142), Frank–Hundertmark–Jex–Nam (doi:10.4171/JEMS/1062) and Corso–Ried (doi:10.1007/s00220-024-05216-y); Levitt's numerics support the conjectured value (doi:10.4171/JST/65).
• 2026. Read and Schulz prove the sharp case $\gamma=1$ (arXiv:2609.10478).

The source of this mission, an OpenAI preprint dated September 23, 2026, proves the conjectured sharp constant for every $1/2<\gamma<3/2$.

Setting

For $0\le W\in L^{\gamma+1/2}(\mathbb R)$, let $H_{-W}$ be the self-adjoint operator of the quadratic form

$$h_{-W}[v]=\int_{\mathbb R}|v'|^2\,dx-\int_{\mathbb R}W|v|^2\,dx,\qquad v\in H^1(\mathbb R).$$

For $\gamma>1/2$ its negative spectrum is discrete; write $\operatorname{Tr}(H_{-W})_-^\gamma=\sum_{\lambda_j<0}|\lambda_j|^\gamma$ with multiplicity, possibly $+\infty$ a priori. The optimal constant is

$$L_{\gamma,1}=\sup_{0\le W\in L^{\gamma+1/2},\ W\not\equiv0}\frac{\operatorname{Tr}(H_{-W})_-^\gamma}{\int W^{\gamma+1/2}},$$

$L^{(1)}_{\gamma,1}$ is the same supremum with only the lowest eigenvalue retained, and the semiclassical constant is

$$L^{\rm cl}_{\gamma,1}=\frac{\Gamma(\gamma+1)}{2\sqrt\pi\,\Gamma(\gamma+3/2)}.$$

Formalization targets

Goal: Theorem 1.1

For $1/2<\gamma<3/2$ and every $0\le W\in L^{\gamma+1/2}(\mathbb R)$,

$$\operatorname{Tr}(H_{-W})_-^\gamma\ \le\ 2\Bigl(\frac{\gamma-1/2}{\gamma+1/2}\Bigr)^{\gamma-1/2}L^{\rm cl}_{\gamma,1}\int_{\mathbb R}W^{\gamma+1/2};$$

the constant equals $L_{\gamma,1}=L^{(1)}_{\gamma,1}$, and with $r=(\gamma-1/2)^{-1}$ equality holds for $W(x)=(r+1)\operatorname{sech}^2(rx)$. The Lean statement OAI.SharpLiebThirring.sharp_lieb_thirring is open on the platform.

Significance

The theorem settles the one-dimensional Lieb–Thirring conjecture on the whole interval $1/2<\gamma<3/2$, extending the case $\gamma=1$ of Read and Schulz: allowing many bound states never beats a single optimally shaped well. Combined with the known endpoint results ($\gamma=1/2$ and $\gamma\ge3/2$), it completes the sharp one-dimensional constants. It also gives the corresponding bound for signed potentials (Corollary 7.3), and through the Laptev–Weidl lifting method one-dimensional sharp constants feed into higher-dimensional estimates.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. A formal proof would certify a proof whose key step is a finite-interval action inequality established by a continuation and degree argument for matrix fields.

Difficulty

Single-state bounds and numerical evidence say nothing about potentials with many bound states, and the conjecture requires a bound uniform over all orthonormal families of eigenfunctions. Methods that work at $\gamma=1$ (where the inequality is dual to a kinetic-energy bound for orthonormal families) do not directly apply at other exponents, since the moment $\sum|\lambda_j|^\gamma$ is not linear in the density matrix. The proof must keep track of the individual eigenvalue scales.

Formalization scope

• H1 packages $u\in L^2(\mathbb R;\mathbb C)$ with a weak derivative in $L^2$, tested against smooth compactly supported functions.
• A negative eigenvalue $-k^2$ ($k>0$) is a weak eigenvalue of the form: $h_{-W}(v,u)=-k^2\langle v,u\rangle$ for all $v\in H^1$.
• negativeMoment γ W is the supremum, in $[0,\infty]$, over all finite orthonormal families of such eigenfunctions of $\sum_ik_i^{2\gamma}$; this counts multiplicity and does not presuppose finiteness. oneStateMoment retains one eigenfunction.
• Admissible γ W is $W\ge0$ a.e. and $W\in L^{\gamma+1/2}$; potentialMass is the lower Lebesgue integral of $W^{\gamma+1/2}$; the optimal constants are suprema over admissible $W$ with positive mass.
• For admissible $W$ the integral $\int W\bar uv$ converges for $u,v\in H^1$, so the form is correctly defined.

A complete development needs Sobolev space $H^1(\mathbb R)$ and form methods, the variational characterization of negative eigenvalues, Gamma-function identities for $L^{\rm cl}_{\gamma,1}$, the explicit $\operatorname{sech}^2$ eigenvalue computation, and the paper's action inequality. Contributions formalizing Theorem 2.1 (action inequality) and the equality computation for the $\operatorname{sech}^2$ potential are welcome.

Selected references

• OpenAI, Sharp one-dimensional Lieb–Thirring constants, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Sharp-One-Dimensional-Lieb-Thirring-Constants-September-23-2026/paper.pdf
• E. H. Lieb, W. E. Thirring, Bound for the kinetic energy of fermions which proves the stability of matter, Phys. Rev. Lett., 1975. https://doi.org/10.1103/PhysRevLett.35.687
• J. B. Keller, Lower bounds and isoperimetric inequalities for eigenvalues of the Schrödinger equation, J. Math. Phys., 1961. https://doi.org/10.1063/1.1703708
• D. Hundertmark, E. H. Lieb, L. E. Thomas, A sharp bound for an eigenvalue moment of the one-dimensional Schrödinger operator, Adv. Theor. Math. Phys., 1998. https://doi.org/10.4310/ATMP.1998.v2.n4.a2
• A. Laptev, T. Weidl, Sharp Lieb–Thirring inequalities in high dimensions, Acta Math., 2000. https://doi.org/10.1007/BF02392782
• D. Hundertmark, A. Laptev, T. Weidl, New bounds on the Lieb–Thirring constants, Invent. Math., 2000. https://doi.org/10.1007/s002220000077
• R. L. Frank, D. Hundertmark, M. Jex, P. T. Nam, The Lieb–Thirring inequality revisited, J. Eur. Math. Soc., 2021. https://doi.org/10.4171/JEMS/1062
• A. Levitt, Best constants in Lieb–Thirring inequalities: a numerical investigation, J. Spectr. Theory, 2014. https://doi.org/10.4171/JST/65
• L. Read, M. R. Schulz, The sharp one-dimensional Lieb–Thirring inequality for the sum of eigenvalues, preprint, 2026. https://arxiv.org/abs/2609.10478

Motivation

A limit cycle of a planar vector field is a periodic orbit that is isolated among periodic orbits. The second part of Hilbert's sixteenth problem asks how many limit cycles a polynomial vector field of a given degree can have, and it is open even for quadratic fields. The classical Liénard systems

$$\dot x=y-F(x),\qquad \dot y=-x,$$

equivalent to the oscillator equation $x''+F'(x)\,x'+x=0$, are the most studied restricted family. In 1977 Lins, de Melo and Pugh conjectured that for $\deg F=n$ the maximum number of limit cycles is $\lfloor (n-1)/2\rfloor$. The conjecture is now known to fail for $n\ge6$, holds for $n\le4$, and degree five was the remaining undecided case, where it predicts exactly two.

This mission asks for a formal proof of the degree-five bound and its sharpness, as stated in an OpenAI preprint dated September 24, 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

• 1975 — Rychkov proves the two-cycle bound for odd quintic $F$ (Differ. Uravn. 11, 1975).
• 1977 — Lins, de Melo and Pugh formulate the $\lfloor(n-1)/2\rfloor$ conjecture (LNM 597).
• 2007 — Dumortier, Panazzolo and Roussarie find four cycles with $\deg F=7$ (Proc. AMS 2007).
• 2011 — De Maesschalck and Dumortier find $\lfloor(n-1)/2\rfloor+2$ cycles for every $n\ge6$ (JDE 2011); De Maesschalck and Huzak later obtain at least $n-2$ (JDDE 2015).
• 2012 — Li and Llibre prove at most one limit cycle for $\deg F=4$ (JDE 2012).
• 2014 — Li and Lu bound by two the cyclicity of nondegenerate slow–fast cycles in degree five (JDE 2014), a limiting-regime result.
• 2017 — Llibre and Zhang survey the conjecture (Expo. Math. 2017).
• September 2026 — The OpenAI preprint claims the unrestricted degree-five bound of two (Theorem 1.1, p. 1).

Setting

For a real polynomial $F$ (the primitive of the damping), consider the vector field $V_F(x,y)=(y-F(x),\,-x)$ on $\mathbb R^2$. A solution is a differentiable $z:\mathbb R\to\mathbb R^2$ with $z'(t)=V_F(z(t))$ for all $t$. A periodic orbit is the image of a nonconstant solution that is periodic with some period $T>0$. A limit cycle is a periodic orbit $C$ having an open neighbourhood $U$ such that every periodic orbit contained in $U$ equals $C$. Limit cycles are counted as sets: once each, regardless of multiplicity, stability or hyperbolicity. The periodic orbits of a centre are not limit cycles.

Formalization targets

Goal: Theorem 1.1 (p. 1)

For every real polynomial $F$ with $\deg F\le5$,

$$\#\{C\subset\mathbb R^2:\ C\ \text{is a limit cycle of }V_F\}\ \le\ 2,$$

and some $F$ with $\deg F\le5$ has exactly two limit cycles. No parity, coefficient-sign, hyperbolicity or amplitude restriction is imposed.

Significance

The result itself. It decides the last open degree of the Lins–de Melo–Pugh conjecture in the affirmative, so the conjecture is true exactly for $\deg F\le5$. Unlike the slow–fast result of Li and Lu, it bounds all cycles of every quintic system, including degenerate (multiple) ones and cycles of large amplitude. The preprint also corrects a proposed four-cycle quintic example from the literature by identifying it with a family known to have exactly two periodic solutions (p. 2).

Formalizing it. The statement uses only polynomials, ODE solutions and planar topology, so it is well suited to formal verification, and it would be one of the first machine-checked global limit-cycle bounds for a nonlinear family. The proof's general comparison results for smooth profiles (Propositions 5.2 and 5.3, pp. 32–34) and the global quadratic fit (Theorem 3.6, p. 18) are independent of the polynomial application and reusable.

Difficulty

Small-amplitude (Hopf/Melnikov) calculations only control cycles near the origin or near a perturbation of a centre; they say nothing about distant cycles. The even coefficients of $F$ prevent the reduction to the odd quintic family settled by Rychkov. Generic-perturbation arguments that remove multiple cycles cannot be used, since the count must include degenerate cycles. The preprint keeps the two half-orbits separate, writes each as an arch in coordinates $u=x^2/2$ valid at every amplitude, fits each arch by a quadratic comparison profile (Theorem 3.6), and controls how the fitted parameters move with width through a Schwarzian-type model inequality (Theorem 4.1, p. 20). Periodic orbits then become zeros of a single matching function (Proposition 2.5, p. 10), whose isolated zeros are bounded using an integrating factor (Section 6).

Formalization scope

• The plane is ℝ × ℝ; vectorField F z = (z.2 - F.eval z.1, -z.1) with F : Polynomial ℝ and F.degree ≤ 5 (this includes constants and the zero polynomial, which have no limit cycles).
• IsSolution requires HasDerivAt at every real time; IsPeriodicOrbit asks for a solution, a period T > 0, non-constancy, and C = range z.
• IsLimitCycle F C is a periodic orbit with an open U ⊇ C such that every periodic orbit C' ⊆ U equals C.
• Counting uses Set.encard on the set of limit cycles, so infinitely many would give ⊤; the goal asks for ≤ 2 for every admissible F and = 2 for some.
• Neither conjunct is vacuous: the lower bound requires two actual distinct isolated periodic orbits.

Welcome contributions: existence and smooth dependence of return maps for planar polynomial flows, and the energy-identity first-order return calculation used for sharpness (Section 7, p. 39).

Selected references

• OpenAI, Two limit cycles for quintic Liénard systems, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/two-limit-cycles-for-quintic-lienard-systems-September-24-2026/two-limit-cycles-for-quintic-lienard-systems-September-24-2026.pdf
• A. Lins, W. de Melo, C. C. Pugh, On Liénard's equation, in Geometry and Topology, LNM 597, Springer, 1977, 335–357. https://doi.org/10.1007/BFb0085364
• G. S. Rychkov, The maximal number of limit cycles of the system ẏ=−x, ẋ=y−Σa_i x^{2i+1} is equal to two, Differ. Uravn. 11 (1975), 390–391. https://www.mathnet.ru/eng/de2400
• F. Dumortier, D. Panazzolo, R. Roussarie, More limit cycles than expected in Liénard equations, Proc. AMS 135 (2007). https://doi.org/10.1090/S0002-9939-07-08688-1
• P. De Maesschalck, F. Dumortier, Classical Liénard equations of degree n≥6 can have ⌊(n−1)/2⌋+2 limit cycles, J. Differential Equations 250 (2011). https://doi.org/10.1016/j.jde.2010.12.003
• P. De Maesschalck, R. Huzak, Slow divergence integrals in classical Liénard equations near centers, J. Dyn. Differ. Equ. 27 (2015). https://doi.org/10.1007/s10884-014-9358-1
• C. Li, J. Llibre, Uniqueness of limit cycles for Liénard differential equations of degree four, J. Differential Equations 252 (2012). https://doi.org/10.1016/j.jde.2011.11.002
• C. Li, K. Lu, Slow divergence integral and its application to classical Liénard equations of degree 5, J. Differential Equations 257 (2014). https://doi.org/10.1016/j.jde.2014.08.015
• J. Llibre, X. Zhang, Limit cycles of the classical Liénard differential systems: a survey on the Lins Neto, de Melo and Pugh's conjecture, Expo. Math. 35 (2017). https://doi.org/10.1016/j.exmath.2016.12.001
• K. Odani, Existence of exactly N periodic solutions for Liénard systems, Funkcial. Ekvac. 39 (1996). https://doi.org/10.24546/0100499900

Motivation: a logarithmic strengthening of Brunn–Minkowski

The Brunn–Minkowski inequality $|(1-\lambda)K+\lambda L|\ge|K|^{1-\lambda}|L|^\lambda$ is a cornerstone of convex geometry, with consequences ranging from the isoperimetric inequality to concentration of measure. The $L_p$ Brunn–Minkowski theory of Firey and Lutwak replaces the Minkowski combination, whose support function is $(1-\lambda)h_K+\lambda h_L$, by a $p$-mean of support functions. As $p\downarrow0$ the $p$-mean becomes the geometric mean $h_K^{1-\lambda}h_L^{\lambda}$, giving the logarithmic combination of two bodies. In 2012 Böröczky, Lutwak, Yang and Zhang conjectured that, for origin-symmetric convex bodies, the logarithmic combination already satisfies the multiplicative Brunn–Minkowski bound. This would be a strict strengthening of the classical inequality in the symmetric case. The conjecture is equivalent to a logarithmic Minkowski inequality for cone-volume measures and, by work of Saroglou, implies the (B)-conjecture for even log-concave measures. Symmetry is essential: the inequality fails for general bodies.

Timeline

• 1962–1993 — Firey introduces $p$-means of convex bodies (Math. Scand. 10); Lutwak develops the $L_p$ Brunn–Minkowski–Firey theory (J. Differential Geom. 38).
• 2012 — Böröczky, Lutwak, Yang and Zhang pose the origin-symmetric log-Brunn–Minkowski conjecture (Problem 1.1), prove it in the plane, and show its equivalence with the logarithmic Minkowski inequality (Adv. Math.); in 2013 they characterize even cone-volume measures (J. Amer. Math. Soc. 26).
• 2015–2016 — Saroglou proves the inequality for bodies unconditional in a common basis (Geom. Dedicata) and shows that the Lebesgue case implies the same inequality for all even log-concave measures, hence the (B)-conjecture (Mathematika).
• 2017 — Colesanti, Livshyts and Marsiglietti prove a local version near Euclidean balls (J. Funct. Anal. 273).
• 2020–2022 — Chen, Huang, Li and Liu prove the global $L_p$ inequality for $p$ close to $1$ (Adv. Math. 368); Kolesnikov and Milman prove the local $L_p$ inequality for $p\ge1-cn^{-3/2}$ (Mem. AMS 277); Putterman proves local-to-global equivalence for all $p\in[0,1)$ (J. Funct. Anal. 280); Böröczky and Kalantzopoulos treat bodies with common reflection symmetries (Trans. AMS 375, 2022).
• 2023 — van Handel proves the local logarithmic inequality for origin-symmetric zonoids (GAFA Seminar).
• 2026 — An OpenAI preprint, The logarithmic Brunn–Minkowski conjecture (OpenAI Math Release, September 23, 2026), claims the conjecture for origin-symmetric convex bodies in every dimension. It has not been peer reviewed, and its proof is not formally verified.

Setting

A convex body $K\subset\mathbb R^n$ is a compact convex set with nonempty interior; it is origin-symmetric if $K=-K$, in which case $0$ is an interior point. Its support function is

$$h_K(u)=\max_{x\in K}\langle x,u\rangle ,\qquad u\in S^{n-1},$$

which is strictly positive for origin-symmetric bodies. For a positive function $f$ on the sphere, the Wulff body is

$$\mathcal W[f]=\bigcap_{u\in S^{n-1}}\{x:\langle x,u\rangle\le f(u)\}.$$

The logarithmic combination of $K,L$ with parameter $\lambda\in[0,1]$ is $\mathcal W[h_K^{1-\lambda}h_L^{\lambda}]$. In general $h_K^{1-\lambda}h_L^{\lambda}$ is not itself a support function, which is why the Wulff body is needed. $|\cdot|$ denotes Lebesgue measure.

Formalization targets

Goal: the even logarithmic Brunn–Minkowski inequality (Theorem 1.1)

For $n\ge1$, origin-symmetric convex bodies $K,L\subset\mathbb R^n$ and $0\le\lambda\le1$,

$$\bigl|\mathcal W[h_K^{1-\lambda}h_L^{\lambda}]\bigr|\ \ge\ |K|^{1-\lambda}\,|L|^{\lambda}.$$

The goal statement is published on the platform with status Open.

Significance

The result itself. By the arithmetic–geometric mean inequality, $\mathcal W[h_K^{1-\lambda}h_L^\lambda]\subseteq(1-\lambda)K+\lambda L$, so the theorem strengthens the multiplicative Brunn–Minkowski inequality for symmetric bodies. It implies the symmetric $L_p$ Brunn–Minkowski inequality for every $0<p<1$ (Corollary 1.2 of the source), the logarithmic Minkowski inequality for cone-volume measures, and, through Saroglou's transfer, the (B)-conjecture: $t\mapsto\mu(e^tK)$ is log-concave for every even log-concave measure $\mu$ and origin-symmetric convex body $K$ (Corollary 8.1 of the source).

Formalizing it. The statement uses only Euclidean space, support functions and Lebesgue measure, all in Mathlib. The proof uses smooth approximation of polytopes, moment coordinates, a variance bound and a tensor estimate. A formal proof would put a long-standing conjecture of convex geometry on a machine-checked footing; Mathlib does not yet contain the classical Brunn–Minkowski inequality in this generality, and that would be a natural reusable milestone.

Difficulty

The classical proofs of Brunn–Minkowski (Prékopa–Leindler, mass transport) apply to Minkowski sums, but the logarithmic combination is not a Minkowski sum and $h_K^{1-\lambda}h_L^\lambda$ is not a support function, so these tools give only the weaker inclusion bound. Local (second-variation) approaches reduce the problem to a spectral gap for the Hilbert–Brunn–Minkowski operator on even functions, but local-to-global arguments had only been completed near the ball, for zonoids, or under extra symmetry. Without symmetry the inequality is false, so any argument must use the evenness of the bodies.

Formalization scope

• Space is EuclideanSpace ℝ (Fin n) with $n\ge1$; convex bodies are compact, convex, with nonempty interior; symmetry is x ∈ K ↔ -x ∈ K.
• The support function is a real sSup of $\langle x,u\rangle$ over $K$, nonempty and bounded for a convex body, so it is the true maximum. Real powers rpow are applied to positive support values (positivity follows from symmetry and nonempty interior).
• The Wulff body is the intersection of half-spaces over unit vectors $u$. Volumes are volume in ℝ≥0∞, with ℝ≥0∞-valued powers $1-\lambda$ and $\lambda$. At $\lambda\in\{0,1\}$ the inequality reduces to $|K|\le|K|$ (resp. $|L|\le|L|$), so the edge cases are consistent.
• Needed infrastructure: support functions and Wulff shapes, polytope approximation, the Prékopa–Leindler inequality, and log-concave measures. Contributions formalizing the planar case, the unconditional case (Saroglou) or Corollary 1.2 from Theorem 1.1 are welcome.

Selected references

• W. J. Firey, p-Means of convex bodies, Math. Scand. 10 (1962), 17–24. https://doi.org/10.7146/math.scand.a-10510
• E. Lutwak, The Brunn–Minkowski–Firey theory I, J. Differential Geom. 38 (1993), 131–150. https://doi.org/10.4310/jdg/1214454097
• K. J. Böröczky, E. Lutwak, D. Yang and G. Zhang, The log-Brunn–Minkowski inequality, Adv. Math. (2012). https://doi.org/10.1016/j.aim.2012.07.015
• K. J. Böröczky, E. Lutwak, D. Yang and G. Zhang, The logarithmic Minkowski problem, J. Amer. Math. Soc. 26 (2013), 831–852. https://doi.org/10.1090/S0894-0347-2012-00741-3
• C. Saroglou, Remarks on the conjectured log-Brunn–Minkowski inequality, Geom. Dedicata (2015). https://doi.org/10.1007/s10711-014-9993-z
• C. Saroglou, More on logarithmic sums of convex bodies, Mathematika (2016). https://doi.org/10.1112/S0025579316000061
• A. V. Kolesnikov and E. Milman, Local $L^p$-Brunn–Minkowski inequalities for $p<1$, Mem. Amer. Math. Soc. 277 (2022). https://doi.org/10.1090/memo/1360
• E. Putterman, Equivalence of the local and global versions of the $L^p$-Brunn–Minkowski inequality, J. Funct. Anal. 280 (2021). https://doi.org/10.1016/j.jfa.2021.108956
• R. van Handel, The local logarithmic Brunn–Minkowski inequality for zonoids, GAFA Seminar 2020–2022 (2023). https://doi.org/10.1007/978-3-031-26300-2_14
• OpenAI, The logarithmic Brunn–Minkowski conjecture, OpenAI Math Release preprint, September 23, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-logarithmic-Brunn-Minkowski-conjecture-September-23-2026/paper.pdf

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

$$Mf(x)=\sup_{r>0}\frac1{\pi r^2}\int_{B(x,r)}|f(y)|\,dy\in[0,\infty].$$

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$),

$$\int_{\mathbb R^2}|\nabla S_{a,b}g|\,dx\le C\int_{\mathbb R^2}|\nabla g|\,dx,$$

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

$$\int_{\mathbb R^2}|\nabla Mf|\,dx\le C\int_{\mathbb R^2}|\nabla f|\,dx.$$

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

$$H^{\varepsilon}_{v,a}f(x)=\int_{\varepsilon<|t|<a} f\bigl(x-t\,v(x)\bigr)\,\frac{dt}{t}.$$

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)$,

$$\sup_{0<\varepsilon<a_*}\|H^{\varepsilon}_{v,a_*}f\|_{L^2}\le C_*\|f\|_{L^2},\qquad \|H_{v,a_*}f\|_2\le C_*\|f\|_2,$$ $$\bigl|\{x:|H_{v,a_*}f(x)|>\lambda\}\bigr|\le C_*^2\lambda^{-2}\|f\|_2^2\qquad(\lambda>0),$$

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

$$E\subset\mathbb R^2\ \text{compact},\ \dim_HE>1\ \Longrightarrow\ \mathcal L^1(\Delta(E))>0.$$

Goal: Theorem 1.1

$$d\ge2,\ E\subset\mathbb R^d\ \text{compact},\ \dim_HE>\tfrac d2\ \Longrightarrow\ \mathcal L^1(\Delta(E))>0.$$

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

The Riemann mapping theorem says that every simply connected proper domain in the plane is conformally equivalent to the unit disk. For domains with more complicated complements one needs a model with many "holes". Koebe's Kreisnormierungsproblem (1908) asks whether every domain in the Riemann sphere is conformally equivalent to a circle domain, one whose complementary components are all round disks or points. Such a model would give a canonical geometric picture of an arbitrary planar domain, and it is closely tied to circle packings, Kleinian groups and the geometry of hyperbolic surfaces of genus zero.

Timeline

• 1908. Koebe poses the problem (Nachr. Ges. Wiss. Göttingen, 1908).
• 1920. Koebe's treatment of the finitely connected case (doi:10.1007/BF01199400).
• 1993. He and Schramm prove the conjecture for countably connected domains (doi:10.2307/2946541).
• 1995. Schramm introduces transboundary extremal length and treats domains bounded by points and $K$-quasicircles (doi:10.1007/BF02788827).
• 2025. Rajala shows that arbitrary interior exhaustions can fail to have circle-domain limits and proves an exhaustion refinement theorem for countably connected domains (doi:10.1353/ajm.2025.a966291); Ntalampekos and Rajala study exhaustions of circle domains (arXiv:2312.06840).
• 2026. Esmayli and Rajala prove uniformization for cospread domains and under a quasitripod condition (arXiv:2401.08485); Karafyllia and Ntalampekos treat spherical Gromov-hyperbolic domains (arXiv:2405.13782). Ntalampekos surveys the area (arXiv:2603.15098).

The source of this mission, an OpenAI preprint dated September 23, 2026, claims the conjecture in its unrestricted form.

Setting

The Riemann sphere is $\widehat{\mathbb C}=\mathbb C\cup\{\infty\}$, with local coordinate $z$ near finite points and $1/z$ near $\infty$. A domain is a nonempty connected open subset. A map $f$ is conformal at $p$ if it is continuous at $p$ and, in these coordinates, complex differentiable at $p$ with nonzero derivative. A conformal equivalence $f:U\to V$ is a bijection that is conformal at every point of $U$ and whose inverse is conformal at every point of $V$.

A closed round disk in $\widehat{\mathbb C}$ is the image of the closed unit disk under a Möbius transformation $z\mapsto (az+b)/(cz+d)$, $ad-bc\ne0$; these are closed Euclidean disks, closed half-planes together with $\infty$, and complements of open disks. A circle domain is a domain each of whose complementary connected components is a closed round disk or a single point. The complement may be empty, finite, countable or uncountable.

Formalization targets

Goal: Theorem 1.1 (circle-domain uniformization)

$$\forall\,G\subset\widehat{\mathbb C}\ \text{domain}\quad\exists\,\Omega\ \text{circle domain},\ \exists\,f:G\xrightarrow{\ \text{conformal}\ }\Omega\ \text{bijective}.$$

Lean: OAI.Problem047.koebe_circle_domain, open on the platform.

Significance

The theorem would complete the existence half of Koebe's problem with no restriction on the number, size or geometry of the complementary components. The paper derives a consequence for hyperbolic geometry (Corollary 8.1): every complete hyperbolic surface of genus zero is isometric to the boundary of the convex hull of a closed set in $\partial_\infty\mathbb H^3$ whose components are round disks or points. Combined with the exhaustion theorem of Ntalampekos and Rajala, it also gives convergent finitely connected approximations for every proper domain. Uniqueness up to Möbius maps is a different question (the He–Schramm rigidity conjecture), addressed in the companion mission on removable boundaries.

The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists. Mathlib has neither the Riemann mapping theorem in full generality nor finitely connected circle-domain uniformization, so a formal proof would build substantial reusable complex-analytic infrastructure.

Difficulty

The standard approach uniformizes finitely connected approximations, whose complements are finitely many round disks, and passes to a limit. The difficulty is control at the limit: with possibly uncountably many complementary components, a limiting component can be strictly larger than the round disk obtained by following one approximating disk, or can be a non-round continuum for which no disk was followed at all. Rajala showed that arbitrary exhaustions can indeed fail to produce circle-domain limits, so the approximations must be chosen with care, and all components must be controlled simultaneously, not one at a time.

Formalization scope

• Sphere := OnePoint ℂ; Möbius maps are Matrix.GeneralLinearGroup (Fin 2) ℂ acting on it.
• IsConformalAt f p: ContinuousAt f p and a nonzero HasDerivAt of $f$ in the charts chart p, chart (f p) (identity coordinate at finite points, $z\mapsto1/z$ at $\infty$).
• IsConformalEquivalence f U V: $f$ conformal on $U$, MapsTo f U V, and a conformal g on $V$ with MapsTo g V U that is a two-sided inverse.
• IsCircleDomain V: open, IsConnected (hence nonempty), and every connectedComponentIn Vᶜ p is a singleton or IsRoundClosedDisk (a Möbius image of the closed unit disk).
• The goal quantifies over all open connected U; there is no countability or regularity assumption on the complement.

A complete development needs finitely connected uniformization, normal families on the sphere, Dirichlet energy and extremal length, and component correspondence for limits. Contributions formalizing the named intermediate results (Theorem 3.1 finite transfer, Theorem 4.3 compatible barrier lemma, Theorem 5.1 positive-law alternative, Theorem 7.5 retained-test transfer) or the classical He–Schramm countable case are welcome.

Selected references

• OpenAI, Koebe's Circle-Domain Conjecture, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Koebes-Circle-Domain-Conjecture-September-23-2026/paper.pdf
• P. Koebe, Über die Uniformisierung beliebiger analytischer Kurven (Dritte Mitteilung), Nachr. Ges. Wiss. Göttingen, 1908.
• P. Koebe, Abhandlungen zur Theorie der konformen Abbildung VI, Math. Z., 1920. https://doi.org/10.1007/BF01199400
• Z.-X. He, O. Schramm, Fixed points, Koebe uniformization and circle packings, Ann. of Math., 1993. https://doi.org/10.2307/2946541
• O. Schramm, Transboundary extremal length, J. Analyse Math., 1995. https://doi.org/10.1007/BF02788827
• K. Rajala, Uniformization of planar domains by exhaustion, Amer. J. Math., 2025. https://doi.org/10.1353/ajm.2025.a966291
• D. Ntalampekos, K. Rajala, Exhaustions of circle domains, IMRN, 2025. https://doi.org/10.1093/imrn/rnaf296
• B. Esmayli, K. Rajala, Conformal uniformization of domains bounded by quasitripods, Duke Math. J., 2026. https://doi.org/10.1215/00127094-2025-0035
• C. Karafyllia, D. Ntalampekos, Uniformization of Gromov hyperbolic domains by circle domains, Duke Math. J., 2026. https://doi.org/10.1215/00127094-2025-0076
• D. Ntalampekos, Uniformization problems in the plane: A survey, preprint, 2026. https://arxiv.org/abs/2603.15098