Analysis

Completed

Combinatorics·Captain: marwahaha

The dyadic case of the Erdős similarity conjectureOpen Problem

Motivation

Finite patterns fit inside positive-measure sets after a sufficiently small affine change. The dyadic similarity problem asks whether one particular infinite pattern can be excluded even from compact sets of nearly full measure. The source manuscript presents the surrounding research claim.

Setting

The dyadic sequence is D={2⁻ⁿ:n≥1}. Its affine copies are x+sD with arbitrary x∈ℝ and nonzero signed scale s. The ambient measure is Lebesgue measure on the real line.

Formalization target

For every 0<η<1, construct a compact E⊆[0,1] with

|E|>1-\eta,\qquad\forall x\in\mathbb R\;\forall s\ne0\;\exists n\ge1,\quad x+s2^{-n}\notin E.

The same E must avoid every translation and both signs of dilation.

The selected formal target is OAI.Problem310.dyadic_affine_avoidance.

Significance and status

The result concerns the dyadic sequence specifically, with a stronger near-full-measure conclusion than merely finding one positive-measure avoiding set. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Excluding a countable collection of copies does not handle the continuum of scales and centers. Finite initial segments cannot replace the entire sequence.

Formalization scope

The definition dyadicPoint accepts n=0, but the theorem explicitly chooses n≥1. Measure is ENNReal-valued and compares with ENNReal.ofReal(1−η). Compactness and interval containment are required conclusions. General infinite sets are outside this selected target.

Selected references

OpenAI, The dyadic case of the Erdős similarity conjecture, preprint, 2026. Pinned manuscript.
OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

48 thms2 active usersReviewed

Completed

Combinatorics·Captain: marwahaha

Asymptotically minimal maxima of real Littlewood polynomialsOpen Problem

Motivation

Choosing real signs in a polynomial controls how much its values can peak around the unit circle. The target seeks asymptotically optimal maximum modulus at every sufficiently large length. The source manuscript presents the surrounding research claim.

Setting

A real Littlewood polynomial has consecutive coefficients εₖ∈{−1,1}: P_N(z)=Σₖ₌₀ᴺ⁻¹ εₖzᵏ. The coefficient family may depend on both its length and the requested accuracy.

Formalization target

Prove

\forall\eta>0\;\exists N_0\ge1\;\forall N\ge N_0\;\exists\varepsilon,\quad\sup_{|z|=1}|P_N(z)|\le(1+\eta)\sqrt N.

All sufficiently large integer lengths are required, rather than a subsequence.

The selected formal target is OAI.AsymptoticallyMinimalLittlewood.main.

Significance and status

The selected target is the uniform maximum-modulus assertion. The companion finite-flatness target gives one sign family whose normalized modulus tends to one in every positive finite Lᵖ moment. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Control at finitely many sample points does not directly give a bound on the full circle. Uniformity in the circle variable and coverage of all large lengths are separate obligations.

Formalization scope

Coefficients are real-valued Fin N functions explicitly constrained to ±1 and evaluated as complex polynomials. The companion theorem uses Haar probability on UnitAddCircle and a single family for every p>0. Both independent definition groups are referenced; finite-flatness is a related endpoint rather than a claimed prerequisite.

Selected references

OpenAI, Asymptotically minimal maxima of real Littlewood polynomials, preprint, 2026. Pinned manuscript.
OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

26 thms2 active usersReviewed

Completed

Captain: marwahaha

A strict inverse-first-power bound for univalent functionsOpen Problem

Motivation

Integral-means spectra record the worst derivative concentration among normalized conformal maps. A strict bound at exponent −1 tests a specific predicted value of that spectrum. The source manuscript presents the surrounding research claim.

Setting

For a normalized univalent disk map f, M(−1,f,r) is the average of |f′|⁻¹ on the circle of radius r. The bounded spectrum B_b uses the extended-real limsup growth exponent, then takes its supremum over maps with bounded image.

Formalization target

Prove that there exist real ε and C with 0<ε<1/4 such that

M(-1,f,r)\le C(1-r)^{-1/4+\varepsilon}

for every normalized univalent f and 1/2≤r<1. Also prove B_b(−1)<1/4 and the failure of the defined Kraetzer prediction to equal B_b at every real exponent.

The selected formal target is OAI.StrictInverseFirstPower.main.

Significance and status

A strictly positive uniform ε is the content of the improvement. The target explicitly includes the spectrum consequence and the negation of the full predicted formula. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

An exponent arbitrarily close to 1/4 from above does not give a strict gap below 1/4. The same ε and C must precede the quantification over f and r.

Formalization scope

The circle estimate covers all normalized univalent maps, whereas the spectrum uses the bounded-image subclass. Complex derivatives, real interval integrals and EReal suprema are the supplied representations. The prediction is the specified piecewise quadratic/linear function.

Selected references

OpenAI, A strict inverse-first-power bound for univalent functions, preprint, 2026. Pinned manuscript.
OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

7 thms2 active usersReviewed

Completed

Captain: marwahaha

Brennan's conjecture and sharp inverse-square integral meansOpen Problem

Motivation

The size of the derivative of a conformal map can concentrate near a domain boundary. Brennan-type integrability and inverse-square integral means quantify how severe that concentration can be. The source manuscript presents the surrounding research claim.

Setting

A schlicht function is an injective holomorphic map f on the unit disk with f(0)=0 and f′(0)=1. M(f,t,r) is the circle average of |f′|ᵗ at radius r, and B(t) is the supremum of the associated extended-real boundary growth exponents.

Formalization target

Prove the four-part MainStatement, including

M(f,-2,r)\le C_\varepsilon(1-r)^{-1-\varepsilon},\qquad B(-2)=1,

uniformly for schlicht f and 1/2 ≤ r < 1. For conformal bijections φ:W→𝔻 on the specified simply connected domains, prove area integrability of |φ′|ˢ for 4/3<s<4; for univalent disk maps prove integrability of |f′|ᵗ for −2<t<2/3.

The selected formal target is OAI.Brennan.main_theorem.

Significance and status

The goal packages the uniform circle bound, exact spectrum value and both area-integrability formulations. A separate endpoint target records sharp failure for the Koebe map and its inverse. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

A growth bound with a constant depending on f does not supply the stated uniform estimate. Boundary behavior must also support the precise open exponent intervals.

Formalization scope

Planar Lebesgue area, a left-hand limit r→1, and extended-real spectra are fixed. W must be open, connected, simply connected and have nontrivial spherical boundary. Main and sharp-endpoint definitions are independent published groups with repeated names, so references coexist without one aggregate import.

Selected references

OpenAI, Brennan's conjecture and sharp inverse-square integral means, preprint, 2026. Pinned manuscript.
OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

8 thms2 active usersReviewed

Optimal Transport·Captain: wurtle

Sharp One-Third Stability of Brenier MapsResearch Paper

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

3 thms2 active usersReviewed

Completed

Partial Differential Equations·Captain: wurtle

The Subcritical Hénon–Lane–Emden ConjectureResearch Paper

Motivation: Liouville theorems for Lane–Emden systems

Liouville theorems say that certain nonlinear elliptic equations have no positive solutions on the whole space. Beyond their own interest, they are the key input in blow-up and rescaling arguments that give a priori bounds, existence results and singularity estimates for equations on bounded domains (Gidas–Spruck 1981; Polačik–Quittner–Souplet 2007). For the scalar equation $-\Delta u=u^p$ , Gidas and Spruck proved nonexistence in the whole subcritical range. For the coupled Lane–Emden system $-\Delta u=v^p$ , $-\Delta v=u^q$ , the corresponding statement — no positive solutions below the critical hyperbola $\frac1{p+1}+\frac1{q+1}=\frac{n-2}{n}$ — is the Lane–Emden conjecture; before the source, it had been proved only in dimensions $n\le4$ and in partial ranges. The weighted Hénon–Lane–Emden version, with factors $|x|^A$ and $|x|^B$ , asks the same question for the weighted hyperbola.

Timeline

1981 — Gidas and Spruck: scalar subcritical Liouville theorem and the blow-up method for a priori bounds (CPAM 1981; CPDE 1981).
1993, 1996 — Mitidieri: a Rellich-type identity for systems and early nonexistence regions (CPDE 1993; DIE 1996).
1996 — Serrin and Zou: the unweighted conjecture for $n=3$ under a growth condition (DIE 1996).
2007 — Polačik, Quittner and Souplet remove the growth condition for $n=3$ (Duke 2007).
2009 — Souplet proves the Lane–Emden conjecture for $n=4$ (Adv. Math. 2009); Chen and Li use integral systems and moving planes under integrability hypotheses (DCDS 2009).
2010 — Bidaut-Véron and Giacomini identify the critical weighted hyperbola in the radial theory and prove radial existence on and above it (ADE 2010).
2012 — Phan formulates the weighted question for $A,B>-2$ (Conjecture C) and proves bounded, low-dimensional and conditional cases (ADE 2012).
2014 — Fazly and Ghoussoub: bounded and stable cases for nonnegative weights (DCDS 2014).
2019 — Li and Zhang prove the Hénon–Lane–Emden conjecture in $\mathbb R^3$ (JDE 2019); Cheng and Huang give an energy-estimate criterion for the unweighted conjecture (DCDS 2019).
2022 — H. Li: restricted exponent ranges in dimensions four and five (Adv. Nonlinear Stud. 2022).
2025–2026 — K. Li, M. Li and Wei: a new unweighted region for $p,q\ge1$ when $n\ge5$ (preprint, 2025). Huang and Zou state the all-real-weight, origin-continuous assertion as Conjecture B (J. London Math. Soc. 2026). Xu and Luo treat radial higher-order systems (JDE 2026).
2026 — An OpenAI preprint, The Subcritical Hénon–Lane–Emden Conjecture (OpenAI Math Release, September 24, 2026), claims the full subcritical nonexistence theorem for every $n\ge2$ and all real weights. It has not been peer reviewed, and the claim has not been formally verified.

Setting

Fix an integer $n\ge2$ , exponents $p,q>0$ and real weights $A,B$ . The Hénon–Lane–Emden system is

-\Delta u=|x|^A\,v^p,\qquad -\Delta v=|x|^B\,u^q\qquad\text{in }\mathbb R^n\setminus\{0\},

where $\Delta=\sum_i\partial_i^2$ is the Laplacian. A solution in the sense of the source is a pair $u,v\in C^2(\mathbb R^n\setminus\{0\})\cap C(\mathbb R^n)$ with $u(x)>0$ and $v(x)>0$ for every $x\in\mathbb R^n$ , including the origin, satisfying both equations at every $x\neq0$ . The exponents are subcritical if

\frac{n+A}{p+1}+\frac{n+B}{q+1}>n-2 .

In Lean, Space n = EuclideanSpace ℝ (Fin n), IsSolution n p q A B u v packages continuity, ContDiffOn ℝ 2 off the origin, strict positivity everywhere and the two equations with Mathlib's Laplacian and real powers, and Subcritical is the displayed inequality.

Formalization targets

Goal: subcritical nonexistence (Theorem 1.1)

n\ge2,\ p,q>0,\ A,B\in\mathbb R,\ \frac{n+A}{p+1}+\frac{n+B}{q+1}>n-2\ \Longrightarrow\ \nexists\,(u,v)\ \text{solving the system as above}.

This is exactly Theorem 1.1 of the source. Taking $A=B=0$ gives the unweighted Lane–Emden conjecture (Corollary 1.2) for $n\ge3$ . 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 gives a positive answer to Huang and Zou's Conjecture B and, with $A=B=0$ , to the Lane–Emden conjecture in every dimension. It needs no radial symmetry, boundedness, integrability, finite energy, stability or growth condition at infinity. Combined with the radial existence theorem of Bidaut-Véron and Giacomini, it also settles Phan's Conjecture C for $n\ge3$ and $A,B>-2$ , including existence on the critical hyperbola (Corollary 6.2). Through the blow-up method, Liouville theorems of this type give a priori bounds and singularity and decay estimates for Lane–Emden-type systems on bounded domains.

Formalizing it. The statement is elementary: classical derivatives, the Euclidean Laplacian and real powers. The proof uses potential estimates, a localized virial (Rellich–Pohozaev type) identity, a geometric interval inequality and a dilation argument. All of these are within reach of Mathlib's analysis library, which makes the theorem a realistic test of large-scale PDE formalization.

Difficulty

The weighted statement does not follow from the unweighted one at the same exponents. For example, $n=5$ , $p=q=4$ , $A=B=3$ is weighted-subcritical, while $\frac1{p+1}+\frac1{q+1}=\frac25<\frac35$ is unweighted-supercritical. Weighted subcriticality also does not give the unweighted input in Phan's transfer argument. Translations do not preserve the weighted equation, so moving-plane and translation-based compactness arguments are unavailable. The level sets $\{|x|^Bu^q>t\}$ have endpoint values that vary with $|x|$ , which breaks the unweighted interval comparison. Finally, since no energy, decay or stability bound is assumed, the localized energy has to be bounded from the subcritical gap alone.

Formalization scope

The domain is EuclideanSpace ℝ (Fin n) with $n\ge2$ , and $p,q,A,B$ are real with $p,q>0$ . Weights are Real.rpow ‖x‖ A, used only at $x\neq0$ , so the junk value of rpow at $0$ never enters. The nonlinearities Real.rpow (v x) p are evaluated at strictly positive arguments.
Regularity is Continuous on all of $\mathbb R^n$ and ContDiffOn ℝ 2 on $\{0\}^c$ . Positivity is required at every point, including the origin, as in the source; differentiability at the origin is not assumed.
The conclusion is the nonexistence of any such pair. Every hypothesis is satisfiable (supercritical solutions exist), so the statement is not trivialized.
Infrastructure needed: Newtonian potentials and distributional extension across a point, Rellich–Pohozaev identities, polar integration and dilation arguments. These pieces would serve other Liouville-type theorems.

Selected references

B. Gidas and J. Spruck, Global and local behavior of positive solutions of nonlinear elliptic equations, Comm. Pure Appl. Math. 34 (1981), 525–598. https://doi.org/10.1002/cpa.3160340406
B. Gidas and J. Spruck, A priori bounds for positive solutions of nonlinear elliptic equations, Comm. PDE 6 (1981), 883–901. https://doi.org/10.1080/03605308108820196
E. Mitidieri, A Rellich type identity and applications, Comm. PDE 18 (1993), 125–151. https://doi.org/10.1080/03605309308820923
E. Mitidieri, Nonexistence of positive solutions of semilinear elliptic systems in $\mathbb R^N$ , Differential Integral Equations 9 (1996), 465–479. https://doi.org/10.57262/die/1367969966
J. Serrin and H. Zou, Non-existence of positive solutions of Lane–Emden systems, Differential Integral Equations 9 (1996), 635–653. https://doi.org/10.57262/die/1367969879
P. Polačik, P. Quittner and P. Souplet, Duke Math. J. 139 (2007), 555–579. https://doi.org/10.1215/S0012-7094-07-13935-8
P. Souplet, The proof of the Lane–Emden conjecture in four space dimensions, Adv. Math. 221 (2009), 1409–1427. https://doi.org/10.1016/j.aim.2009.02.014
W. Chen and C. Li, An integral system and the Lane–Emden conjecture, Discrete Contin. Dyn. Syst. 24 (2009), 1167–1184. https://doi.org/10.3934/dcds.2009.24.1167
M.-F. Bidaut-Véron and H. Giacomini, A new dynamical approach of Emden–Fowler equations and systems, Adv. Differential Equations 15 (2010), 1033–1082. https://doi.org/10.57262/ade/1355854434
Q. H. Phan, Adv. Differential Equations 17 (2012), 605–634. https://doi.org/10.57262/ade/1355702970
M. Fazly and N. Ghoussoub, On the Hénon–Lane–Emden conjecture, Discrete Contin. Dyn. Syst. 34 (2014), 2513–2533. https://doi.org/10.3934/dcds.2014.34.2513
K. Li and Z. Zhang, Proof of the Hénon–Lane–Emden conjecture in $\mathbb R^3$ , J. Differential Equations 266 (2019), 202–226. https://doi.org/10.1016/j.jde.2018.07.036
Z. Cheng and G. Huang, A Liouville theorem for the subcritical Lane–Emden system, Discrete Contin. Dyn. Syst. 39 (2019), 1359–1377. https://doi.org/10.3934/dcds.2019058
H. Li, Adv. Nonlinear Stud. 22 (2022), 517–533. https://doi.org/10.1515/ans-2022-0027
L.-H. Huang and W. Zou, J. London Math. Soc. 113 (2026), e70412. https://doi.org/10.1112/jlms.70412
Y. Xu and H. Luo, Liouville type theorems for higher order elliptic systems, J. Differential Equations 453 (2026), 113823. https://doi.org/10.1016/j.jde.2025.113823
OpenAI, The Subcritical Hénon–Lane–Emden Conjecture, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Subcritical-Henon-Lane-Emden-Conjecture-September-24-2026/paper.pdf

10 thms2 active usersReviewed

Mathematical Physics Partial Differential Equations·Captain: wurtle

Nonuniqueness for the periodic hard-sphere Boltzmann equationResearch Paper

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

4 thms2 active usersReviewed

Completed

Functional Analysis·Captain: wurtle

Exact asymptotic moduli in a Daugavet subspace of L1Research Paper

Motivation

A norm is uniformly convex when midpoints of far-apart unit vectors are pushed strictly inside the unit ball. In infinite-dimensional Banach spaces the useful notions are asymptotic: one asks for a gain only in directions taken from a subspace of finite codimension, chosen after the center is fixed. Two such notions are compared here. Asymptotic uniform convexity (AUC) asks for growth of $\|x+ty\|$ in every far-out unit direction $y$ ; asymptotic midpoint uniform convexity (AMUC) asks only that the average of $\|x+ty\|$ and $\|x-ty\|$ grows. These properties control nonlinear embeddings (for instance of countably branching diamond graphs) and are standard tools in the asymptotic geometry of Banach spaces.

Dilworth, Kutzarova, Randrianarivony, Revalski and Zhivkov (2016) asked whether AMUC and AUC are equivalent up to renorming. Baudier (2026) answered no, using subspaces of $L^1$ whose unit ball is compact in measure and the Daugavet-property example of Kadets and Werner. This mission asks for the exact values of both moduli in that setting.

Timeline

1980. Bourgain and Rosenthal construct a subspace of $L^1$ whose unit ball is relatively compact in measure but which fails the Radon–Nikodym property (doi:10.1007/BF02762868).
1983. Brézis and Lieb prove their splitting identity for pointwise convergent sequences in $L^p$ (doi:10.1090/S0002-9939-1983-0699419-3).
2000. Kadets, Shvidkoy, Sirotkin and Werner give the slice characterization of the Daugavet property (arXiv:math/9709216); Shvydkoy gives its weak-open form (doi:10.1006/jfan.2000.3626).
2004. Kadets and Werner refine the Bourgain–Rosenthal construction to obtain a space with the Schur and Daugavet properties (doi:10.1090/S0002-9939-03-07278-2).
2016. Dilworth et al. introduce AMUC and ask whether it is equivalent to AUC up to renorming (doi:10.1016/j.jmaa.2015.11.061).
2026. Baudier proves AMUC for measure-compact subspaces of $L^1$ and deduces a negative answer via the Kadets–Werner space (arXiv:2609.21283).

The source of this mission is an OpenAI preprint dated September 27, 2026, which computes both moduli exactly.

Setting

All spaces are real. For a Banach space $X$ with norm $N$ , let $\operatorname{cof}(X)$ be its closed linear subspaces of finite codimension. For $N(x)=1$ and $t>0$ ,

H_N(x,t)=\sup_{F\in\operatorname{cof}(X)}\ \inf_{\substack{y\in F\\ N(y)\ge1}}\Bigl(\frac{N(x+ty)+N(x-ty)}2-1\Bigr),\qquad D_N(x,t)=\sup_{F\in\operatorname{cof}(X)}\ \inf_{\substack{y\in F\\ N(y)=1}}\bigl(N(x+ty)-1\bigr).

The averaged midpoint modulus $\widehat\delta_N(t)$ and the one-sided modulus $\overline\delta_N(t)$ are the infima of $H_N(x,t)$ and $D_N(x,t)$ over unit $x$ . $N$ is AUC if $\overline\delta_N(t)>0$ for all $t>0$ . A norm $N$ is equivalent to $\|\cdot\|$ if $a\|x\|\le N(x)\le b\|x\|$ with $a,b>0$ .

A space has the Daugavet property if $\|I+T\|=1+\|T\|$ for every rank-one bounded operator $T$ . On a probability space $(\Omega,\mathbb P)$ , convergence in measure is given by the metric

d(f,g)=\inf\{a>0:\ \mathbb P(|f-g|>a)<a\}.

A set is totally bounded in measure if for each $\varepsilon>0$ it is covered by finitely many $d$ -balls of radius $\varepsilon$ .

Formalization targets

Goal: Theorem 1.1

Let $E$ be an infinite-dimensional closed subspace of $L^1(\Omega,\mathbb P)$ , $\mathbb P$ a probability measure, whose unit ball is totally bounded in measure and whose norm has the Daugavet property. Then for every unit $x\in E$ and $t>0$

H_E(x,t)=\max\{t/2,\ t-1\},\qquad D_E(x,t)=\max\{0,\ t-2\},

so $\widehat\delta_E(t)=\max\{t/2,t-1\}$ and $\overline\delta_E(t)=\max\{0,t-2\}$ , and $E$ admits no equivalent AUC norm. Lean: OAI.ExactModuli.exact_main (open on the platform).

Milestone: Theorem 6.1 (Kadets–Werner construction)

On $([0,1]^{\mathbb N},\lambda^{\mathbb N})$ there is an infinite-dimensional closed subspace $E\subseteq L^1$ whose unit ball is totally bounded in measure and which has the Daugavet slice property. Lean: OAI.ExactModuli.kadets_werner_existence. The proposal also carries OAI.ExactModuli.exact_example, the combination of the two theorems for this space.

Significance

The formulas show how far apart the two moduli can be: the averaged modulus grows linearly from $0$ , while the one-sided modulus vanishes on the whole interval $(0,2]$ . They refine Baudier's qualitative AMUC statement and linear lower bound into exact curves at every unit center, and the renorming clause shows that no equivalent norm can repair the one-sided modulus. Together with Theorem 6.1, they give a concrete space realizing the separation.

The results are proved in an OpenAI preprint; they have not been peer reviewed, and no machine-checked proof exists. The Daugavet slice characterization, Bourgain's lemma on slices and weak neighborhoods (Lemma 3.2), and the construction itself are reusable pieces of Banach space theory that a formalization would supply.

Difficulty

The lower bound for $H_E$ must hold uniformly over all directions in some finite-codimensional subspace, while the hypothesis only says that the unit ball is compact in a weak metric. A compactness argument along subsequences (Baudier's route via Brézis–Lieb) gives positivity but not the exact constant. The upper bounds need directions in a prescribed finite-codimensional subspace that are almost at distance $2$ from $x$ ; the Daugavet property supplies such vectors only in weak neighborhoods, and they must then be corrected into the subspace. The renorming clause must handle an arbitrary equivalent norm, for which neither formula is available.

Formalization scope

Cofinite F is a closed submodule with finite-dimensional quotient. H, D, averagedModulus, oneSidedModulus follow the displayed sup/inf order; H ranges over $N(y)\ge1$ , D over $N(y)=1$ .
EquivalentNorm N is a Seminorm with two-sided comparison constants $a,b>0$ ; AUC N is positivity of oneSidedModulus N t for every $t>0$ .
Daugavet X quantifies over rank-one operators written as ell.smulRight v.
measureDistance is the metric $d$ on Lp ℝ 1 μ; MeasurePrecompactBall μ E requires finite $\varepsilon$ -nets (centers in $L^1$ ) of the unit ball of $E$ ; μ is a probability measure.
kwMeasure is the product of Lebesgue measures on $\mathbb N\to[0,1]$ .
The moduli are real-valued sSup/sInf; for infinite-dimensional $E$ the relevant sets are nonempty and bounded, so the junk values are not used.

A full development needs the Daugavet slice characterization (Lemma 3.1), Bourgain's lemma (Lemma 3.2), the weak-neighborhood diameter-two property (Lemma 3.3), $L^1$ truncation estimates, and the Kadets–Werner iteration (Lemmas 6.2–6.3). Formalizations of these lemmas are welcome.

Selected references

OpenAI, Exact asymptotic moduli in a Daugavet subspace of $L^1$ , preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Exact-asymptotic-moduli-in-a-Daugavet-subspace-of-L1-September-27-2026/manuscript.pdf
F. P. Baudier, The Kadets–Werner modification of Bourgain–Rosenthal space is asymptotically midpoint uniformly convex, preprint, 2026. https://arxiv.org/abs/2609.21283
S. J. Dilworth, D. Kutzarova, N. L. Randrianarivony, J. P. Revalski, N. V. Zhivkov, Lenses and asymptotic midpoint uniform convexity, J. Math. Anal. Appl., 2016. https://doi.org/10.1016/j.jmaa.2015.11.061
V. Kadets, D. Werner, A Banach space with the Schur and the Daugavet property, Proc. Amer. Math. Soc., 2004. https://doi.org/10.1090/S0002-9939-03-07278-2
J. Bourgain, H. P. Rosenthal, Martingales valued in certain subspaces of $L^1$ , Israel J. Math., 1980. https://doi.org/10.1007/BF02762868
V. M. Kadets, R. V. Shvidkoy, G. G. Sirotkin, D. Werner, Banach spaces with the Daugavet property, Trans. Amer. Math. Soc., 2000. https://arxiv.org/abs/math/9709216
R. V. Shvydkoy, Geometric aspects of the Daugavet property, J. Funct. Anal., 2000. https://doi.org/10.1006/jfan.2000.3626
H. Brézis, E. Lieb, A relation between pointwise convergence of functions and convergence of functionals, Proc. Amer. Math. Soc., 1983. https://doi.org/10.1090/S0002-9939-1983-0699419-3

4 thms2 active usersReviewed

Completed

Functional Analysis·Captain: wurtle

Midpoint lenses in segment spacesResearch Paper

Motivation

In a uniformly convex space, if $x$ is nearly as long as $R$ and both $x+y$ and $x-y$ have length at most $R$ , then the displacement $y$ must be short. The set of such displacements,

\mathcal L(x,R)=\{y:\ \|x+y\|\le R,\ \|x-y\|\le R\},

is a symmetric lens. In infinite dimensions the right question is asymptotic: is $y$ short after discarding finitely many directions? Dilworth, Kutzarova, Randrianarivony, Revalski and Zhivkov (2016) characterized asymptotic midpoint uniform convexity (AMUC) through the measure of noncompactness of such lenses. AMUC is the property that, together with asymptotic uniform convexity (AUC), governs which countably branching graphs embed into a Banach space with bounded distortion.

This mission asks for an explicit lens estimate in two James-type tree spaces, with a bound depending only on the squared-radius deficit $R^2-\|x\|^2$ of the center and holding for every displacement simultaneously after one finite set of coordinates is removed.

Timeline

1974. James introduces the square-sum norm over disjoint segments of a tree (doi:10.1090/S0002-9904-1974-13580-9).
1985. Ghoussoub and Maurey study $G_\delta$ -embeddings in Hilbert space (doi:10.1016/0022-1236(85)90039-4); the coordinate predual $B_\infty$ used here is the Ghoussoub–Maurey–Schachermayer construction as presented by Banakh (2000).
2001. Girardi proves AUC of the canonical predual and of the full dual of the binary James tree space (doi:10.4064/sm147-2-2).
2016. Dilworth et al. introduce AMUC and characterize it by lenses (doi:10.1016/j.jmaa.2015.11.061).
2017. Baudier, Causey, Dilworth, Kutzarova, Randrianarivony, Schlumprecht and Zhang show that an equivalent AMUC norm prevents uniform embeddings of countably branching diamonds (arXiv:1612.01984).
2021. Perreau asks whether the canonical predual of the countably branching James tree space is AMUC (Question 6 of arXiv:2104.10494).
2026. Baudier shows that AMUC does not imply AUC renormability, via the Kadets–Werner modification of the Bourgain–Rosenthal space (arXiv:2609.21283).

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

Setting

All scalars are real.

Finite-height forest. For $h\ge1$ let $T_h=\mathbb N^{\le h}$ be the tree of words of length at most $h$ , ordered by extension (the root is the empty word). The forest $\mathcal F$ is the disjoint union of one copy $\{h\}\times T_h$ for each $h\ge1$ . Write $a\preceq b$ if $a$ is an ancestor of $b$ in the same component. A segment is a nonempty interval $[a,b]=\{v: a\preceq v\preceq b\}$ . For finitely supported $u$ put $u(S)=\sum_{v\in S}u(v)$ and

\rho(u)=\sup\Bigl\{\Bigl(\sum_{i=1}^m u(S_i)^2\Bigr)^{1/2}:\ S_1,\dots,S_m\ \text{pairwise disjoint segments}\Bigr\}.

Let $J$ be the completion of $(c_{00}(\mathcal F),\rho)$ and $X=J^*$ with the dual norm. Coordinate evaluation gives functionals $e_v^*\in X$ .

Infinite tree. Let $T_\infty=\mathbb N^{<\omega}$ (all finite words, root included), $J_\infty$ the completion for the same norm, and $B_\infty=\overline{\operatorname{span}}\{e_v^*\}\subset J_\infty^*$ , closed in the dual norm.

A finite set $H$ of vertices is ancestral if it contains all ancestors of its elements. On either space,

P_Hx=\sum_{v\in H}x(e_v)\,e_v^*,\qquad Q_Hx=x-P_Hx.

Formalization targets

Goal: Theorem 1.1

For $Y\in\{X,\ B_\infty\}$ , every finite ancestral $H$ , every $x,y\in Y$ with $x=P_Hx$ , and every $R\ge0$ with $\|x+y\|\le R$ and $\|x-y\|\le R$ ,

\|Q_Hy\|\ \le\ 2\sqrt{R^2-\|x\|^2}.

The Lean statement OAI.SegmentLenses.midpoint_lens_main is the conjunction of the two cases. It is open on the platform. The displacement $y$ may have a nonzero head $P_Hy$ ; only its tail is controlled.

Significance

The estimate is uniform over the lens: one finite head $H$ controls every admissible displacement, which is exactly what is needed when a single center has infinitely many approximate midpoints. As a consequence (Corollary 7.1 of the source) both given norms are AMUC with $\widehat\delta(t)\ge(\sqrt{1+t^2/4}-1)/2$ , while Proposition 9.1 shows that neither space admits an equivalent AUC norm. In particular the infinite-height case answers Perreau's question for the specified real norm on $B_\infty$ , and the finite-height forest gives a reflexive space separating AMUC from AUC renormability. A companion preprint uses this theorem to force distortion $D^2\ge1+k/4$ for depth- $k$ countably branching diamonds.

The result is proved only in the OpenAI preprint; it is not peer reviewed and has no machine-checked proof. Formalizing it would certify the cancellation analysis that drives the constant $2$ .

Difficulty

The natural attempt is to represent a nearly norming functional for the center as a convex combination of disjoint segment functionals and read off the tail. The obstacle is cancellation: two atoms leaving the head $H$ through the same vertex can have segment sums of opposite sign, and a naive estimate loses all control. The bound must also hold for every displacement with the same $H$ , so compactness arguments that choose $H$ after $y$ do not suffice, and an independent radial approach in the source gives only the weaker $(\sqrt2+\sqrt6)\sqrt{R(R-\|x\|)}$ .

Formalization scope

Vertices: ForestVertex is the subtype of pairs $(h,w)$ with $1\le h$ and $|w|\le h$ ; InfiniteVertex := List ℕ. Ancestry is equality of heights plus List.IsPrefix (resp. prefix only).
Segments: IsInterval ancestor S asserts $S=[a,b]$ with $a\preceq b$ , so segments are nonempty. A test family is a finite set of pairwise disjoint segments, and segmentSeminorm is the supremum of the Euclidean norms of the vectors of segment sums.
Spaces: X := StrongDual ℝ (UniformSpace.Completion (Test ForestVertex)); BInfinite is the closed span of the coordinate functionals inside the full dual of the infinite-tree completion, carrying the subspace (dual) norm.
head H x = ∑ v ∈ H, x(e_v) • e_v^* and tail H x = x - head H x; ancestrality is Ancestral.
Trivialization check: $R\ge0$ is required as in the source, and since $\|x\|\le R$ follows from the lens condition, the square root argument is never negative.

A full development needs the James segment norm, its completion and dual, contractivity of coordinate projections, the $\ell_2$ decomposition of the tail over descendant cones (Lemma 2.2), and the atomic description of finite head balls (Section 4). This infrastructure is shared with the other missions in the same family. Formalizations of Lemma 2.1, Lemma 2.2, Corollary 7.1 and Proposition 9.1 are welcome as supporting results.

Selected references

OpenAI, Midpoint lenses in segment spaces, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Midpoint-lenses-in-segment-spaces-September-27-2026/manuscript.pdf
S. J. Dilworth, D. Kutzarova, N. L. Randrianarivony, J. P. Revalski, N. V. Zhivkov, Lenses and asymptotic midpoint uniform convexity, J. Math. Anal. Appl., 2016. https://doi.org/10.1016/j.jmaa.2015.11.061
R. C. James, A separable somewhat reflexive Banach space with nonseparable dual, Bull. Amer. Math. Soc., 1974. https://doi.org/10.1090/S0002-9904-1974-13580-9
M. Girardi, The dual of the James tree space is asymptotically uniformly convex, Studia Math., 2001. https://doi.org/10.4064/sm147-2-2
Y. Perreau, On the embeddability of countably branching bundle graphs into dual spaces, preprint, 2021. https://arxiv.org/abs/2104.10494
F. Baudier, R. Causey, S. Dilworth, D. Kutzarova, N. L. Randrianarivony, T. Schlumprecht, S. Zhang, On the geometry of the countably branching diamond graphs, J. Funct. Anal., 2017. https://arxiv.org/abs/1612.01984
F. P. Baudier, The Kadets–Werner modification of Bourgain–Rosenthal space is asymptotically midpoint uniformly convex, preprint, 2026. https://arxiv.org/abs/2609.21283
N. Ghoussoub, B. Maurey, $G_\delta$ -embeddings in Hilbert space, J. Funct. Anal., 1985. https://doi.org/10.1016/0022-1236(85)90039-4

12 thms2 active usersReviewed

Completed

Functional Analysis·Captain: wurtle

Asymptotic midpoint uniform convexity and unbounded diamond distortion in a reflexive tree spaceResearch Paper

Motivation

Uniform convexity of a norm says that the midpoint of two far-apart points of the unit sphere lies strictly inside the ball. In infinite dimensions there is an asymptotic version: one only asks for a gain in directions that lie far out, that is, inside some closed subspace of finite codimension. Asymptotic uniform convexity and its relatives control the large-scale geometry of a Banach space, and in particular which infinite graphs can be embedded into the space with bounded distortion.

Two such properties are compared here. Asymptotic uniform convexity (AUC) demands a gain in every far-out direction separately; asymptotic midpoint uniform convexity (AMUC), introduced by Dilworth, Kutzarova, Randrianarivony, Revalski and Zhivkov (2016), only asks for a gain when a direction and its opposite are tested together. Every AUC norm is AMUC. The question is how far apart the two notions are, both up to renorming and in terms of metric embeddings of the countably branching diamond graphs $D_k$ .

Timeline

1974. James introduces the square-sum norm over disjoint segments of a tree (the James tree space) (doi:10.1090/S0002-9904-1974-13580-9).
2001. Girardi proves that the coordinate predual and the full dual of the binary James tree space are AUC (doi:10.4064/sm147-2-2).
2004 and 2009. Lee and Naor obtain quantitative $L_p$ distortion bounds for finite binary diamonds; Johnson and Schechtman relate diamond embeddings to super-reflexivity (doi:10.1007/s00039-004-0473-8, doi:10.1142/S1793525309000114).
2016. Dilworth et al. define AMUC and construct an AMUC norm on $\ell_2$ that is not AUC (doi:10.1016/j.jmaa.2015.11.061).
2017. Baudier, Causey, Dilworth, Kutzarova, Randrianarivony, Schlumprecht and Zhang show that an equivalent AMUC norm prevents uniform embeddings of the countably branching diamonds, and that for reflexive spaces with unconditional asymptotic structure, failure of AUC renormability forces uniform diamond embeddings (arXiv:1612.01984).
2018 and 2021. Swift extends the embedding construction to countably branching bundle graphs under the same hypotheses (arXiv:1710.00877); Perreau treats duals of separable spaces with weak-star unconditional asymptotic structure (arXiv:2104.10494).
2025. Baudier and Lancien record, as Problem 39 of their monograph, whether the diamond implication holds for general reflexive spaces (arXiv:2512.00817).
2026. Baudier shows that AMUC renormability does not imply AUC renormability, using the Kadets–Werner modification of the Bourgain–Rosenthal space, which is not reflexive (arXiv:2609.21283).

The source of this mission, an OpenAI preprint dated September 27, 2026, gives a reflexive example that separates the two notions and answers the reflexive diamond question negatively.

Setting

All spaces are real. For a Banach space $Y$ with norm $N$ , let $\operatorname{cof}(Y)$ be the closed subspaces of finite codimension. For $t>0$ ,

\overline\delta_N(t)=\inf_{N(x)=1}\ \sup_{F\in\operatorname{cof}(Y)}\ \inf_{y\in F,\ N(y)=1}\bigl(N(x+ty)-1\bigr),

\widehat\delta_N(t)=\inf_{N(x)=1}\ \sup_{F\in\operatorname{cof}(Y)}\ \inf_{y\in F,\ N(y)=1}\Bigl(\tfrac{N(x+ty)+N(x-ty)}{2}-1\Bigr).

$N$ is AUC if $\overline\delta_N(t)>0$ for every $t>0$ , and AMUC if $\widehat\delta_N(t)>0$ for every $t>0$ . A norm $N$ is equivalent to $\|\cdot\|$ if $a\|x\|\le N(x)\le b\|x\|$ for some $0<a\le b$ .

The forest. For $h\ge1$ let $T_h=\mathbb N^{\le h}$ be the rooted tree of words of length at most $h$ , ordered by extension. The forest $\mathcal F$ is the disjoint union of one copy of $T_h$ for every $h\ge1$ . A segment is an interval $[a,b]$ of an ancestral chain. For a finitely supported $u:\mathcal F\to\mathbb R$ ,

\rho(u)=\sup\Bigl\{\Bigl(\sum_{i=1}^m u(S_i)^2\Bigr)^{1/2} : S_1,\dots,S_m\ \text{pairwise disjoint segments}\Bigr\},\qquad u(S)=\sum_{v\in S}u(v).

Let $J$ be the completion and $X=J^*$ with the dual norm.

Diamonds. $D_0$ is one edge; $D_{k+1}$ replaces every edge of $D_k$ by countably many internally disjoint two-edge paths. With the shortest-path metric $d_k$ , a map $f:D_k\to X$ has distortion at most $C$ if some scale $s>0$ gives $s\,d_k(u,v)\le\|f(u)-f(v)\|\le Cs\,d_k(u,v)$ for all $u,v$ .

Formalization targets

Goal: Theorem 1.1

X\ \text{is infinite dimensional, separable and reflexive, and admits no equivalent AUC norm;}

\widehat\delta_X(t)\ \ge\ \sqrt{1+t^2/12}-1\quad(t>0);

\text{every embedding of }D_k\text{ into }X\text{ has distortion}\ \ge\ \sqrt{1+k/12}\quad(k\ge0).

The Lean statement OAI.ForestSpace.main_theorem is the conjunction of these six clauses. It is open on the platform.

Significance

The theorem separates AMUC from AUC renormability inside the reflexive class, which Baudier's 2026 example (non-reflexive) does not. Because AMUC is a property of the given norm while the diamond obstruction is invariant under renorming, the theorem also shows that, for general reflexive spaces, failure of AUC renormability does not force the countably branching diamonds to embed uniformly. This answers Problem 39 of Baudier–Lancien negatively and shows that the unconditional asymptotic structure hypothesis in the 2017 embedding theorem cannot simply be dropped. The quantitative modulus and distortion bounds are explicit, not merely positivity statements.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. A formal proof would certify the full construction, including reflexivity of $J^*$ for a non-locally-finite forest and the square-sum distortion recursion.

Difficulty

Two points are delicate. First, reflexivity: the classical James tree space is not reflexive, and here reflexivity comes from using trees of finite but unbounded height together with countable branching; the full dual $J^*$ , not the coordinate completion, is the space. Second, the midpoint estimate: a segment test may cross from a finite ancestral set to its complement, and simply adding norming tests for the two parts produces uncontrolled positive cross terms. Non-renormability, by contrast, must be proved for every equivalent norm at once, so it cannot be read off from any computation with the given norm.

Formalization scope

The space is FullDual Vertex := StrongDual ℝ (J Vertex), where J V is the UniformSpace.Completion of TestVector V (finitely supported functions with norm rho). Vertex packs a height $h\ge1$ and a word in $\mathbb N^*$ of length $\le h$ ; the order is equality of heights plus prefix order.
Segments are finite order-convex chains (IsSegment); the empty segment is allowed and contributes zero.
Reflexive is surjectivity of the canonical map NormedSpace.inclusionInDoubleDual, not an abstract isomorphism with the bidual.
EquivalentNorm E α β stores a Seminorm with explicit constants $0<\alpha\le\beta$ ; the lower bound makes it a norm. The non-renormability clause quantifies over all such structures.
aucModulus and averageModulus take the inf/sup/inf order above, with sInf/sSup over real sets; for an infinite-dimensional space these sets are nonempty and bounded, so the Lean defaults are not triggered.
Diamond.diamond k iterates the edge replacement starting from one edge; distances are SimpleGraph.dist of the undirected graph, and EmbeddingBound is the scaled bi-Lipschitz condition above.

A complete development needs the James-type segment norm, its completion and dual, coordinate projections onto ancestral sets, and graph distances on the diamonds. The segment-norm and diamond infrastructure is shared with the other missions of this family. Contributions formalizing Lemma 2.1 (structure and reflexivity), Lemma 3.2 (bounded trees exclude AUC renorming), Lemma 4.1 (paired head–tail estimate) and Lemma 5.1 (lens lemma) are welcome.

Selected references

OpenAI, Asymptotic midpoint uniform convexity and unbounded diamond distortion in a reflexive tree space, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Asymptotic-midpoint-uniform-convexity-and-unbounded-diamond-distortion-in-a-reflexive-tree-space-September-27-2026/manuscript.pdf
S. J. Dilworth, D. Kutzarova, N. L. Randrianarivony, J. P. Revalski, N. V. Zhivkov, Lenses and asymptotic midpoint uniform convexity, J. Math. Anal. Appl., 2016. https://doi.org/10.1016/j.jmaa.2015.11.061
F. Baudier, R. Causey, S. Dilworth, D. Kutzarova, N. L. Randrianarivony, T. Schlumprecht, S. Zhang, On the geometry of the countably branching diamond graphs, J. Funct. Anal., 2017. https://arxiv.org/abs/1612.01984
F. P. Baudier, G. Lancien, Asymptotic and nonlinear geometries of Banach spaces and their interactions, Cours Spécialisés, SMF, 2026. https://arxiv.org/abs/2512.00817
F. P. Baudier, The Kadets–Werner modification of Bourgain–Rosenthal space is asymptotically midpoint uniformly convex, preprint, 2026. https://arxiv.org/abs/2609.21283
R. C. James, A separable somewhat reflexive Banach space with nonseparable dual, Bull. Amer. Math. Soc., 1974. https://doi.org/10.1090/S0002-9904-1974-13580-9
M. Girardi, The dual of the James tree space is asymptotically uniformly convex, Studia Math., 2001. https://doi.org/10.4064/sm147-2-2
A. Swift, A coding of bundle graphs and their embeddings into Banach spaces, Mathematika, 2018. https://arxiv.org/abs/1710.00877
Y. Perreau, On the embeddability of countably branching bundle graphs into dual spaces, preprint, 2021. https://arxiv.org/abs/2104.10494

27 thms2 active usersReviewed

Completed

Functional Analysis·Captain: wurtle

A positive solution to Tingley’s problemResearch Paper

Motivation: isometries of unit spheres

The Mazur–Ulam theorem (1932) says that every surjective isometry between real normed spaces is affine. The whole space is not always available, though: often only distances between unit vectors are known. Tingley's problem (1987) asks whether the metric of the unit sphere alone already determines the linear structure, that is, whether every surjective isometry between the unit spheres of two real Banach spaces extends to a real-linear isometry of the spaces (Tingley 1987). The question has been studied for almost four decades, mostly class by class: for sequence spaces, $L^p$ spaces, operator algebras and two-dimensional spaces. Nearly all known positive results depend on the structure of the particular spaces involved.

Timeline

1932 — Mazur and Ulam: surjective isometries between real normed spaces are affine.
1972 — Mankiewicz extends isometries between convex sets with nonempty interior. A unit sphere has empty interior, so this does not apply.
1987 — Tingley poses the problem and shows that surjective isometries between spheres of finite-dimensional spaces preserve antipodal points (Tingley 1987).
1994 — Wang treats spheres of $C_0(\Omega)$ -type spaces (Wang 1994).
2003 — Ding handles $\ell^p(\Gamma)$ -type spaces, $p>1$ , $p\ne 2$ (Ding 2003).
2011 — Cheng and Dong formulate the Mazur–Ulam property (sphere isometries from a given space into an arbitrary target extend linearly) (Cheng–Dong 2011).
2012 — Tan proves the Mazur–Ulam property for real $L^p(\mu)$ , $1<p<\infty$ , $p\neq 2$ (Tan 2012).
2014 — Tanaka: sphere isometries preserve maximal convex subsets of the sphere (Tanaka 2014).
2018 — Fernández-Polo and Peralta (von Neumann algebras, JMAA 2018); Mori (preduals, JMAA 2018).
2020 — Mori and Ozawa: Mazur–Ulam property for unital $C^*$ -algebras and real von Neumann algebras (Studia Math. 2020).
2022 — Banakh: every two-dimensional real Banach space has the Mazur–Ulam property (Banakh 2022).
2025–2026 — Further class results: Schreier spaces (Fakhoury 2025); Haagerup noncommutative $L_p$ and Schatten classes (Huang–Zhu, arXiv:2608.30131; arXiv:2607.11244).
2026 — An OpenAI preprint, A positive solution to Tingley's problem (OpenAI Math Release, September 23, 2026), claims the general affirmative answer for all real Banach spaces. It has not been peer reviewed, and the claim has not been formally verified.

Setting

Let $X$ and $Y$ be real Banach spaces, both nonzero. The unit sphere is $S_X=\{x\in X:\|x\|=1\}$ with the metric inherited from $X$ . A map $f:S_X\to S_Y$ is an isometry if $\|f(x)-f(y)\|=\|x-y\|$ for all $x,y\in S_X$ , and it is surjective if every point of $S_Y$ is attained.

Any linear extension of $f$ is forced to be the radial extension

T(0)=0,\qquad T(x)=\|x\|\,f\!\left(\frac{x}{\|x\|}\right)\quad(x\neq 0).

In Lean, UnitSphere X is the subtype $\{x : X \mid \|x\|=1\}$ and normalize x hx is $x/\|x\|$ as an element of it.

Formalization targets

Goal: Tingley's problem (Theorem 1.1)

For nonzero real Banach spaces $X,Y$ and every surjective isometry $f:S_X\to S_Y$ there is a surjective real-linear isometry $T:X\to Y$ such that

T|_{S_X}=f,\qquad T(0)=0,\qquad T(x)=\|x\|\,f\!\left(\tfrac{x}{\|x\|}\right)\ (x\neq0),

and $T$ is the only real-linear map $X\to Y$ that agrees with $f$ on $S_X$ . This is the full statement of Theorem 1.1 of the source. The goal is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. An affirmative answer turns a forty-year class-by-class programme into a single theorem: the metric of the unit sphere of any real Banach space determines the space up to linear isometry. Every space then has the Mazur–Ulam property in the sense of Cheng and Dong, with no separability, reflexivity, smoothness or strict convexity assumptions. For complex Banach spaces viewed as real spaces the conclusion is real-linearity only; complex-linearity is not claimed.

Formalizing it. The claimed proof combines classical tools (supporting functionals, Banach-space ultrapowers, Darbo's fixed-point theorem with the Kuratowski measure of noncompactness, the Mazur–Ulam theorem) with new geometric estimates on aligned chords. A machine-checked proof would certify a result whose proof has not yet been refereed. The Mazur–Ulam theorem itself is already in Mathlib (IsometryEquiv.toRealLinearIsometryEquiv); ultrapowers of Banach spaces and Darbo's theorem are not.

Difficulty

The radial map $T$ preserves norms and preserves distances between points of the same radius. What has to be shown is that it preserves distances between points on different spheres, $\|f(x)-qf(y)\|=\|x-qy\|$ for $0<q<1$ , using only distances measured on a single sphere. Once this holds, $T$ is a surjective isometry fixing $0$ and Mazur–Ulam gives linearity. The obvious attempt (extend the isometry to a neighbourhood, or use convex-set extension theorems such as Mankiewicz's) fails because the sphere has empty interior. Structural arguments (smoothness, facial structure, explicit duals) cover only special classes of spaces. In general, the maximal defect $\sup|\|f(x)-qf(y)\|-\|x-qy\||$ need not be attained, and no compactness is available in infinite dimensions.

Formalization scope

$X$ and $Y$ are arbitrary types with NormedAddCommGroup, NormedSpace ℝ and CompleteSpace, and Nontrivial (the source's "nonzero"). Universe levels are independent, and no separability or dimension hypothesis is imposed.
The sphere is UnitSphere X := {x // ‖x‖ = 1} with the subtype metric; Isometry f and Function.Surjective f are the hypotheses.
The conclusion is an existential over X ≃ₗᵢ[ℝ] Y (a bijective real-linear isometry) with the five clauses: agreement on the sphere, $T0=0$ , the radial formula, surjectivity, and uniqueness among all X →ₗ[ℝ] Y that agree with $f$ on the sphere. No hypothesis assumes any distance between different radii, so the statement is not trivialized.
Infrastructure a full development needs: Hahn–Banach supporting functionals, Banach-space ultrapowers (or another attainment device), the Kuratowski measure of noncompactness and Darbo's fixed-point theorem, together with Mathlib's Mazur–Ulam theorem. Ultrapowers and Darbo's theorem would be reusable well beyond this mission.

Selected references

D. Tingley, Isometries of the unit sphere, Geom. Dedicata 22 (1987), 371–378. https://doi.org/10.1007/BF00147942
S. Mazur and S. Ulam, Sur les transformations isométriques d'espaces vectoriels normés, C. R. Acad. Sci. Paris 194 (1932), 946–948.
P. Mankiewicz, On extension of isometries in normed linear spaces, Bull. Acad. Polon. Sci. Sér. Sci. Math. Astronom. Phys. 20 (1972).
R. S. Wang, Isometries between the unit spheres of $C_0(\Omega)$ type spaces, Acta Math. Sci. 14 (1994), 82–89. https://doi.org/10.1016/S0252-9602(18)30093-6
G. G. Ding, The isometric extension problem in the unit spheres of $\ell^p(\Gamma)$ $(p>1)$ type spaces, Sci. China Ser. A 46 (2003), 333–338. https://doi.org/10.1360/03ys9035
L. Cheng and Y. Dong, On a generalized Mazur–Ulam question, J. Math. Anal. Appl. 377 (2011), 464–470. https://doi.org/10.1016/j.jmaa.2010.11.025
D.-N. Tan, Extension of isometries on the unit sphere of $L^p$ spaces, Acta Math. Sin. (Engl. Ser.) 28 (2012), 1197–1208. https://doi.org/10.1007/s10114-011-0302-6
R. Tanaka, A further property of spherical isometries, Bull. Aust. Math. Soc. 90 (2014), 304–310. https://doi.org/10.1017/S0004972714000185
F. J. Fernández-Polo and A. M. Peralta, On the extension of isometries between the unit spheres of von Neumann algebras, J. Math. Anal. Appl. 466 (2018), 127–143. https://doi.org/10.1016/j.jmaa.2018.05.062
M. Mori, Tingley's problem through the facial structure of operator algebras, J. Math. Anal. Appl. 466 (2018), 1281–1298. https://doi.org/10.1016/j.jmaa.2018.06.050
M. Mori and N. Ozawa, Mankiewicz's theorem and the Mazur–Ulam property for $C^*$ -algebras, Studia Math. 250 (2020), 265–281. https://doi.org/10.4064/sm180727-14-11
T. Banakh, Every 2-dimensional Banach space has the Mazur–Ulam property, Linear Algebra Appl. 632 (2022), 268–280. https://doi.org/10.1016/j.laa.2021.09.020
G. Darbo, Punti uniti in trasformazioni a codominio non compatto, Rend. Sem. Mat. Univ. Padova 24 (1955), 84–92.
OpenAI, A positive solution to Tingley's problem, OpenAI Math Release preprint, September 23, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-positive-solution-to-Tingleys-problem-September-23-2026/paper.pdf

2 thms2 active usersReviewed

Completed

Functional Analysis·Captain: wurtle

Backward intertwiners and a transitive commutantResearch Paper

Motivation

A closed subspace $\mathcal M$ of a Hilbert space $H$ is hyperinvariant for a bounded operator $S$ if $A\mathcal M\subseteq\mathcal M$ for every operator $A$ commuting with $S$ . The hyperinvariant subspace problem asks whether every bounded nonscalar operator on an infinite-dimensional separable complex Hilbert space has a nonzero proper closed hyperinvariant subspace. It is a strengthening of the invariant subspace problem, closely tied to the theory of transitive operator algebras: $S$ has no such subspace exactly when its commutant $\{S\}'$ is transitive. A related classical question asks whether every unital transitive operator algebra is strongly dense in $B(H)$ ; Arveson's density theorem gives a positive answer when the algebra contains a maximal abelian self-adjoint subalgebra.

Timeline

1967. Arveson proves that a transitive algebra containing a maximal abelian self-adjoint subalgebra is strongly dense in $B(H)$ (doi:10.1215/S0012-7094-67-03467-9).
1972. Douglas and Pearcy relate hyperinvariant subspaces to transitive algebras (doi:10.1307/mmj/1029000793).
1981–1982. Domar describes translation-invariant subspaces of weighted $\ell^p$ and $L^p$ spaces (doi:10.7146/math.scand.a-11926); Grabiner studies unicellular shifts.
1999. Atzmon and Sodin construct completely indecomposable bilateral weighted shifts with spectrum the unit circle, leaving open whether they have proper hyperinvariant subspaces (doi:10.1006/jfan.1999.3454).
2005. Dykema observes that hyperinvariant subspaces of an operator in a von Neumann algebra have projections in that algebra (doi:10.1007/s00208-005-0669-8).
2025–2026. A preprint of Kérchy and Pearcy claiming an equivalence between the invariant and hyperinvariant problems is withdrawn after a counterexample to its Theorem 3 (arXiv:2503.13005); Kérchy studies hyperinvariant subspaces of operators containing unilateral shifts (doi:10.1007/s11785-026-02038-9).

The source of this mission is an OpenAI preprint dated September 27, 2026. A companion OpenAI preprint of the same date reaches the same existence conclusion through invariant projections in an irrational-rotation factor, by a different construction.

Setting

Let $H$ be a complex Hilbert space and $B(H)$ its bounded operators. For $S\in B(H)$ :

the commutant is $\{S\}'=\{A\in B(H):AS=SA\}$ , a unital subalgebra of $B(H)$ ;
$\{S\}'$ is transitive if the only closed subspaces $\mathcal M$ with $A\mathcal M\subseteq\mathcal M$ for all $A\in\{S\}'$ are $\{0\}$ and $H$ ;
$S$ is norm-quasinilpotent if $\|S^n\|^{1/n}\to0$ ;
the strong operator topology on $B(H)$ is the topology of pointwise norm convergence: $A_\lambda\to A$ iff $A_\lambda x\to Ax$ for every $x\in H$ .

Formalization targets

Goal: Corollary 1.2

For every infinite-dimensional separable complex Hilbert space $H$ there is $S\in B(H)$ with

S\neq0,\qquad \lim_{n\to\infty}\|S^n\|^{1/n}=0,\qquad \{S\}'\ \text{transitive},\qquad \{S\}'\neq B(H),\qquad \{S\}'\ \text{strongly closed}.

The Lean statement OAI.BackwardIntertwiners.direct_algebra_corollary is open on the platform. The family statement OAI.Hyperinvariant.main_theorem asserts the same proposition and is included as a reference item.

Significance

Corollary 1.2 gives a negative answer to the hyperinvariant subspace problem on every separable infinite-dimensional Hilbert space, and its commutant is a proper, strongly closed, unital transitive algebra, so it also answers negatively whether every unital transitive operator algebra is strongly dense in $B(H)$ . The construction behind it (Theorem 1.1) is explicit: a weighted shift over the 2-adic odometer whose fibres have only coordinate-tail invariant subspaces, an explicit bound $\|S^n\|\le\exp(-10\lfloor(n+1)^2/4\rfloor)$ , and a bounded commuting operator moving those tails backward. The operator does have many ordinary invariant subspaces, so the invariant subspace problem itself is untouched.

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

Difficulty

Weighted shifts have rich lattices of invariant subspaces, so one must first pin down the invariant subspaces of each fibre (a quadratic weighted-translation criterion in the style of Domar) and then find enough operators in the commutant to destroy every candidate. Multiplication operators and the shift alone leave every fixed tail $L^2(X;K_{\ge h})$ invariant. The essential step is a bounded operator commuting with $S$ that moves tails backward across fibres; this requires opposite logarithmic drifts of the weights at the two ends of the bilateral sequence and one measurable normalization valid on the whole base. Arveson's theorem cannot be used, since the multiplier algebra has infinite multiplicity and is not maximal abelian.

Formalization scope

H is any type with [InnerProductSpace ℂ H] [CompleteSpace H] [SeparableSpace H] and ¬FiniteDimensional ℂ H; the claim is existential in T : H →L[ℂ] H.
commutant T is Subalgebra.centralizer ℂ {T}; TransitiveCommutant T quantifies over closed Submodules invariant under every A with A * T = T * A.
Quasinilpotence is Tendsto (fun n => ‖T ^ n‖ ^ (1 / n)) atTop (𝓝 0) (the $n=0$ term is irrelevant to the limit).
The strong operator topology is TopologicalSpace.induced from the pointwise (product) topology on functions H → H.

A complete development needs vector-valued $L^2$ spaces over the 2-adic integers with Haar measure, weighted shifts and their invariant subspaces, measurable fields of projections, and transport to an arbitrary separable Hilbert space by a unitary. Contributions formalizing Theorem 1.1 (the construction), Lemma 2.1 (weighted translation criterion), Proposition 4.3 (a bounded backward intertwiner) and Lemma 5.1 (strict descent) are welcome.

Selected references

OpenAI, Backward intertwiners and a transitive commutant, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Backward-intertwiners-and-a-transitive-commutant-September-27-2026/paper.pdf
OpenAI, Invariant-projection counterexamples for every irrational rotation, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Invariant-projection-counterexamples-for-every-irrational-rotation-September-27-2026/paper.pdf
W. B. Arveson, A density theorem for operator algebras, Duke Math. J., 1967. https://doi.org/10.1215/S0012-7094-67-03467-9
R. G. Douglas, C. Pearcy, Hyperinvariant subspaces and transitive algebras, Michigan Math. J., 1972. https://doi.org/10.1307/mmj/1029000793
Y. Domar, Translation invariant subspaces of weighted $l^p$ and $L^p$ spaces, Math. Scand., 1981. https://doi.org/10.7146/math.scand.a-11926
A. Atzmon, M. Sodin, Completely indecomposable operators and a uniqueness theorem of Cartwright–Levinson type, J. Funct. Anal., 1999. https://doi.org/10.1006/jfan.1999.3454
K. Dykema, Hyperinvariant subspaces for some B-circular operators, Math. Ann., 2005. https://doi.org/10.1007/s00208-005-0669-8
L. Kérchy, C. Pearcy, Hyperinvariant subspaces of block-triangular operators on Hilbert space, withdrawn preprint, 2025. https://arxiv.org/abs/2503.13005

23 thms2 active usersReviewed

Completed

Mathematical Physics Probability·Captain: wurtle

A radial continuum phase transition with algebraic decayResearch Paper

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

14 thms2 active usersReviewed

Completed

Mathematical Physics Probability·Captain: wurtle

A continuum temperature singularity for a radial pair potentialResearch Paper

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

$\phi(r)\to+\infty$ as $r\downarrow0$ ;
$\phi\le-a<0$ on some interval $[r_1,r_2]$ with $0<r_1<r_2$ ;
$\int_R^\infty r^2|\phi(r)|\,dr<\infty$ for some $R$ ;
(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

5 thms2 active usersReviewed

Completed

Dynamical Systems·Captain: wurtle

Boundedness and persistence of weakly reversible mass-action systemsResearch Paper

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

2 thms2 active usersReviewed

Completed

Discrete Geometry Functional Analysis·Captain: wurtle

A doubling Hilbert subset with no finite-dimensional bi-Lipschitz embeddingResearch Paper

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

25 thms2 active usersReviewed

Completed

Discrete Geometry·Captain: wurtle

Petty’s projection-volume conjecture in dimensions at least fourResearch Paper

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

8 thms2 active usersReviewed

Completed

Number Theory·Captain: wurtle

The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane Re(s) > 7/8Research Paper

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).

13 thms2 active usersReviewed

Operations Research Probability Stochastic Systems+1·Captain: mikedeng1

Some Useful Functions for Functional Limit Theorems 3: The First-Passage-Time Map Is M₁-Continuous and J₁-Continuous at Strictly Increasing PathsResearch Paper

Why first passage times need a continuity theorem

Functional limit theorems in queueing and applied probability are rarely proved from scratch. A limit theorem is established once for a primitive process, such as a random walk, a cumulative input or a renewal-reward process, and then transferred to the quantities of interest through the continuous mapping theorem: if $X_n \Rightarrow X$ in a function space and $f$ is continuous at almost every path of $X$ , then $f(X_n) \Rightarrow f(X)$ . The method works only if the functions in use are known to be continuous, and in which topology.

Ward Whitt's 1980 paper supplies these facts for composition, addition, the supremum, the reflecting barrier, the inverse or first passage time, and time reversal. This mission covers §7, the first passage time. Its role in applications is direct: the counting process of a renewal process is the first passage time of the partial-sum process. A limit theorem for cumulative work can therefore yield one for the number of completed jobs, and a limit theorem for a cumulative input can yield one for the time it takes to reach a level, when the mapping theorem's hypotheses hold.

Timeline. Skorohod (1956) introduced the topologies $J_1$ and $M_1$ on the space $D$ of right-continuous paths with left limits. Vervaat (1972) studied functional central limit theorems for processes with positive drift and their inverses, and Whitt (1971) studied weak convergence of first passage time processes. Whitt's 1980 paper restates $M_1$ continuity (Theorem 7.1) and adds the $J_1$ result: the map is continuous at every strictly increasing path (Theorem 7.2), although it is not $J_1$ -continuous on its whole domain.

Setting

A path is a function $x : [0,\infty) \to \mathbb R$ . It belongs to $D = D([0,\infty),\mathbb R)$ when it is right-continuous and has a left limit at every $t > 0$ .

$J_1$ convergence. On a compact interval $[0,b]$ , $x_n \to x$ in $J_1$ when there are increasing homeomorphisms $\lambda_n$ of $[0,b]$ with $\sup_t |\lambda_n(t) - t| \to 0$ and $\sup_t |x_n(t) - x(\lambda_n(t))| \to 0$ . On $[0,\infty)$ this is required on $[0,b]$ for every $b$ at which $x$ is continuous.
$U$ convergence. Uniform convergence on compact subintervals.
$M_1$ convergence. The completed graph of $x$ on $[0,b]$ adds to the graph the vertical segment joining $x(t-)$ and $x(t)$ at each jump. $x_n \to x$ in $M_1$ when the completed graphs admit parametric representations (continuous, order-preserving maps from $[0,1]$ onto the completed graph) that are uniformly close in both time and space.
The supremum. $x^{\uparrow}(t) = \sup_{0 \le s \le t} x(s)$ .
The domain $E$ . The set of $x \in D$ that are unbounded above and have $x(0) \ge 0$ .
First passage time. For $x \in E$ ,

x^{-1}(t) = \inf\{s \ge 0 : x(s) > t\}, \qquad t \ge 0.

$D_0$ . The nondecreasing paths in $D$ , and $C$ the continuous ones.

Formalization targets

Goal: Theorem 7.2, continuity clause

If $x_n, x \in E$ , $x$ is strictly increasing, and $x_n \to x$ in $J_1$ , then

x_n^{-1} \to x^{-1} \quad (J_1).

The theorem says that every strictly increasing path is a continuity point of the first passage time map for $J_1$ . It fixes no constants, so a sharper variant of a milestone does not invalidate it.

Milestones

$J_1$ convergence implies $M_1$ convergence (§6, p. 80).
The supremum map is $M_1$ -continuous on paths with $x(0) \ge 0$ (§6, p. 80, as used in the proof of Theorem 7.1).
$x \in E$ implies $x^{-1} \in E \cap D_0([0,\infty),[0,\infty))$ (§7, p. 82).
$x^{\uparrow} \in E$ and $(x^{\uparrow})^{-1} = x^{-1}$ (proof of Theorem 7.1).
Theorem 7.1. If $x_n, x \in E$ and $x_n \to x$ in $M_1$ , then $x_n^{-1} \to x^{-1}$ in $M_1$ .
For strictly increasing $x \in E$ , $x^{-1}$ is continuous with $x^{-1}(0) = 0$ .
$M_1$ convergence to a continuous limit starting at $0$ is $U$ convergence.
$U$ convergence implies $J_1$ convergence.
Theorem 7.4. If $c_n \to \infty$ , $x_n \in E$ , $c_n(x_n^{\uparrow} - e) \to x$ and $c_n(x_n^{-1} - e) \to -x$ in $J_1$ , then $x \in C$ .

Significance

The result. Theorem 7.2 lets $J_1$ functional limit theorems pass to first passage times when the limit has strictly increasing paths. The typical case is the fluid limit $x(t) = \mu t$ of a cumulative process, with $\mu>0$ . Together with the composition results of §3, it supports Theorem 7.3's centered inverse limit: if $c_n \to \infty$ , $x_n \in E$ , $x(0)=0$ , $x$ has no positive jumps, and $c_n(x_n-e) \to x$ in $J_1$ , then $c_n(x_n^{-1}-e) \to -x$ in $J_1$ . This is one step from a central limit theorem for partial sums to one for counting processes. Theorem 7.4 shows a limitation: convergence of both the centered supremum and the centered inverse in $J_1$ forces a continuous limit.

Formalizing it. The results are proved and classical, but none of them has a machine-checked proof. The mission produces the $M_1$ topology on $D([0,\infty),\mathbb R)$ in Lean, the first passage time map with its basic properties, and the comparison between $J_1$ , $M_1$ and $U$ . That infrastructure is reused by every later formalization that goes through counting processes or the $M_1$ topology, including the planned wave of §§3–7 corollaries in this series.

Difficulty

The first passage time map is not $J_1$ -continuous. On p. 82 the paper gives paths $x_n \to x$ in $J_1$ whose inverses converge only in $M_1$ : a flat stretch of the limit becomes a jump of $x^{-1}$ , which the inverses of the approximating paths approach through two separate jumps. Inverting the time changes $\lambda_n$ of the $J_1$ convergence cannot handle that split, because $J_1$ matches jumps one to one. The hypothesis that $x$ is strictly increasing excludes flat stretches of the limit. The technical weight lies in completed graphs and their parametric representations, which Mathlib does not have, and in the restriction to compact intervals at continuity points of the limit.

Formalization scope

Paths are total functions $\mathbb R \to \mathbb R$ . Only $[0,\infty)$ matters, and every statement is on Ici 0. All convergences are sequential, which is equivalent because the spaces are metrizable (Theorem 2.6). Membership of every path in $D$ is part of each convergence.
$J_1$ is the shared layer of the series: the metric (2.1) with $[0,\infty]$ -valued distances, extended to $[0,\infty)$ through restrictions to $[a,b]$ whose endpoints are continuity points or endpoints.
$M_1$ is not defined in the paper. The mission defines it with the convention $x(0-) := 0$ at the origin, so the completed graph on $[0,b]$ starts with the segment from $(0,0)$ to $(0,x(0))$ . With the convention $x(0-) = x(0)$ , Theorem 7.1 is false. For $x(s) = (s-1)^+$ and $x_n = x + 1/n$ , $x_n^{-1}$ jumps from $0$ to $1$ at $t = 1/n$ while $x^{-1}(0) = 1$ . The convention is Whitt's later $M_1'$ . Two milestones carry a hypothesis that this convention forces, and each says so: the supremum milestone requires $x_n(0), x(0) \ge 0$ (as on $E$ ), and the $M_1 \Rightarrow U$ milestone requires $x(0) = 0$ . The goal, which is stated in $J_1$ , does not depend on the convention.
$x^{-1}$ is a real infimum. Its set is nonempty because paths in $E$ are unbounded above, so every statement that uses $x^{-1}$ assumes membership in $E$ . The inequality $x(s) > t$ is strict, as on the page.
Omitted. The measurability clause of Theorem 7.2 refers to the Borel σ-field of $J_1$ , which the series does not build, and it is not stated. Replacing it by measurability for the product σ-algebra would be a different statement. The second clause of the §6 sentence on $D_0$ is also not stated.
Ruled out. A formalization in which $x^{-1}$ is applied outside $E$ (giving the junk value $0$ ), or in which $J_1$ convergence omits membership in $D$ (making the restriction clause vacuous), would trivialize the goal. Both are excluded.

Contributions welcome: the general theory of parametric representations (existence, and the $M_1$ comparison with $J_1$ and $U$ ), which is reusable for any $M_1$ result. Alternative proofs of Theorem 7.2 that avoid $M_1$ are also welcome.

Selected references

W. Whitt, Some Useful Functions for Functional Limit Theorems, Mathematics of Operations Research 5(1), 1980, 67–85. https://doi.org/10.1287/moor.5.1.67
A. V. Skorohod, Limit theorems for stochastic processes, Theory of Probability and Its Applications 1(3), 1956, 261–290. https://doi.org/10.1137/1101022
W. Whitt, Weak convergence of first passage time processes, Journal of Applied Probability 8(2), 1971, 417–422. https://doi.org/10.2307/3211913
W. Vervaat, Functional central limit theorems for processes with positive drift and their inverses, Zeitschrift für Wahrscheinlichkeitstheorie 23, 1972, 245–253. https://doi.org/10.1007/BF00532510
W. Whitt, Stochastic-Process Limits, Springer, 2002, §13.6. https://doi.org/10.1007/b97479

14 thms2 active usersReviewed

Completed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

The G/GI/N Queue in the Halfin–Whitt Regime 2: The Diffusion-Limit Equation Is Equivalent to a Renewal-Function Equation, Which Has a Unique Càdlàg SolutionResearch Paper

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

(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.
(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)$ .
The identity $F_e(t)+\int_0^tF_e(t-s)\,dM(s)=t$ for $t\ge0$ (p. 30).
(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.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).

11 thms2 active usersReviewed

Algorithmic Game Theory Operations Research Optimization·Captain: mikedeng1

Cooperative Fuzzy Games 3: The Diagonal Formula Is the Unique Continuous Linear Pareto-Optimal, Symmetric and Atomic Value of Smooth Fuzzy GamesResearch Paper

Motivation

A value for cooperative games assigns to every game a payoff vector, chosen by axioms rather than by bargaining. Shapley's value (1953) does this for finite games with side payments, and Aumann and Shapley (Values of Non-Atomic Games, 1974) extended it to games with a continuum of players, where it is given by a diagonal formula: a player's value is the average of their marginal worth along the diagonal from the empty coalition to the grand coalition. Aubin's Cooperative Fuzzy Games (Math. Oper. Res. 6(1), 1981, doi:10.1287/moor.6.1.1) brings this formula to finitely many players who may participate in coalitions at fractional rates, and characterises it by axioms in §8.

The result matters in cost allocation: the Aumann–Shapley price mechanism (Billera, Heath and Raanan 1978; Mirman and Tauman 1982) shares the cost of a bundle of products by exactly this diagonal formula, applied to a smooth cost function of the quantities produced. Theorem 8.1 is the finite-player, fuzzy-coalition version of the axiomatic justification behind that mechanism.

Setting

There are $n$ players $N=\{1,\dots,n\}$ . A fuzzy coalition is a vector $\tau\in[0,1]^n$ , where $\tau_i$ is the rate at which player $i$ participates; an ordinary coalition $A$ is its indicator vector $\tau^A$ , and $\tau^N=(1,\dots,1)$ is the grand coalition.

A smooth fuzzy game is a coalitional worth function $v:[0,1]^n\to\mathbb R$ that is continuously differentiable and satisfies $v(0)=0$ . These form the space $V^n$ , a Banach space under the $C^1$ norm $\sup_{[0,1]^n}|v|+\sup_{[0,1]^n}\|Dv\|$ .

A sequence of fuzzy values is a family of continuous linear operators $\psi_n:V^n\to\mathbb R^n$ satisfying three axioms.

Pareto optimality: $\sum_{i\in N}(\psi_n v)_i=v(\tau^N)$ .
Symmetry: for a permutation $\theta$ of $N$ , with $(\theta^*v)(\tau)=v(\tau_{\theta^{-1}(1)},\dots,\tau_{\theta^{-1}(n)})$ and $(\theta^*c)_i=c_{\theta(i)}$ , one has $\psi_n(\theta^*v)=\theta^*(\psi_n v)$ .
Atomicity: a partition $P=\{A_1,\dots,A_m\}$ of $N$ into nonempty types sends a fuzzy coalition $\sigma\in[0,1]^m$ of types to the fuzzy coalition $(P\cdot\sigma)_i=\sigma_j$ for $i\in A_j$ , and an $n$ -player game $v$ to the $m$ -type game $(P^*v)(\sigma)=v(P\cdot\sigma)$ . The axiom requires $\psi_m(P^*v)_j=\sum_{i\in A_j}(\psi_nv)_i$ : a type receives what its members receive.

The core of a game $v$ with side payments is the set of $c\in\mathbb R^n$ with $\sum_ic_i=v(\tau^N)$ and $\sum_i\tau_ic_i\ge v(\tau)$ for every $\tau\in[0,1]^n$ (§2 (4)).

Formalization targets

Goal: Theorem 8.1

There exists a unique sequence of fuzzy values, given by the diagonal formula

\psi_n v=\int_0^1 Dv(t\tau^N)\,dt\qquad(v\in V^n).\tag{4}

For every linear $A:\mathbb R^m\to\mathbb R^n$ with $A\tau^M=\tau^N$ ,

\psi_m(v\circ A)=A^*\psi_n v\qquad(v\in V^n),\tag{5}

where $A^*$ is the transpose of $A$ . If $v\in V^n$ is concave and positively homogeneous, then $\psi_nv$ is the unique element of the core.

Milestones

These are the steps of the proof in the paper (pp. 10–11), in attack order:

the maps (4) are linear, continuous and satisfy (5);
they satisfy the Pareto optimality, symmetry and atomicity axioms;
the monomials $\tau_1^{k_1}\cdots\tau_n^{k_n}$ ( $k\ne0$ ) span a dense subspace of $V^n$ ;
Pareto optimality and symmetry force $\psi_n(\tau_1\cdots\tau_n)=\frac1n\tau^N$ ;
the three axioms force $(\psi_n\tau^k)_i=k_i/(k_1+\dots+k_n)$ , which is also the value of (4);
for positively homogeneous $v$ , $Dv(t\tau^N)=Dv(\tau^N)$ , so $\psi_nv=Dv(\tau^N)$ ;
(Remark 8.2) $\psi_n$ applied to Owen's multilinear extension of a game with side payments is its Shapley value.

Significance

The result. Theorem 8.1 singles out the diagonal formula among all ways of valuing smooth fuzzy games, using only efficiency, anonymity and invariance under merging players into types. Property (5) shows that the value transforms correctly under every linear change of coordinates fixing the grand coalition. The core statement links the value to stability: for concave homogeneous games (for instance, market games), the value is the only allocation no fuzzy coalition can improve upon. Through Owen's extension, the classical Shapley value is recovered as a special case.

Formalizing it. The theorem is proved in the paper, briefly, and its proof leans on an unproved density claim and on a short appeal to atomicity. A formalization makes the uniqueness argument complete: in particular, how atomicity, which only allows nonempty types, determines the value of a monomial in which some player has exponent $0$ . No machine-checked version of the Aumann–Shapley diagonal formula or its axiomatisation is known to us. Mathlib has the Stone–Weierstrass theorem for continuous functions but no $C^1$ density of polynomials on a cube; the latter is reusable well beyond game theory.

Difficulty

Existence (milestones 1–2) is calculus: differentiation under the integral sign and the chain rule. The difficulty sits in uniqueness. The first idea, computing $\psi_n$ on monomials by symmetry alone, fails as soon as the exponents differ: symmetry relates only games that are permutations of each other. Atomicity relates games with different numbers of players, and its types must be nonempty, so a player with exponent $0$ cannot simply be merged away. Uniqueness on all of $V^n$ then needs density of polynomials in the $C^1$ norm, not merely the uniform norm: without continuity in the $C^1$ norm, linear maps that agree on polynomials can disagree elsewhere, and the theorem is false.

Formalization scope

Players are Fin n, fuzzy coalitions and payoff vectors are Fin n → ℝ, and the cube is Set.Icc 0 1 in the product order.
$V^n$ is a submodule of functions on all of $\mathbb R^n$ that are $C^1$ there and vanish at $0$ . Every $C^1$ function on the cube extends to such a function, and only values and derivatives on the cube enter the norm and the axioms. The global domain makes $v\circ A$ meaningful for every linear $A$ .
"Continuous" means $\|\psi_nv\|\le C\,\|v\|_{C^1}$ with the $C^1$ seminorm of the cube (sup norm on $\mathbb R^n$ , operator norm on $Dv$ ). This is the continuity of the Banach space $V^n$ . Continuity for the uniform norm alone would make formula (4) discontinuous, and dropping continuity would make uniqueness false.
The axioms are stated for all $n\ge1$ ; the paper's " $\forall n\in N$ " in the symmetry axiom is read as $n\ge1$ . In the atomicity axiom (3), the paper's " $\forall v\in V^m$ " is read as $v\in V^n$ , because $P^*v$ is defined by (2) for an $n$ -player game. A partition into nonempty types is a surjection Fin n → Fin m. The symbols $\tau_{\theta-1(i)}$ are $\tau_{\theta^{-1}(i)}$ .
The games $\theta^*v$ , $P^*v$ and $v\circ A$ are passed as elements of $V^n$ , $V^m$ together with their defining identities; they always lie in those spaces.
In the core statement, concavity and positive homogeneity ( $v(t\tau)=tv(\tau)$ for $t>0$ , $\tau\ge0$ ) are required on the orthant $\mathbb R^n_+$ , to which §2 (2) extends $v$ ; the core quantifies over the cube, as in §2 (4)(a). The paper's " $V^N$ " there is $V^n$ .
Remark 8.2 is stated for games defined on all coalitions with $v(\emptyset)=0$ , since formula (7) uses $v(A\setminus\{i\})$ for every $A$ . The Shapley value is the published platform definition Supermodularity.Cooperative.ShapleyValue, whose formula is (7) re-indexed by $S=A\setminus\{i\}$ . The Cornet extension of the same remark is left out because it is not $C^1$ on the boundary of the cube.
A trivializing reading is ruled out: the goal asserts both existence of a sequence satisfying all axioms with $C^1$ continuity and uniqueness among all such sequences, so neither an empty axiom system nor a vacuous continuity requirement makes it hold.

Infrastructure that a complete development needs, and that is welcome as separate contributions: $C^1$ approximation of functions on a cube by polynomials; differentiation under the integral sign for the diagonal integral; Euler's identity and the supergradient inequality for concave homogeneous $C^1$ functions.

Selected references

J.-P. Aubin, Cooperative Fuzzy Games, Mathematics of Operations Research 6(1) (1981) 1–13. https://doi.org/10.1287/moor.6.1.1
R. J. Aumann and L. S. Shapley, Values of Non-Atomic Games, Princeton University Press, 1974. https://doi.org/10.1515/9781400867080
L. S. Shapley, A Value for n-Person Games, in Contributions to the Theory of Games II, Annals of Mathematics Studies 28 (1953) 307–317. https://doi.org/10.1515/9781400881970-018
G. Owen, Multilinear Extensions of Games, Management Science 18(5) (1972) P64–P79. https://doi.org/10.1287/mnsc.18.5.64
L. J. Billera, D. C. Heath and J. Raanan, Internal Telephone Billing Rates — A Novel Application of Non-Atomic Game Theory, Operations Research 26(6) (1978) 956–965. https://doi.org/10.1287/opre.26.6.956
L. J. Mirman and Y. Tauman, Demand Compatible Equitable Cost Sharing Prices, Mathematics of Operations Research 7(1) (1982) 40–56. https://doi.org/10.1287/moor.7.1.40

12 thms2 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Implicit Renewal Theory and Tails of Solutions of Random Equations 3: Rate of Approach — t^κP(R > t) Equals C₊ Minus a Contour Integral Plus O(t^{−β/2})Research Paper

Motivation

Random equations of the form $R \overset{\mathcal L}{=} \Psi(R)$ , with $\Psi$ a random function independent of $R$ , describe the stationary laws of many stochastic recursions: perpetuities in insurance and finance, the stationary law of ARCH-type volatility models, random difference equations $R = Q + MR$ , and the stationary workload of certain queueing and storage models. When $\Psi(t)$ acts like multiplication by a random variable $M$ for large $|t|$ , and $\mathbf E|M|^\kappa = 1$ for some $\kappa > 0$ , the solution has power-law tails: $P(R > t) \sim C_+ t^{-\kappa}$ . This is the implicit renewal theorem of Goldie (Ann. Appl. Probab. 1991, Theorem 2.3), which recovers and extends Kesten's 1973 theorem on random difference equations.

A tail asymptotic alone says nothing about how fast $t^\kappa P(R > t)$ approaches $C_+$ . For tail estimation, for the accuracy of extreme-quantile approximations used in risk management, and for second-order regular variation, the rate matters. Section 3 of the same paper answers this: under an exponential moment condition slightly beyond the Cramér condition, the error has an explicit second-order term determined by the zeros of $1 - \hat\eta$ , where $\eta$ is a tilted law of $\log M$ , plus a remainder $O(t^{-\beta/2})$ .

Timeline: Kesten (1973) proved power tails for random difference equations; Grincevičius (1975) developed an implicit-renewal approach; Stone (1966) decomposed exponentially decaying renewal measures into an absolutely continuous part with explicit asymptotics and a finite part; Ganelius (1962) proved the Tauberian remainder theorem used to unsmooth; Goldie (1991) combined these into the rate result formalized here.

Setting

Let $(\Omega, \mathcal A, P)$ be a probability space carrying independent real random variables $M \ge 0$ and $R$ . Fix $\kappa > 0$ with $\mathbf E M^\kappa = 1$ (the Cramér condition, (2.3)) and $\beta > 0$ with $\mathbf E M^{\kappa+\beta} < \infty$ (3.3).

The tilted law of $M$ is the probability measure $\eta(dx) = e^{\kappa x} P(\log M \in dx)$ on $\mathbb R$ , computed on $\{M > 0\}$ . Its transforms are $\tilde\eta(\beta) = \int e^{\beta t}\eta(dt)$ for real $\beta$ and $\hat\eta(\theta) = \int e^{i\theta t}\eta(dt)$ for complex $\theta$ ; for a function $f$ , $\hat f(\theta) = \int e^{i\theta t} f(t)\,dt$ . Convolution powers are $\eta^{(0)} = \delta_0$ , $\eta^{(n+1)} = \eta^{(n)} * \eta$ , and the renewal measure is $\nu = \sum_{n \ge 0}\eta^{(n)}$ . A law is spread out when some convolution power has a nonzero absolutely continuous component; (3.4) asks this of the conditional law of $\log M$ given $M \ne 0$ .

Set $m = \mathbf E M^\kappa \log M$ and

g_1(t) = e^{\kappa t}\big(P(R > e^t) - P(MR > e^t)\big), \qquad C_+ = \frac1m\int_0^\infty \big(P(R > t) - P(MR > t)\big) t^{\kappa - 1}\,dt,

with $g_{-1}$ and $C_-$ defined the same way for the lower tail. The strip is $D = \{\theta : -\beta < \Im\theta < 0\}$ , and $\mathscr C$ denotes a positively oriented closed contour in $D$ enclosing every zero of $1 - \hat\eta$ in $D$ .

Formalization targets

Goal: Theorem 3.2

If, in addition, $\eta^{(n_0)} = (1 - \delta)\varphi_0 + \delta\varphi_1$ for some $n_0$ , with $\delta \in [0, 1)$ , $\varphi_0$ absolutely continuous and $\delta\tilde\varphi_1(\beta) < 1$ , and $\hat\eta \ne 1$ on $\Im\theta = -\beta$ , then $\int_0^\infty |P(R > t) - P(MR > t)|\,t^{\kappa+\beta-1}dt < \infty$ implies

t^\kappa P(R > t) = C_+ - \frac1{2\pi}\,\Re\oint_{\mathscr C} e^{-i\theta\log t}\,\frac{\hat g_1(\theta)}{1 - \hat\eta(\theta)}\,d\theta + O(t^{-\beta/2}), \qquad t \to \infty,

with the analogous statement for $P(R < -t)$ ; and if $R \overset{\mathcal L}{=} \Psi(R)$ with $R$ independent of $(M, \Psi)$ , the integrability hypotheses may be replaced by $\mathbf E|(\Psi(R)^\pm)^{\kappa+\beta} - ((MR)^\pm)^{\kappa+\beta}| < \infty$ . The theorem also asserts that $\eta$ is a spread-out probability measure.

Milestones

Lemma 9.5: Stone's inversion formula for the density of $\sum_n \chi * \mu^{(n)}$ .
Theorem 3.1: the renewal measure splits as $\nu = \nu_0 + \nu_1$ , $\nu_1$ finite with $\tilde\nu_1(\beta) < \infty$ , $\nu_0$ with continuous bounded density

p(t) = \frac1m - \frac1{2\pi}\oint_{\mathscr C} e^{-i\theta t}\frac{d\theta}{1 - \hat\eta(\theta)} + o(e^{-\beta t}).

(9.23) and (9.24): the smoothed identity and the smoothed rate $K * \Re r_1(t) = o(e^{-\beta t})$ for the kernel $K(t) = be^{-bt}\mathbf 1_{t>0}$ .
Theorem 9.6: the Beurling–Ganelius Tauberian remainder theorem.

Significance

Theorem 3.2 turns the first-order tail asymptotic of the implicit renewal theorem into an expansion: the second-order terms are finitely many terms of the form $(\log t)^{j-1}t^{\Im\theta_l}$ times oscillating factors, one family for each zero $\theta_l$ of $1 - \hat\eta$ with $0 < -\Im\theta_l \le \beta/2$ , and their form does not depend on the unknown law of $R$ . It applies to every random equation covered by the implicit renewal theorem once the stronger moment condition holds, including perpetuities and the random difference equation. Theorem 3.1 is of independent use: it is an explicit-rate version of Stone's decomposition of renewal measures with exponential moments.

The results are proved in the paper; none is formalized. Mathlib has the Fourier transform on the real line, convolution of measures, and rectangle Cauchy theorems, but no renewal theory, no Stone decomposition, and no Tauberian remainder theorem. Formalizing the mission produces a machine-checked renewal density expansion and a checked Beurling–Ganelius theorem, both reusable outside this paper.

Difficulty

The first-order theorem follows from the key renewal theorem applied to $r(t) = e^{\kappa t}P(R > e^t)$ . That route gives no rate: the key renewal theorem has no remainder, and the integrability hypothesis yields $e^{\beta t}g_1 \in L^1$ but not $e^{\beta t}g_1(t) = o(1)$ , so a remainder cannot be read off directly even with a spread-out step law. The proof therefore works with a smoothed version of $r$ , where Stone's decomposition with the contour expansion of the renewal density gives an $o(e^{-\beta t})$ remainder, and has to unsmooth. Unsmoothing is the Tauberian step: it requires a one-sided regularity condition on the unsmoothed function, verified for $r$ and for the contour term, and costs half the exponent. The contour expansion itself requires showing that $1 - \hat\eta$ has finitely many zeros in the strip and handling their orders through residues.

Formalization scope

All objects live in the namespace GoldieRenewal.Rates. Random variables are measurable maps $\Omega \to \mathbb R$ on a probability space; $M \ge 0$ almost surely; independence is IndepFun. Tail probabilities are real numbers P.real {ω | t < R ω}. Moments such as $\mathbf E M^{\kappa+\beta}$ and $\tilde\mu(\beta)$ are lower Lebesgue integrals in $[0, \infty]$ . The transforms $\hat\mu$ and $\hat f$ are Bochner integrals at complex arguments with the $+i$ sign of the paper. Asymptotic statements use Asymptotics.IsBigO and IsLittleO along atTop.

The contour. A contour $\mathscr C$ is the positively oriented boundary of an axis-parallel rectangle whose closure lies in $D$ and whose interior contains every zero of $1 - \hat\eta$ in $D$ ; the contour integral is the sum of the four edge integrals (RectangleIntegral, from the published ResidueCalcOnRectangles_defs). Expansions are stated for every such rectangle.

The variable in (3.8) and (3.10). The paper prints $e^{-i\theta t}$ in the contour term, but its proof establishes the expansion in the logarithmic variable $s = \log t$ . The targets are stated with $e^{-i\theta\log t}$ , which is what the proof gives. With the printed $e^{-i\theta t}$ the contour term would decay exponentially and the statement would claim $t^\kappa P(R > t) = C_+ + O(t^{-\beta/2})$ , which is not what is proved. Hypothesis (3.7) is printed with $P(R > -t)$ and is read with $P(R > t)$ .

Excluded trivializations. The contour term may not be dropped; the hypotheses do not exclude zeros of $1 - \hat\eta$ in $D$ ; and the contour must enclose all zeros in the strip, not a chosen subset.

Theorem 9.6 is stated for a complex-valued kernel and a finite strip width $a$ ; the application with $a = \infty$ follows by restricting to a finite strip. Lemma 9.5 carries an added hypothesis that the density of $\chi$ has compact support, which the proof uses and the application provides.

Contributions welcome: renewal-measure infrastructure (convolution powers, Blackwell-type limits), Fourier analysis of measures at complex arguments, residue computations on rectangles, and Tauberian remainder theory. Each is reusable well beyond this paper.

Selected references

C. M. Goldie, Implicit renewal theory and tails of solutions of random equations, Ann. Appl. Probab. 1(1):126–166, 1991. https://doi.org/10.1214/aoap/1177005985
H. Kesten, Random difference equations and renewal theory for products of random matrices, Acta Math. 131:207–248, 1973. https://doi.org/10.1007/BF02392040
C. Stone, On absolutely continuous components and renewal theory, Ann. Math. Statist. 37(1):271–275, 1966. https://doi.org/10.1214/aoms/1177699617
T. H. Ganelius, The remainder in Wiener's Tauberian theorem, Acta Univ. Gothoburgensis, Mathematica Gothoburgensia 1, 1962 (cited in Goldie 1991).
A. K. Grincevičius, One limit distribution for a random walk on the line, Lithuanian Math. J. 15:580–589, 1975 (cited in Goldie 1991).

12 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Probability·Captain: mikedeng1

Values of Large Games II: Oceanic Games 2: Oceanic Values Are Limits of Values of Finite Weighted Majority GamesResearch Paper

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.

8 thms2 active usersReviewed

Completed

Harmonic Analysis Probability·Captain: mikedeng1

Distribution Function Inequalities for Martingales 8: For Concave Φ, EΦ(Σ z_k) ≤ 2·EΦ(Σ E(z_k | 𝒜_{k−1})) for Nonnegative z_kResearch Paper

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

(§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)$ .
(20.2) The truncated inequality

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

(§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

6 thms2 active usersReviewed

Completed

Harmonic Analysis Probability·Captain: mikedeng1

Distribution Function Inequalities for Martingales 7: A Martingale of Bounded Mean Oscillation Satisfies E exp(tS²(f)) ≤ (1 − t)⁻¹Research Paper

Motivation

A martingale can have individually well behaved increments while the sum of their squares remains large on rare sample paths. The square function records that accumulated variation. Bounds on its distribution tell probabilists how much a martingale can fluctuate even when a terminal value alone gives little pathwise information. In Section 19 of Distribution Function Inequalities for Martingales, D. L. Burkholder studies a conditional tail bound for squared increments and obtains an explicit exponential moment for the entire square function. The result is Theorem 19.1, with a one-parameter constant fixed exactly as $(1-t)^{-1}$ for $0<t<1$ (Burkholder 1973, p. 37).

The paper calls the linear span of martingales satisfying this normalized tail condition BMO, and notes that bounded martingales belong to it after a suitable scaling. It connects this martingale notion to bounded mean oscillation of functions, introduced by John and Nirenberg, and to the surrounding work on the duality with $H^1$ (Burkholder 1973, p. 38). The mission isolates the article's concrete exponential estimate, which can be read and used without developing the whole later theory of BMO.

Setting

Let $(\Omega,\mathcal A,P)$ be a probability space and let $(\mathcal A_n)_{n\ge0}$ be an increasing sequence of sub-sigma-fields. A real martingale is written $f=(f_n)_{n\ge1}$ relative to $(\mathcal A_n)_{n\ge1}$ . Following the article's convention, put $f_0=0$ for its difference sequence, so $d_1=f_1$ and $d_n=f_n-f_{n-1}$ for $n\ge2$ . The partial square function and the full square function are

S_n(f)=\left(\sum_{k=1}^{n}d_k^2\right)^{1/2},\qquad S(f)=\left(\sum_{k=1}^{\infty}d_k^2\right)^{1/2}=\sup_{n\ge1}S_n(f).

These are nonnegative random variables and the full one may initially take the value $+\infty$ . The paper fixes this notation in Section 1 (Burkholder 1973, p. 20).

The condition used here is a bound on the expected squared-increment tail after conditioning on the information $\mathcal A_n$ available at time $n$ :

\mathbf E\left[\sum_{k=n}^{\infty}d_k^2\,\middle|\,\mathcal A_n\right]\le1\quad\text{almost surely, for every }n\ge1.\tag{19.1}

The sum starts at $k=n$ , including $d_n^2$ , and the conditioning sigma-field is $\mathcal A_n$ . Both indices matter; shifting either changes the hypothesis. The value $1$ is a normalization, not an unnamed bound whose choice can depend on the martingale (Burkholder 1973, p. 37).

Formalization targets

Tail integral estimate

The first milestone is the distribution estimate displayed in the proof of Theorem 19.1. For every $a>0$ ,

\int_a^\infty P\big(S(f)^2>x\big)\,dx\le P\big(S(f)^2>a\big).

It records exactly the quantitative link between the conditional hypothesis and the distribution of the full square function (Burkholder 1973, p. 37).

Exponential-moment lemma

The second milestone is Lemma 18.1. For a nonnegative measurable $g$ and a constant $\alpha>0$ , suppose

\int_a^\infty P(g>x)\,dx\le\alpha P(g>a)\quad(a>0).

Then $g$ has an exponential moment at every $0<t<\alpha^{-1}$ , bounded by $(1-\alpha t)^{-1}$ . The lemma is stated for any probability space and any nonnegative measurable $g$ , so it is reusable beyond martingale square functions (Burkholder 1973, p. 36).

Goal: Theorem 19.1

Under (19.1), the goal is the article's explicit estimate

\mathbf E\big[\exp(tS(f)^2)\big]\le(1-t)^{-1},\qquad 0<t<1.\tag{19.2}

In particular, $S(f)$ is finite almost surely. The exact coefficient and the whole open interval for $t$ are part of the target (Burkholder 1973, p. 37).

Significance

The conclusion gives more than finiteness of the square function or any fixed moment: one conditional second-moment tail condition yields a family of exponential bounds for its square. The paper points out that bounded martingales meet the condition after scaling, placing a familiar class within this BMO framework (Burkholder 1973, pp. 37–38). The constant $(1-t)^{-1}$ makes the normalization of (19.1) visible and allows later users to choose a value of $t$ without recovering an unspecified constant.

Formalizing this result produces a reusable interface between conditional expectations of nonnegative series, tail probabilities, and exponential moments. The exact Theorem 19.1 and Lemma 18.1 are posed as Lean statements here; their proofs are not yet machine checked in this mission. Mathlib supplies probability measures, filtrations, martingales, extended nonnegative integrals, and generalized conditional expectation. Completing the mission would establish the paper's stated quantitative bound in that setting, while the standalone exponential lemma could also be imported by developments with different stochastic objects.

Difficulty

The hypothesis bounds a conditional expectation of the entire future squared-increment tail at every time. It does not bound $S(f)^2$ pointwise: rare paths may accumulate a large sum while the conditional average remains controlled. A direct attempt to bound the exponential term by bounding each increment separately loses the dependence across times and does not yield the stated coefficient. The central mathematical gap is therefore the passage from time-indexed conditional tail information to a global distribution estimate that is strong enough for the exact exponential constant (Burkholder 1973, pp. 36–37).

Formalization scope

The Lean development represents $d_n$ and $S_n(f)$ by explicit definitions and $S(f)$ as the supremum of its partial square functions, valued in $[0,\infty]$ . Thus a divergent square function has value $+\infty$ , rather than a default real supremum. Probability tails and expectations of nonnegative functions use extended nonnegative measures and integrals. Condition (19.1) uses generalized conditional expectation of the nonnegative series; ordinary real conditional expectation could return a default zero on a non-integrable tail and make the assumption empty. The inequality holds almost everywhere, as conditional expectations are determined only up to null sets.

The article starts its martingale at index one and sets $f_0=0$ for differences. Mathlib's martingale is indexed from zero. Its index-zero value can be supplied by a conditional expectation of $f_1$ ; the shared difference-sequence definition still reads the paper's $f_0=0$ . The squared tail begins at $n\ge1$ and is conditioned on $\mathcal A_n$ . The goal states almost-sure finiteness of $S(f)$ as a conclusion before applying the real exponential to its finite value. This avoids treating $+\infty$ as zero through an extended-real conversion. No finiteness of $S(f)$ , integrability of its square, or exponential moment is assumed at the outset. The zero martingale on a one-point probability space satisfies the condition, so the hypotheses admit a concrete instance.

The common martingale definitions also include maximal functions, stopped values, $L^p$ norms, a conditional square function, and the class of moderate-growth functions $\Phi$ used by other missions from this article. The reusable contributions especially welcome here are the tail integral lemma for extended nonnegative functions and results connecting generalized conditional expectation with a nonnegative infinite sum. The exact source indices, constants, and boundary conventions are fixed by the source pages cited above.

Selected references

D. L. Burkholder, Distribution Function Inequalities for Martingales, The Annals of Probability 1(1), 19–42, 1973. DOI: 10.1214/aop/1176997023.

5 thms2 active usersReviewed

Missions

The dyadic case of the Erdős similarity conjectureOpen Problem

Motivation

Setting

Formalization target

Significance and status

Difficulty

Formalization scope

Selected references

Asymptotically minimal maxima of real Littlewood polynomialsOpen Problem

Motivation

Setting

Formalization target

Significance and status

Difficulty

Formalization scope

Selected references

A strict inverse-first-power bound for univalent functionsOpen Problem

Motivation

Setting

Formalization target

Significance and status

Difficulty

Formalization scope

Selected references

Brennan's conjecture and sharp inverse-square integral meansOpen Problem

Motivation

Setting

Formalization target

Significance and status

Difficulty

Formalization scope

Selected references

Sharp One-Third Stability of Brenier MapsResearch Paper

Motivation

Timeline

Setting

Formalization targets

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

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

Significance

Difficulty

Formalization scope

Selected references

The Subcritical Hénon–Lane–Emden ConjectureResearch Paper

Motivation: Liouville theorems for Lane–Emden systems

Timeline

Setting

Formalization targets

Goal: subcritical nonexistence (Theorem 1.1)

Significance

Difficulty

Formalization scope

Selected references

Nonuniqueness for the periodic hard-sphere Boltzmann equationResearch Paper

Motivation: uniqueness of weak Boltzmann solutions

Timeline

Setting

Formalization targets

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

Significance

Difficulty

Formalization scope

Selected references

Exact asymptotic moduli in a Daugavet subspace of L1Research Paper

Motivation

Timeline

Setting

Formalization targets

Goal: Theorem 1.1

Milestone: Theorem 6.1 (Kadets–Werner construction)

Significance

Difficulty

Formalization scope

Selected references

Midpoint lenses in segment spacesResearch Paper

Motivation

Timeline

Setting