Differential Geometry

Motivation

A measure-preserving system may have low information production yet fail to admit a smooth realization. The target asks for a single ergodic system excluding every finite-dimensional smooth positive-volume model. The source manuscript presents the surrounding research claim.

Setting

The system is a measurable equivalence T of a standard nonatomic probability space. Standard nonatomic is expressed by an isomorphism with the unit interval after removing null sets. A smooth model is a compact smooth manifold, a smooth diffeomorphism and an invariant probability measure with strictly positive smooth local coordinate density.

Formalization target

Construct a system satisfying

$$T\text{ is ergodic},\qquad h_{KS}(T)<\infty,\qquad T\text{ has no smooth positive-volume model}.$$

The formal finite-entropy predicate requires every finite-partition entropy rate to converge, with one finite real upper bound.

The selected formal target is OAI.SmoothObstruction.main.

Significance and status

The obstruction ranges over every finite dimension, nonorientable manifolds and positive-dimensional smooth boundary models. The manuscript asserts zero entropy; the selected published theorem requires finite entropy only. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Failure of a particular embedding does not exclude all measure-theoretic conjugacies and all dimensions. Conjugacy is allowed after discarding invariant null sets.

Formalization scope

The goal quantifies over measurable equivalences and uses conull measurable conjugacy, not topological conjugacy. Entropy is measured in bits by the supplied finite-partition definition. Closed models include dimension zero, boundary models require positive dimension, and no orientation hypothesis is imposed.

Selected references

• OpenAI, A zero-entropy system without a smooth positive-volume model, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Algebraic ampleness and positivity of a smooth Hermitian metric are different kinds of positivity for a vector bundle. The target asks for one concrete family where they separate. The source manuscript presents the surrounding research claim.

Setting

The quadric surface is ℙ¹×ℙ¹. Rank-two algebraic bundles are specified by principal affine charts and regular 2×2 transition matrices. For a bundle G, E(m) is its coordinatewise m-th-power pullback twisted by the polarization O(1,1).

Formalization target

Construct G and a family E(m) such that

$$m>0\Longrightarrow E(m)\text{ is ample},\qquad m\ge m_0\Longrightarrow E(m)\text{ has no strictly Griffiths-positive smooth metric},$$

for one positive integer m₀, with the required pullback-twist identities for every positive m.

The selected formal target is OAI.QuadricCounterexample.main_theorem.

Significance and status

The assertion compares two precise positivity conditions on the same family. The goal is existential and does not provide a numerical threshold m₀. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Proving ampleness supplies projective sections, whereas excluding every positive metric is a quantified differential-geometric obstruction. Testing one candidate metric cannot settle nonexistence.

Formalization scope

The reference defines ℙ¹ as the one-point compactification of ℂ, bundles by cocycles, ampleness through symmetric sections giving a closed projective embedding, and strict positivity by a matrix Hessian expression. SourceMainTheorem retains all of these conventions. Only the published definition block and target are attached.

Selected references

• OpenAI, Ample rank-two bundles on the quadric surface without Griffiths-positive metrics, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation: when are optimal transport maps continuous?

Given two probability densities $\rho_0,\rho_1$ on a compact Riemannian manifold, optimal transport with the quadratic cost $c(x,y)=d(x,y)^2/2$ seeks the map $T$ pushing $\rho_0\,\mathrm{vol}$ to $\rho_1\,\mathrm{vol}$ at least total cost. McCann proved that such a map exists and is unique almost everywhere (McCann 2001). Whether it is continuous when the densities are merely bounded above and below depends on the geometry of the cost: the Ma–Trudinger–Wang (MTW) condition, a sign condition on a fourth derivative of $c$, is the decisive curvature hypothesis, and its weak form is known to be necessary. The question is whether weak MTW is also sufficient on every compact manifold, with estimates that do not degenerate as transport graphs approach conjugate points.

Background

• 1992 — Caffarelli's regularity theory for maps with convex potentials, based on sections and contact-volume comparison (Caffarelli 1992).
• 2001 — McCann's polar factorization on Riemannian manifolds (McCann 2001).
• 2005 — Ma, Trudinger and Wang introduce the curvature condition (MTW 2005).
• 2009 — Loeper links MTW to supporting cost functions and shows its necessity for continuity (Loeper 2009).
• 2010 — Loeper and Villani: uniform estimates under strict MTW and nonfocality (Loeper–Villani 2010).
• 2011 — Figalli, Rifford and Villani: transport continuity implies convex injectivity domains and weak MTW; on surfaces continuity is equivalent to their conjunction, and the equivalence with weak MTW alone is posed (FRV 2011).
• 2013 — Figalli, Kim and McCann: Hölder continuity and injectivity of optimal maps under weak MTW with cost-convexity hypotheses (FKM 2013), and products of round spheres (FKM 2013).
• 2015 — Figalli, Gallouët and Rifford: weak MTW implies convex injectivity domains on nonfocal manifolds (FGR 2015).
• 2019 — Lebedeva, Petrunin and Zolotov list the convexity and continuity questions (LPZ 2019, Questions 8.6–8.7).
• 2026 — Two OpenAI preprints (OpenAI Math Release, September 25, 2026): a companion proving that weak MTW forces convex injectivity domains and global support, and Uniform Bi-Hölder Transport from Weak MTW (this mission), claiming uniform bi-Hölder optimal maps for every density-bounded class. Neither is peer reviewed, and the theorem is not formally verified.

Setting

Let $(M,g)$ be a smooth, connected, compact Riemannian manifold without boundary, of dimension $n\ge2$, with distance $d$ and volume $\mathrm{vol}$. Put $c(x,y)=\tfrac12 d(x,y)^2$ and let

$$I(x)=\{p\in T_xM:\ d(x,\exp_x(ap))=a|p| \text{ for some } a>1\}$$

be the open injectivity domain. Weak MTW: for every $p\in I(x)$ and $\xi\perp\eta$ in $T_xM$,

$$-\frac32\,\frac{\partial^4}{\partial s^2\partial t^2}\,c\big(\exp_x(t\xi),\exp_x(p+s\eta)\big)\Big|_{s=t=0}\ \ge 0 .$$

For $0<\lambda\le\Lambda$, the density class consists of measurable $\rho$ with $\int\rho\,d\mathrm{vol}=1$ and $\lambda\le\rho\le\Lambda$ almost everywhere. An optimal map from $\rho_0$ to $\rho_1$ is a measurable $T$ with $T_\#(\rho_0\mathrm{vol})=\rho_1\mathrm{vol}$ minimizing $\int c(x,T(x))\rho_0(x)\,d\mathrm{vol}$ among such maps.

In Lean, metricVolume n is the $n$-dimensional Hausdorff measure normalized to agree with Lebesgue measure on $\mathbb R^n$ (which equals Riemannian volume), riemannianExp is defined from complete geodesics, and WeakMTW uses iteratedDeriv 2 twice.

Formalization targets

Goal: uniform bi-Hölder optimal maps

Fix $(M,g)$ satisfying weak MTW and $0<\lambda\le\Lambda$ with a nonempty density class. There are $\alpha\in(0,1]$ and $C<\infty$, depending only on $(M,g),\lambda,\Lambda$, such that for all densities $\rho_0,\rho_1$ in the class, the almost-everywhere unique optimal map has a homeomorphic representative $\widetilde T$ with

$$d(\widetilde T x,\widetilde T x')\le C\,d(x,x')^\alpha,\qquad d(\widetilde T^{-1}y,\widetilde T^{-1}y')\le C\,d(y,y')^\alpha .$$

This is Theorem 1.1 of the source. The goal is published on the platform with status Open.

Significance

The result itself. The constants are common to the whole density class; they do not depend on the densities or their derivatives, and the theorem allows conjugate cut points without nonfocality, strict MTW, or cut avoidance. Combined with the necessity result of Figalli–Rifford–Villani it gives the equivalence of weak MTW with transport continuity for bounded densities on compact manifolds, with uniform estimates in the forward direction. No explicit exponent is obtained (the positive exponent comes from a contradiction argument).

Formalizing it. The Lean statement packages existence, almost-everywhere uniqueness, homeomorphic regularity and uniform bi-Hölder bounds in one assertion over all density pairs, making precise what "class-uniform" means. A proof requires the companion geometric results (convex injectivity domains, global support), McCann's theorem, and Caffarelli-type section estimates on manifolds — none currently in Mathlib.

Difficulty

Hölder estimates obtained after localizing near a smooth part of the cost give a density-dependent exponent and localization scale; they do not give a common scale or constant for a family whose transport graphs approach conjugate pairs, where the cost stops being smooth. Weak MTW constrains the cost only where it is smooth and only for orthogonal directions. Earlier uniform results needed strict MTW and nonfocality, or special geometry (products of spheres).

Formalization scope

• Volume is the normalized Hausdorff measure euclideanVolumeFactor n • μH[n]; densities are AEMeasurable, integrable, of mass one, and between lam and cap almost everywhere; nonemptiness of the class is a hypothesis, as in the source.
• IsOptimalMap requires measurability, the pushforward identity for withDensity measures, and minimality among all measurable maps with that pushforward; uniqueness is almost everywhere for $\rho_0\,\mathrm{vol}$.
• The conclusion requires one $\alpha\in(0,1]$ and one $C\ge0$ before quantifying over densities, and a homeomorphism M ≃ₜ M with the same exponent and constant for $T$ and $T^{-1}$; a trivializing choice is excluded because $T$ must itself be optimal.
• Weak MTW is a hypothesis only at $p\in I(x)$ and orthogonal $\xi,\eta$.
• Needed infrastructure: Riemannian geodesics and cut locus, semiconvex potentials, Kantorovich duality and McCann's theorem, Hausdorff measure versus Riemannian volume, Caffarelli-type sections.

Selected references

• L. A. Caffarelli, The regularity of mappings with a convex potential, J. Amer. Math. Soc. 5 (1992), 99–104. https://doi.org/10.1090/S0894-0347-1992-1124980-8
• R. J. McCann, Polar factorization of maps on Riemannian manifolds, Geom. Funct. Anal. 11 (2001), 589–608. https://doi.org/10.1007/PL00001679
• X.-N. Ma, N. S. Trudinger and X.-J. Wang, Regularity of potential functions of the optimal transportation problem, Arch. Ration. Mech. Anal. 177 (2005), 151–183. https://doi.org/10.1007/s00205-005-0362-9
• G. Loeper, On the regularity of solutions of optimal transportation problems, Acta Math. 202 (2009), 241–283. https://doi.org/10.1007/s11511-009-0037-8
• G. Loeper and C. Villani, Regularity of optimal transport in curved geometry: the nonfocal case, Duke Math. J. 151 (2010), 431–485. https://doi.org/10.1215/00127094-2010-003
• A. Figalli, L. Rifford and C. Villani, Necessary and sufficient conditions for continuity of optimal transport maps on Riemannian manifolds, Tohoku Math. J. 63 (2011), 855–876. https://doi.org/10.2748/tmj/1325886291
• A. Figalli, Y.-H. Kim and R. J. McCann, Hölder continuity and injectivity of optimal maps, Arch. Ration. Mech. Anal. 209 (2013), 747–795. https://doi.org/10.1007/s00205-013-0629-5
• A. Figalli, Y.-H. Kim and R. J. McCann, Regularity of optimal transport maps on multiple products of spheres, J. Eur. Math. Soc. 15 (2013), 1131–1166. https://doi.org/10.4171/JEMS/388
• A. Figalli, T. O. Gallouët and L. Rifford, On the convexity of injectivity domains on nonfocal manifolds, SIAM J. Math. Anal. 47 (2015), 969–1000. https://doi.org/10.1137/140961821
• N. Lebedeva, A. Petrunin and V. Zolotov, Bipolar comparison, Geom. Funct. Anal. 29 (2019), 258–282. https://doi.org/10.1007/s00039-019-00481-9
• OpenAI, Global Support and Convex Injectivity Domains under Weak MTW, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Global-Support-and-Convex-Injectivity-Domains-under-Weak-MTW-September-25-2026/paper.pdf
• OpenAI, Uniform Bi-Hölder Transport from Weak MTW, OpenAI Math Release preprint, September 25, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Uniform-Bi-Holder-Transport-from-Weak-MTW-September-25-2026/paper.pdf

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 isoperimetric problem asks, for each prescribed volume, for the regions of least boundary area. In Euclidean space the answer is the round ball. In a compact space with topology the answer changes with the volume: small regions still look like balls, but larger regions can save area by wrapping around the space. The unit cubic flat three-torus $\mathbb R^3/\mathbb Z^3$ is the simplest compact example in three dimensions, and the periodic isoperimetric problem on it is equivalent, by reflection, to the relative isoperimetric problem in a cube. It is a standard test case for how local Euclidean geometry interacts with global topology, and it has been studied in connection with periodic minimal and constant-mean-curvature surfaces (Hauswirth–Pérez–Romon–Ros 2004; Ros 2005).

The conjectured answer is a sequence of three phases: balls, solid circular tubes around shortest closed geodesics, and slabs between parallel coordinate tori, followed by their complements. This mission asks for a machine-checked proof of that conjecture, including the classification of every minimizer, as claimed in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal below is open.

Timeline

• 1972 — Hadwiger proves that a coordinate cut minimizes at half volume for the cube (Monatsh. Math. 1972).
• 1992–1996 — Ritoré and Ros develop stability and structure results for constant-mean-curvature surfaces in flat three-manifolds (Comment. Math. Helv. 1992; Trans. AMS 1996); Ritoré's thesis records Hsiang's coordinate reflection symmetry (1994).
• 2000 — Barthe and Maurey recover Hadwiger's half-volume result by Gaussian comparison (Ann. IHP 2000). Morgan and Johnson's small-volume comparison implies that balls minimize for sufficiently small volume on compact flat manifolds (Indiana Univ. Math. J. 2000, Theorem 4.4).
• 2004 — Hauswirth, Pérez, Romon and Ros state the ball–tube–slab prediction and prove that a nonstandard minimizing boundary is connected of genus $2$, $3$ or $4$, with curvature–area bounds (Trans. AMS 2004).
• 2005 — Ros's survey records the conjecture for the cubic torus and cube (Clay Math. Proc. 2, 2005, Section 1.6).
• 2013 — Acerbi, Fusco and Morini prove that slabs are the only minimizers near half volume (Comm. Math. Phys. 2013, Theorem 5.3), without effective ranges.
• 2026 — Milman obtains effective ranges for the phases, including the ball phase up to volume fraction $0.120582\ldots$, and reduces the profile conjecture to the two transition volumes $4\pi/81$ and $1/\pi$ (Comm. Pure Appl. Math. 2026, Theorems 1.2–1.3).
• September 2026 — The OpenAI preprint claims the full conjecture with all equality cases (Theorem 1.1, p. 1).

Setting

Let $\mathbb T=\mathbb R^3/\mathbb Z^3$ with its flat metric and volume measure $|\cdot|$ (total volume $1$). For a measurable $E\subseteq\mathbb T$, its perimeter is the De Giorgi perimeter

$$P(E)=\sup\Bigl\{\int_E \operatorname{div}F : F \text{ a smooth vector field on }\mathbb T,\ |F|\le1\Bigr\}\in[0,\infty],$$

which equals the boundary area when $\partial E$ is smooth, and is insensitive to null-set changes. $E$ has finite perimeter if $P(E)<\infty$. A minimizer at volume $V$ is a finite-perimeter $E$ with $|E|=V$ and $P(E)\le P(F)$ for all finite-perimeter $F$ with $|F|=V$.

For $0<V<1$ put $v=\min(V,1-V)$ and

$$I(V)=\min\Bigl\{(36\pi)^{1/3}v^{2/3},\;2\sqrt{\pi v},\;2\Bigr\}.$$

The three expressions are the perimeters of a ball of volume $v$, a solid circular tube of volume $v$ around a shortest closed geodesic (a coordinate circle of length $1$), and a slab of width $v$ between two coordinate tori. The branches cross at $V_1=4\pi/81$ and $V_2=1/\pi$.

Formalization targets

Goal: Theorem 1.1 (p. 1)

For every $V\in(0,1)$:

1. a minimizer at volume $V$ exists;
2. every minimizer has perimeter exactly $I(V)$;
3. a set $E$ is a minimizer at volume $V\le 1/2$ if and only if, up to an isometry of $\mathbb T$ and a null set, it is a ball of radius $(3V/(4\pi))^{1/3}$ when $V\le 4\pi/81$, a solid tube of radius $\sqrt{V/\pi}$ about a shortest closed geodesic when $4\pi/81\le V\le1/\pi$, or a slab of width $V$ between coordinate tori when $1/\pi\le V$; for $V>1/2$ the minimizers are exactly the complements of those at volume $1-V$.

The ranges are closed, so at each transition volume both adjacent types are minimizers and there are no others. This is OAI.CubicTorus.unit_cubic_isoperimetric.

Significance

The result itself. It determines the isoperimetric profile of the cubic three-torus and the reflected relative profile of the unit cube at every volume, settling a conjecture explicitly posed by Hauswirth–Pérez–Romon–Ros and Ros. The equality classification at the transitions is new even granting Milman's reduction, which classifies minimizers on the open branches once the endpoint values are known but leaves extra co-minimizers at $4\pi/81$ and $1/\pi$ to be excluded.

Formalizing it. The proof combines geometric measure theory (existence and regularity of minimizers), structure theorems for stable CMC surfaces, a differential inequality for the profile, and certified one-variable numerics. A formal proof would certify the whole chain; existence and regularity of isoperimetric regions in a flat torus are themselves substantial missing library pieces. No machine-checked version of the result, or of the Euclidean isoperimetric inequality for finite-perimeter sets in this generality, is known to exist.

Difficulty

The main obstruction is to rule out minimizers whose boundary is a connected surface of genus $2$, $3$ or $4$ (Theorem 2.1, p. 3, quoting Hauswirth–Pérez–Romon–Ros). The general curvature–area bound and the profile differential inequality (Lemma 2.3, p. 4) exclude such surfaces away from the transitions but not at $V_1,V_2$ themselves. At the cylinder–slab transition $V_2=1/\pi$, the planar isoperimetric inequality applied to horizontal sections leaves a deficit in a central curvature range; the preprint closes it with a calibration of a corner section, a nesting argument for planar sections, and a Jensen estimate (Section 6, Proposition 6.7, p. 19), supplemented by certified numerical bounds (Appendix B).

Formalization scope

• The torus is PiLp 2 (fun _ : Fin 3 => AddCircle 1), whose metric is the flat torus metric; volume is the pushforward of Lebesgue measure on the half-open unit cube.
• Perimeter is the De Giorgi supremum over $C^\infty$ $\mathbb Z^3$-periodic vector fields on $\mathbb R^3$ with $|F|\le1$, valued in ℝ≥0∞; no regularity of $E$ is assumed. Finite perimeter also requires null-measurability.
• Minimizers are global: the comparison ranges over all finite-perimeter sets of the same volume.
• The canonical ball is the metric ball about $0$; the tube is $\{x:\|x_1\|^2+\|x_2\|^2<V/\pi\}$ around the $x_0$-direction geodesic; the slab is $\{x:\|x_0\|<V/2\}$. CongruentAE allows any isometry of $\mathbb T$ followed by a null-set change.
• The phase ranges are closed, so both types are included at ties, matching the source. The statement is not vacuous: existence is part of the conclusion, and the profile value is a concrete real number.

Useful reusable infrastructure: sets of finite perimeter on flat tori, compactness and lower semicontinuity of perimeter, and the Euclidean isoperimetric inequality.

Selected references

• OpenAI, The Isoperimetric Conjecture for the Cubic Flat Three-Torus, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Isoperimetric-Conjecture-for-the-Cubic-Flat-Three-Torus-September-24-2026/article.pdf
• L. Hauswirth, J. Pérez, P. Romon, A. Ros, The periodic isoperimetric problem, Trans. Amer. Math. Soc. 356 (2004), 2025–2047. https://doi.org/10.1090/S0002-9947-03-03362-2
• A. Ros, The isoperimetric problem, in Global Theory of Minimal Surfaces, Clay Math. Proc. 2 (2005), 175–209. https://www.claymath.org/wp-content/uploads/2022/03/cmip02.pdf
• E. Milman, Isoperimetric inequalities on slabs with applications to cubes and Gaussian slabs, Comm. Pure Appl. Math. 79 (2026), 1012–1072. https://doi.org/10.1002/cpa.70020
• E. Acerbi, N. Fusco, M. Morini, Minimality via second variation for a nonlocal isoperimetric problem, Comm. Math. Phys. 322 (2013), 515–557. https://doi.org/10.1007/s00220-013-1733-y
• H. Hadwiger, Gitterperiodische Punktmengen und Isoperimetrie, Monatsh. Math. 76 (1972), 410–418. https://doi.org/10.1007/BF01297304
• F. Morgan, D. L. Johnson, Some sharp isoperimetric theorems for Riemannian manifolds, Indiana Univ. Math. J. 49 (2000), 1017–1041. https://www.lehigh.edu/~dlj0/papers/morgan-johnson.pdf
• M. Ritoré, A. Ros, Stable constant mean curvature tori and the isoperimetric problem in three space forms, Comment. Math. Helv. 67 (1992), 293–305. https://doi.org/10.1007/BF02566501

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

A Riemannian metric is Einstein if its Ricci curvature is a constant multiple of the metric, $\mathrm{Ric}=\lambda g$. Einstein metrics are the critical points of total scalar curvature and the vacuum solutions of general relativity in Riemannian signature, and in dimension four they are tied to gauge theory and to the topology of four-manifolds. A natural rigidity question asks which closed four-manifolds carry Einstein metrics of strictly positive sectional curvature. Three examples are known: the round sphere $S^4$, the round real projective space $\mathbb{RP}^4$, and the complex projective plane $\mathbb{CP}^2$ with its Fubini–Study metric. The classification conjecture, stated as Conjecture 1 by D. Yang in 2000, asserts that there are no others up to scaling and isometry.

Background

• 1961. Berger proves rigidity under strict quarter pinching (doi:10.1007/BF02417787).
• 1993. Micallef and Wang prove local symmetry under nonnegative isotropic curvature in dimension four.
• 1999. Gursky and LeBrun obtain the Fubini–Study conclusion for nonnegative sectional curvature with a nonzero positive-definite intersection form, and a Weyl-norm gap (doi:10.1023/A:1006597912184).
• 2000–2018. Yang, Costa, and Cao–Tran prove rigidity under quantitative pinching hypotheses (doi:10.1007/PL00005792, doi:10.1016/j.geomphys.2003.10.013, arXiv:1612.06023).
• 2010. Brendle extends Einstein rigidity under nonnegative isotropic curvature to all dimensions (doi:10.1215/00127094-2009-061).
• 2014. Koca treats Hermitian Einstein metrics of positive sectional curvature (arXiv:1112.4181).
• 2026. Dameno, Catino–Dameno and Di Cerbo obtain rigidity under twistor, eigenvalue-separation or Weyl-norm equality hypotheses; Cheng proves the oriented classification when $\chi\le3$ (arXiv:2609.23337); Gursky and Malchiodi prove it when $2\chi-3|\tau|\le4$ (arXiv:2609.30803).

All earlier results keep an additional curvature, topological or symmetry hypothesis. The source of this mission is an OpenAI preprint dated September 23, 2026, which claims the classification with no extra hypothesis and no orientability assumption.

Setting

Let $M$ be a connected, compact smooth four-manifold without boundary, with a smooth Riemannian metric $g$. In a chart with Christoffel symbols $\Gamma^k_{ij}$, the curvature tensor is

$$R^l{}_{ijk}=\partial_i\Gamma^l_{jk}-\partial_j\Gamma^l_{ik}+\Gamma^l_{ip}\Gamma^p_{jk}-\Gamma^l_{jp}\Gamma^p_{ik},$$

the Ricci tensor is $R_{ij}=R^k{}_{kij}$, and the sectional curvature of the plane spanned by $u,v$ has the sign of $g(R(u,v)v,u)$. The metric is Einstein if $R_{ij}=\lambda g_{ij}$ for a single constant $\lambda$, and positively curved if $g(R(u,v)v,u)>0$ for all linearly independent $u,v$. Strict positivity forces $\lambda>0$.

The three models are $S^4\subset\mathbb R^5$ with distance $\arccos\langle p,q\rangle$, $\mathbb{RP}^4$ with distance $\arccos|\langle p,q\rangle|$ for unit representatives, and $\mathbb{CP}^2$ with the Fubini–Study distance $\arccos|\langle p,q\rangle_{\mathbb C}|$.

Formalization targets

Milestone: Corollary 8.9 (oriented classification)

If $M$ is in addition oriented, then for some $a>0$, $(M,ag)$ is isometric to $S^4$ or to $\mathbb{CP}^2$.

Goal: Theorem 1.1

$$\exists\,a>0:\quad (M,ag)\ \cong\ S^4,\quad \mathbb{CP}^2_{\mathrm{FS}},\quad\text{or}\quad \mathbb{RP}^4.$$

The Lean statement OAI.PositiveEinsteinFour.classification is open on the platform.

Significance

The theorem completes the four-dimensional picture for positively curved Einstein metrics: only the symmetric examples occur. It removes all the pinching, topological and symmetry hypotheses of previous results. The paper's central intermediate result, half-conformal flatness (one Weyl block vanishes, Proposition 8.1), connects the problem to Hitchin's classification of self-dual Einstein four-manifolds.

The result is stated in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. Parts of the argument rely on explicit polynomial and matrix certificates (Section 7), which are well suited to formal verification.

Difficulty

In dimension four the curvature of an Einstein metric splits into two Weyl blocks $W^\pm$ acting on self-dual and anti-self-dual two-forms. The Einstein equation does not force either block to vanish, and earlier arguments controlled them only under extra pinching or topological assumptions. Scalar Weyl-norm gaps (Gursky–LeBrun) control each block separately; the difficulty is the interaction of two nonzero blocks under the exact sectional-positivity condition, which is stronger than any norm bound and must be used in its tensorial form. Once one block vanishes, the classical rigidity theory finishes the proof.

Formalization scope

• Manifolds are ChartedSpace (EuclideanSpace ℝ (Fin 4)) with IsManifold I4 ∞, compact, connected, Hausdorff, second countable; the model has no boundary.
• The metric is a ContMDiffRiemannianMetric; Christoffel symbols, curvature and Ricci are computed in coordinates from fderiv of the chart expression of $g$, at the centre of the chart at each point.
• IsEinstein uses one constant $\lambda$ for all points; HasPositiveSectionalCurvature requires $g(R(u,v)v,u)>0$ for every linearly independent pair.
• ScaledIsometricTo g a d asks for a bijection $M\simeq N$ with $d(f x,f y)=\sqrt a\,d_g(x,y)$, $d_g$ the Riemannian distance.
• The oriented milestone represents an orientation as a clopen choice of positively oriented orthonormal frames, consistent in each fibre.

A complete development needs Riemannian geometry in coordinates, Weyl decomposition in dimension four, Hodge theory on two-forms, characteristic-number identities (Gauss–Bonnet–Chern, Hirzebruch signature), volume comparison, and Hitchin's classification. Contributions formalizing Proposition 8.1 (half-conformal flatness), Proposition 4.9 (balanced Weyl moments) and Lemma 8.7 (curvature of the standard models) are welcome.

Selected references

• OpenAI, Positively curved Einstein four-manifolds, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Positively-curved-Einstein-four-manifolds-September-23-2026/paper.pdf
• D. Yang, Rigidity of Einstein 4-manifolds with positive curvature, Invent. Math., 2000. https://doi.org/10.1007/PL00005792
• M. J. Gursky, C. LeBrun, On Einstein manifolds of positive sectional curvature, Ann. Global Anal. Geom., 1999. https://doi.org/10.1023/A:1006597912184
• M. Berger, Sur quelques variétés d'Einstein compactes, Ann. Mat. Pura Appl., 1961. https://doi.org/10.1007/BF02417787
• X. Cao, H. Tran, Einstein four-manifolds of pinched sectional curvature, Adv. Math., 2018. https://arxiv.org/abs/1612.06023
• S. Brendle, Einstein manifolds with nonnegative isotropic curvature are locally symmetric, Duke Math. J., 2010. https://doi.org/10.1215/00127094-2009-061
• N. J. Hitchin, Kählerian twistor spaces, Proc. London Math. Soc., 1981. https://doi.org/10.1112/plms/s3-43.1.133
• M. J. Gursky, A. Malchiodi, Einstein four-manifolds of positive sectional curvature and ADM mass, 2026. https://arxiv.org/abs/2609.30803

Motivation

A symplectic embedding preserves the standard symplectic form $\omega_0=\sum_j dx_j\wedge dy_j$ on $\mathbb C^n$, and in particular preserves volume. Gromov's nonsqueezing and two-ball theorems showed that symplectic embeddings obey constraints invisible to volume (Gromov 1985). The ball-packing problem asks exactly when finitely many balls can be embedded disjointly and symplectically into a given ball, and so measures how far symplectic rigidity goes beyond volume.

In real dimension four the answer involves infinitely many obstructions coming from pseudoholomorphic curves and algebraic geometry (McDuff–Polterovich 1994; Biran 1997). In higher dimensions Siegel and Yao conjectured that only two obstructions survive: volume and Gromov's two-ball obstruction (Conjecture A of Siegel–Yao 2025).

This mission asks for a machine-checked proof of Theorem 1.1 of an OpenAI preprint dated September 23, 2026 (source), which claims Conjecture A in every real dimension $2n\ge6$. The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.

Background

• 1985 — Gromov introduces pseudoholomorphic curves and proves the two-ball obstruction $R_1+R_2\le R$ (Invent. Math. 1985).
• 1994 — McDuff and Polterovich connect packing to blowups and algebraic geometry (Invent. Math. 1994).
• 1995 — Traynor gives explicit packing constructions (J. Differential Geom. 1995).
• 1997–2001 — Biran proves packing stability in dimension four (GAFA 1997; GAFA 2001).
• 2005 — Schlenk's monograph develops folding and planar constructions (de Gruyter 2005).
• 2011–2016 — Buse and Hind extend equal-ball stability to higher dimensions (Geom. Topol. 2011; Compos. Math. 2013); Buse, Hind and Opshtein prove unequal-ball stability in dimension four for small capacities (Trans. AMS 2016).
• 2025 — Siegel and Yao formulate Conjecture A for higher-dimensional packings.
• 2026 — The OpenAI preprint claims Conjecture A for all $n\ge3$ (Theorem 1.1, p. 2).

Setting

For $R>0$ write

$$B^{2n}(R)=\Bigl\{z\in\mathbb C^n:\ \pi\sum_{j=1}^n|z_j|^2\le R\Bigr\},$$

so $R$ is the capacity, the Euclidean radius is $\sqrt{R/\pi}$, and $\mathrm{vol}\,B^{2n}(R)=R^n/n!$. An embedding of a closed ball into the open ball $\operatorname{int}B^{2n}(R)$ means a smooth map defined on an open neighbourhood of the closed ball, which is a topological embedding there, pulls $\omega_0$ back to $\omega_0$, and sends the closed ball into the open target. A packing of $B^{2n}(R_1),\dots,B^{2n}(R_k)$ is a family of such embeddings whose images of the closed balls are pairwise disjoint.

Formalization targets

Milestone: necessity in Theorem 1.1 (p. 4)

If $n\ge3$, $k\ge1$, $R,R_i>0$ and a packing exists, then

$$\sum_{i=1}^kR_i^n<R^n\qquad\text{and}\qquad R_i+R_j<R\ \ (i\ne j).$$

The images lie in some $\operatorname{int}B^{2n}(\sigma)$ with $\sigma<R$ by compactness, so the volume bound and Gromov's two-ball obstruction give the strict inequalities.

Goal: Theorem 1.1 (p. 2)

For integers $n\ge3$, $k\ge1$ and positive reals $R,R_1,\dots,R_k$, a symplectic embedding $\bigsqcup_iB^{2n}(R_i)\hookrightarrow\operatorname{int}B^{2n}(R)$ exists if and only if the two inequalities above hold.

Significance

The result itself. In every real dimension at least six, the volume and two-ball obstructions are the only obstructions to packing balls of arbitrary capacities into a ball. This contrasts with dimension four, where infinitely many further obstructions are essential, and it goes beyond packing-stability results, which concern many small balls. The theorem settles Siegel and Yao's Conjecture A.

Formalizing it. The necessity direction needs Gromov's two-ball theorem, which rests on pseudoholomorphic curve theory and has no formalization. The sufficiency direction uses Hamiltonian flows, Moser isotopies, toric domains, Kähler forms on projective degenerations and normal-cone transfer. A formal proof would require substantial new symplectic and algebro-geometric infrastructure, all of it reusable.

Difficulty

Sufficiency is the hard direction. The volume inequality is an integral condition, but a packing needs pointwise room; in the preprint's toric models over a surface with a handle, the unused-area profile $P$ has positive integral but need not be positive at every moment, and a Hamiltonian comparison theorem (Lemma 2.1, p. 5) is needed to rearrange it into disjoint ball layers (Lemma 3.3, p. 12). The models must then be transferred symplectically into the target ball using Kähler degenerations; three geometric cases arise (all capacities below $R/2$, Proposition 5.2, p. 25; one large capacity in dimension $\ge8$, Proposition 5.3, p. 26; one large capacity in dimension six, Proposition 6.7, p. 39). For necessity the obvious volume argument gives only non-strict inequalities; strictness comes from compactness of the images, and the pairwise bound is genuinely symplectic.

Formalization scope

• Phase space is Fin n → ℂ with capacity $\pi\sum_j|z_j|^2$ and $\omega_0(u,v)=\sum_j(\mathrm{Re}\,u_j\,\mathrm{Im}\,v_j-\mathrm{Im}\,u_j\,\mathrm{Re}\,v_j)$.
• SymplecticOn U f: $U$ open, $f$ is $C^\infty$ on $U$, $f|_U$ is a topological embedding, and fderiv preserves $\omega_0$ at every point of $U$.
• HasPacking n k R r: each closed ball $B^{2n}(r_i)$ lies in an open $U_i$ on which $f_i$ is symplectic, $f_i$ maps the closed ball into the open ball of capacity $R$, and images of distinct closed balls are disjoint.
• PackingInequalities uses strict inequalities and quantifies over ordered pairs $i\ne j$; the goal assumes $n\ge3$, $k\ge1$, $R>0$, $r_i>0$, matching the source exactly.
• Neither side is vacuous: for one ball the pairwise condition is empty and the statement reduces to $r_1<R$.

Selected references

• OpenAI, Symplectic Ball Packings in Higher Dimensions, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Symplectic-Ball-Packings-in-Higher-Dimensions-September-23-2026/paper.pdf
• K. Siegel, Y. Yao, On symplectic packing problems in higher dimensions, Math. Ann. 392 (2025), 5361–5392. https://doi.org/10.1007/s00208-025-03221-7
• M. Gromov, Pseudo holomorphic curves in symplectic manifolds, Invent. Math. 82 (1985), 307–347. https://doi.org/10.1007/BF01388806
• D. McDuff, L. Polterovich, Symplectic packings and algebraic geometry, Invent. Math. 115 (1994), 405–429. https://doi.org/10.1007/BF01231766
• P. Biran, Symplectic packing in dimension 4, Geom. Funct. Anal. 7 (1997), 420–437. https://doi.org/10.1007/s000390050014
• O. Buse, R. Hind, Ellipsoid embeddings and symplectic packing stability, Compos. Math. 149 (2013), 889–902. https://doi.org/10.1112/S0010437X12000826
• O. Buse, R. Hind, E. Opshtein, Packing stability for symplectic 4-manifolds, Trans. Amer. Math. Soc. 368 (2016), 8209–8222. https://doi.org/10.1090/tran/6802
• L. Traynor, Symplectic packing constructions, J. Differential Geom. 41 (1995), 735–751. https://doi.org/10.4310/jdg/1214456483
• F. Schlenk, Embedding Problems in Symplectic Geometry, de Gruyter (2005). https://doi.org/10.1515/9783110199697

Motivation: can every surface be realized locally in $\mathbb R^3$?

A Riemannian surface is abstract: it is given by a rule $g$ for measuring lengths and angles in local coordinates, not as a surface sitting in space. The local isometric realization problem asks whether every such surface can, near each point, be realized as an honest smooth surface in Euclidean three-space with the same lengths. The question goes back to the classical theory of surfaces. It is settled for real-analytic metrics and for smooth metrics with nonvanishing curvature, while the unrestricted smooth case is listed as open by Yau (Yau 2000, p. 236) and in Ghomi's problem survey (Ghomi 2019, §1.5, Problem 1.9).

Timeline

• 1926–1927 — Janet and Cartan: every real-analytic surface metric is locally realizable analytically in $\mathbb R^3$ (Janet 1926; Cartan 1927).
• 1954–1955 — Nash and Kuiper: $C^1$ isometric realizations exist with great flexibility (Nash 1954; Kuiper 1955). At $C^1$ regularity there is no curvature constraint.
• 1971 — Pogorelov constructs a $C^{2,1}$ metric with no local $C^2$ realization (Pogorelov 1971).
• 1985–1986 — C.-S. Lin: local realization for nonnegative curvature and for curvature changing sign cleanly, with finite differentiability (Lin 1985; Lin 1986).
• 1989 — Nakamura and Maeda: smooth local existence when the curvature changes sign cleanly (Trans. AMS 1989).
• 2002 — A Nadirashvili–Yuan preprint states a smooth counterexample with $K\le0$ (arXiv:math/0208127); their published 2008 paper instead proves a $C^{2,1}$ counterexample with $K\ge0$ and leaves the smooth question open (Calc. Var. PDE 2008).
• 2007–2009 — Khuri: counterexamples to local solvability for general Monge–Ampère equations (CPDE 2007), and work on Darboux's equation that leaves the needed curvature profile open (Khuri 2009).
• 2010–2016 — Positive results under finite-order conditions on the curvature zero set (Han–Khuri 2010; T.-Y. Lin 2016).
• 2026 — An OpenAI preprint, A Smooth Metric with No Local Isometric Immersion into Three-Space (OpenAI Math Release, September 24, 2026), claims a smooth metric on $(-1,1)^2$ that has no smooth isometric immersion on any neighborhood of the origin. It has not been peer reviewed, and the claim has not been formally verified.

Setting

Work in coordinates $p=(p_1,p_2)$ on the open square $Q=(-1,1)^2\subset\mathbb R^2$. A Riemannian metric on $Q$ is a map $p\mapsto g(p)$ to symmetric $2\times2$ real matrices that are positive definite; it is $C^\infty$ if every entry $g_{ij}$ is smooth. An isometric immersion of $(U,g)$, for an open set $U\subseteq Q$, is a map $F:U\to\mathbb R^3$ whose differential reproduces $g$:

$$\langle dF_p(v),\,dF_p(w)\rangle_{\mathbb R^3}=v^{\mathsf T} g(p)\,w\qquad(p\in U,\ v,w\in\mathbb R^2),$$

equivalently $\langle\partial_iF,\partial_jF\rangle=g_{ij}$. Positive definiteness forces $dF$ to have rank $2$. In Lean, Coord = Fin 2 → ℝ, Ambient = EuclideanSpace ℝ (Fin 3), square is $Q$, and LocalSmoothPositive packages smoothness of every entry and Matrix.PosDef at every point.

Formalization targets

Goal: a nonrealizable smooth metric (Theorem A)

$$\exists\, g\ \text{smooth, positive definite on } Q\ \text{ such that for every open } U\subseteq Q \text{ with } 0\in U,\ \text{there is no } C^\infty\ F:U\to\mathbb R^3 \text{ with } F^*\langle\cdot,\cdot\rangle=g .$$

This is Theorem A of the source (p. 1). Because a smooth isometric immersion restricts to an embedding near any point, it also rules out local smooth isometric embeddings. The stronger statement that $g$ can be chosen with the full Euclidean Taylor jet at the origin (Corollary 5.3) is not part of the goal. The goal is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The theorem shows that smooth local isometric realization in $\mathbb R^3$ can fail, which answers negatively the unrestricted smooth problem recorded by Yau and Ghomi. It separates the smooth case from the analytic case (Janet–Cartan) and from finite regularity (Pogorelov, Nadirashvili–Yuan 2008). It also shows, by Corollary 5.3, that the infinite-order jet of the metric at a point does not decide realizability. It leaves open the same question under a sign condition $K\ge0$ or $K\le0$, since the construction uses both signs of curvature.

Formalizing it. The statement is short, but the claimed proof combines PDE estimates for Darboux's equation, hyperbolic propagation, a Baire-category argument and a boundary-saddle geometric step. The literature has disagreed about the status of the smooth question (NY2002 versus NY2008), so a machine-checked proof would remove the ambiguity. Mathlib has the manifold calculus needed to state the result (ContMDiff, mfderiv) but none of the PDE layer.

Difficulty

Where the Gaussian curvature $K$ is nonzero, the realization equations are elliptic or hyperbolic and can be solved locally, so any counterexample must exploit degeneracy where $K$ vanishes and changes type. Finite-regularity counterexamples (Pogorelov) do not carry over: existence at every finite order, on neighborhoods that shrink with the order, does not give one smooth map on a fixed neighborhood. Nonsolvable Monge–Ampère equations are also not enough by themselves, because the coefficients of the Darboux equation come from the same metric, so the obstruction has to be built into $g$ itself. Finally, the conclusion must hold for every neighborhood of the origin and every smooth immersion, with no a priori bounds on $F$.

Formalization scope

• The metric is a function on the subtype of the open set coordinateSquareOpen with values in Matrix (Fin 2) (Fin 2) ℝ. Each entry is ContMDiff … ∞ and each value is Matrix.PosDef, which includes symmetry (Hermitian over ℝ).
• The quantifier ranges over all U : Opens Coord with $U\subseteq Q$ and $0\in U$, and over all maps F : U → Ambient that are ContMDiff … ∞ on the open submanifold $U$. The isometry condition is stated with mfderiv and the Euclidean inner product: $\langle dF_p v, dF_p w\rangle = v\cdot(g(p)w)$.
• The conclusion is a negation of existence, so it is not trivialized by a junk value: $g$ must be genuinely smooth and positive definite, and an immersion on any neighborhood, however small, is excluded.
• Infrastructure needed: Gauss equation and second fundamental form in coordinates, Darboux's equation, energy and weighted elliptic estimates, hyperbolic propagation, and the Baire category theorem (available in Mathlib). The surface-theory layer is reusable for other isometric-embedding projects.

Selected references

• M. Janet, Sur la possibilité de plonger un espace riemannien donné dans un espace euclidien, Ann. Soc. Polon. Math. 5 (1926), 38–43. https://rcin.org.pl/dlibra/publication/31746/edition/15034
• É. Cartan, Sur la possibilité de plonger un espace riemannien donné dans un espace euclidien, Ann. Soc. Polon. Math. 6 (1927), 1–7. https://rcin.org.pl/dlibra/publication/32955/edition/18106
• J. Nash, $C^1$ isometric imbeddings, Ann. of Math. 60 (1954), 383–396. https://doi.org/10.2307/1969840
• N. H. Kuiper, On $C^1$-isometric imbeddings. I, Nederl. Akad. Wetensch. Proc. Ser. A 58 (1955), 545–556.
• A. V. Pogorelov, An example of a two-dimensional Riemannian metric admitting no local realization in $E^3$, Dokl. Akad. Nauk SSSR 198 (1971), 42–43. https://www.mathnet.ru/eng/dan36135
• C.-S. Lin, The local isometric embedding in $\mathbb R^3$ of 2-dimensional Riemannian manifolds with nonnegative curvature, J. Differential Geom. 21 (1985), 213–230. https://doi.org/10.4310/jdg/1214439563
• C.-S. Lin, The local isometric embedding in $\mathbb R^3$ of two-dimensional Riemannian manifolds with Gaussian curvature changing sign cleanly, Comm. Pure Appl. Math. 39 (1986), 867–887. https://doi.org/10.1002/cpa.3160390607
• G. Nakamura and Y. Maeda, Local smooth isometric embeddings of low-dimensional Riemannian manifolds into Euclidean spaces, Trans. Amer. Math. Soc. 313 (1989), 1–51. https://doi.org/10.1090/S0002-9947-1989-0992597-8
• N. Nadirashvili and Y. Yuan, Counterexamples for local isometric embedding, preprint (2002). https://arxiv.org/abs/math/0208127v1
• N. Nadirashvili and Y. Yuan, Improving Pogorelov's isometric embedding counterexample, Calc. Var. PDE 32 (2008), 319–323. https://doi.org/10.1007/s00526-007-0140-7
• M. A. Khuri, Counterexamples to the local solvability of Monge–Ampère equations in the plane, Comm. PDE 32 (2007), 665–674. https://doi.org/10.1080/03605300600635061
• M. A. Khuri, On the local solvability of Darboux's equation, Discrete Contin. Dyn. Syst. (2009, Supplement), 451–456. https://doi.org/10.3934/proc.2009.2009.451
• Q. Han and M. Khuri, Comm. Anal. Geom. 18 (2010), 649–704. https://doi.org/10.4310/CAG.2010.v18.n4.a2
• T.-Y. Lin, Comm. PDE 41 (2016), 1553–1592. https://doi.org/10.1080/03605302.2016.1227336
• S.-T. Yau, Review of geometry and analysis, Asian J. Math. 4 (2000), 235–278. https://doi.org/10.4310/AJM.2000.v4.n1.a16
• M. Ghomi, Open problems in geometry of curves and surfaces, survey (2019), §1.5. https://ghomi.math.gatech.edu/Papers/op.pdf
• OpenAI, A Smooth Metric with No Local Isometric Immersion into Three-Space, OpenAI Math Release preprint, September 24, 2026 (Theorem A, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Smooth-Metric-with-No-Local-Isometric-Immersion-into-Three-Space-September-24-2026/paper.pdf

Motivation

An isometric immersion realizes an abstract Riemannian manifold as a surface in Euclidean space whose induced lengths are exactly the prescribed ones. How many dimensions are needed is a classical question. Nash showed that every compact Riemannian $n$-manifold embeds smoothly and isometrically in some Euclidean space; for surfaces his bound is $\mathbb R^{17}$ (Nash 1956). Gromov lowered the immersion dimension for closed surfaces to $\mathbb R^5$ (Partial Differential Relations, 1986, §3.2.4). Three dimensions do not suffice even locally in the smooth category, and Gromov recorded the question whether every smooth Riemannian surface admits a smooth isometric immersion into $\mathbb R^4$ (Gromov 2000, §I, Remark (d)), later attributing it to Chern around 1950 (Gromov 2015, p. 4).

This mission asks for a machine-checked proof of Theorem 1.1 of an OpenAI preprint dated September 23, 2026 (source), which answers the compact, boundaryless form of that question: every closed smooth Riemannian surface admits a smooth isometric immersion into $\mathbb R^4$. The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.

Background

• 1926–1927 — Janet and Cartan: analytic Riemannian surfaces embed locally isometrically in $\mathbb R^3$ (Janet 1926; Cartan 1927).
• 1954–1955 — Nash and Kuiper: strictly short immersions in positive codimension can be uniformly approximated by $C^1$ isometric immersions (Nash 1954; Kuiper 1955).
• 1956 — Nash's smooth embedding theorem, dimension $n(3n+11)/2$, i.e. $17$ for surfaces.
• 1973 — Poznyak: $C^{3,\alpha}$ metrics on compact parts of simply connected planar domains admit $C^{2,\alpha}$ isometric immersions into $\mathbb R^4$ (Russ. Math. Surveys 1973).
• 1986 — Gromov: smooth isometric immersions of closed surfaces into $\mathbb R^5$.
• 2026 — Lewicka proves $C^{1,\alpha}$ flexibility in $\mathbb R^4$ for low-regularity metrics on disk-type planar domains (arXiv:2511.16305); a companion OpenAI preprint gives a smooth metric on a square with no local smooth isometric immersion into $\mathbb R^3$; the present preprint claims the closed-surface case in $\mathbb R^4$ (Theorem 1.1, p. 2).

Setting

A closed surface $M$ is a compact smooth two-dimensional manifold without boundary; it need not be orientable or connected. A Riemannian metric $g$ assigns to each $p\in M$ a positive definite inner product $g_p$ on $T_pM$, depending smoothly on $p$. A smooth map $F:M\to\mathbb R^4$ is an isometric immersion if

$$\langle dF_p(v),dF_p(w)\rangle=g_p(v,w)\qquad(p\in M,\ v,w\in T_pM).$$

Positive definiteness of $g$ forces $dF_p$ to be injective, so $F$ is an immersion; self-intersections are allowed.

Formalization targets

Goal: Theorem 1.1 (p. 2)

For every closed smooth Riemannian surface $(M,g)$ there is a $C^\infty$ map $F:M\to\mathbb R^4$ with $F^*\delta_4=g$, where $\delta_4=\sum_{i=1}^4dx_i^2$. In Lean this is OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth_isometric_immersion.

Significance

The result itself. The theorem lowers Gromov's immersion dimension for closed surfaces from five to four, with no restriction on curvature or topology, and settles the closed case of the question Gromov attributes to Chern. Dimension four is the first codimension in which the smooth problem can have a global answer for all surfaces, since smooth metrics with no local isometric immersion into $\mathbb R^3$ exist. The open (noncompact) case of the question is not addressed.

Formalizing it. Mathlib now has smooth manifolds, tangent bundles and smooth Riemannian metrics, so the statement is expressible without custom geometry. A complete proof would add Whitney's immersion theorem, Sard's theorem in equal dimensions, metric decompositions into rank-one terms, Nash–Moser-type smoothing estimates, and oscillatory correction schemes; none of these are formalized at this level, and all are reusable in geometric analysis.

Difficulty

The isometric immersion equation $dF^{\mathsf T}dF=g$ is a nonlinear system of three equations in four unknown functions, and its linearization loses derivatives, so a direct implicit function argument fails. Convex integration in the Nash–Kuiper style produces only $C^1$ solutions. Poznyak's smooth theory works on planar domains with boundary, but on a closed surface the successive local corrections must remain compatible globally. The preprint keeps a nondegenerate normal geometry (a nonzero vector-valued second fundamental form) through every step, adds the metric deficit one positive rank-one term $a^2dx^2$ at a time via a velocity loop in a plane normal to $F_y$ and $F_{yy}$ (Proposition 3.1, p. 8; Proposition 7.1, p. 25), and then corrects the approximate metric exactly by a smoothing scheme that solves the linearized equation only on oscillatory modes (Proposition 5.1, p. 15). Nonorientable surfaces are handled by starting from an immersion into a small round $3$-sphere, whose radial direction is a global normal (Lemma 9.1, p. 35).

Formalization scope

• $M$ is a type with ChartedSpace (EuclideanSpace ℝ (Fin 2)) M and IsManifold 𝓘(ℝ, ℝ²) ∞ M, assumed compact, Hausdorff and second countable. Being modeled on $\mathbb R^2$ (not a half-space) encodes "without boundary"; no orientability or connectedness is assumed.
• The metric is Mathlib's Bundle.ContMDiffRiemannianMetric of class $C^\infty$ on the tangent bundle.
• The conclusion asks for ContMDiff … ∞ F and equality of the Euclidean inner product of mfderiv images with g.inner p v w for all tangent vectors; immersivity follows and is not stated separately.
• The statement is not trivialized: the conclusion is an exact pointwise identity for a smooth map, and the hypotheses are satisfied by every closed surface with any metric.

Selected references

• OpenAI, Smooth isometric immersions of closed surfaces into Euclidean four-space, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Smooth-isometric-immersions-of-closed-surfaces-into-Euclidean-four-space-September-23-2026/paper.pdf
• J. Nash, The imbedding problem for Riemannian manifolds, Ann. of Math. 63 (1956). https://doi.org/10.2307/1969989
• J. Nash, C¹-isometric imbeddings, Ann. of Math. 60 (1954). https://doi.org/10.2307/1969840
• M. Gromov, Partial Differential Relations, Springer (1986). https://doi.org/10.1007/978-3-662-02267-2
• M. Gromov, Spaces and questions, Geom. Funct. Anal. (2000). https://www.ihes.fr/~gromov/wp-content/uploads/2018/08/SpacesandQuestions.pdf
• M. Gromov, Geometric, algebraic and analytic descendants of Nash isometric embedding theorems (2015). https://www.ihes.fr/~gromov/wp-content/uploads/2018/08/nash-copy-Oct9.pdf
• E. G. Poznyak, Isometric immersions of two-dimensional Riemannian metrics in Euclidean space, Russian Math. Surveys (1973). https://doi.org/10.1070/RM1973v028n04ABEH001591
• M. Lewicka, Full flexibility of isometric immersions of metrics with low Hölder regularity in Poznyak theorem's dimension, arXiv:2511.16305v3 (2026). https://arxiv.org/abs/2511.16305v3
• H. Whitney, The singularities of a smooth n-manifold in (2n−1)-space, Ann. of Math. 45 (1944). https://doi.org/10.2307/1969266
• R. S. Hamilton, The inverse function theorem of Nash and Moser, Bull. AMS 7 (1982). https://doi.org/10.1090/S0273-0979-1982-15004-2

Motivation: which bounded domains cover compact spaces?

A bounded symmetric domain is a bounded connected open set in $\mathbb C^m$ with, at every point, a holomorphic involution having that point as an isolated fixed point. Examples are the ball, the polydisc and the Siegel upper half-spaces in their bounded realizations. They are the universal covers of compact locally symmetric varieties, such as compact quotients of the ball, and play a central role in algebraic geometry and number theory. A classical theme in several complex variables is that a bounded domain with a large automorphism group must be very special: Wong and Rosay showed that an automorphism orbit accumulating at a strongly pseudoconvex boundary point forces the ball, and Frankel showed that convex domains with compact quotients are symmetric.

Kollár and Pardon, studying algebraic varieties whose universal cover is semialgebraic, asked the following bounded-domain question: if a bounded semialgebraic open subset of a complex affine variety admits a properly discontinuous cocompact group of biholomorphisms, must it be a bounded symmetric domain? Semialgebraicity is a finiteness condition on the shape of the domain. It does not make the boundary smooth or convex, and it imposes nothing on the group.

Timeline

• 1970 — Vey proves that a divisible generalized Siegel domain is symmetric (Ann. Sci. ÉNS 3).
• 1977 — Wong characterizes the ball by its automorphism group among strongly pseudoconvex domains (Invent. Math. 41).
• 1979 — Rosay localizes Wong's theorem to a single $C^2$ strongly pseudoconvex boundary point (Ann. Inst. Fourier 29).
• 1989 — Frankel proves that a convex hyperbolic domain with compact quotient is a bounded symmetric domain, including non-free actions (Acta Math. 163).
• 2012 — Kollár and Pardon pose the bounded semialgebraic domain question (arXiv v2, Question 25) in Algebraic varieties with semialgebraic universal cover (J. Topol. 5; arXiv:1104.2309v2).
• 2021 — Zimmer shows that a $C^{1,1}$-bounded domain covering a compact manifold is a ball (Indiana Univ. Math. J. 70).
• 2026 — An OpenAI preprint, Symmetry of semialgebraic bounded domains with compact quotient (OpenAI Math Release, September 24, 2026), claims an affirmative answer to the Kollár–Pardon question. It has not been peer reviewed, and its proof is not formally verified.

Setting

An affine variety is a reduced complex algebraic set $V\subset\mathbb C^n$, the common zero locus of a set of polynomials. A subset of $\mathbb C^n$ is semialgebraic if it is a finite Boolean combination of sets $\{p=0\}$ and $\{p>0\}$, with $p$ a real polynomial in the real and imaginary parts of the coordinates. Let $U\subseteq V$ be open in $V$, connected, semialgebraic and bounded. A map on $U$ is holomorphic if near each point it is the restriction of a holomorphic map on an open subset of $\mathbb C^n$; a biholomorphism is a homeomorphism that is holomorphic in both directions. A group $\Gamma$ acts properly discontinuously if the action is proper for the discrete topology on $\Gamma$ (finite stabilizers are allowed), and the action is cocompact if $U/\Gamma$ is compact. $U$ is smooth if each point has a neighbourhood in $U$ biholomorphic to an open subset of some $\mathbb C^m$.

Formalization targets

Goal: semialgebraic bounded domains with compact quotient are symmetric (Theorem 1.1)

Let $U$ be a nonempty connected semialgebraic bounded open subset of a complex affine variety $V\subset\mathbb C^n$, and let a group $\Gamma$ act on $U$ by biholomorphisms, properly discontinuously and with $U/\Gamma$ compact. Then

$$U\ \text{is smooth, and}\quad U\cong D\ \text{biholomorphically for some bounded symmetric domain } D\subset\mathbb C^m .$$

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

Significance

The result itself. The theorem answers the Kollár–Pardon question affirmatively. The ambient variety may be singular and nonnormal, the quotient may have finite quotient singularities, and no convexity, boundary regularity or homogeneity is assumed. It shows that semialgebraicity of a single affine realization forces the classical picture: a compact quotient of a semialgebraic bounded domain is a compact quotient of a bounded symmetric domain. This complements the universal-cover classification of the companion preprint on semialgebraic universal covers of normal projective varieties.

Formalizing it. The statement only uses polynomials, real-analytic Boolean combinations, holomorphic maps on subsets of $\mathbb C^n$ and group actions, all available in Mathlib. The proof, however, draws on Nash cell decompositions, analytic discs, scaling limits of automorphisms and Vey's theorem on divisible Siegel domains, none of which is formalized. A formal development would provide reusable semialgebraic geometry and several-complex-variables infrastructure.

Difficulty

The classical rigidity arguments (Wong–Rosay, Frankel, Zimmer) need a smooth strongly pseudoconvex or convex boundary point at which rescaled automorphisms converge to a model domain. A semialgebraic boundary can have corners with several complex-normal directions, and the normal fibres can shrink at rates that depend on tangential parameters, so the naive rescaling limit can collapse to a degenerate set. Moreover $U$ is not known to be a manifold at the start, so smoothness must be proved from the group action before any differential geometry is available. The heart of the proof is a noncollapse estimate that yields a Siegel-type quadratic model $\{\operatorname{Im}w-H(z,z)\in C\}$ to which Vey's theorem applies.

Formalization scope

• $V$ is IsAffineAlgebraic, the zero set of a set of complex polynomials in Fin n → ℂ; $U\subseteq V$ is open in the subspace topology of $V$, IsConnected (hence nonempty), bounded, and semialgebraic through an inductive predicate on real polynomials in $(\operatorname{Re}z,\operatorname{Im}z)$, closed under complement and union.
• $\Gamma$ is an arbitrary group with the discrete topology acting on the subtype $U$, with ProperSMul and a compact orbit space. Each $\gamma$ acts holomorphically in the sense of local ambient analytic extension; since $\gamma^{-1}$ also acts, the elements act by biholomorphisms. A non-faithful action is allowed and is harmless, since properness forces finite stabilizers.
• IsSmooth U asks for local biholomorphisms of neighbourhoods in $U$ onto open subsets of some $\mathbb C^m$. IsBoundedSymmetricDomain D asks that $D$ be open, connected and bounded, and have at each point an involutive biholomorphism fixing it with that point isolated among its fixed points.
• The zero-dimensional case (a point) is included and is trivial, matching the source convention.
• Needed infrastructure: semialgebraic cell decomposition and selection, Montel-type compactness on singular analytic sets, analytic discs, Kobayashi/Carathéodory-type distance estimates and the structure theory of Siegel domains. Each would be reusable.

Selected references

• J. Vey, Sur la division des domaines de Siegel, Ann. Sci. École Norm. Sup. (4) 3 (1970), 479–506. https://www.numdam.org/article/ASENS_1970_4_3_4_479_0.pdf
• B. Wong, Characterization of the unit ball in $\mathbb C^n$ by its automorphism group, Invent. Math. 41 (1977), 253–257. https://doi.org/10.1007/BF01403050
• J.-P. Rosay, Sur une caractérisation de la boule parmi les domaines de $\mathbb C^n$ par son groupe d'automorphismes, Ann. Inst. Fourier 29 (1979), 91–97. https://doi.org/10.5802/aif.768
• S. Frankel, Complex geometry of convex domains that cover varieties, Acta Math. 163 (1989), 109–149. https://doi.org/10.1007/BF02392734
• J. Kollár and J. Pardon, Algebraic varieties with semialgebraic universal cover, J. Topol. 5 (2012), 199–212. https://doi.org/10.1112/jtopol/jts001
• A. Zimmer, Smoothly bounded domains covering compact manifolds, Indiana Univ. Math. J. 70 (2021), 2653–2676. https://arxiv.org/abs/1910.05288v2
• M. Coste, Real algebraic sets, lecture notes, 2005. https://indico.ictp.it/event/a04204/session/10/contribution/7/material/0/0.pdf
• OpenAI, Symmetry of semialgebraic bounded domains with compact quotient, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Symmetry-of-semialgebraic-bounded-domains-with-compact-quotient-September-24-2026/paper.pdf

Motivation: when is a split tangent bundle integrable?

If a complex manifold is a product $X_1\times X_2$, its tangent bundle splits as the sum of the pulled-back tangent bundles of the factors, and each summand is integrable: the bracket of two local holomorphic vector fields tangent to a summand stays in that summand. Conversely, given a holomorphic decomposition $T_X=E_1\oplus E_2$, one wants to know whether it comes from a product. Integrability of the summands is the necessary local condition, and it can fail: Höring exhibited a non-integrable summand on the product of an abelian surface with $\mathbb P^1$ (Höring 2007, Example 2.14). For rationally connected projective manifolds — those in which two general points lie on a rational curve, a class including all Fano manifolds — Höring showed that integrability of one summand already yields a compatible product decomposition, which made automatic integrability the remaining question.

Timeline

• 2000 — Beauville studies how a tangent splitting of a compact Kähler manifold leads to a product decomposition of its universal cover (Beauville 2000).
• 2002 — Campana and Peternell treat Fano manifolds with a two-summand splitting when one summand has rank one or two, hence every two-summand splitting of a Fano manifold of dimension at most five (Campana–Peternell 2002, Theorems 3.5–3.6, Corollary 3.7).
• 2007 — Höring proves that on a rationally connected projective manifold integrability of one summand gives a compatible product (Höring 2007, Theorem 1.4).
• 2008 — Höring conjectures that at least one summand is integrable and proves it when all summands of a uniruled manifold have rank at most two (Höring 2008, Conjecture 1.2, Lemma 4.21).
• 2026 — Höring proves integrability with algebraic leaves on $\mathbb Q$-factorial klt varieties of Fano type, giving actual products in the smooth Fano case, and formulates the smooth rationally connected statement as Conjecture 1.5; a singular rationally connected counterexample shows smoothness matters (Höring 2026).
• 2026 — An OpenAI preprint, Integrability of split tangent bundles on rationally connected manifolds (OpenAI Math Release, September 23, 2026), claims this conjecture in full: both summands are always integrable. The preprint has not been peer reviewed, and its main theorem is not formally verified.

Setting

A complex manifold $X$ of dimension $n$ is a Hausdorff, second-countable space with a holomorphic atlas to $\mathbb C^n$. $X$ is projective if it admits an injective holomorphic immersion into a complex projective space $\mathbb P^N$; for compact $X$ this is a closed embedding.

A rational curve in $X$ is a holomorphic map $\mathbb P^1\to X$. A compact connected projective manifold is rationally connected if there is a nonempty Zariski-open set $U\subseteq X\times X$ such that every pair $(x,y)\in U$ lies on the image of a rational curve. Here Zariski-open is measured through the projective embedding: $U$ is the complement of the common zero set of a family of bihomogeneous polynomials in the two sets of homogeneous coordinates.

A holomorphic splitting $T_X=E_1\oplus E_2$ is given by a holomorphic field of idempotent linear maps $P_x$ on the tangent spaces, with $E_1=\operatorname{im}P$ and $E_2=\ker P$, both of positive rank at every point. A family of subspaces $D$ is integrable if for every open $U$ and every pair of holomorphic vector fields $V,W$ on $U$ with values in $D$, the Lie bracket $[V,W]$ takes values in $D$.

Formalization targets

Goal: Theorem 1.1 (automatic integrability)

Let $X$ be a smooth connected projective complex manifold of dimension at least two which is rationally connected. For every holomorphic decomposition $T_X=E_1\oplus E_2$ into subbundles of positive rank,

$$[\Gamma(U,E_1),\Gamma(U,E_1)]\subseteq\Gamma(U,E_1)\quad\text{and}\quad[\Gamma(U,E_2),\Gamma(U,E_2)]\subseteq\Gamma(U,E_2)$$

for every open $U\subseteq X$, where $\Gamma(U,E_i)$ denotes holomorphic sections over $U$. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The theorem has no rank or positivity hypothesis, and it settles the smooth rationally connected case of Höring's conjecture. Combined with Höring's product theorem it gives Corollary 1.2: every holomorphic splitting of the tangent bundle of a smooth rationally connected projective manifold comes from an isomorphism $X\simeq X_1\times X_2$ identifying $E_i$ with the factor tangent bundles. It also applies to general fibers of the rationally connected quotient of a uniruled compact Kähler manifold, supplying the integrability premise in Höring's structure theorems (Corollary 5.1). Together with the companion preprint on universal-cover splitting for compact Kähler manifolds, it covers both the integrability question and the global product question.

Formalizing it. The statement involves projective embeddings, Zariski-open sets of pairs, rational curves and holomorphic distributions, all expressed from first principles over Mathlib's manifold library. A machine-checked proof would certify a classical-looking but new geometric argument; the compatible product (Corollary 1.2) is not part of this goal.

Difficulty

The bracket of two sections of $E_1$, projected to $E_2$, is a tensor $\bigwedge^2E_1\to E_2$, and the task is to show it vanishes. The natural approach is to restrict to rational curves and use positivity, as in the Fano and low-rank cases, but without positivity or rank assumptions the restricted bundles can have summands of either sign and no vanishing follows directly. Smoothness cannot be dropped: a singular rationally connected example with a non-integrable summand exists (Höring 2026, Example 4.3), so the argument must use the manifold structure in an essential way. Rational connectedness is also needed: Höring's example on an abelian surface times $\mathbb P^1$ is a smooth projective manifold with a non-integrable summand.

Formalization scope

• ComplexManifold carries its dimension, a Hausdorff second-countable topology, and an analytic (ω) atlas modeled on Fin dim → ℂ. The theorem assumes ConnectedSpace, CompactSpace and 2 ≤ X.dim.
• ProjectiveEmbedding X is an injective map to ℙ ℂ (Fin (N+1) → ℂ) that is holomorphic and immersive in every affine patch.
• RationalCurve X is a holomorphic map from $\mathbb P^1$ given by two holomorphic maps $\mathbb C\to X$ agreeing via $z\mapsto z^{-1}$; RationallyConnected e asks for a nonempty, dense, Zariski-open set of pairs (bihomogeneous polynomial complement) all joined by rational curves. Density is automatic for a nonempty Zariski-open subset of the irreducible variety $X\times X$, so stating it does not narrow the class.
• TangentSplitting X is a holomorphic idempotent field on the tangent bundle with range and kernel of positive rank at every point. Integrable uses VectorField.mlieBracketWithin for sections that are holomorphic on an open set.
• The conclusion asserts integrability of both the range and the kernel; the compatible product of Corollary 1.2 is not asserted.
• Infrastructure needed: holomorphic maps from $\mathbb P^1\times\mathbb P^1$, resolution of indeterminacy for rational maps of surfaces, holomorphic bundles on $\mathbb P^1$, families of rational curves. The splitting and integrability definitions are reusable for the companion universal-cover mission.

Selected references

• A. Beauville, Complex manifolds with split tangent bundle, in Complex Analysis and Algebraic Geometry (de Gruyter, 2000), 61–70. https://arxiv.org/abs/math/9809033v2
• F. Campana, T. Peternell, Projective manifolds with splitting tangent bundle, I, Math. Z. 241 (2002), 613–637. https://doi.org/10.1007/s00209-002-0435-5
• A. Höring, Uniruled varieties with split tangent bundle, Math. Z. 256 (2007), 465–479. https://arxiv.org/abs/math/0505327v3
• A. Höring, The structure of uniruled manifolds with split tangent bundle, Osaka J. Math. 45 (2008), 1067–1084. https://www.i-repository.net/contents/osakacu/sugaku/111F0000002-04504-14.pdf
• A. Höring, Fano varieties with split tangent sheaf, preprint (2026). https://arxiv.org/abs/2602.15427v1
• J. Kollár, Y. Miyaoka, S. Mori, Rationally connected varieties, J. Algebraic Geom. 1 (1992), 429–448.
• OpenAI, Integrability of split tangent bundles on rationally connected manifolds, OpenAI Math Release preprint, September 23, 2026 (source of the goal; Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Integrability-of-split-tangent-bundles-on-rationally-connected-manifolds-September-23-2026/main.pdf

Motivation

In one complex variable, every smooth function $g$ on a disc is $\partial\psi/\partial\bar z$ of some smooth $\psi$, and this is what makes the Mittag-Leffler theorem work: local principal parts can be glued into a global meromorphic function. In several variables the corresponding equation is the $\bar\partial$-problem: given a differential form $\eta$ with $\bar\partial\eta = 0$, find $\omega$ with $\bar\partial\omega = \eta$. Whether it is solvable on a domain $U \subset \mathbb{C}^n$ is measured by the Dolbeault cohomology groups $H^{(p,q)}(U)$. Their vanishing characterizes domains of holomorphy, and it drives the solution of the additive Cousin I problem, the several-variable Mittag-Leffler problem.

This mission follows §4.4–4.6 of Jiří Lebl's open textbook Tasty Bits of Several Complex Variables (version 4.4, 2026). There the $\bar\partial$-problem is solved on polydiscs, from the one-variable Cauchy transform through the Dolbeault–Grothendieck lemma. The result is then applied to the Cousin I problem and to domains of holomorphy. The Dolbeault lemma goes back to P. Dolbeault (1953) and A. Grothendieck. The global theory on pseudoconvex domains is due to Hörmander (An Introduction to Complex Analysis in Several Variables, 1966) and to Cartan's Theorem B.

Setting

Write $z_k = x_k + i y_k$ for the coordinates of $\mathbb{C}^n$. The Wirtinger derivative of a function $f$ is $\partial f/\partial\bar z_k = \tfrac12(\partial f/\partial x_k + i\,\partial f/\partial y_k)$.

For strictly increasing tuples $\alpha = (\alpha_1<\dots<\alpha_p)$ and $\beta = (\beta_1<\dots<\beta_q)$ in $\{1,\dots,n\}$, write $dz_\alpha = dz_{\alpha_1}\wedge\cdots\wedge dz_{\alpha_p}$ and $d\bar z_\beta = d\bar z_{\beta_1}\wedge\cdots\wedge d\bar z_{\beta_q}$. A smooth $(p,q)$-form on an open $U\subset\mathbb{C}^n$ is

$$\eta = \sum_{\alpha,\beta}\eta_{\alpha\beta}\,dz_\alpha\wedge d\bar z_\beta,$$

where $\alpha$ and $\beta$ run over the increasing $p$- and $q$-tuples and each $\eta_{\alpha\beta}$ is $C^\infty$ on $U$. The operator

$$\bar\partial\eta = \sum_{\alpha,\beta}\sum_{k=1}^n \frac{\partial\eta_{\alpha\beta}}{\partial\bar z_k}\,d\bar z_k\wedge dz_\alpha\wedge d\bar z_\beta$$

maps $(p,q)$-forms to $(p,q+1)$-forms. A form is $\bar\partial$-closed if $\bar\partial\eta = 0$ and $\bar\partial$-exact if $\eta = \bar\partial\omega$; by convention the only exact $(p,0)$-form is $0$. The statement $H^{(p,q)}(U) = 0$ means that every smooth $\bar\partial$-closed $(p,q)$-form on $U$ is $\bar\partial$-exact.

A possibly unbounded polydisc is a product $\Delta = D_1\times\cdots\times D_n$ in which each $D_k$ is either a disc $\{|z_k - a_k|<\rho_k\}$ or all of $\mathbb{C}$; for example $\mathbb{C}^n$ itself. The finite polydisc is $\Delta_r(w) = \{z : |z_\ell - w_\ell| < r_\ell\ \forall\ell\}$.

Cousin I data on an open $U$ consist of an open covering $\{U_\iota\}_{\iota\in I}$ of $U$ and holomorphic $h_{\iota\kappa}$ on $U_\iota\cap U_\kappa$ with $h_{\iota\kappa}+h_{\kappa\iota}=0$ and $h_{\iota\kappa}+h_{\kappa\lambda}+h_{\lambda\iota}=0$ on the respective intersections. A solution is a family of holomorphic $f_\iota$ on $U_\iota$ with $h_{\iota\kappa} = f_\iota - f_\kappa$. The problem is solvable on $U$ if all Cousin I data on $U$ have solutions.

In Lean these are wirtingerBar, FormCoeffs, dbar, IsSmoothForm, DolbeaultVanishes, polydisc, IsPossiblyUnboundedPolydisc, IsCousinISolvable and IsDomainOfHolomorphy in the namespace LeblSCV.Dolbeault.

Formalization targets

Goal: Theorem 4.4.5

Let $\Delta\subset\mathbb{C}^n$ be a possibly unbounded polydisc, $p\ge0$, $q\ge1$, and $\eta$ a smooth $(p,q)$-form on $\Delta$ with $\bar\partial\eta = 0$. Then there is a smooth $(p,q-1)$-form $\omega$ on $\Delta$ with

$$\bar\partial\omega = \eta\quad\text{on }\Delta,\qquad\text{that is,}\qquad H^{(p,q)}(\Delta) = 0 \ \ (q\ge1).$$

Milestones

1. Lemma 4.4.6 (for a disc $U$). If $g$ is smooth near $\overline U$, then $\psi(z) = \frac{1}{2\pi i}\int_U \frac{g(\zeta)}{\zeta-z}\,d\zeta\wedge d\bar\zeta$ is smooth on $U$ and $\partial\psi/\partial\bar z = g$.
2. Lemma 4.4.7 (Dolbeault–Grothendieck). If $0<s_\ell<r_\ell$, every smooth $\bar\partial$-closed $(p,q)$-form on $\Delta_r(w)$, $q\ge1$, is $\bar\partial$ of a smooth $(p,q-1)$-form on $\Delta_s(w)$.
3. Lemma 4.6.4. Smooth Cousin I data on any open set have smooth solutions.
4. Theorem 4.6.5. On a domain with $H^{(0,1)}(U)=0$ the Cousin I problem is solvable.
5. Corollary 4.6.6. The Cousin I problem is solvable on every possibly unbounded polydisc.
6. Theorem 4.5.6. A domain $U\subset\mathbb{C}^n$ with $H^{(0,q)}(U)=0$ for $1\le q\le n-1$ is a domain of holomorphy.

Significance

Theorem 4.4.5 is the model case of the vanishing theorem $H^{(p,q)}(U)=0$, $q\ge1$, on domains of holomorphy. In particular it solves the $\bar\partial$-problem on all of $\mathbb{C}^n$. Through Theorem 4.6.5 it gives the Cousin I problem on polydiscs, and therefore the existence of meromorphic functions with prescribed local principal parts there. Theorem 4.5.6 is one half of the cohomological characterization of domains of holomorphy (Remark 4.5.8, item (viii)). The other half is Cartan's Theorem B, which the book states without proof as Theorem 4.4.2.

All targets are classical and fully proved in the book. As far as a search of the Prove2Me corpus and of Mathlib shows, none of them is formalized. Mathlib has real Fréchet derivatives, smooth bump functions and partitions of unity, and Lebesgue measure on $\mathbb{C}$. It has no bidegree forms, no $\bar\partial$ operator on forms, no Cauchy transform and no Dolbeault cohomology. This mission builds the $(p,q)$-form layer and the first global solvability theorem for $\bar\partial$.

Difficulty

The one-variable step needs the Cauchy–Pompeiu formula and differentiation under an integral with a weakly singular kernel. Both the smoothness of $\psi$ and the identity $\partial\psi/\partial\bar z = g$ require care near $\zeta = z$.

In several variables, the natural idea is to solve $\bar\partial\omega=\eta$ on each of an exhausting sequence of polydiscs and take a limit. It fails as stated: solutions on successive polydiscs differ by $\bar\partial$-closed forms and need not converge. For $q\ge2$ the discrepancy has to be corrected exactly, by applying the lemma again with a cutoff. For $q=1$ the discrepancies are holomorphic functions, and they have to be made small by polynomial approximation, so that the corrected solutions converge. The Dolbeault–Grothendieck lemma loses a little of the polydisc at each step, so the argument has to shrink the polydiscs at each stage.

On the formal side, $\bar\partial$ on forms carries signs from reordering wedge products. A wrong sign changes which forms are closed. So the sign convention is fixed in the definition and checked against $\bar\partial\circ\bar\partial = 0$.

Formalization scope

• $\mathbb{C}^n$ is Fin n → ℂ with 0-based indices. Polydiscs use the modulus in each coordinate, as in the book, so the sup norm of Fin n → ℂ agrees with them. No Euclidean ball occurs.
• A form is a coefficient family FormCoeffs n = Finset (Fin n) → Finset (Fin n) → (Fin n → ℂ) → ℂ: an increasing tuple is the set of its entries, and η A B z is the coefficient of $dz_A\wedge d\bar z_B$. IsSmoothForm U p q η requires every coefficient to be ContDiffOn ℝ ∞ on $U$ and the coefficients of the wrong bidegree to vanish on $U$. Only values on $U$ matter.
• dbar is Definition 4.4.1 written in the increasing basis. The coefficient of $dz_A\wedge d\bar z_C$ is $\sum_{k\in C}(-1)^{|A|+\#\{j\in C:j<k\}}\,\partial\eta_{A,C\setminus\{k\}}/\partial\bar z_k$. A sorry-free check confirms that this sign convention makes the mixed second derivatives cancel in $\bar\partial\bar\partial\eta$, and that $\partial\bar z_1/\partial\bar z_1 = 1$.
• $H^{(p,q)}(U)=0$ is stated as "every closed smooth $(p,q)$-form is exact"; the quotient space is not built. The solution $\omega$ is required to be smooth.
• Radii of a possibly unbounded polydisc lie in ℝ≥0∞, with $\infty$ meaning the factor $\mathbb{C}$.
• Holomorphic on an open set is DifferentiableOn ℂ. A domain is an open connected set. Cousin index types range over Type, which loses nothing.
• Restriction: Lemma 4.4.6 is stated for $U$ an open disc. The book allows any bounded open set with piecewise-$C^1$ boundary. The disc is the case that the Dolbeault–Grothendieck lemma uses. The measure $d\zeta\wedge d\bar\zeta$ is $-2i$ times Lebesgue measure.
• The goal cannot be trivialized through the form layer. A definition of $\bar\partial$ with a wrong sign, or one that drops the smoothness of $\omega$ or the $\bar\partial$-closedness of $\eta$, states a different theorem and is ruled out. Hypotheses are satisfiable: $\eta = 0$ is closed, and $\mathbb{C}^n$ is a possibly unbounded polydisc (checked sorry-free).
• Needed infrastructure: the Cauchy transform and Cauchy–Pompeiu formula, differentiation under the integral with parameters, smooth cutoffs, uniform approximation of holomorphic functions by polynomials on polydiscs, and partitions of unity. The form layer is reusable in later work on the $\bar\partial$-problem (balls, Hartogs triangle, pseudoconvex domains). Proofs of $\bar\partial^2 = 0$ for the dbar defined here, or of the one-variable lemma for general piecewise-$C^1$ domains, are welcome.

Selected references

• J. Lebl, Tasty Bits of Several Complex Variables, version 4.4, 2026, §4.4–4.6. https://www.jirka.org/scv/
• L. Hörmander, An Introduction to Complex Analysis in Several Variables, North-Holland Mathematical Library 7, 3rd ed., 1990.
• P. Dolbeault, Sur la cohomologie des variétés analytiques complexes, C. R. Acad. Sci. Paris 236 (1953), 175–177.