Motivation: continuum phase transitions with a power-law tail

Whether identical classical particles in $\mathbb R^3$, interacting only through a stable radial pair potential, can undergo a phase transition is a classical existence problem of rigorous statistical mechanics, highlighted in Simon's list of problems in mathematical physics (Simon 1984). A transition shows up as a singularity of the thermodynamic free energy. Earlier rigorous continuum transitions rely on extra structure — two species, many-body terms, hard cores, or interactions defined through a fixed partition into boxes — or on a mean-field limit in which the potential itself changes. A natural requirement for a satisfactory answer is a single fixed pair potential with a bounded core and an explicit integrable power-law tail.

Timeline

• 1965 — Motzkin and Straus's weighted-graph maximization, later used for occupation bounds (Motzkin–Straus 1965).
• 1966 — Lebowitz and Penrose: rigorous van der Waals–Maxwell theory in the Kac limit (Lebowitz–Penrose 1966).
• 1970 — Ruelle's superstability framework (Ruelle 1970).
• 1971 — Ruelle: transition for a symmetric two-species continuum system (Ruelle 1971).
• 1973 — Gerardi, Marchioro, Olivieri and Presutti extend the Lebowitz–Penrose limit to superstable references (GMOP 1973).
• 1984 — Simon lists the problem among fifteen problems in mathematical physics.
• 1998–1999 — Lebowitz, Mazel and Presutti: liquid–vapor transition with attractive pair and repulsive four-body interactions (PRL 1998, J. Stat. Phys. 1999).
• 2026 — He, Jauslin, Lebowitz and Peled: transition for a finite-range box-modified Kac pair interaction (CMP 2026); Dereudre and Renaud-Chan: density coexistence for saturated many-body interactions (arXiv:2602.11078).
• 2026 — Two OpenAI preprints (OpenAI Math Release, September 24, 2026): a radial potential with divergent core and $o(r^{-3})$ tail with a temperature singularity, and the present A radial continuum phase transition with algebraic decay, which claims a bounded continuous potential with $|\phi(r)|\le Cr^{-3-1/32}$. Neither is peer reviewed, and the theorem is not formally verified.

Setting

Particles live in $\mathbb R^3$; a radial pair potential is a function $\phi:[0,\infty)\to\mathbb R$ (in Lean, ℝ≥0 → ℝ) applied to pair distances. For the cube $\Lambda_L=[0,L]^3$ and $N\ge0$,

$$U^\phi(x_1,\dots,x_N)=\sum_{i<j}\phi(|x_i-x_j|),\qquad Z_{L,N}(\beta)=\frac1{N!}\int_{\Lambda_L^N}e^{-\beta U^\phi}\,dx,\qquad Z_{L,0}=1 .$$

The potential is stable if $U^\phi\ge -BN$ for all configurations. The canonical free energy at density $\rho$ is

$$f(\beta,\rho)=-\lim_{L\to\infty}\frac1{\beta L^3}\log Z_{L,\lfloor\rho L^3\rfloor}(\beta).$$

The packing constant is $p=\lim_{L\to\infty}M_L/L^3$, where $M_L$ is the largest number of points in $[0,L]^3$ at mutual distance $\ge1$; in Lean IsPackingDensity p asserts this limit. StrictTemperatureCorner f βc asserts finite left and right derivatives at $\beta_c$ with the right one strictly smaller, and non-differentiability.

Formalization targets

Milestone: the corner at the central density

At the single density $\rho=5p/3$: there are a bounded continuous stable $\phi$ with $|\phi(r)|\le Cr^{-3-1/32}$ for $r\ge1$ and $\beta_c\in[7/8,9/8]$ such that $f(\cdot,5p/3)$ exists for all $\beta>0$ and

$$f'_-(\beta_c,5p/3)>f'_+(\beta_c,5p/3).$$

Goal: a common corner on a density interval

There are a bounded continuous $\phi$, constants $B,C>0$ with

$$\sum_{i<j}\phi(|x_i-x_j|)\ge -BN,\qquad |\phi(r)|\le C\,r^{-3-1/32}\ (r\ge1),$$

an open interval $I=(5p/3-\eta,\,5p/3+\eta)\subset(0,\infty)$ and one $\beta_c\in[7/8,9/8]$ such that for every $\rho\in I$ the free energy $f(\beta,\rho)$ exists and is finite for every $\beta>0$, and

$$f'_-(\beta_c,\rho)>f'_+(\beta_c,\rho).$$

This is Theorem 1.1 of the source. Both statements are published on the platform with status Open.

Significance

The result itself. The theorem gives a single-species, bounded, continuous radial pair potential with an explicit integrable power-law tail whose canonical free energy has a strict temperature corner at one critical inverse temperature for a whole interval of densities. The interaction is a genuine radial function of separations with all long-range terms kept; boxes appear only in the estimates. It does not treat Lennard–Jones-type potentials and does not identify the phases as conventional fluids. The companion preprint has a divergent core but only an $o(r^{-3})$ tail; the fixed power margin $1/32$ here needs a quantitative range estimate not present there.

Formalizing it. The statement fixes the model completely (free boundary conditions on $[0,L]^3$, Lebesgue measure without temperature normalization, $1/N!$, $\lfloor\rho L^3\rfloor$ particles), so a formal proof would settle exactly which version of the problem is solved. The infrastructure (thermodynamic limits, convex duality for pressures, Kac comparisons) is reusable for the companion mission.

Difficulty

The Lebowitz–Penrose theory produces non-convex mean-field free energies only in the limit where the attraction range tends to infinity, and that limiting object is not the free energy of any fixed potential. A single potential must therefore contain infinitely many attractions at growing ranges, and the required singularity must survive all of them. Density coexistence at fixed temperature does not by itself give a temperature corner at a fixed density: two supporting slopes with equal density coordinate and different energy coordinates are needed. A pointwise power bound constrains how strong the successive attractions may be relative to their ranges, which is why a quantitative comparison with an explicit error is required.

Formalization scope

• Positions are EuclideanSpace ℝ (Fin 3); distances enter through nndist, so the potential is a function on ℝ≥0. Boundedness, continuity, stability with $B>0$, and decay with $C>0$ are separate conjuncts.
• $p$ is existentially quantified but pinned by IsPackingDensity p (a limit), and $p>0$ is required; packingNumber is a sSup over a bounded set of naturals.
• IsCanonicalFreeEnergy φ ρ f asserts $-\log Z/(\beta L^3)\to f(\beta)$ for every $\beta>0$, so $f$ is determined on $(0,\infty)$; one-sided derivatives use HasDerivWithinAt on Iic βc and Ici βc.
• The goal requires the interval to lie in $(0,\infty)$ and $\beta_c$ to be independent of $\rho$.
• Needed infrastructure: superstability and occupation moments, existence of thermodynamic limits and their convex duality, a Motzkin–Straus bound, quantitative Kac comparison, and subdifferential persistence arguments.

Selected references

• B. Simon, Fifteen problems in mathematical physics, in Perspectives in Mathematics, Birkhäuser, 1984, 423–454. https://math.caltech.edu/SimonPapers/R27.pdf
• T. S. Motzkin and E. G. Straus, Maxima for graphs and a new proof of a theorem of Turán, Canad. J. Math. 17 (1965), 533–540. https://doi.org/10.4153/CJM-1965-053-6
• J. L. Lebowitz and O. Penrose, Rigorous treatment of the van der Waals–Maxwell theory of the liquid-vapor transition, J. Math. Phys. 7 (1966), 98–113. https://doi.org/10.1063/1.1704821
• D. Ruelle, Superstable interactions in classical statistical mechanics, Comm. Math. Phys. 18 (1970), 127–159. https://doi.org/10.1007/BF01646091
• D. Ruelle, Existence of a phase transition in a continuous classical system, Phys. Rev. Lett. 27 (1971), 1040–1041. https://doi.org/10.1103/PhysRevLett.27.1040
• A. Gerardi, C. Marchioro, E. Olivieri and E. Presutti, Van der Waals–Maxwell theory, Lebowitz–Penrose limit and superstable interactions, Comm. Math. Phys. 29 (1973), 219–231. https://doi.org/10.1007/BF01645248
• J. L. Lebowitz, A. E. Mazel and E. Presutti, Liquid–vapor phase transitions for systems with finite-range interactions, J. Stat. Phys. 94 (1999), 955–1025. https://doi.org/10.1023/A:1004591218510
• Q. He, I. Jauslin, J. Lebowitz and R. Peled, Liquid-vapor transition in a model of a continuum particle system with finite-range modified Kac pair potential, Comm. Math. Phys. 407 (2026), 240. https://doi.org/10.1007/s00220-026-05735-w
• D. Dereudre and C. Renaud-Chan, First-order phase transition for Gibbs point processes with saturated interactions, arXiv:2602.11078 (2026). https://arxiv.org/abs/2602.11078v1
• R. T. Rockafellar and R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3
• OpenAI, A continuum temperature singularity for a radial pair potential, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-continuum-temperature-singularity-for-a-radial-pair-potential-September-24-2026/paper.pdf
• OpenAI, A radial continuum phase transition with algebraic decay, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-radial-continuum-phase-transition-with-algebraic-decay-September-24-2026/paper.pdf

Motivation: phase transitions for continuum particles

Whether a single species of classical particles in $\mathbb R^3$, interacting only through a stable radial pair potential, can undergo a phase transition is one of the long-standing existence questions of rigorous statistical mechanics; it appears in Simon's list of problems in mathematical physics (Simon 1984). A phase transition is detected as a loss of regularity of the thermodynamic free energy. Lattice models and continuum models with extra structure (several species, many-body terms, hard cores, box-restricted interactions) were handled long ago; ordinary pair potentials finite at every positive separation remained the difficult case.

Timeline

• 1966 — Lebowitz and Penrose give the rigorous van der Waals–Maxwell theory in the Kac (long-range) limit (Lebowitz–Penrose 1966).
• 1970 — Ruelle's superstability framework for classical continuum systems (Ruelle 1970).
• 1971 — Ruelle proves a transition for the two-species Widom–Rowlinson model (Ruelle 1971).
• 1975 — Israel's convex construction gives coexistence for hard-core continuum particles with a spherically symmetric pair perturbation (Israel 1975).
• 1984 — Simon lists the continuum phase-transition problem among fifteen problems in mathematical physics.
• 1998–1999 — Lebowitz, Mazel and Presutti prove a liquid–vapor transition for attractive pair plus repulsive four-body interactions (PRL 1998, J. Stat. Phys. 1999).
• 2025–2026 — He, Jauslin, Lebowitz and Peled: coexistence for a box-modified Kac pair interaction (CMP 2026); Dereudre and Renaud-Chan: low-temperature coexistence for saturated (many-body) interactions (arXiv:2602.11078).
• 2026 — An OpenAI preprint, A continuum temperature singularity for a radial pair potential (OpenAI Math Release, September 24, 2026), claims an admissible radial pair potential in $\mathbb R^3$ whose canonical free energy has a temperature corner at one critical inverse temperature for every density in an open interval. It has not been peer reviewed and the theorem is not formally verified.

Setting

A radial pair potential is $\Phi(x)=\phi(|x|)$ on $\mathbb R^3$ with $\Phi(0)=+\infty$. It is admissible if $\Phi$ is Borel measurable, $\phi$ is finite and locally bounded on $(0,\infty)$, and

1. $\phi(r)\to+\infty$ as $r\downarrow0$;
2. $\phi\le-a<0$ on some interval $[r_1,r_2]$ with $0<r_1<r_2$;
3. $\int_R^\infty r^2|\phi(r)|\,dr<\infty$ for some $R$;
4. (stability) $U_N(x_1,\dots,x_N)=\sum_{i<j}\Phi(x_i-x_j)\ge -BN$ for all $N$ and all configurations.

With $\Lambda_L=[-L/2,L/2]^3$ and free boundary conditions, the canonical partition function is

$$Z_{\Lambda_L,N}(\beta)=\frac1{N!}\int_{\Lambda_L^N}e^{-\beta U_N}\,dx,\qquad Z_{\Lambda_L,0}=1,\quad e^{-\beta\cdot\infty}=0,$$

and the canonical free-energy density at density $\rho>0$ is

$$f(\beta,\rho)=-\frac1\beta\lim_{L\to\infty}L^{-3}\log Z_{\Lambda_L,\lfloor\rho L^3\rfloor}(\beta).$$

In Lean, radialPotential φ takes values in EReal (value ⊤ at the origin), energy is the pair sum, partition φ β L N is the integral above, and HasCanonicalFreeEnergy φ f says $L^{-3}\log Z\to-\beta f(\beta,\rho)$ for all $\beta,\rho>0$.

Formalization targets

Goal: a strict temperature corner throughout a density interval

There exist an admissible $\phi$ with $\phi(r)=o(r^{-3})$ as $r\to\infty$, a free-energy function $f$ realizing the canonical limit for every $\beta>0,\rho>0$, a nonempty open interval $I\subset(0,\infty)$ and one $\beta_c\in(1/2,3/2)$ such that for every $\rho\in I$ the one-sided $\beta$-derivatives exist and

$$D^-_\beta f(\beta_c,\rho)\;>\;D^+_\beta f(\beta_c,\rho).$$

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

Significance

The result itself. The theorem exhibits a genuine one-species pair potential, finite at every positive separation and with all cross-cube interactions retained, whose canonical free energy is not $C^1$ in temperature at a fixed density, with one critical temperature for an entire interval of densities. It does not concern the Lennard–Jones potential, does not identify the coexisting states as liquid/vapor/solid, and does not give a power-law tail $|\phi(r)|\le Cr^{-3-\varepsilon}$; formulations of the historical problem that require such a margin are not resolved by it. A companion preprint (A radial continuum phase transition with algebraic decay) gives a bounded potential with tail $r^{-3-1/32}$.

Formalizing it. The statement is fully explicit about the model, normalization, and boundary conditions, so a formal proof would remove any ambiguity about which version of the problem is solved. It requires thermodynamic limits for superstable continuum systems, convex-analytic facts about pressures, and a Kac/Lebowitz–Penrose comparison with uniform estimates, none of which is currently in Mathlib.

Difficulty

Density coexistence for a grand-canonical system does not by itself produce a temperature corner at a fixed density; one needs two supporting slopes of the pressure with the same density coordinate and different energy coordinates. Classical tools for transitions (Peierls arguments, reflection positivity, Kac limits) either need lattice structure, many-body terms, or a limit in which the potential itself changes. Here a single fixed potential must be built through infinitely many attractions at growing ranges, and the convex supporting-slope information must survive every approximation step while preserving stability and integrable tails.

Formalization scope

• Space is EuclideanSpace ℝ (Fin 3); the potential is EReal-valued with ⊤ at the origin, and the Boltzmann weight is $0$ when the energy is ⊤. Stability is stated in EReal, which also rules out ⊥.
• Free boundary conditions on the closed cube $[-L/2,L/2]^3$, Lebesgue measure without temperature normalization, $1/N!$, and $N=\lfloor\rho L^3\rfloor$ via Nat.floor; the limit is over real $L\to\infty$.
• One-sided derivatives are HasDerivWithinAt on Iic βc and Ici βc, so both are finite real numbers; $f$ is pinned by HasCanonicalFreeEnergy for every $\beta>0,\rho>0$, so it cannot be chosen freely near $\beta_c$.
• $I$ is open, order-connected, nonempty and contained in $(0,\infty)$; $\beta_c$ is independent of $\rho$.
• Needed infrastructure: superstability estimates, existence of canonical and grand-canonical thermodynamic limits, Legendre duality for pressures, the Lebowitz–Penrose limit. These are reusable for the companion mission.

Selected references

• B. Simon, Fifteen problems in mathematical physics, in Perspectives in Mathematics, Birkhäuser, 1984, 423–454. https://math.caltech.edu/SimonPapers/R27.pdf
• J. L. Lebowitz and O. Penrose, Rigorous treatment of the van der Waals–Maxwell theory of the liquid-vapor transition, J. Math. Phys. 7 (1966), 98–113. https://doi.org/10.1063/1.1704821
• D. Ruelle, Superstable interactions in classical statistical mechanics, Comm. Math. Phys. 18 (1970), 127–159. https://doi.org/10.1007/BF01646091
• D. Ruelle, Existence of a phase transition in a continuous classical system, Phys. Rev. Lett. 27 (1971), 1040–1041. https://doi.org/10.1103/PhysRevLett.27.1040
• R. B. Israel, Existence of phase transitions for long-range interactions, Comm. Math. Phys. 43 (1975), 59–68. https://doi.org/10.1007/BF01609141
• J. L. Lebowitz, A. E. Mazel and E. Presutti, Liquid–vapor phase transitions for systems with finite-range interactions, J. Stat. Phys. 94 (1999), 955–1025. https://doi.org/10.1023/A:1004591218510
• Q. He, I. Jauslin, J. Lebowitz and R. Peled, Liquid–vapor transition in a model of a continuum particle system with finite-range modified Kac pair potential, Comm. Math. Phys. 407 (2026), 240. https://doi.org/10.1007/s00220-026-05735-w
• D. Dereudre and C. Renaud-Chan, First-order phase transition for Gibbs point processes with saturated interactions, arXiv:2602.11078 (2026). https://arxiv.org/abs/2602.11078v1
• OpenAI, A radial continuum phase transition with algebraic decay, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-radial-continuum-phase-transition-with-algebraic-decay-September-24-2026/paper.pdf
• OpenAI, A continuum temperature singularity for a radial pair potential, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-continuum-temperature-singularity-for-a-radial-pair-potential-September-24-2026/paper.pdf

Motivation: can a weakly reversible reaction network lose a species or blow up?

Chemical reaction network theory studies the polynomial differential equations that describe concentrations of interacting species under mass-action kinetics, where each reaction proceeds at a rate proportional to the product of the concentrations of its reactants. A central theme is which properties of the dynamics are forced by the structure of the reaction graph alone, independently of the (usually unknown) rate constants. Weak reversibility — every reaction can be undone by some directed path of reactions — is the main structural condition in this theory. Two long-standing conjectures ask whether weak reversibility alone guarantees that no species dies out (persistence) and that no concentration grows without bound (boundedness). These questions matter for systems biology and chemical engineering, where extinction of a species or unbounded growth would contradict the modeled behavior, and they are closely tied to the global attractor conjecture for complex-balanced systems.

Timeline

• 1972 — Horn and Jackson develop the equilibrium and stability theory of complex-balanced mass-action systems (ARMA 1972); Horn (ARMA 1972) and Feinberg (ARMA 1972) give complex-balancing criteria and the deficiency-zero analysis.
• 1987 — Feinberg formulates the expectation that a positive trajectory of a weakly reversible system cannot converge to a boundary point (Chem. Eng. Sci. 1987, Remark 6.1.E).
• 2010 — August and Barahona state the general boundedness and persistence conclusion (IFAC 2010); the source identifies a gap in one step of their proof (p. 2).
• 2011 — Anderson separates the boundedness conjecture from the persistence conjecture and proves boundedness for a single linkage class (J. Math. Chem. 2011); he also proves the global attractor conjecture in the single-linkage case (SIAM J. Appl. Math. 2011).
• 2012–2013 — Pantea proves persistence of bounded trajectories when the stoichiometric subspace has dimension two (SIAM J. Math. Anal. 2012); Craciun, Nazarov and Pantea prove boundedness, persistence and permanence for two-species systems (SIAM J. Appl. Math. 2013).
• 2014 — Gopalkrishnan, Miller and Shiu prove permanence for strongly endotactic systems (SIAM J. Appl. Dyn. Syst. 2014).
• 2019–2020 — Boros proves every positive stoichiometric class of a weakly reversible system contains a positive equilibrium (SIAM J. Math. Anal. 2019); Boros and Hofbauer reprove single-linkage permanence (SIAM J. Appl. Dyn. Syst. 2020).
• 2026 — Craciun's revised toric-differential-inclusion approach gives persistence for bounded trajectories (arXiv:1501.02860v3).
• 2026 — The OpenAI preprint Boundedness and persistence of weakly reversible mass-action systems (OpenAI Math Release, September 25, 2026) claims both conjectures for constant positive rates in every dimension. It has not been peer reviewed and its theorem is not formally verified.

Setting

Fix $d\ge1$ species. A reaction network consists of a finite set of complexes $\mathcal C\subset\mathbb Z_{\ge0}^d$ and a set $\mathcal R$ of reactions $y\to y'$ with $y,y'\in\mathcal C$, $y\neq y'$. It is weakly reversible if for every reaction $y\to y'$ there is a directed path of reactions from $y'$ back to $y$. Given positive rate constants $\kappa_{y\to y'}>0$, the mass-action system is

$$\dot x = f(x)=\sum_{y\to y'\in\mathcal R}\kappa_{y\to y'}\,x^{y}\,(y'-y),\qquad x^y=\prod_{i=1}^d x_i^{y_i}.$$

A positive trajectory is persistent if $\liminf_{t\to\infty}x_i(t)>0$ for every $i$.

In Lean (namespace OAI.Problem326), a ReactionNetwork d has a Finset of complexes in Fin d → ℕ and a Finset of reactions between them with distinct source and target; WeaklyReversible is Relation.TransGen reachability from target back to source; massAction N κ is the vector field above; and IsGlobalForwardSolution N κ x0 x means $x(0)=x_0$ and $x$ has derivative $f(x(t))$ at every $t\ge0$.

Formalization targets

Goal: global existence, boundedness and persistence (Theorem 1.1)

Let $d\ge1$, let the network be weakly reversible and all rates positive. For every $x^0\in\mathbb R_{>0}^d$ the solution with $x(0)=x^0$ exists for all $t\ge0$, and there is $\varepsilon\in(0,1)$, depending on the network, the rates and $x^0$, such that

$$\varepsilon\le x_i(t)\le\varepsilon^{-1}\qquad(t\ge0,\ 1\le i\le d).$$

The goal is published on the platform with status Open.

Significance

The result itself. The theorem proves the boundedness conjecture and the persistence conjecture together, for arbitrary constant positive rates, any number of linkage classes and any number of species; earlier results needed a single linkage class, two species, or a two-dimensional stoichiometric subspace. It applies whether or not the stoichiometric compatibility class is bounded. Combined with complex balance, it yields convergence to the unique positive equilibrium in each class (the global attractor conclusion; Remark 3.5, p. 15). The proof also produces, for each positive initial point, a compact convex forward-invariant polytope in the open orthant (Proposition 3.3, p. 13), which gives a short proof of Boros's existence theorem for positive equilibria (Corollary 3.4, p. 14).

Formalizing it. Statements about reaction networks quantify over all networks and all rates, so they are a natural fit for formal verification; the history includes a published proof with a gap in one step. A machine-checked proof would settle the status of the general theorem independently of that history.

Difficulty

The natural approach is to find a Lyapunov function or an invariant region whose boundary each reaction crosses inward. Individual reactions need not point inward across any fixed face, and near the orthant boundary and at infinity different monomials dominate in different regions, with ties between monomials that an arbitrary choice of face normal can reverse. The argument must control the combined flux across cuts of the reaction graph using the return paths given by weak reversibility, and must do so simultaneously for small and large concentrations; a naive comparison of monomials by total degree fails, as the source's example $2A\rightleftarrows B$ with $(a,b)=(T,T^3)$ shows.

Formalization scope

• Complexes are vectors in Fin d → ℕ, so exponents are nonnegative integers and $f$ is a polynomial vector field on $\mathbb R^d$; the reaction set is a Finset with source ≠ target. Empty reaction sets and isolated complexes are allowed, as in the source.
• Rates are a function on reactions with ∀ e, 0 < κ e; $d>0$ is a hypothesis.
• The conclusion asserts existence of some global forward solution and bounds for every global forward solution from $x^0$ (uniqueness is therefore not assumed). Solutions are functions ℝ → (Fin d → ℝ) with HasDerivAt at every $t\ge0$, including a two-sided derivative at $t=0$.
• The same $\varepsilon$ works for all $t\ge0$ and all species; it may depend on $x^0$. No uniformity over initial points is claimed.
• Needed infrastructure: Picard–Lindelöf for polynomial fields, forward invariance of convex polytopes (Nagumo-type tangency conditions), and graph-cut flux estimates. ODE invariance tools are reusable beyond this mission.

Selected references

• F. Horn and R. Jackson, General mass action kinetics, Arch. Rational Mech. Anal. 47 (1972). https://doi.org/10.1007/BF00251225
• M. Feinberg, Complex balancing in general kinetic systems, Arch. Rational Mech. Anal. 49 (1972). https://doi.org/10.1007/BF00255665
• M. Feinberg, Chemical reaction network structure and the stability of complex isothermal reactors — I, Chem. Eng. Sci. 42 (1987). https://doi.org/10.1016/0009-2509(87)80099-4
• E. August and M. Barahona, Solutions of weakly reversible chemical reaction networks are bounded and persistent, IFAC Proc. Vol. 43 (2010). https://doi.org/10.3182/20100707-3-BE-2012.0018
• D. F. Anderson, Boundedness of trajectories for weakly reversible, single linkage class reaction systems, J. Math. Chem. 49 (2011). https://doi.org/10.1007/s10910-011-9886-4
• C. Pantea, On the persistence and global stability of mass-action systems, SIAM J. Math. Anal. 44 (2012). https://doi.org/10.1137/110840509
• G. Craciun, F. Nazarov and C. Pantea, Persistence and permanence of mass-action and power-law dynamical systems, SIAM J. Appl. Math. 73 (2013). https://doi.org/10.1137/100812355
• M. Gopalkrishnan, E. Miller and A. Shiu, A geometric approach to the global attractor conjecture, SIAM J. Appl. Dyn. Syst. 13 (2014). https://doi.org/10.1137/130928170
• B. Boros, Existence of positive steady states for weakly reversible mass-action systems, SIAM J. Math. Anal. 51 (2019). https://doi.org/10.1137/17M115534X
• G. Craciun, Toric differential inclusions and a proof of the global attractor conjecture, arXiv:1501.02860v3, 2026. https://arxiv.org/abs/1501.02860v3
• OpenAI, Boundedness and persistence of weakly reversible mass-action systems, OpenAI Math Release preprint, September 25, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Boundedness-and-persistence-of-weakly-reversible-mass-action-systems-September-25-2026/paper.pdf

Motivation

A metric space is doubling if every ball can be covered by a bounded number of balls of half the radius. Every subset of a finite-dimensional Euclidean space is doubling, so doubling is a necessary condition for a metric space to embed bi-Lipschitzly into some $\mathbb R^k$. Whether it is also sufficient, for subsets of Hilbert space, is the Lang–Plaut problem. It sits at the meeting point of metric geometry and algorithm design: doubling is a standard notion of "intrinsic dimension" for data, and a positive answer would mean that intrinsically low-dimensional Euclidean data can always be represented in a bounded number of coordinates with bounded distortion.

Timeline

• 1983. Assouad proves that every doubling metric space embeds bi-Lipschitzly into some $\mathbb R^k$ after snowflaking, i.e. after replacing the distance $d$ by $d^\alpha$ with $0<\alpha<1$ (doi:10.24033/bsmf.1997).
• 2001. Lang and Plaut ask whether every doubling subset of Hilbert space admits a bi-Lipschitz embedding into a finite-dimensional Euclidean space (Question 2.4) (doi:10.1023/A:1012093209450).
• 2003. Gupta, Krauthgamer and Lee independently pose the question for algorithmic dimension reduction (doi:10.1109/SFCS.2003.1238226).
• 2012. Naor and Neiman bound the target dimension in Assouad's theorem independently of the snowflake exponent near $1$ (doi:10.4171/RMI/706).
• 2014. Lafforgue and Naor construct, for $p>2$, a doubling subset of $L_p$ with no bi-Lipschitz embedding into any $\mathbb R^k$ (doi:10.1007/s10711-013-9924-4).
• 2015. Bartal, Gottlieb and Neiman obtain obstructions for doubling subsets of $\ell_p$ via Laakso-type configurations (doi:10.1137/140977655); Gottlieb and Krauthgamer embed snowflakes of finite Hilbert subsets with distortion close to one (doi:10.1007/s00454-015-9707-9).
• 2017. Schioppa announces a negative answer for $\ell_2$ and later withdraws the preprint (arXiv:1703.10265).
• 2021. Baudier, Świȩcicki and Swift give an elementary proof of the fixed-set theorem for $\ell_q$, $q>2$ (doi:10.1016/j.jmaa.2021.125407).

The Hilbert case ($p=2$) remained open. The source of this mission, an OpenAI preprint dated September 25, 2026, claims a negative answer.

Setting

A metric space $(X,d)$ is doubling with constant at most $\lambda$ if for every $x\in X$ and $r>0$, the ball of radius $r$ about $x$ is covered by at most $\lambda$ balls of radius $r/2$ with centers in $X$. A map $f:X\to\mathbb R^k$ is a bi-Lipschitz embedding with distortion at most $D$ if some scale $a>0$ satisfies

$$a\,d(x,y)\ \le\ \|f(x)-f(y)\|\ \le\ D\,a\,d(x,y)\qquad(x,y\in X).$$

Real $\ell_2$ is the Hilbert space of square-summable real sequences indexed by $\mathbb N$; subsets carry the induced distance.

Formalization targets

Corollary 6 (milestone)

There is a universal $\Lambda$ such that every infinite-dimensional real Banach space $B$ contains a compact set $K_B$ with doubling constant at most $\Lambda$ that admits no bi-Lipschitz embedding into any finite-dimensional real normed space at any finite distortion.

Goal: Theorem 1

$$\exists\, S\subset\ell_2:\quad S\ \text{is doubling with constant}\ \le 76800,\ \text{and}\ \forall k\ge1,\ S\ \text{admits no bi-Lipschitz embedding into}\ \mathbb R^k.$$

The set is fixed once, independently of $k$ and of the distortion. The Lean statement OAI.DoublingHilbert.main is open on the platform. The constant $76800=300\cdot16^2$ comes from the paper's covering count; any finite universal constant would answer the Lang–Plaut problem, but the Lean goal records the paper's value.

Significance

The theorem answers the Lang–Plaut problem negatively: there is no function of the doubling constant alone that bounds both the dimension and the distortion for doubling subsets of Hilbert space. It extends the Lafforgue–Naor and Bartal–Gottlieb–Neiman obstructions from $p>2$ to the Hilbert case, which is the case of most interest for applications. By Gaussian isometric embedding the same metric space sits in every $L_p[0,1]$, $1\le p<\infty$ (Corollary 5), and by Dvoretzky's theorem a compact version sits in every infinite-dimensional Banach space (Corollary 6). Assouad's theorem shows that any snowflake of the set does embed, so the obstruction is specific to the original distance.

The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. A previous announced proof of this statement (Schioppa, 2017) was withdrawn, which makes an independent formal verification particularly informative.

Difficulty

Doubling gives covering control at every scale, and Assouad's theorem shows that any loss in the exponent of the metric removes the obstruction, so a counterexample must be sharp at the level of exact Lipschitz bounds. The $p>2$ constructions rely on uniform convexity estimates of $L_p$ that degenerate at $p=2$, and Hilbert space has the most symmetric geometry available, so the standard Laakso and diamond-type obstructions do not transfer. The set must also be chosen before the target dimension and distortion, so a single set has to defeat every $k$ and every $D$ simultaneously.

Formalization scope

• The ambient space is RealL2 := lp (fun _ : ℕ => ℝ) 2; $S$ is a Set RealL2 with the subspace metric.
• DoublingAtMost S bound: for each $x\in S$ and $r>0$ there is a Finset of at most bound centers in $S$ such that every $y\in S$ with $d(y,x)<r$ satisfies $d(y,c)<r/2$ for some center (open balls; centers in $S$).
• AdmitsBiLipschitzEmbedding S k: there are $f:S\to$ EuclideanSpace ℝ (Fin k), $a>0$ and $D\ge1$ with the two-sided bound above.
• For Corollary 6, CompactBanach.main quantifies over all complete real normed spaces that are not finite-dimensional and all finite-dimensional real normed targets, with the doubling constant $\Lambda$ chosen before $B$.

A complete development needs Hilbert direct sums, the explicit strip-colored set, covering estimates, a.e. differentiability of Lipschitz maps on open subsets of $\mathbb R^2$ (Rademacher), and a Euclidean packing bound. Rademacher's theorem and packing estimates are reusable well beyond this mission. Contributions formalizing Proposition 2 (the doubling bound) are a natural first step.

Selected references

• OpenAI, A doubling Hilbert subset with no finite-dimensional bi-Lipschitz embedding, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-doubling-Hilbert-subset-with-no-finite-dimensional-bi-Lipschitz-embedding-September-25-2026/main.pdf
• U. Lang, C. Plaut, Bilipschitz embeddings of metric spaces into space forms, Geom. Dedicata, 2001. https://doi.org/10.1023/A:1012093209450
• P. Assouad, Plongements lipschitziens dans $\mathbb R^n$, Bull. Soc. Math. France, 1983. https://doi.org/10.24033/bsmf.1997
• A. Gupta, R. Krauthgamer, J. R. Lee, Bounded geometries, fractals, and low-distortion embeddings, FOCS 2003. https://doi.org/10.1109/SFCS.2003.1238226
• A. Naor, O. Neiman, Assouad's theorem with dimension independent of the snowflaking, Rev. Mat. Iberoam., 2012. https://doi.org/10.4171/RMI/706
• V. Lafforgue, A. Naor, A doubling subset of $L_p$ for $p>2$ that is inherently infinite dimensional, Geom. Dedicata, 2014. https://doi.org/10.1007/s10711-013-9924-4
• Y. Bartal, L.-A. Gottlieb, O. Neiman, On the impossibility of dimension reduction for doubling subsets of $\ell_p$, SIAM J. Discrete Math., 2015. https://doi.org/10.1137/140977655
• F. P. Baudier, K. Świȩcicki, A. Swift, No dimension reduction for doubling subsets of $\ell_q$ when $q>2$ revisited, J. Math. Anal. Appl., 2021. https://doi.org/10.1016/j.jmaa.2021.125407

Motivation

The projection body $\Pi K$ of a convex body $K\subset\mathbb R^n$ packages the areas of all shadows of $K$ into a single convex body: its support function in direction $u$ is the $(n-1)$-dimensional volume of the orthogonal projection of $K$ onto $u^\perp$. The normalized volume $|\Pi K|/|K|^{n-1}$ is invariant under translations and invertible linear maps, so asking for its extremizers is an affine isoperimetric problem. Petty's projection-volume conjecture (Petty, 1971) predicts that this ratio is minimized exactly by ellipsoids. It is related to, but distinct from, Petty's projection inequality for the polar body $\Pi^\circ K$, which is a classical theorem; inequalities in this family underlie affine Sobolev inequalities and isoperimetric inequalities in normed spaces.

This mission asks for a formal proof of the conjecture in every dimension $n\ge4$, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1971 — Petty formulates the conjecture (Isoperimetric problems, Proc. Conf. Convexity and Combinatorial Geometry, Univ. of Oklahoma, 1971).
• 1990 — Lutwak reformulates it as a lower bound for a two-body integral with kernel $|u\cdot v|$ against surface-area measures (Contemp. Math. 113, 1990) and derives lower-degree consequences (Geom. Dedicata 1990).
• 2015–2018 — Saroglou's class-reduction results for the second projection body (Adv. Appl. Math. 2015); Saroglou–Zvavitch local minimality near the ball in $L^\infty$ (JFA 2017); Ivaki's local rigidity for $C^2$ solutions of $\Pi^2K=cK$ (Mathematika 2018).
• 2026 — Mielke-Sulz proves the conjecture for bodies of revolution (arXiv:2609.13517); Chen, Feng, Li, Xi and Xu prove the unrestricted three-dimensional case with ellipsoid equality (preprint, August 2026).
• September 2026 — The OpenAI preprint claims all dimensions $n\ge4$ (Theorem 1.1, p. 1).

Setting

A convex body $K\subset\mathbb R^n$ is a compact convex set with nonempty interior, and $|\cdot|$ denotes $n$-dimensional Lebesgue volume. For a unit vector $u$, let $\operatorname{proj}_{u^\perp}K$ be the orthogonal projection of $K$ onto the hyperplane $u^\perp$ and $\operatorname{vol}_{n-1}$ the Lebesgue measure on that hyperplane. The projection body is

$$\Pi K=\{x\in\mathbb R^n:\ \langle u,x\rangle\le \operatorname{vol}_{n-1}(\operatorname{proj}_{u^\perp}K)\ \text{for every unit }u\},$$

the convex body with support function $h_{\Pi K}(u)=\operatorname{vol}_{n-1}(\operatorname{proj}_{u^\perp}K)$. Write $\kappa_m$ for the volume of the Euclidean unit ball $B_2^m$. An ellipsoid is a set $a+TB_2^n$ with $a\in\mathbb R^n$ and $T$ an invertible linear map. Since $\Pi B_2^n=\kappa_{n-1}B_2^n$, the ball has ratio $\kappa_{n-1}^n\kappa_n^{2-n}$.

Formalization targets

Goal: Theorem 1.1 (p. 1)

For every integer $n\ge4$ and every convex body $K\subset\mathbb R^n$,

$$\frac{|\Pi K|}{|K|^{n-1}}\ \ge\ \kappa_{n-1}^{\,n}\,\kappa_n^{\,2-n},$$

with equality if and only if $K$ is an ellipsoid.

Significance

The result itself. Together with the separately proved three-dimensional case, it settles Petty's conjecture for all $n\ge3$ (in dimension $2$ the ratio is constant up to the standard identification). The preprint derives from it the Lutwak–Petty lower-degree inequalities, a mixed determinant-gradient inequality strengthening the Sobolev–Zhang affine $L^1$ inequality, and the sharp Holmes–Thompson isoperimetric inequality in normed spaces (Corollaries 7.1–7.3, pp. 27–29). Those corollaries for $n=3$ rely on the external three-dimensional theorem.

Formalizing it. The proof uses the first variation of volume, spherical harmonics with explicit cosine and Funk transform multipliers, a strict harmonic estimate for arbitrary norms, a variational representation of support functionals, and Brouwer's fixed-point theorem. Mathlib has Brouwer-type results only in limited forms and has no spherical-harmonic decomposition of $L^2(S^{n-1})$; these would be reusable. No machine-checked proof of any case $n\ge2$ of the conjecture is known.

Difficulty

Previous results are local: they require the body, after a linear change of variables, to be close to the ball, because the harmonic analysis of the projection operator only controls perturbations of the ball. A global argument must handle arbitrary bodies without symmetry or regularity. In the preprint (pp. 2–3) the degree-two spherical harmonic component is not a zero mode of the relevant sign-test operator and has to be removed by choosing affine coordinates; this needs a continuous family of variational minimizers extended to singular matrices and a fixed-point argument (Proposition 5.5, p. 23). Harmonics of degree at least four are controlled by a strict norm estimate valid for every norm (Theorem 4.1, p. 12). The equality case must come out of the same estimates.

Formalization scope

• Space n is EuclideanSpace ℝ (Fin n); IsConvexBody K is compact, convex, nonempty interior; $n\ge4$.
• shadowVolume K u is the measure, in the induced Euclidean volume on the submodule $(\operatorname{span}\{u\})^\perp$, of the image of $K$ under orthogonalProjectionOnto. projectionBody K is the intersection of half-spaces over unit vectors, which has support function shadowVolume K because that function is itself a support function.
• projectionRatio K = volume.real (projectionBody K) / volume.real K ^ (n - 1); for a convex body both volumes are finite and the denominator is positive.
• pettyConstant n = kappa (n-1) ^ n * kappa n ^ (2 - n) with an integer exponent, $\kappa_m$ the volume of the closed unit ball.
• IsEllipsoid K: $K = a + T(\text{closed unit ball})$ for a linear equivalence $T$.
• The goal is the conjunction of the inequality and the iff equality characterization; neither part is vacuous for $n\ge4$.

Selected references

• OpenAI, Petty's projection-volume conjecture in dimensions at least four, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Pettys-projection-volume-conjecture-in-dimensions-at-least-four-September-24-2026/paper.pdf
• C. M. Petty, Isoperimetric problems, Proc. Conf. Convexity and Combinatorial Geometry, Univ. of Oklahoma, 1971, 26–41.
• E. Lutwak, On a conjectured projection inequality of Petty, Contemp. Math. 113 (1990), 171–182.
• E. Lutwak, On quermassintegrals of mixed projection bodies, Geom. Dedicata 33 (1990), 51–58. https://doi.org/10.1007/BF00147600
• C. Saroglou, A. Zvavitch, Iterations of the projection body operator and a remark on Petty's conjectured projection inequality, J. Funct. Anal. 272 (2017), 613–630. https://doi.org/10.1016/j.jfa.2016.08.015
• M. N. Ivaki, A local uniqueness theorem for minimizers of Petty's conjectured projection inequality, Mathematika 64 (2018), 1–19. https://doi.org/10.1112/S0025579317000444
• S. Chen, Y. Feng, Y. Li, D. Xi, L. Xu, Petty's conjectured projection inequality in dimension three, preprint (2026). https://archive.ymsc.tsinghua.edu.cn/pacm_download/741/12780-pettyinequality.pdf
• F. Mielke-Sulz, The Petty conjecture for convex bodies of revolution, arXiv:2609.13517 (2026). https://arxiv.org/abs/2609.13517v1
• G. Zhang, The affine Sobolev inequality, J. Differential Geom. 53 (1999), 183–202.
• R. J. Gardner, The Brunn–Minkowski inequality, Bull. AMS 39 (2002), 355–405. https://doi.org/10.1090/S0273-0979-02-00941-2

Motivation

The Riemann zeta function $\zeta(s) = \sum_{n\ge1} n^{-s}$ ($\Re s > 1$), continued meromorphically to $\mathbb{C}$, encodes the distribution of primes through its zeros. Riemann (1859) conjectured that all nontrivial zeros lie on $\Re s = 1/2$. Hadamard and de la Vallée Poussin (1896) proved there are no zeros on $\Re s = 1$, which gives the prime number theorem, but all classical zero-free regions shrink toward the line $\Re s = 1$ as the height grows. The quasi-Riemann hypothesis asks for a fixed $\sigma_0 < 1$ such that $\zeta(s) \ne 0$ for all $\Re s > \sigma_0$: one zero-free gap valid at every height. The uniform version for all Dirichlet $L$-functions is a standard formulation in analytic number theory (e.g. Friedlander–Goldston).

This preprint claims a proof with $\sigma_0 = 7/8$, for $\zeta$, for all Dirichlet $L$-functions, and for all finite-order Hecke $L$-functions over $\mathbb{Q}(\sqrt{-3})$.

Background

• 1837. Dirichlet introduces character $L$-series to prove infinitude of primes in arithmetic progressions.
• 1859. Riemann relates zeros of $\zeta$ to primes and formulates the Riemann hypothesis.
• 1896. Hadamard and de la Vallée Poussin prove $\zeta(s) \ne 0$ on $\Re s = 1$.
• 1918. Hecke develops $L$-functions of characters over number fields.
• 1969, 1977. Kubota's metaplectic theory and Patterson's cubic theta series supply the automorphic objects used here.
• 2000–2014. Heath-Brown's cubic large sieve; Goldmakher–Louvel's quadratic large sieve over number fields; Blomer–Goldmakher–Louvel's higher-order recursion.
• 2026. Guth and Maynard improve zero-density bounds for $\zeta$ (which bound the number of zeros but do not exclude them). The OpenAI preprint The Quasi-Riemann Hypothesis (dated September 30, 2026) claims the zero-free half-plane $\Re s > 7/8$. It has not been peer reviewed or independently verified; the Lean goal is open on this platform. The Riemann hypothesis itself is not claimed.

Setting

For a Dirichlet character $\chi$ modulo $q$ (extended by zero on non-units), $L(s,\chi) = \sum_{n \ge 1}\chi(n) n^{-s}$ for $\Re s > 1$, continued meromorphically; the character modulo $1$ gives $\zeta$. For $F = \mathbb{Q}(\sqrt{-3})$ with ring of integers $\mathcal{O}$, a finite-order Hecke character modulo a nonzero ideal $\mathfrak{f}$ is a character of the ray class group modulo $\mathfrak f$, extended by zero, and $L_F(s,\eta) = \sum_{\mathfrak a \ne 0}\eta(\mathfrak a)(N\mathfrak a)^{-s}$. Principal characters have a pole at $s = 1$.

In Lean, $\zeta$ is Mathlib's riemannZeta, Dirichlet $L$-functions are Mathlib's DirichletCharacter.LFunction, and the Hecke family is OAI.SevenEighths.HeckeFamily.LFunction: a Character is a multiplicative character of $\mathcal O/\mathfrak m$ trivial on units (for this class-number-one field these are exactly the ray class characters), and its $L$-function is a lattice sum over $\mathcal{O} = \mathbb{Z}[\omega]$ divided by the $6$ units, continued through a theta-type functional equation pair.

Formalization targets

Goal: Theorem 1.1 for $\zeta$ (quasi-Riemann hypothesis)

$$\Re s > 7/8 \implies \zeta(s) \ne 0 .$$

Milestone: Theorem 1.1 for Dirichlet $L$-functions

For every Dirichlet character $\chi$ modulo $q \ge 1$ and every $s$ with $\Re s > 7/8$, $L(s,\chi) \ne 0$, except at the pole $s = 1$ of a principal character.

Milestone: Theorem 1.1 for Hecke $L$-functions over $\mathbb{Q}(\sqrt{-3})$

For every finite-order Hecke character $\eta$ of $F = \mathbb{Q}(\sqrt{-3})$ and every $s$ with $\Re s > 7/8$, $L_F(s,\eta) \ne 0$, except at the pole $s = 1$ of a principal character.

The three statements are ordered from weakest to strongest; the proof in the preprint goes through the whole Hecke family even for $\zeta$, because Poisson summation introduces Hecke twists of the target.

Significance

The result. A fixed zero-free half-plane would give power-saving error terms in the prime number theorem and in prime counts in arithmetic progressions, uniformly in the modulus, and would exclude Siegel zeros beyond $7/8$. The preprint derives (Corollary 1.2) that the least quadratic nonresidue modulo $p$ is $O((\log p)^A)$, proving Vinogradov's conjecture, and a deterministic polynomial-time square-root algorithm modulo primes.

Formalizing it. This is a claimed resolution of a long-standing question in an unrefereed preprint; a machine-checked proof would be strong independent verification. The goal uses only Mathlib definitions, so it cannot be weakened by a definitional choice. The Hecke milestone uses a custom $L$-function definition that must also be checked against the source.

Difficulty

Classical zero-free regions come from positivity arguments (the $3 + 4\cos\theta + \cos 2\theta$ inequality) that give regions of width $c/\log(|t|+q)$ shrinking to the line $\Re s = 1$; they cannot produce a fixed half-plane. Zero-density estimates bound the number of zeros to the right of a line but do not exclude every zero. The preprint instead continues reciprocals $1/L$ across a uniform distance by comparing two exact representations of a completed cubic-theta sum, with exponent margins independent of the target character.

Formalization scope

• The goal: ∀ s : ℂ, 7/8 < s.re → riemannZeta s ≠ 0. Mathlib assigns $\zeta(1)$ a finite nonzero value, so no pole exclusion is needed.
• The Dirichlet milestone excludes exactly the case χ = 1 ∧ s = 1, where Mathlib's value is a junk value at the pole.
• The Hecke milestone excludes χ.residue = 1 ∧ s = 1.
• The boundary $\Re s = 7/8$ is not included.

The goal is not vacuous and cannot be satisfied by a convention: it is a statement about Mathlib's riemannZeta on an open half-plane.

Needed infrastructure: Hecke $L$-functions over imaginary quadratic fields and their functional equations, cubic and sextic residue symbols, Patterson's cubic theta coefficients, large sieve inequalities over $\mathbb{Z}[\omega]$, and Mellin inversion. Contributions toward the $11/12$ half-plane (Theorem 3.1) as an intermediate target are welcome.

Selected references

• OpenAI, The Quasi-Riemann Hypothesis, OpenAI Math Release preprint, September 30, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Quasi-Riemann-Hypothesis-September-30-2026/paper.pdf
• B. Riemann, Ueber die Anzahl der Primzahlen unter einer gegebenen Grösse, Monatsber. Königl. Preuss. Akad. Wiss. Berlin (1859).
• J. Hadamard, Sur la distribution des zéros de la fonction ζ(s) et ses conséquences arithmétiques, Bull. Soc. Math. France 24 (1896).
• E. Hecke, Eine neue Art von Zetafunktionen und ihre Beziehungen zur Verteilung der Primzahlen, Math. Z. 1 (1918).
• J. B. Friedlander, D. A. Goldston, Sums of three or more primes, Trans. Amer. Math. Soc. 349 (1997).
• K. Billington, M. Cheng, J. Schettler, A. I. Suriajaya, The average number of Goldbach representations and zero-free regions of the Riemann zeta-function, Int. J. Number Theory 21 (2025).
• S. J. Patterson, A cubic analogue of the theta series, J. Reine Angew. Math. 296 (1977).
• D. R. Heath-Brown, Kummer's conjecture for cubic Gauss sums, Israel J. Math. 120 (2000). https://doi.org/10.1007/s11856-000-1273-y
• V. Blomer, L. Goldmakher, B. Louvel, L-functions with n-th-order twists, IMRN 2014.
• L. Guth, J. Maynard, New large value estimates for Dirichlet polynomials, Ann. of Math. 203 (2026). https://doi.org/10.4007/annals.2026.203.2.6
• T. Tao, The Elliott–Halberstam conjecture implies the Vinogradov least quadratic nonresidue conjecture, Algebra Number Theory 9 (2015).

Motivation

A G/GI/N queue has $N$ identical servers, a general arrival process, a first-come-first-served waiting room and i.i.d. service times with a general distribution $F$ of mean $1$. In the Halfin–Whitt regime the number of servers grows while the traffic intensity $\rho^N$ approaches $1$ at rate $\sqrt N(1-\rho^N)\to\beta\in\mathbb R$; this is the standard asymptotic model for large call centers, where a positive fraction of customers wait but waiting times are short. Halfin and Whitt (Oper. Res. 1981) obtained a diffusion limit for exponential service times. Reed (arXiv:0912.2837, Ann. Appl. Probab. 2009) proved the corresponding limit for general service times: the centred and scaled queue length converges (Theorem 5.1) to the solution of a nonlinear stochastic convolution equation, (5.33) below.

Equation (5.33) is written in terms of an infinite-server limit, and it is not evident from its form that it reduces to the Halfin–Whitt diffusion when service is exponential. Section 5.5 of the paper gives a second representation, Corollary 5.2, in which the convolution against $F$ is replaced by a convolution against the renewal function of $F$. With exponential service the renewal function is $M(t)=t$, and the representation becomes the Halfin–Whitt diffusion. This mission formalizes Corollary 5.2 and the renewal-theoretic steps of its proof.

Timeline. Halfin–Whitt (1981): exponential service, diffusion limit. Reed (2009): general service with finite mean; Corollary 5.2 links the general limit back to 1981. Karlin–Taylor (1975) and Ross (1983): the renewal-type equation and the renewal equation that the proof cites.

Setting

Let $\mu$ be a probability measure on $[0,\infty)$ with mean $\int x\,d\mu(x)=1$ (the service-time law), $F(t)=\mu((-\infty,t])$ its distribution function and $G=1-F$ its tail. The equilibrium distribution is

$$F_e(x)=\int_0^x G(u)\,du,\qquad x\ge0.\tag{5.4}$$

Let $\mu^{*n}$ be the $n$-fold convolution of $\mu$ (the law of the $n$th renewal epoch $S_n$). The renewal measure is $dM=\sum_{n\ge1}\mu^{*n}$ and the renewal function is $M(t)=\sum_{n\ge1}F^{*n}(t)$, the expected number of renewals by time $t$.

A path $x:\mathbb R\to\mathbb R$ is càdlàg on $[0,\infty)$ if it is right continuous at every $t\ge0$ with finite left limits at every $t>0$; only its values on $[0,\infty)$ matter. Fix a càdlàg driving path $\zeta$ (in the paper $\tilde\zeta=\tilde M_Q+\tilde Q_I$, (5.40)) and $\beta\in\mathbb R$. Write $y^+=\max(y,0)$ and $y^-=\min(y,0)\le0$. The two equations are

$$q(t)=\zeta(t)-\beta F_e(t)+\int_0^t q^+(t-s)\,dF(s),\qquad t\ge0,\tag{5.33}$$ $$q(t)=\zeta(t)+\int_0^t\zeta(t-u)\,dM(u)-\beta t-\int_0^t q^-(t-u)\,dM(u),\qquad t\ge0.\tag{5.41}$$

All Stieltjes integrals are over the closed interval $[0,t]$.

Formalization targets

Goal: Corollary 5.2 (p. 29)

For every service law $\mu$, every càdlàg $\zeta$ and every $\beta$:

$$\forall q\ \text{càdlàg}:\quad q\ \text{solves (5.33)}\iff q\ \text{solves (5.41)},$$

and (5.41) has a càdlàg solution that is unique on $[0,\infty)$ among càdlàg paths.

Milestones, in proof order

1. (5.39): $M$ is finite, solves $M(t)=F(t)+\int_0^tM(t-u)\,dF(u)$, and is its unique locally bounded measurable solution.
2. (5.42)–(5.43): for locally bounded measurable $H$, $r=H+\int_0^tH(t-u)\,dM(u)$ is the unique locally bounded solution of $r(t)=H(t)+\int_0^tr(t-u)\,dF(u)$.
3. The identity $F_e(t)+\int_0^tF_e(t-s)\,dM(s)=t$ for $t\ge0$ (p. 30).
4. (5.44): every càdlàg solution of (5.33) satisfies (5.41) with $-\beta t$ replaced by $-\beta\bigl(F_e(t)+\int_0^tF_e(t-s)\,dM(s)\bigr)$.
5. (5.46) (further): for exponential service of rate $1$, $M(t)=t$ and (5.41) becomes $q(t)=\zeta(t)+\int_0^t\zeta(s)\,ds-\beta t-\int_0^tq^-(s)\,ds$.

Significance

The result. Corollary 5.2 expresses the many-server diffusion limit as an equation that is linear in the driving process $\zeta$ and whose only nonlinearity is the idle-server term $\int_0^tq^-(t-u)\,dM(u)$. This is how the paper verifies that its general-service limit agrees with Halfin and Whitt's for exponential service, and the paper's sequel interprets the integral term as the limiting idle time of the servers. Uniqueness in (5.41) also yields the paper's remark that $\tilde Q^N\Rightarrow\tilde Q_M$, the solution of (5.41).

The formalization. The result is proved in the paper, but only partly written: the printed proof shows that the solution of (5.33) satisfies (5.41), while the converse and the uniqueness are asserted. The mission states both. It also produces, independently of queueing, the renewal measure of a law on $[0,\infty)$ with possible atoms, its finiteness on bounded sets, the renewal equation and the solution of renewal-type equations, and the identity $F_e+F_e*dM=t$; none of these is in Mathlib or published on the platform. To our knowledge nothing in this mission has a machine-checked proof.

Difficulty

The forward direction is formal once (5.42)–(5.43) is available, but (5.42)–(5.43) itself needs the renewal measure to be finite on bounded intervals when $F$ may have an atom at $0$, and the uniqueness half needs an argument that does not assume the kernel has mass below one on any window starting at $0$. The converse direction, (5.41) $\Rightarrow$ (5.33), cannot be read off the printed proof, because (5.41) is not an equation of renewal type in $q$. The uniqueness of (5.41) is not a contraction argument either: the atom of $dM$ at $0$ has mass $F(0)/(1-F(0))$, which may exceed $1$, so a naive Picard estimate on $[0,\delta]$ fails.

Formalization scope

• Paths are functions $\mathbb R\to\mathbb R$; every equation is asserted for $t\ge0$ and every uniqueness is equality on $[0,\infty)$. Values at negative times are never read.
• The service law is a probability measure $\mu$ on $\mathbb R$ with $\mu((-\infty,0))=0$, integrable identity and mean $1$. The paper places "no additional restrictions on $F$ beyond a first moment".
• The renewal measure is defined as $\sum_{n\ge1}\mu^{*n}$ (Mathlib's additive convolution of measures), not through an i.i.d. sequence; the paper's "expected number of renewals" equals it by Tonelli.
• Stieltjes integrals are Lebesgue integrals over the closed $[0,t]$, so atoms at $0$ of $dF$ and $dM$ are included. $q^-$ is $\min(q,0)$, not Mathlib's negPart.
• Explicit readings: "unique strong solution" is existence and uniqueness among càdlàg paths, pathwise for each fixed $\zeta$. The paper's random statement follows by applying it to each sample path, which lies in $D[0,\infty)$ almost surely (p. 30). "Locally bounded" is bounded on every $[0,T]$, with measurability added for the functions in (5.39) and (5.42).
• Corrected slip: (5.42) prints $\int_0^tr(t)\,dF(t-u)$; the stated equation is $\int_0^tr(t-u)\,dF(u)$. Milestone (5.42)–(5.43) assumes $F$ carried by $[0,\infty)$ with $F(0)<1$, under which the cited result holds.
• Ruled out: the solution of (5.33) is not assumed to exist (it exists by the paper's Proposition 3.1 with $a=0$, $B=F$, which the solver must supply). $M$ is the renewal measure of the same $F$, never an arbitrary measure assumed to satisfy (5.39). Uniqueness is among càdlàg paths on $[0,\infty)$, so no non-measurable path makes an integral vanish.
• Not in the mission: Theorems 4.1 and 5.1 (weak convergence in the Skorohod space), whose limit this corollary rewrites, and the Brownian-motion claim after (5.46).
• Related platform items, credited but not the same object: BellmanDP.Inventory.renewal_equation_exists_unique (a renewal equation with a density kernel of mass below $1$); ChenWhitt93.Reflection.Basic (càdlàg paths on $[0,T]$). Reusable output: the renewal measure, (5.39) and (5.42)–(5.43) serve any renewal-theoretic development. Alternative proofs of the converse and of uniqueness are welcome.

Selected references

• J. Reed, The G/GI/N queue in the Halfin–Whitt regime, Ann. Appl. Probab. 19(6), 2009, 2211–2269. https://arxiv.org/abs/0912.2837 (v1), https://doi.org/10.1214/09-AAP609
• S. Halfin and W. Whitt, Heavy-traffic limits for queues with many exponential servers, Oper. Res. 29(3), 1981, 567–588. https://doi.org/10.1287/opre.29.3.567
• S. Karlin and H. M. Taylor, A First Course in Stochastic Processes, 2nd ed., Academic Press, 1975 (reference [11] of the paper).
• S. M. Ross, Stochastic Processes, Wiley, 1983 (reference [19] of the paper, Exercise 3.4).

Motivation

Weighted voting models assign a coalition a win when its combined vote reaches a quota. The Shapley value measures a player's contribution by averaging the change it makes when added to every possible predecessor coalition. This is straightforward to define for a finite list of voters, but a voting body may contain a few major holders and a very large population of individually small holders. A calculation made for a finite approximation should then have a stable meaning as the small holdings are divided more finely. Milnor and Shapley's oceanic game gives that question a precise form and asks whether its major-player values agree with the limits of finite weighted majority games. Milnor and Shapley, RAND RM-2649 (1961).

The question matters whenever a finite voting model is used to represent a diffuse electorate or ownership base. Without a continuity result, the measured power of a major voter could depend on how an otherwise identical mass of minor votes was artificially split. The memo's Theorem 1 establishes the required stability under an explicit small-weight condition. The result is a known theorem from the 1961 memorandum; the task here is its Lean formalization, including the mathematical objects that make its statement meaningful.

Setting

Fix a finite set $M=\{1,\ldots,m\}$ of major players, with nonnegative weights $w_i$. The ocean is a continuum of individually insignificant voters represented by the unit interval $I=[0,1]$, with total weight $\alpha>0$. A coalition's vote is its major-player weight plus $\alpha$ times the Lebesgue measure of its oceanic part. It wins when that vote reaches a quota $c\ge0$. The formal development uses Fin m for $M$ and real weights; the underlying voting rule is the one in §2 of the memorandum. Milnor and Shapley, §2.

To assign a value to a major player, insert each major player independently and uniformly into the ordered ocean. A position vector $x=(x_1,\ldots,x_m)$ lies in the cube $I^m$. Write $P(t)=\{j\in M:x_j<t\}$ and $w(S)=\sum_{j\in S}w_j$. Major player $i$ is pivotal when the predecessor weight is below the quota and adding $i$ reaches it, in the memo's weak-boundary form

$$w(P(x_i))+\alpha x_i\le c\le w(P(x_i))+w_i+\alpha x_i.$$

The oceanic major-player value $\phi_i$ is the probability of this event. Since the insertion positions are uniform, it is also the $m$-dimensional Lebesgue volume of the corresponding set $A_i\subseteq I^m$. Equalities at boundary positions have zero volume. Milnor and Shapley, (2.3)–(2.4), pp. 4–5.

At stage $\ell$, the finite approximation has the same $m$ major players, followed by $n_\ell$ minor players with nonnegative weights $a_{j,\ell}$. Its quota and major weights are $c_\ell$ and $w_{i,\ell}$. A coalition has value one if its weight is at least $c_\ell$, and zero otherwise. The finite-game value $\phi_{i,\ell}$ is the Shapley value of that coalition function. The published Shapley-value definition is reused for this general finite-game object; only the quota game and its oceanic limit are defined for this mission. Milnor and Shapley, Appendix (A.1), (A.4).

Formalization targets

Theorem 1: continuity of major-player values

The principal target says that if quotas and major weights converge, the total minor weight tends to $\alpha$, and every minor weight becomes small, then each major-player value converges:

$$c_\ell\to c,\quad w_{i,\ell}\to w_i,\quad \sum_j a_{j,\ell}\to\alpha>0,\quad \max_j a_{j,\ell}\to0 \quad\Longrightarrow\quad \phi_{i,\ell}\to\phi_i.$$

This is Theorem 1, equations (3.1)–(3.2), of the memorandum. Its conclusion refers to the pivotal-probability definition of $\phi_i$ above. Milnor and Shapley, Theorem 1, p. 6.

Supporting statements

The milestone list follows three statements present in the source: equation (3.4) partitions $A_i$ by the predecessor set $S$; equations (3.5)–(3.6) give the volume of each part as a one-variable integral with clamped endpoints; and Appendix (A.1)–(A.3) states the finite-game limit as a sum of those integrals. Their shared expression is

$$L_i(c,w,\alpha)=\sum_{S\subseteq M\setminus\{i\}}\int_{[0,1]\cap[(c-w(S)-w_i)/\alpha,(c-w(S))/\alpha]} t^{|S|}(1-t)^{m-|S|-1}\,dt.$$

The appendix's limit statement concerns $L_i$; Theorem 1 concerns $\phi_i$. Both are separate targets in the formalization. Milnor and Shapley, §3 and Appendix.

Significance

The theorem makes the major-player value independent of a particular fine division of the minor vote, provided the total minor weight and the other parameters converge as stated. The same oceanic game can therefore stand for many finite approximating sequences. The integral expression also gives a precise comparison point between finite Shapley values and the geometric definition by pivotal volume. Milnor and Shapley, §1 and Theorem 1.

The mathematical result is proved in the cited memorandum, and its appendix recapitulates a limit theorem from the preceding work in the series. The formalization work is to state and prove these known claims over Lean's finite index types, Lebesgue measure, integrals, and limits. Reusable components include the quota-game characteristic function and the interface between a finite Shapley value and a changing number of minor players. The mission does not claim that the historical theorem is open, nor that these target statements already have machine-checked proofs.

Difficulty

The number of minor players changes with $\ell$, so the finite Shapley sum does not have a fixed set of coalitions. Merely taking a limit term by term in that sum does not justify its limit: the number and weights of the terms also change. The condition that the largest minor weight tends to zero controls a triangular family of games, while the oceanic definition is a measure of a geometric pivotal event. Matching the two descriptions requires care at the quota boundaries and at intervals that may be empty. These are the central issues represented by the appendix milestone and by equations (3.4)–(3.6). Milnor and Shapley, §3 and Appendix.

Formalization scope

The Lean model uses Fin m for major players and Fin (n l) for minor players at stage $l$, concatenated with majors first. It uses a real-valued quota characteristic function, the published finite Shapley-value definition, and product Lebesgue volume on the cube $[0,1]^m$ for uniform insertion positions. The predecessor relation is strict, $x_j<x_i$, exactly as in §2; the complementary cell relation is weak. The pivotal inequalities follow (2.4), and the oceanic value is defined from their volume. Defining it as $L_i$ would make the comparison demanded by Theorem 1 empty, so that equality remains a theorem-level obligation.

The source defines oceanic games with $c\ge0$, $w_i\ge0$, and $\alpha>0$. The finite approximants are read as weighted majority games with nonnegative weights; that condition is explicit in Lean. No sign condition is imposed on the stage quotas $c_\ell$, since (3.2) states none (only the limit satisfies $c\ge0$). The statement does not impose the footnote's upper bound $c\le w(M)+\alpha$ because Theorem 1 only concerns major-player values, which are zero in a null game. An empty minor list is permitted at an early stage. Rather than taking the maximum of an empty list, Lean says that for each $\varepsilon>0$, all minor weights are eventually at most $\varepsilon$; with nonnegative weights this is the paper's vanishing-maximum condition. A positive limiting ocean weight also excludes an eventually empty minor population.

The integral in (A.3) is a set integral over the stated intersection of closed intervals, so an empty intersection contributes zero. For (3.5), the endpoints are clamped to $[0,1]$. The condition $S\subseteq M\setminus\{i\}$ ensures $m-|S|-1$ is nonnegative before it is represented as a natural-number exponent. Contributions that strengthen the measure-theoretic partition, the cell-volume computation, or the varying-population finite limit are within scope; a proof may use other intermediate lemmas while keeping the sourced target statements unchanged.

Selected references

• John W. Milnor and Lloyd S. Shapley, Values of Large Games, II: Oceanic Games, RAND Research Memorandum RM-2649, 1961. RAND publication page.
• Lloyd S. Shapley and Norman Shapiro, Values of Large Games, I: A Limit Theorem, RAND Research Memorandum RM-2648, 1960. RAND publication page.

Motivation

A recurring task in martingale theory is to compare a sum of nonnegative random variables $z_1, z_2, \dots$ with the sum of their predictable projections $E(z_k \mid \mathcal A_{k-1})$: the conditional expectation of each term given the information available one step earlier. Such comparisons are the step that turns a statement about the conditional square function $s(f)$ of a martingale into a statement about the martingale itself, and they recur in the proofs of the Burkholder–Davis–Gundy inequalities and of their conditional variants.

In his 1971 Wald Memorial Lectures, published as Distribution Function Inequalities for Martingales (Burkholder 1973), D. L. Burkholder proves two such comparisons for a function $\Phi$ applied to the sums. For convex $\Phi$ of moderate growth, the sum of predictable projections is controlled by the sum itself, up to a constant (Lemma 16.1, the "convexity lemma", §16). For concave $\Phi$, §20 proves the reverse comparison, with the explicit constant $2$. This mission is the concave case, Theorem 20.1.

The same section derives Theorem 20.2 from it: for a martingale $f$ and concave $\Phi$, $E\Phi((f^*)^2) \le 5\,E\Phi(s^2(f))$. For the concave powers $\Phi(\lambda) = \lambda^p$, $0 < p \le 1$, that bound had been proved by another method in Burkholder, Davis and Gundy 1972. Comparisons of the same kind between an increasing process and its compensator were later systematized as the Lenglart domination principle (Lenglart 1977).

Setting

Let $(\Omega, \mathcal A, P)$ be a probability space and $\mathcal A_0 \subseteq \mathcal A_1 \subseteq \cdots$ a non-decreasing sequence of sub-$\sigma$-fields of $\mathcal A$. In Lean this is a probability measure P together with a filtration ℱ : Filtration ℕ mΩ, ℱ k $= \mathcal A_k$.

Let $z_1, z_2, \dots$ be nonnegative measurable functions on $(\Omega, \mathcal A)$, with values in $[0, \infty]$. They need not be integrable, and they need not be adapted: $z_k$ is only $\mathcal A$-measurable. For a nonnegative function the conditional expectation $E(z_k \mid \mathcal A_{k-1})$ always exists as an $\mathcal A_{k-1}$-measurable function with values in $[0, \infty]$, determined up to null sets by $\int_A E(z_k \mid \mathcal A_{k-1})\,dP = \int_A z_k\,dP$ for $A \in \mathcal A_{k-1}$. Put

$$Z = \sum_{k=1}^\infty z_k, \qquad W = \sum_{k=1}^\infty E(z_k \mid \mathcal A_{k-1}),$$

and, for $0 \le n \le \infty$, the partial sums $Z_n$, $W_n$ over $1 \le k \le n$.

A function $\Phi : [0, \infty] \to [0, \infty]$ is concave as above in the paper's sense if it is non-decreasing and continuous on $[0, \infty]$, $\Phi(0) = 0$, it satisfies the growth condition $\Phi(2\lambda) \le c\,\Phi(\lambda)$ for $\lambda > 0$, and it is concave on $[0, \infty)$. Concavity alone already gives $\Phi(2\lambda) \le 2\Phi(\lambda)$. Examples: $\Phi(\lambda) = \lambda^p$ for $0 < p \le 1$, $\Phi(\lambda) = \lambda \wedge a$, $\Phi(\lambda) = \log(1 + \lambda)$.

For a martingale $f = (f_1, f_2, \dots)$ with differences $d_k = f_k - f_{k-1}$ ($f_0 = 0$), the maximal function is $f^* = \sup_n |f_n|$ and the conditional square function is $s(f) = \bigl[\sum_{k=1}^\infty E(d_k^2 \mid \mathcal A_{k-1})\bigr]^{1/2}$.

Formalization targets

Goal: Theorem 20.1 (p. 38)

$$E\Phi\Bigl(\sum_{k=1}^\infty z_k\Bigr) \le 2\,E\Phi\Bigl(\sum_{k=1}^\infty E(z_k \mid \mathcal A_{k-1})\Bigr)$$

for every $\Phi$ concave as above and all nonnegative measurable $z_1, z_2, \dots$. The constant $2$ is universal: it does not depend on $\Phi$, on the growth constant $c$, on the probability space or on the $z_k$.

Milestones

1. (§20, proof of Theorem 20.1.) For $\tau = \inf\{n \ge 0 : W_{n+1} > \lambda\}$: $EZ_\tau = EW_\tau \le E(W \wedge \lambda)$ and $E[\lambda I(\tau < \infty)] = \lambda P(W > \lambda) \le E(W \wedge \lambda)$.
2. (20.2) The truncated inequality

$$E(Z \wedge \lambda) \le 2\,E(W \wedge \lambda), \qquad \lambda > 0.$$

3. (§20, proof of Theorem 20.1.) Inequality (20.2) implies (20.1). This is stated for arbitrary measurable $[0, \infty]$-valued $Z$ and $W$, since the paper's argument uses nothing about $Z$ and $W$ beyond (20.2).

Further result: Theorem 20.2 (p. 39)

For a martingale $f$ and $\Phi$ concave as above,

$$E\Phi\bigl((f^*)^2\bigr) \le 5\,E\Phi\bigl(s^2(f)\bigr).$$

It is posed as a separate theorem and is not a milestone of the goal.

Significance

Theorem 20.1 holds without any integrability and without adaptedness, so it applies to arbitrary nonnegative sequences. With $z_k = d_k^2$ it compares the square function $S^2(f) = \sum d_k^2$ of a martingale with $s^2(f)$: for concave $\Phi$, $E\Phi(S^2(f)) \le 2E\Phi(s^2(f))$. Together with the Burkholder–Davis–Gundy comparison of $S(f)$ and $f^*$, this is one route from the conditional square function to the maximal function in the range of exponents $p \le 2$, where the convex methods of the rest of the paper do not apply. Theorem 20.2 is the result of this kind that the paper states.

The paper proves Theorem 20.1 in about half a page. As far as is known, neither Theorem 20.1 nor Theorem 20.2 has been formalized in any proof assistant. Mathlib provides the $[0, \infty]$-valued conditional expectation (condLExp), filtrations, stopping times and Lebesgue integrals of extended nonnegative functions. It has no comparison theorem of this type between a sum and its predictable projections. A formal proof would therefore add a new, reusable tool to Mathlib's discrete-time martingale library, one that an eventual formal Lenglart inequality or conditional BDG inequality would need.

Difficulty

The obvious first idea is Jensen's inequality for conditional expectations. For concave $\Phi$ it gives $E(\Phi(z_k) \mid \mathcal A_{k-1}) \le \Phi(E(z_k \mid \mathcal A_{k-1}))$ term by term, but $\Phi$ of a sum is not the sum of the $\Phi$'s, and summing the termwise bounds loses the comparison. Another first idea, comparing $EZ$ and $EW$ (which are equal by the tower property), handles only linear $\Phi$, and both sides may be infinite.

The content lies in two places. The first is the truncated inequality for $\Phi(t) = t \wedge \lambda$, where neither $Z$ nor $W$ is integrable in general and the comparison must hold level by level. The second is the passage from the truncated family to an arbitrary concave $\Phi$. It needs a representation of concave $\Phi$ through the truncations $t \wedge \lambda$, including the cases $t = 0$ and $t = \infty$ and a possibly infinite right derivative at $0$ (as for $\lambda^p$). Both steps must be carried out in $[0, \infty]$ arithmetic.

Formalization scope

• Values in $[0, \infty]$. $z_k$, the sums $Z$, $W$, $\Phi$ and all expectations are ℝ≥0∞-valued; expectations are lower Lebesgue integrals ∫⁻. The conditional expectation is Mathlib's condLExp (notation P⁻[z | ℱ k]), never the Bochner P[z | ℱ k]. The Bochner version is $0$ on non-integrable functions and would make the goal false (take $W = 0$).
• Indexing. z (k+1) is $z_{k+1}$ and is paired with ℱ k $= \mathcal A_k$, so $z_1$ is conditioned on $\mathcal A_0$, as in the paper. z 0 is unused.
• "Concave as above" is IsPhi Φ c for an arbitrary constant c, together with IsConcavePhi Φ: concavity of $t \mapsto \Phi(t)$ on $[0, \infty)$, read through real values. This is honest because IsPhi forces $\Phi$ to be finite on finite arguments. The growth condition is required for every $x \in [0, \infty]$, which is equivalent to (6.1) by continuity. The paper's exclusion of $\Phi \equiv 0$ is dropped, since the conclusion is trivial there.
• Measurability. The $z_k$ are $\mathcal A$-measurable and are not assumed adapted. $\lambda$ in (20.2) is a positive real (l : ℝ≥0).
• Theorem 20.2 uses Mathlib's Martingale f ℱ P. It reads f n only for $n \ge 1$, with the paper's convention $f_0 = 0$. Mathlib's extra constraint on f 0 is no restriction, since every martingale of the paper extends by $f_0 := E(f_1 \mid \mathcal A_0)$.
• Ruled out. Assuming the $z_k$ integrable or square integrable, using the Bochner conditional expectation, or letting the constant depend on $\Phi$ would each change the theorem. None of them is used.
• Infrastructure. A complete development needs the tower and pull-out properties of condLExp for indicators of $\mathcal A_{k-1}$-sets, monotone convergence for condLExp, and the integral representation of a concave non-decreasing $\Phi$ with $\Phi(0) = 0$ as a mixture of the functions $t \mapsto t \wedge \lambda$ plus a linear part. The last is reusable well beyond this mission. Contributions to any of these are welcome.

Selected references

• D. L. Burkholder, Distribution Function Inequalities for Martingales, Annals of Probability 1(1), 19–42, 1973. https://doi.org/10.1214/aop/1176997023
• D. L. Burkholder, B. J. Davis and R. F. Gundy, Integral inequalities for convex functions of operators on martingales, Proc. Sixth Berkeley Symp. Math. Statist. Prob. 2, 223–240, 1972. https://projecteuclid.org/proceedings/berkeley-symposium-on-mathematical-statistics-and-probability/Proceedings-of-the-Sixth-Berkeley-Symposium-on-Mathematical-Statistics-and/Chapter/Integral-inequalities-for-convex-functions-of-operators-on-martingales/bsmsp/1200514225
• E. Lenglart, Relation de domination entre deux processus, Annales de l'Institut Henri Poincaré B 13(2), 171–179, 1977. http://www.numdam.org/item/AIHPB_1977__13_2_171_0/
• A. Zygmund, Trigonometric Series, Vol. I, Cambridge University Press, 1959 (the concave-function representation the paper cites, p. 24). https://doi.org/10.1017/CBO9781316036587