OAI Math

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

The relativistic Vlasov–Maxwell system is the basic kinetic model of a collisionless plasma: a cloud of charged particles, described by a phase-space density, moves under the electromagnetic field it generates, and the field evolves by Maxwell's equations with the particles as sources. Whether smooth, compactly supported data in three dimensions always produce a solution that stays smooth for all time has been the central question about the Cauchy problem for this system since the 1980s. Weak solutions exist globally, but they come without regularity or uniqueness, and every previous global classical result required smallness, a dimensional reduction, symmetry, or a nearby global reference solution.

This mission asks for a machine-checked proof of global existence and uniqueness of classical solutions for arbitrary smooth admissible data, as claimed in an OpenAI preprint dated September 23, 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

• 1984 — Wollman proves local existence and uniqueness of classical solutions (CPAM 1984).
• 1986 — Glassey and Strauss show that a classical solution continues as long as the momentum support stays bounded (ARMA 1986); in 1987 they prove global existence for initially dilute plasmas (CMP 1987).
• 1985–1998 — Glassey and Schaeffer obtain global classical solutions for symmetric relativistic Vlasov–Poisson (CMP 1985) and for reduced Vlasov–Maxwell models in one and one-half, two and one-half, and two dimensions (1990, 1997, 1998).
• 1989 — DiPerna and Lions prove global existence of weak solutions for large data (CPAM 1989); Rein treats the relativistic case directly (CMS 2004).
• 1990 — Rein proves stability of global existence near suitable global solutions (CMP 1990).
• 2002–2003 — New proofs of the continuation criterion by Klainerman–Staffilani (CPAA 2002) and Bouchut–Golse–Pallard (ARMA 2003).
• 2004–2016 — Refined continuation criteria: Schaeffer's small-data theorem with momentum tails (IUMJ 2004), Pallard (IUMJ 2005), Luk and Strain's two-dimensional projection criterion (CMP 2014) and moment bounds (ARMA 2016).
• 2020–2025 — Small-particle global results with large fields: Bigorgne (CMP 2020; APDE 2025), Wei–Yang (CMP 2021).
• 2026 — Wang establishes large-data global existence under cylindrical symmetry (arXiv:2203.01199, arXiv:2607.14685).
• September 2026 — The OpenAI preprint claims the general large-data result without symmetry (Theorem 1.1, p. 3).

Setting

For momentum $v\in\mathbb R^3$ let $q(v)=\sqrt{1+|v|^2}$ and $u(v)=v/q(v)$ (the relativistic velocity, $|u|<1$). The unknowns are a particle density $f(t,x,v)\ge0$ and fields $E(t,x),B(t,x)\in\mathbb R^3$, with charge and current densities $\rho_f=\int f\,dv$ and $j_f=\int u(v)f\,dv$. In the one-species normalization the system is

$$\partial_tf+u(v)\cdot\nabla_xf+(E+u(v)\times B)\cdot\nabla_vf=0,$$ $$\partial_tE-\nabla_x\times B=-j_f,\qquad \partial_tB+\nabla_x\times E=0,\qquad \nabla_x\cdot E=\rho_f,\qquad \nabla_x\cdot B=0 .$$

A smooth admissible datum $(f_0,E_0,B_0)$ has $f_0\in C_c^\infty(\mathbb R^3_x\times\mathbb R^3_v)$, $f_0\ge0$, $E_0,B_0$ smooth with every derivative bounded and $E_0,B_0\in L^2$, and satisfies $\nabla\cdot E_0=\rho_{f_0}$, $\nabla\cdot B_0=0$. A classical solution on $[0,\infty)$ is a $C^1$ triple solving the system pointwise, with $E,B$ continuous in time with values in $L^2$, and with $f(t,\cdot,\cdot)$ supported in a fixed compact set on each bounded time interval.

Formalization targets

Goal: Theorem 1.1 (p. 3)

Every smooth admissible datum generates a classical solution on $[0,\infty)$ with the given initial values; for every finite $T$ the solution is $C^\infty$ on $[0,T]\times\mathbb R^6$ (respectively $[0,T]\times\mathbb R^3$ for the fields) with compact phase-space support on $[0,T]$; and any other classical solution with the same datum agrees with it at every $t\ge0$. This is OAI.RVM.global_classical_solution.

Significance

The result itself. It settles the large-data global classical regularity problem for three-dimensional relativistic Vlasov–Maxwell, with no size, symmetry or neutrality assumption; nonzero total charge with its Coulomb tail is allowed. Global well-posedness at this level is the starting point for questions about long-time behaviour, scattering and stability of plasma equilibria that previously could only be posed for small or symmetric data.

Formalizing it. The proof combines the Glassey–Strauss representation of fields along backward light cones, energy-flux estimates, a delicate signed bootstrap, and local well-posedness and continuation theory. None of this PDE infrastructure (wave-equation representation formulas, characteristics of transport equations in phase space, Sobolev local theory) is currently available in a proof assistant at the needed level, so each component is reusable.

Difficulty

By the Glassey–Strauss criterion it suffices to bound the momentum support on finite time intervals. The natural approach estimates the absolute value of the force along a characteristic using the retarded field representation and energy flux through light cones. At receiver energy $w$ this loses a factor $\sqrt w$ relative to what is needed (Section 1.2, p. 4); the loss comes from sources whose velocity is much closer to the light ray than the receiver's. The preprint instead estimates the signed momentum increment $V_X(t_2)-V_X(t_1)$, integrating the retarded force along source trajectories before taking norms (Proposition 2.1, p. 5; Lemma 6.1, p. 24), controls direction changes (Lemma 7.1, p. 29), and closes a bootstrap whose time-to-double lower bounds have a divergent sum (Section 9).

Formalization scope

• Space and momentum are EuclideanSpace ℝ (Fin 3); derivatives are Fréchet derivatives in coordinate directions; the time derivative is derivWithin on $[0,\infty)$, so $t=0$ is one-sided.
• Admissible encodes $C^\infty$ with compact support and nonnegativity for $f_0$; ContDiff ℝ ∞ with all iterated derivatives bounded and MemLp 2 for $E_0,B_0$; and both Gauss constraints pointwise.
• Classical requires $C^1$ regularity on the closed half-spaces, $f\ge0$, continuity of $t\mapsto E(t),B(t)$ into $L^2$ on $[0,\infty)$, compact phase support on each $[0,T]$, all five equations pointwise for $t\ge0$ (including both constraints), and the initial values.
• The conclusion asserts existence, smoothness on every finite horizon, and uniqueness within the same classical class; uniqueness is pointwise equality at all $t\ge0$. The hypotheses are satisfiable (e.g. $f_0=0$, $E_0=B_0=0$), so the statement is not vacuous.
• $\rho$ and $j$ are Bochner integrals in $v$; for compactly supported $f$ these are the genuine moments.

Selected references

• OpenAI, Global classical solutions of the three-dimensional relativistic Vlasov–Maxwell system, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Global-classical-solutions-of-the-three-dimensional-relativistic-Vlasov-Maxwell-system-September-23-2026/paper.pdf
• R. T. Glassey, W. A. Strauss, Singularity formation in a collisionless plasma could occur only at high velocities, Arch. Ration. Mech. Anal. 92 (1986). https://doi.org/10.1007/BF00250732
• R. T. Glassey, W. A. Strauss, Absence of shocks in an initially dilute collisionless plasma, Comm. Math. Phys. 113 (1987). https://doi.org/10.1007/BF01223511
• S. Wollman, An existence and uniqueness theorem for the Vlasov–Maxwell system, Comm. Pure Appl. Math. 37 (1984). https://doi.org/10.1002/cpa.3160370404
• R. J. DiPerna, P.-L. Lions, Global weak solutions of Vlasov–Maxwell systems, Comm. Pure Appl. Math. 42 (1989). https://doi.org/10.1002/cpa.3160420603
• J. Luk, R. M. Strain, A new continuation criterion for the relativistic Vlasov–Maxwell system, Comm. Math. Phys. 331 (2014). https://doi.org/10.1007/s00220-014-2108-8
• F. Bouchut, F. Golse, C. Pallard, Classical solutions and the Glassey–Strauss theorem for the 3D Vlasov–Maxwell system, Arch. Ration. Mech. Anal. 170 (2003). https://doi.org/10.1007/s00205-003-0265-6
• S. Klainerman, G. Staffilani, A new approach to study the Vlasov–Maxwell system, Commun. Pure Appl. Anal. 1 (2002). https://doi.org/10.3934/cpaa.2002.1.103
• X. Wang, Large data global solution of the 3D RVM system with cylindrical symmetry, arXiv:2203.01199 and arXiv:2607.14685 (2026). https://arxiv.org/abs/2607.14685v1

Motivation: uniqueness of weak Boltzmann solutions

The Boltzmann equation describes a dilute gas through a density $F(t,x,v)$ of particles at position $x$ with velocity $v$, evolving by free transport and binary collisions. For hard spheres, the collision rate is proportional to the normal relative speed. In 1989 DiPerna and Lions constructed global renormalized solutions for all initial data with finite mass, energy and entropy, and weak stability holds at the same level. Existence and stability do not give uniqueness, though: the physical bounds do not even make the quadratic collision term locally integrable, and the uniqueness of general renormalized solutions is a basic question in kinetic theory (Silvestre 2022, §2). Uniqueness is known only under much stronger assumptions, such as Maxwellian upper bounds or closeness to equilibrium.

Timeline

• 1974 — Ukai: global existence and uniqueness near a Maxwellian for periodic cutoff hard potentials (Proc. Japan Acad. 1974).
• 1978 — Kaniel and Shinbrot: uniqueness and local existence under Maxwellian upper bounds (CMP 1978).
• 1988 — Golse, Lions, Perthame and Sentis: velocity averaging lemmas (JFA 1988).
• 1989 — DiPerna and Lions: global renormalized solutions and weak stability (Ann. of Math. 1989); the entropy inequality follows in 1991 (ARMA 1991).
• 1999 — For the spatially homogeneous hard-sphere equation, Mischler and Wennberg prove uniqueness among conservative solutions with finite mass and energy (Ann. IHP C 1999); Wennberg gives homogeneous nonuniqueness examples in which the energy increases (J. Stat. Phys. 1999).
• 2010 — Levermore and Masmoudi give a periodic formulation of renormalized solutions relative to a Maxwellian (ARMA 2010).
• 2024–2026 — Ill-posedness results: Chen–Holmer for the constant kernel (Ann. PDE 2024), Chen–Guo–Shen–Zhang for hard spheres in Gaussian-weighted $L^2_vH^s_x$ (arXiv:2606.01331). Gismondi, Golding and Novack conjecture nonuniqueness of renormalized inhomogeneous Landau and Boltzmann solutions for a dense class of data (arXiv:2608.13758).
• 2026 — An OpenAI preprint, Nonuniqueness for the periodic hard-sphere Boltzmann equation (OpenAI Math Release, September 23, 2026), claims a single finite-entropy datum on $\mathbb T^3\times\mathbb R^3$ with two distinct admissible solutions. It has not been peer reviewed, and the claim has not been formally verified.

Setting

Phase space is $\Omega=\mathbb T^3_x\times\mathbb R^3_v$, with $\mathbb T^3=\mathbb R^3/\mathbb Z^3$. For incoming velocities $v,v_*$ and a collision normal $\omega\in S^2$, put $a=(v-v_*)\cdot\omega$, $v'=v-a\omega$, $v_*'=v_*+a\omega$. The hard-sphere collision operator is

$$Q(F,F)(v)=\int_{\mathbb R^3\times S^2}|a|\,\big(F(v')F(v_*')-F(v)F(v_*)\big)\,dv_*\,d\omega ,$$

with ordinary surface measure on $S^2$; the two terms are the gain and the loss. The Cauchy problem is $(\partial_t+v\cdot\nabla_x)F=Q(F,F)$, $F(0)=F_0$. An initial datum has finite entropy if it is nonnegative and $\int_\Omega F_0(1+|v|^2+|\log F_0|)<\infty$.

A solution is admissible (Definition 2.1 of the source) if, with $M(v)=(2\pi)^{-3/2}e^{-|v|^2/2}$:

• it is renormalized: the equation holds weakly for $M\beta(F/M)$ for every $C^1$ $\beta$ with $\beta(0)=0$ and $|\beta'(z)|\le C_\beta/(1+z)$, and the separately renormalized gain and loss are integrable on bounded time intervals;
• it is weakly continuous in $L^1$ against every bounded measurable test and takes the initial value $F_0$;
• mass, energy and absolute entropy stay bounded on bounded time intervals;
• it conserves local mass and total momentum, and satisfies the energy inequality and the relative-entropy inequality with the full entropy dissipation at every time.

Formalization targets

Goal: two admissible solutions from one datum (Theorem 1.1)

There is a nonnegative finite-entropy datum $F_0$ with bounded velocity support, two admissible global solutions $F,G$ with initial datum $F_0$, and a time $T>0$ such that

$$F,G\in C([0,T];L^1(\Omega)),\qquad Q^\pm(F),\,Q^\pm(G)\in L^1([0,T]\times\Omega),\qquad F(t)\neq G(t)\ \text{in } L^1 \text{ for some } t\in[0,T].$$

This is Theorem 1.1 of the source (p. 3), with the difference placed in the common interval of strong continuity, which is where the source establishes it. 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 shows that the DiPerna–Lions framework, even with local mass conservation, momentum conservation and the energy and entropy inequalities retained, does not determine the evolution uniquely. The example is spatially inhomogeneous and periodic, and the two solutions start from exactly the same datum, unlike ill-posedness results that compare nearby data. On the interval where they differ, both solutions satisfy the unrenormalized equation. The datum has bounded velocities but unbounded amplitudes concentrated at smaller and smaller spatial scales, which points to the kind of extra control a uniqueness theorem has to impose.

Formalizing it. The statement fixes a long list of admissibility conditions. Its definitions are a useful contribution in their own right: renormalized solutions, entropy dissipation and kinetic test functions on the torus are not in Mathlib. The 65-page proof (colored decompositions, Carleman representation, velocity averaging, a dilation limit and a branching analysis) is a long-term target. Its propositions are natural milestones.

Difficulty

Constructing two different weak limits is not the hard part: approximations with and without a small "hot seed" give two candidate solutions. The difficulty is to show that they really differ. A vanishing seed can produce a hit on the a priori cap that carries arbitrarily little mass, and weak compactness can erase it in the limit. The source must rule out this loss of information uniformly as the cold velocity distributions collapse onto an axis, where the weight controlling the hot density is singular. At the same time every admissibility condition, including the entropy-dissipation inequality and local mass conservation, has to survive the limits. Energy-increasing constructions (Wennberg) and homogeneous examples do not meet these constraints.

Formalization scope

• Velocities live in EuclideanSpace ℝ (Fin 3), positions in Fin 3 → AddCircle 1, and densities are real functions on phase space. The sphere carries (volume).toSphere, which is ordinary surface area, not a probability measure.
• gain and loss are Bochner integrals. To prevent them from silently returning $0$ on non-integrable fibers, AdmissibleGlobal requires fiberwise integrability and space-time integrability of the renormalized gain and loss.
• AdmissibleGlobal f₀ F encodes Definition 2.1: finite entropy at each time, a.e. initial value, weak continuity against bounded measurable tests, uniform moment bounds, the renormalized equation for all Renormalization $\beta$ and all smooth periodic KineticTest $\varphi$, local mass conservation against MassTest, total momentum conservation, the energy inequality, and the entropy inequality in ℝ≥0∞ with the lower semicontinuous extension of $(A-B)\log(A/B)$.
• StrongEarly T F adds $T>0$, strong $L^1$ continuity on $[0,T]$ via eLpNorm, and integrability of gain and loss on $[0,T]$. Distinctness is ¬ (F t =ᵐ G t) for some $t\in[0,T]$.
• Infrastructure needed: averaging lemmas, renormalized-solution compactness, the Carleman representation, and estimates on free transport on the torus. Contributions to any of these are welcome.

Selected references

• R. J. DiPerna and P.-L. Lions, On the Cauchy problem for Boltzmann equations: global existence and weak stability, Ann. of Math. 130 (1989), 321–366. https://doi.org/10.2307/1971423
• R. J. DiPerna and P.-L. Lions, Global solutions of Boltzmann's equation and the entropy inequality, Arch. Ration. Mech. Anal. 114 (1991), 47–55. https://doi.org/10.1007/BF00375684
• C. D. Levermore and N. Masmoudi, From the Boltzmann equation to an incompressible Navier–Stokes–Fourier system, Arch. Ration. Mech. Anal. 196 (2010), 753–809. https://doi.org/10.1007/s00205-009-0254-5
• L. Silvestre, Regularity estimates and open problems in kinetic equations, arXiv:2204.06401 (2022). https://doi.org/10.48550/arXiv.2204.06401
• S. Kaniel and M. Shinbrot, The Boltzmann equation. I. Uniqueness and local existence, Comm. Math. Phys. 58 (1978), 65–84. https://doi.org/10.1007/BF01624788
• S. Ukai, On the existence of global solutions of mixed problem for non-linear Boltzmann equation, Proc. Japan Acad. 50 (1974), 179–184. https://doi.org/10.3792/pja/1195519027
• S. Mischler and B. Wennberg, On the spatially homogeneous Boltzmann equation, Ann. Inst. H. Poincaré C 16 (1999), 467–501. https://doi.org/10.1016/S0294-1449(99)80025-0
• B. Wennberg, An example of nonuniqueness for solutions to the homogeneous Boltzmann equation, J. Stat. Phys. 95 (1999), 469–477. https://doi.org/10.1023/A:1004546031908
• F. Golse, P.-L. Lions, B. Perthame and R. Sentis, Regularity of the moments of the solution of a transport equation, J. Funct. Anal. 76 (1988), 110–125. https://doi.org/10.1016/0022-1236(88)90051-1
• X. Chen and J. Holmer, Well/ill-posedness bifurcation for the Boltzmann equation with constant collision kernel, Ann. PDE 10 (2024), Art. 14. https://doi.org/10.1007/s40818-024-00177-w
• X. Chen, Y. Guo, S. Shen and Z. Zhang, Sharp $H^s_x$ ill-posedness of the hard-sphere Boltzmann equation, arXiv:2606.01331 (2026). https://doi.org/10.48550/arXiv.2606.01331
• N. Gismondi, W. Golding and M. Novack, A sharp rigidity/flexibility threshold for the isotropic Landau equation, arXiv:2608.13758 (2026). https://doi.org/10.48550/arXiv.2608.13758
• OpenAI, Nonuniqueness for the periodic hard-sphere Boltzmann equation, OpenAI Math Release preprint, September 23, 2026 (Theorem 1.1, p. 3; Definition 2.1, p. 8). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Nonuniqueness-for-the-periodic-hard-sphere-Boltzmann-equation-September-23-2026/paper.pdf

Motivation

Calderón's inverse conductivity problem asks whether the electrical conductivity inside a body is determined by voltage and current measurements on its boundary. Mathematically, a conductivity $\gamma$ on a domain $\Omega$ defines the elliptic equation $\operatorname{div}(\gamma\nabla u)=0$, and the boundary data are encoded by the Dirichlet-to-Neumann (DN) operator $\Lambda_\gamma$, which maps a boundary voltage to the resulting boundary current. The problem underlies electrical impedance tomography and is the model case of a large family of inverse boundary-value problems. Calderón (1980) posed it for bounded measurable conductivities bounded away from zero; how much regularity uniqueness requires has been a central question since.

Background

• 1974. Miller constructs elliptic divergence-form equations with nonunique continuation (doi:10.1007/BF00247634).
• 1980. Calderón poses the problem and proves injectivity of the linearization at constant conductivities.
• 1987. Sylvester and Uhlmann prove uniqueness for smooth conductivities in dimension $n\ge3$ (doi:10.2307/1971291).
• 2006. Astala and Päivärinta prove uniqueness for bounded measurable conductivities in the plane (doi:10.4007/annals.2006.163.265).
• 2015–2016. Haberman proves uniqueness for $W^{1,n}$ conductivities in dimensions three and four (doi:10.1007/s00220-015-2460-3); Caro and Rogers prove it for Lipschitz conductivities in all dimensions $n\ge3$ (doi:10.1017/fmp.2015.9).
• 2020. Daudé, Kamran and Nicoleau give anisotropic (matrix-valued) counterexamples with partial data, via nonunique continuation (doi:10.1017/fms.2020.1).

In dimension $n\ge3$, uniqueness for merely bounded measurable scalar conductivities remained unresolved. The source of this mission is an OpenAI preprint dated September 23, 2026, which constructs a counterexample in dimension three.

Setting

Let $\Omega=B(0,3)\subset\mathbb R^3$. A conductivity is a measurable $\gamma:\Omega\to\mathbb R$ with $0<c\le\gamma\le C$ almost everywhere. Let $H^1(\Omega)$ be the Sobolev space, $H^1_0(\Omega)$ the closure of compactly supported smooth functions, and $H^{1/2}(\partial\Omega)\cong H^1(\Omega)/H^1_0(\Omega)$ the trace space, with dual $H^{-1/2}(\partial\Omega)$. For a trace $f$, let $u_f\in H^1(\Omega)$ be the unique function with trace $f$ such that

$$\int_\Omega\gamma\,\nabla u_f\cdot\nabla\varphi\,dx=0\qquad(\varphi\in H^1_0(\Omega)).$$

The DN operator $\Lambda_\gamma:H^{1/2}(\partial\Omega)\to H^{-1/2}(\partial\Omega)$ is

$$\langle\Lambda_\gamma f,g\rangle=\int_\Omega\gamma\,\nabla u_f\cdot\nabla v\,dx,\qquad \operatorname{Tr}v=g.$$

Formalization targets

Goal: Theorem 1.1

There are $\gamma_0,\gamma_1\in L^\infty(B(0,3))$ and $0<c<C$ with

$$c\le\gamma_j\le C\ \text{a.e.},\qquad \gamma_j=1\ \text{near }\partial B(0,3),\qquad |\{\gamma_0\ne\gamma_1\}|>0,\qquad \Lambda_{\gamma_0}=\Lambda_{\gamma_1}.$$

The Lean statement OAI.ScalarConductivity.main_nonuniqueness is open on the platform.

Significance

The theorem shows that scalar Calderón uniqueness fails in the bounded measurable class in dimension three, in contrast with the planar theorem of Astala–Päivärinta and the Lipschitz and $W^{1,n}$ uniqueness results in higher dimensions. It locates the regularity threshold for uniqueness strictly between $L^\infty$ and the known positive classes. By Corollary 1.2, counterexamples can be localized: any finite family of disjoint balls inside any Lipschitz domain supports $2^m$ distinct conductivities with the same DN map.

The result is stated in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.

Difficulty

Matrix-valued counterexamples exist, but they do not transfer to scalar conductivities: scalar coefficients can approximate matrix ones only in the sense of $G$- or $H$-convergence, and Rondi's example shows that exact realization of a full boundary map by a scalar coefficient can fail. Moreover, Daudé–Kamran–Nicoleau note an obstruction for full-boundary data: a weakly harmonic factor with constant full boundary trace is constant. One must therefore match the entire DN operator (every boundary input) exactly, with a scalar coefficient, and with uniform ellipticity bounds; the paper does so with a nested family of scalar blocks realizing prescribed current triples exactly.

Formalization scope

• $H^1(B(0,3))$ is the closure, in $L^2(B;\mathbb R^4)$, of the jets $(f,\nabla f)$ of smooth $f$; $H^1_0$ is the closure of jets of smooth $f$ with compact support in the ball; the trace space is the quotient and the DN operator is a continuous linear map into its continuous dual.
• IsDirichletToNeumann γ Λ requires existence and uniqueness of the weak $\gamma$-harmonic extension of every trace and the weak flux identity against every $v\in H^1$.
• EqualOneNearBoundary asks for $r<3$ with $\gamma=1$ a.e. on $\{r<|x|<3\}$; bounds and measurability are stated almost everywhere on the ball.

A complete development needs Sobolev spaces on a ball, weak solutions of divergence-form equations (Lax–Milgram), trace spaces, and the paper's block constructions (convex-integration-type scalarization). Contributions formalizing Theorem 3.1 (exact finite-field scalarization), Proposition 4.1 (branching block) and Corollary 1.2 are welcome.

Selected references

• OpenAI, Nonuniqueness for Bounded Measurable Scalar Conductivities in Three Dimensions, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Nonuniqueness-for-Bounded-Measurable-Scalar-Conductivities-in-Three-Dimensions-September-23-2026/paper.pdf
• A. P. Calderón, On an inverse boundary value problem, Seminar on Numerical Analysis and its Applications to Continuum Physics, Rio de Janeiro, 1980.
• J. Sylvester, G. Uhlmann, A global uniqueness theorem for an inverse boundary value problem, Ann. of Math., 1987. https://doi.org/10.2307/1971291
• K. Astala, L. Päivärinta, Calderón's inverse conductivity problem in the plane, Ann. of Math., 2006. https://doi.org/10.4007/annals.2006.163.265
• P. Caro, K. M. Rogers, Global uniqueness for the Calderón problem with Lipschitz conductivities, Forum Math. Pi, 2016. https://doi.org/10.1017/fmp.2015.9
• B. Haberman, Uniqueness in Calderón's problem for conductivities with unbounded gradient, Comm. Math. Phys., 2015. https://doi.org/10.1007/s00220-015-2460-3
• T. Daudé, N. Kamran, F. Nicoleau, On nonuniqueness for the anisotropic Calderón problem with partial data, Forum Math. Sigma, 2020. https://doi.org/10.1017/fms.2020.1

Motivation

Heat in an insulated planar plate evolves by the heat equation with Neumann boundary condition. For generic initial temperature, after a long time the temperature minus its average is dominated by an eigenfunction of the first positive Neumann eigenvalue. Rauch asked in 1974 where the hottest and coldest points of the plate end up, and conjectured that they move to the boundary (Rauch 1975). In spectral form, the hot spots conjecture asks whether a first nonconstant Neumann eigenfunction attains its maximum and minimum only on the boundary. The question links spectral geometry, reflected Brownian motion and elliptic PDE, and it is known to depend on topology: it fails for some domains with holes.

This mission asks for a machine-checked proof of the strict form of the conjecture for all smooth bounded simply connected planar domains, as claimed in an OpenAI preprint dated September 24, 2026 (source): every nonzero first-positive Neumann eigenfunction has no interior critical point at all. 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

• 1975 — Rauch poses the problem in lectures on qualitative PDE theory (Rauch 1975).
• 1999 — Bañuelos and Burdzy distinguish strict and nonstrict formulations and prove cases by coupling of reflected Brownian motions (J. Funct. Anal. 1999). Burdzy and Werner construct a counterexample with two holes (Ann. of Math. 1999).
• 2000 — Jerison and Nadirashvili prove the conjecture for convex planar domains with two axes of symmetry (JAMS 2000); Bass and Burdzy find examples with both extrema in the interior (Duke 2000).
• 2002–2004 — Pascu treats convex domains with one symmetry (Trans. AMS 2002); Atar and Burdzy treat lip domains (JAMS 2004).
• 2005 — Burdzy obtains a counterexample with a single hole and states the simply connected planar conjecture explicitly (Duke 2005, Conjecture 1.2(ii)).
• 2007 — Miyamoto handles nearly circular convex domains under a spectral-diameter condition.
• 2015–2022 — Siudeja proves the conjecture for a class of acute triangles (Math. Z. 2015); Judge and Mondal exclude interior critical points on every triangle (Ann. of Math. 2020, erratum 2022).
• 2021–2024 — Rohleder introduces a variational principle for tangent vector fields (arXiv:2106.05224; 2024), the starting point of the preprint.
• 2025–2026 — Sharp bounds on the failure of the conjecture (de Dios Pont–Hsu–Taylor, 2025); classification of critical points on triangles (Chen–Gui–Yao, Invent. Math. 2026).
• September 2026 — The OpenAI preprint claims the strict conjecture for all smooth bounded simply connected planar domains (Theorem 1.1, p. 1).

Setting

Let $\Omega\subset\mathbb R^2$ be a nonempty bounded open simply connected set with $C^\infty$ boundary. The first positive Neumann eigenvalue is

$$\mu=\mu_1(\Omega)=\inf\Bigl\{\frac{\int_\Omega|\nabla v|^2}{\int_\Omega v^2}: v\in H^1(\Omega),\ \int_\Omega v=0,\ v\ne0\Bigr\},$$

counting only positive eigenvalues (many sources call it $\mu_2$). The first positive Neumann eigenspace $V$ consists of the $u\in H^1(\Omega)$ with $\int_\Omega u=0$ and

$$\int_\Omega\nabla u\cdot\nabla v=\mu\int_\Omega uv\qquad\text{for all }v\in H^1(\Omega).$$

This weak formulation encodes $-\Delta u=\mu u$ in $\Omega$ with $\partial_\nu u=0$ on $\partial\Omega$. Eigenspace functions are smooth up to the boundary.

Formalization targets

Goal: Theorem 1.1 (p. 1)

For every nonzero $u\in V$,

$$\nabla u(x)\ne0\quad(x\in\Omega),\qquad\text{and}\qquad \min_{\partial\Omega}u<u(x)<\max_{\partial\Omega}u\quad(x\in\Omega).$$

This holds for every member of the eigenspace, also when $\mu$ is a multiple eigenvalue. In Lean this is OAI.StrictHotSpots.main_theorem.

Significance

The result itself. It resolves Burdzy's simply connected planar hot spots conjecture in its strongest form: not only do the extrema lie on the boundary, but there are no interior saddle points either, for every eigenfunction in the eigenspace. Combined with the Burdzy–Werner and Burdzy one-hole counterexamples, it shows that simple connectivity is exactly the dividing line among smooth planar domains. The intermediate kernel theorem (Theorem 5.1, p. 12), a conditional negativity statement for reciprocal Green kernels of the disk, is stated independently of the eigenfunction problem.

Formalizing it. A complete development needs Sobolev spaces on smooth planar domains, the Riemann mapping theorem with boundary regularity, Neumann elliptic regularity, and the theory of conditionally negative definite kernels. Each is reusable. No machine-checked proof of any hot spots result, including the triangle case, is known to exist.

Difficulty

Each Cartesian derivative of an eigenfunction solves the same Helmholtz equation, but its boundary values have no fixed sign, so a maximum-principle argument on one directional derivative fails on a general domain with no preferred direction. Coupling methods need convexity or symmetry. The preprint instead uses the Neumann condition jointly on both derivatives (the gradient is tangent to the boundary), via a nonnegative quadratic form whose null space consists exactly of eigenfunction gradients (Proposition 3.1, p. 7). The central difficulty is to build enough scalar boundary multipliers preserving that null space; this requires proving that a reciprocal kernel $K(p,s)K(p,t)/N(s,t)$ is conditionally negative semidefinite (Theorem 5.1, p. 12), through regularized Green kernels, a complete Nevanlinna–Pick-type matrix property, and a boundary limit.

Formalization scope

• $\Omega$ is a subset of EuclideanSpace ℝ (Fin 2): nonempty, open, bounded, IsSimplyConnected (which includes path-connectedness), with a smooth local defining function $\rho$ with nonzero derivative at every boundary point.
• $H^1$ is encoded by HasH1Gradient Ω v g: $v,g\in L^2(\Omega)$ and $g$ is the weak gradient of $v$ against smooth test functions compactly supported in $\Omega$. $\mu$ is the sInf of Rayleigh quotients over mean-zero nonzero $H^1$ functions; this set is nonempty and bounded below by $0$.
• InFirstNeumannEigenspace Ω u requires $u\in C^\infty(\overline\Omega)$, mean zero, and the weak eigen-equation for all $H^1$ test pairs. The smoothness-up-to-the-boundary clause is a standard regularity fact for Neumann eigenfunctions on smooth domains (the preprint cites Showalter for it), so it does not exclude any eigenfunction.
• The hypothesis $u\ne0$ is pointwise somewhere in $\Omega$. The conclusion uses sInf/sSup of $u$ on frontier Ω, which is compact and nonempty, so these are the true minimum and maximum.
• A vacuous reading is excluded: the eigenspace is nontrivial on every such domain (Rellich compactness), so the goal is a genuine statement about actual eigenfunctions.

Selected references

• OpenAI, Strict hot spots and absence of interior critical points on smooth simply connected planar domains, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Strict-hot-spots-and-absence-of-interior-critical-points-on-smooth-simply-connected-planar-domains-September-24-2026/main.pdf
• J. Rauch, Five problems: an introduction to the qualitative theory of partial differential equations, in Partial Differential Equations and Related Topics, LNM 446 (1975). https://doi.org/10.1007/BFb0070610
• R. Bañuelos, K. Burdzy, On the "hot spots" conjecture of J. Rauch, J. Funct. Anal. 164 (1999). https://doi.org/10.1006/jfan.1999.3397
• K. Burdzy, W. Werner, A counterexample to the "hot spots" conjecture, Ann. of Math. 149 (1999). https://doi.org/10.2307/121027
• K. Burdzy, The hot spots problem in planar domains with one hole, Duke Math. J. 129 (2005), 481–502. https://doi.org/10.1215/S0012-7094-05-12932-5
• D. Jerison, N. Nadirashvili, The "hot spots" conjecture for domains with two axes of symmetry, J. Amer. Math. Soc. 13 (2000), 741–772. https://doi.org/10.1090/S0894-0347-00-00346-5
• R. Atar, K. Burdzy, On Neumann eigenfunctions in lip domains, J. Amer. Math. Soc. 17 (2004), 243–265. https://doi.org/10.1090/S0894-0347-04-00453-9
• C. Judge, S. Mondal, Euclidean triangles have no hot spots, Ann. of Math. 191 (2020). https://doi.org/10.4007/annals.2020.191.1.3
• J. Rohleder, A new approach to the hot spots conjecture, arXiv:2106.05224 (2021). https://arxiv.org/abs/2106.05224v4

Motivation

An isotropic elastic body is described by two spatially varying Lamé moduli: the shear modulus $\mu$ and the parameter $\lambda$ (the bulk modulus is $\lambda+2\mu/3$). The elastic inverse problem asks whether static boundary measurements, the boundary tractions produced by all prescribed boundary displacements, determine both moduli inside the body. It is the elasticity analogue of Calderón's conductivity problem, with applications to elastography and nondestructive testing, and it is harder because two coefficients are coupled through a vector-valued system rather than a scalar equation.

Background

• 1980, 1987. Calderón poses the scalar conductivity problem; Sylvester and Uhlmann prove uniqueness for smooth conductivities in dimension $n\ge3$ using complex geometric optics (doi:10.2307/1971291).
• 1995. Nakamura and Uhlmann recover the boundary Taylor series of the Lamé moduli (doi:10.1137/S0036141093247494).
• 2002–2003. Eskin and Ralston develop matrix complex geometric optics with planar transport frames and prove restricted uniqueness results (doi:10.1088/0266-5611/18/3/324).
• 2003. Nakamura and Uhlmann's erratum corrects their earlier global claim, proving uniqueness only when $\nabla\mu$ is small in $C^m$ (doi:10.1007/s00222-002-0276-1).
• 2015. Imanuvilov and Yamamoto prove global uniqueness in two dimensions (doi:10.1088/0266-5611/31/3/035004).
• 2017, 2023. Lin and Nakamura reconstruct boundary values at finite regularity (doi:10.1088/1361-6420/aa942d); Tan and Liu treat boundary jets on manifolds and analytic global recovery (doi:10.1088/1361-6420/ace649).

Without smallness, analyticity or symmetry hypotheses, three-dimensional global uniqueness was not established. The source of this mission is an OpenAI preprint dated September 24, 2026, which claims it for all smooth moduli satisfying the energy-positivity conditions.

Setting

Let $\Omega\subset\mathbb R^3$ be a bounded connected domain with $C^\infty$ boundary, and let $\lambda,\mu\in C^\infty(\overline\Omega)$ satisfy

$$\mu>0,\qquad 3\lambda+2\mu>0\qquad\text{on }\overline\Omega.$$

For a displacement $u:\Omega\to\mathbb R^3$, the strain is $e(u)=\tfrac12(\nabla u+\nabla u^{T})$, the stress $\sigma(u)=\lambda(\operatorname{div}u)I+2\mu\,e(u)$, and the elasticity system is $\operatorname{div}\sigma(u)=0$. For boundary data $f\in H^{1/2}(\partial\Omega;\mathbb R^3)$ let $u_f\in H^1(\Omega;\mathbb R^3)$ be the unique weak solution with trace $f$. The displacement-to-traction map is

$$\langle\Lambda_{\lambda,\mu}f,g\rangle=\int_\Omega\bigl[\lambda\,(\operatorname{div}u_f)(\operatorname{div}v_g)+2\mu\,e(u_f):e(v_g)\bigr]\,dx,\qquad \operatorname{Tr}v_g=g.$$

Formalization targets

Goal: Theorem 1.1

For admissible pairs $(\lambda_1,\mu_1)$, $(\lambda_2,\mu_2)$ on $\Omega$,

$$\Lambda_{\lambda_1,\mu_1}=\Lambda_{\lambda_2,\mu_2}\ \Longrightarrow\ \lambda_1=\lambda_2\ \text{and}\ \mu_1=\mu_2\ \text{in }\Omega.$$

The Lean statement OAI.Elasticity.global_uniqueness is open on the platform.

Significance

The theorem settles the smooth three-dimensional isotropic elastic Calderón uniqueness question under the natural energy-positivity assumptions, with no analyticity, no closeness to constants, and no prior agreement near the boundary. It identifies both moduli from the full zero-frequency boundary operator. It does not give a reconstruction algorithm or stability estimates, which remain natural follow-up questions.

The result is stated in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.

Difficulty

The scalar complex-geometric-optics method does not apply directly to the Lamé system. Earlier reductions to auxiliary systems ran into two problems documented in the Nakamura–Uhlmann erratum: the planar matrix transport equation with prescribed initial data need not be solvable, and the corrected solutions lead to a pseudodifferential rather than a differential identity. The Eskin–Ralston reduction from auxiliary fields to physical displacements is not injective, so equality of physical boundary maps does not by itself give equality of auxiliary Cauchy data. A proof must work with exact physical solutions and keep track of their actual divergences.

Formalization scope

• Domain Ω: open, connected, bounded, with smooth boundary given by local $C^\infty$ diffeomorphisms of $\mathbb R^3$ flattening $\partial\Omega$.
• Admissible Ω λ μ: both moduli smooth on an open neighbourhood of $\overline\Omega$, with $\mu>0$ and $3\lambda+2\mu>0$ on $\overline\Omega$.
• $H^1(\Omega;\mathbb R^3)$ is the closure of jets $(f,\partial_1f,\partial_2f,\partial_3f)$ of smooth $f$ in $L^2$; boundary data are $H^1$ modulo the closure of compactly supported smooth jets.
• DN Ω λ μ f g is the energy pairing of a weak solution with trace $f$ against any representative of $g$; the goal assumes equality of these two-variable functions and concludes pointwise equality of the moduli on $\Omega$.

A complete development needs vector-valued Sobolev spaces, Korn's inequality, the weak Dirichlet problem for the Lamé system, Carleman estimates and complex geometric optics for elliptic systems. These tools are reusable for other inverse problems. Contributions formalizing Lemma 2.1 (common exterior extension), Proposition 2.2 (transfer of physical solutions) and Proposition 3.2 (supported Carleman estimate) are welcome.

Selected references

• OpenAI, Global Uniqueness for the Smooth Isotropic Elasticity Inverse Problem, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Global-Uniqueness-for-the-Smooth-Isotropic-Elasticity-Inverse-Problem-September-24-2026/article.pdf
• G. Nakamura, G. Uhlmann, Erratum: Global uniqueness for an inverse boundary value problem arising in elasticity, Invent. Math., 2003. https://doi.org/10.1007/s00222-002-0276-1
• G. Nakamura, G. Uhlmann, Inverse problems at the boundary for an elastic medium, SIAM J. Math. Anal., 1995. https://doi.org/10.1137/S0036141093247494
• G. Eskin, J. Ralston, On the inverse boundary value problem for linear isotropic elasticity, Inverse Problems, 2002. https://doi.org/10.1088/0266-5611/18/3/324
• O. Yu. Imanuvilov, M. Yamamoto, Global uniqueness in inverse boundary value problems for the Navier–Stokes equations and Lamé system in two dimensions, Inverse Problems, 2015. https://doi.org/10.1088/0266-5611/31/3/035004
• J. Sylvester, G. Uhlmann, A global uniqueness theorem for an inverse boundary value problem, Ann. of Math., 1987. https://doi.org/10.2307/1971291
• Y.-H. Lin, G. Nakamura, Boundary determination of the Lamé moduli for the isotropic elasticity system, Inverse Problems, 2017. https://doi.org/10.1088/1361-6420/aa942d

Motivation

Given a source probability measure $\rho$ and a target $\mu$ on $\mathbb R^d$, Brenier's theorem (Brenier 1991) says that when $\rho$ is absolutely continuous there is a unique map $T_\mu$ pushing $\rho$ to $\mu$ that minimizes the quadratic cost $\int|x-T(x)|^2\,d\rho$, and that it is the gradient of a convex function. Fixing $\rho$, the assignment $\mu\mapsto T_\mu$ embeds the space of probability measures into $L^2(\rho)$; this linearization of optimal transport is used in statistics, data analysis and machine learning to compare measures by comparing their maps. Its usefulness depends on quantitative stability: how far apart can $T_\mu$ and $T_\nu$ be when $\mu$ and $\nu$ are close in Wasserstein distance? For general targets the map cannot be Lipschitz in the target, and the question is which Hölder exponent holds uniformly.

This mission asks for a machine-checked proof that, for a uniform source on a convex body, the sharp uniform exponent is exactly $1/3$, as claimed in an OpenAI preprint dated September 25, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal below is open.

Timeline

• 1991 — Brenier proves existence and uniqueness of quadratic optimal maps as gradients of convex potentials (CPAM 1991).
• 2011 — Gigli reports Ambrosio's local one-half Hölder estimate along target curves near regular data (Proc. Edinb. Math. Soc. 2011, Corollary 3.4).
• 2020–2021 — Berman obtains stability for varying sources against fixed targets (Found. Comput. Math. 2021); Mérigot, Delalande and Chazal derive target-uniform bounds, including a $W_1^{2/15}$ estimate for a uniform convex source (AISTATS 2020).
• 2023 — Delalande and Mérigot prove an $L^2$ map bound of order $W_1^{1/6}$ for densities bounded above and below on convex domains, with a convex-gradient interpolation inequality (Duke 2023).
• 2024 — Letrouit and Mérigot extend potential stability to John domains (arXiv:2411.04908).
• 2025 — Divol, Niles-Weed and Pooladian obtain a $W_2^{1/3}$ map estimate for nondegenerate finite targets, with constants depending on the number, masses and geometry of the atoms (IMRN 2025).
• 2026 — Letrouit proves that exponents above $1/3$ fail for a nonconvex source and conjectures uniform square-root stability in $W_2$ for uniform convex sources (C. R. Math. 2026, Theorem 2 and Conjecture 3).
• September 2026 — The OpenAI preprint claims the uniform $W_2^{1/3}$ bound for every uniform convex source and shows that no larger exponent holds, disproving the square-root conjecture (Theorem 1.1, p. 2; Proposition 2.2, p. 4).

Setting

Fix $d\ge2$, a compact convex $K\subset\mathbb R^d$ with nonempty interior, and the uniform source $\rho=\mathbf 1_K\,dx/|K|$. Fix a nonempty compact $Y\subset\mathbb R^d$ and let $\mathrm{Prob}(Y)$ be the Borel probability measures with $\mu(\mathbb R^d\setminus Y)=0$. A coupling of $\mu,\nu$ is a probability measure on $\mathbb R^d\times\mathbb R^d$ with marginals $\mu,\nu$, and

$$W_2(\mu,\nu)=\Bigl(\inf_{\pi}\int|y-z|^2\,d\pi(y,z)\Bigr)^{1/2}.$$

For $\mu\in\mathrm{Prob}(Y)$, $T_\mu$ is the Brenier map: a measurable $T$ with $T_\#\rho=\mu$ whose graph coupling $(\mathrm{id},T)_\#\rho$ is the unique optimal coupling of $\rho$ and $\mu$. Distances between maps are measured in $L^2(\rho)$: $\|T-S\|_{L^2(\rho)}=(\int|T-S|^2d\rho)^{1/2}$.

Formalization targets

Milestone: Proposition 2.2 (p. 4) — the exponent cannot be improved

For every $d\ge2$, with $K=Y=[-1,1]^d$ and every $\alpha>1/3$,

$$\sup_{\mu\ne\nu\in\mathrm{Prob}(Y)}\frac{\|T_\mu-T_\nu\|_{L^2(\rho)}}{W_2(\mu,\nu)^\alpha}=+\infty,$$

and the supremum stays infinite when both targets have exactly three atoms. In Lean (one_third_exponent_is_sharp): for every $\alpha>1/3$ and $C>0$ there are distinct three-atom probability measures on the cube with unique optimal maps $T,T'$ and $C\,W_2^\alpha<\|T-T'\|$.

Goal: Theorem 1.1 (p. 2) — uniform one-third stability

For every $K$, $Y$ as above there is a finite constant $C(K,Y)$ such that for all $\mu,\nu\in\mathrm{Prob}(Y)$ the Brenier maps exist, are unique, and

$$\|T_\mu-T_\nu\|_{L^2(\rho)}\le C(K,Y)\,W_2(\mu,\nu)^{1/3}.$$

The targets may be atomic, singular or absolutely continuous; the constant does not depend on them. In Lean this is one_third_stability. Together the two statements determine the sharp exponent in this uniform class, which is the second sentence of Theorem 1.1.

Significance

The result itself. The upper bound improves every earlier target-uniform exponent ($2/15$, $1/6$, $1/5$, $1/4$ in $W_1$ or $W_2$) to $1/3$ in $W_2$, with a constant independent of atom counts, atom masses, separations and density bounds. The lower bound disproves Letrouit's conjectured exponent $1/2$ with only three atoms on a cube. The pair gives the exact uniform stability exponent of the linearized optimal-transport embedding for uniform convex sources.

Formalizing it. Mathlib has measures, couplings and Lebesgue integration but no optimal-transport theory. A formal development would supply Wasserstein distance, existence and uniqueness of Brenier maps for semi-discrete and general targets, and Lipschitz convex potentials, all reusable. The sharpness statement is the more elementary one and is a natural first milestone.

Difficulty

The standard route bounds the difference of convex potentials and then converts it to a gradient bound by an interpolation inequality; previous potential estimates lose a power, giving exponents below $1/3$. The preprint's key step is a linear $W_2$ bound on the $L^2(\rho)$ distance of potentials, obtained by moving the sites of finite targets along an optimal coupling with fixed masses and controlling the intercept velocity through a uniform moment inequality for the cells of a maximum of affine functions (Lemma 4.1, p. 9; Proposition 5.1, p. 12). The constant must stay uniform as cell masses or faces degenerate, which rules out any argument relying on a spectral gap of the cell graph Laplacian. The final passage from finite to arbitrary Borel targets needs stability of optimal maps under approximation (Proposition 6.3, p. 16).

Formalization scope

• Space is EuclideanSpace ℝ (Fin d) with Borel measures. uniformMeasure K is $(\mathrm{vol}\,K)^{-1}\cdot\mathrm{vol}|_K$; with $K$ compact convex with nonempty interior its volume is positive and finite.
• IsSupported μ Y means $\mu(Y^c)=0$. Couplings are probability measures with the two marginals; costs are lower integrals in ℝ≥0∞; $W_2$ is the square root of the real part of the infimal cost, finite here because supports are bounded.
• IsUniqueQuadraticOptimalMap ρ μ T asserts that $T$ is measurable, pushes $\rho$ to $\mu$, is cost-optimal among all couplings, and that every coupling of no larger cost equals the graph coupling. The goal must therefore also produce the Brenier maps; they are not assumed.
• The constant is chosen after $d$, $K$, $Y$ and before $\mu,\nu$, and is required to be finite and nonnegative.
• The sharpness milestone fixes $K=Y=[-1,1]^d$, requires exactly three distinct atoms with positive weights, $\mu\ne\nu$ and $W_2>0$, so it cannot be satisfied trivially.

Selected references

• OpenAI, Sharp One-Third Stability of Brenier Maps, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Sharp-One-Third-Stability-of-Brenier-Maps-September-25-2026/article.pdf
• Y. Brenier, Polar factorization and monotone rearrangement of vector-valued functions, Comm. Pure Appl. Math. 44 (1991), 375–417. https://doi.org/10.1002/cpa.3160440402
• C. Letrouit, Unstable optimal transport maps, C. R. Math. 364 (2026), 333–344. https://doi.org/10.5802/crmath.834
• A. Delalande, Q. Mérigot, Quantitative stability of optimal transport maps under variations of the target measure, Duke Math. J. 172 (2023), 3321–3357. https://doi.org/10.1215/00127094-2022-0106
• Q. Mérigot, A. Delalande, F. Chazal, Quantitative stability of optimal transport maps and linearization of the 2-Wasserstein space, AISTATS 2020, PMLR 108. https://proceedings.mlr.press/v108/merigot20a.html
• V. Divol, J. Niles-Weed, A.-A. Pooladian, Tight stability bounds for entropic Brenier maps, IMRN 2025, rnaf078. https://doi.org/10.1093/imrn/rnaf078
• C. Letrouit, Q. Mérigot, Gluing methods for quantitative stability of optimal transport maps, arXiv:2411.04908 (2024). https://arxiv.org/abs/2411.04908v3
• R. J. Berman, Convergence rates for discretized Monge–Ampère equations and quantitative stability of optimal transport, Found. Comput. Math. 21 (2021), 1099–1140. https://doi.org/10.1007/s10208-020-09480-x
• N. Gigli, On Hölder continuity-in-time of the optimal transport map towards measures along a curve, Proc. Edinb. Math. Soc. 54 (2011), 401–409. https://doi.org/10.1017/S001309150800117X

Motivation

Real zeros of Dirichlet L-functions close to one obstruct uniform estimates for primes in arithmetic progressions. A conductor-independent logarithmic gap is the precise quantitative issue addressed here. The source manuscript presents the surrounding research claim.

Setting

A Dirichlet character χ modulo an integer q is primitive, nonprincipal, and real-valued when its complex values have zero imaginary part. Its analytically continued L-function is denoted L(s,χ). The zero β is real and lies strictly between zero and one; log is the natural logarithm.

Formalization target

Prove that one positive real constant works for every allowed modulus, character and zero:

$$\exists c>0\;\forall q\ge3,\quad L(\beta,\chi)=0,\ 0<\beta<1\Longrightarrow c\le(1-\beta)\log q.$$

The constant must be independent of q and χ.

The selected formal target is OAI.SiegelZeros.WeightedTorusJets.exists_absolute_real_zero_gap.

Significance and status

This is the uniform zero-gap conclusion itself, not a statement for a bounded family of conductors. The source dated October 1, 2026 states this as its principal result. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

A bound whose constant varies with the character cannot establish this quantifier order. The arithmetic and analytic estimates must retain one positive constant across every conductor and every real primitive character.

Formalization scope

The goal uses Mathlib’s actual Dirichlet characters and L-functions over ℂ, with q : ℕ, a nonzero instance and q ≥ 3. Both available published formulations are referenced. The second formulation merely groups the zero hypotheses differently and is not presented as an independent milestone. The manuscript’s interpolation and determinant lemmas have no supplied published theorem IDs and are not attached as milestones.

Selected references

• OpenAI, Uniform exclusion of Landau–Siegel zeros, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Closed diagonal orbits encode lattices in totally real number fields. Their distribution tests whether arithmetic families fill the space of unimodular lattices as their discriminants grow. The source manuscript presents the surrounding research claim.

Setting

For a fixed prime n=d+1 ≥ 5, Xₙ is the quotient of SLₙ(ℝ) by its integral lattice subgroup. A packet consists of normalized full lattices of one local homothety type, including the specified sign translates. Its measure averages orbital probabilities with orbit-volume weights.

Formalization target

For any sequence of totally real degree-n fields and full lattices whose multiplier discriminants tend to infinity, prove

$$\exists\nu,\quad\nu\text{ is Haar probability},\qquad\mu_i\Rightarrow\nu,$$

and tightness of the entire family {μᵢ}. Weak convergence uses every bounded continuous real test function and includes the probability normalization of every μᵢ.

The selected formal target is OAI.DukePrimeDegree.prime_degree_packet_measure_equidistribution_unconditional.

Significance and status

The conclusion addresses arbitrary local types and includes absence of escape of mass. The fixed-Haar formulation is also available as a supporting target. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Convergence on compactly supported tests alone would not establish the requested probability convergence on a noncompact quotient. The packet normalization and tightness must be justified uniformly through the discriminant limit.

Formalization scope

The source definitions use completed lattices over ℤₚ, diagonal-flow period covolumes and volume-weighted sums over distinct orbits. The theorem fixes prime degree at least five and allows both fields and local types to vary. Both published formulations and their shared definitions are referenced.

Selected references

• OpenAI, Equidistribution of Prime-Degree Torus Packets with Arbitrary Local Type, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Cubic Gauss sums oscillate even after normalization. Their first moment asks whether this cancellation retains a precise lower-order bias when averaged over arithmetic primes. The source manuscript presents the surrounding research claim.

Setting

Work in the Eisenstein integers ℤ[ω], with ω=exp(2πi/3). A primary prime p is a prime element congruent to one modulo three. N(p)=|p|², G(p) is the normalized cubic Gauss sum, and c*=(2π)^(2/3)/(3Γ(2/3)).

Formalization target

At the real sharp cutoff X, establish

$$\sum_{\substack{p\text{ primary prime}\\N(p)\le X}}G(p)=\frac65c_*\frac{X^{5/6}}{\log X}+o\!\left(\frac{X^{5/6}}{\log X}\right).$$

The two supporting targets compare each fixed angular mode to its explicit model and give cancellation for every nonzero mode.

The selected formal target is OAI.CubicFirstMoment.patterson_firstMoment.

Significance and status

The coefficient and scale specify the first moment, rather than only an order-of-magnitude estimate. Both conjugate prime elements are included when they satisfy the primary-prime predicate. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Pointwise estimates on G(p) do not isolate the X^(5/6)/log X bias. The error must be little-o at that scale with the exact arithmetic normalization.

Formalization scope

The published definitions use residue-class representatives, the cubic residue symbol, the trace exponential phase, and complex-valued cutoff sums. Little-o is taken as real X tends to positive infinity. Angular modes are integers held fixed before the limit.

Selected references

• OpenAI, An unconditional first moment for cubic Gauss sums, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.