Functional Analysis

Motivation

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

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

Background

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

Setting

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

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

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

Formalization targets

Goal: Theorem 1.1 (p. 2)

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

Bose–Einstein condensation (BEC) means that a single one-particle state carries a macroscopic fraction of a many-boson system. It was predicted for the ideal gas by Bose and Einstein (1924–1925) and is observed in dilute atomic gases, but for interacting particles in the thermodynamic limit there was no rigorous proof, even in the ground state. The Penrose–Onsager criterion (Phys. Rev. 1956) identifies condensation with a macroscopic eigenvalue of the one-particle density matrix. Energy asymptotics of the dilute gas are now known to second order, but they do not determine single-orbital occupation, since the one-particle spectral gap closes as the volume grows. Lieb and Yngvason explicitly separated the condensation question from their energy theorem, and Solovej's 2025 survey lists fixed-density ground-state condensation as a major problem in the field (C. R. Physique 2025, Section 5).

This mission asks for a formal proof of ground-state condensation for the dilute three-dimensional hard-sphere Bose gas, 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

• 1924–1925 — Bose and Einstein predict condensation in the ideal Bose gas (Z. Phys. 1924).
• 1947 — Bogoliubov's theory assumes a macroscopically occupied zero mode.
• 1956 — Penrose and Onsager's density-matrix criterion for condensation.
• 1957 — Dyson's bounds on the hard-sphere ground-state energy (Phys. Rev. 1957); Lee, Huang and Yang predict depletion of order $\sqrt{\rho a^3}$ (Phys. Rev. 1957).
• 1998 — Lieb and Yngvason prove the leading dilute energy asymptotics $4\pi\rho a$ (PRL 1998).
• 2002 — Lieb and Seiringer prove BEC for trapped gases in the Gross–Pitaevskii limit (PRL 2002).
• 2020 — Deuchert and Seiringer: homogeneous Gross–Pitaevskii limit at positive temperature (ARMA 2020).
• 2021–2026 — Fournais's length scales for BEC (EMS 2021); Fournais–Solovej's Lee–Huang–Yang lower bound including hard cores (Invent. Math. 2023); Basti et al.'s matching upper bound for hard spheres (arXiv:2603.13084); results of Chong–Liang–Nam (JFA 2026) and Junge (arXiv:2603.20776) in joint dilute and large-volume limits.
• September 2026 — The OpenAI preprint claims condensation at fixed density and fixed exclusion distance (Theorem 1.1, p. 3).

Setting

Let $\Lambda_L=(\mathbb R/L\mathbb Z)^3$ be the flat torus with torus distance $d_L$. For $N$ particles and exclusion distance $a>0$, the allowed configurations are

$$\Omega_{N,L,a}=\{X\in\Lambda_L^N:\ d_L(x_i,x_j)>a\ \text{for } i<j\}.$$

The hard-sphere Hamiltonian is the operator of the Dirichlet form $q[f]=\sum_{i=1}^N\int|\nabla_if|^2$ on $H^1_0(\Omega_{N,L,a})$ restricted to symmetric (bosonic) functions; wave functions vanish on forbidden configurations, and $a$ is the scattering length. A ground vector is a normalized bosonic minimizer of $q$. For a normalized bosonic $\Psi$, the condensate fraction in the constant orbital $\varphi_0=L^{-3/2}$ is

$$B(\Psi)=\frac{\langle\varphi_0,\Gamma^{(1)}_\Psi\varphi_0\rangle}{N}=\frac1{L^3}\int_{\Lambda_L^{N-1}}\Bigl|\int_{\Lambda_L}\Psi(x,Y)\,dx\Bigr|^2dY\in[0,1],$$

and for a density operator it is defined by linearity. The gas parameter is $\rho a^3$ with $\rho$ the density.

Formalization targets

Goal: Theorem 1.1 and Corollary 1.2 (p. 3)

There are absolute constants $\varepsilon_0,c_0>0$ such that, for all $a,\rho>0$ with $\rho a^3<\varepsilon_0$ and every sequence $N_k\to\infty$, $L_k\to\infty$ with $N_k/L_k^3\to\rho$:

1. for every choice of (possibly complex) bosonic ground vectors $\Psi_k$, $\ \liminf_k B(\Psi_k)\ge c_0$;
2. for every sequence of density operators $T_k$ supported on the bosonic ground spaces, the same bound holds for the occupation of $T_k$ (in particular for the normalized ground-space projections).

The constant $c_0$ does not depend on the gas parameter in this range.

Significance

The result itself. It is a proof of macroscopic condensation in an interacting continuum Bose gas with fixed density and fixed hard core, in the thermodynamic limit, uniformly over all ground states including degenerate ground spaces. Previous rigorous results let the gas parameter tend to zero with the volume, or concerned traps, scaling limits, or positive-temperature settings with different potentials. The theorem gives a positive fraction only; it does not reach the Lee–Huang–Yang depletion law.

Formalizing it. The statement involves Sobolev spaces with Dirichlet conditions on a configuration space of the torus, bosonic symmetry, density operators, and partial traces, none of which are packaged in Mathlib; the Lean development builds them concretely. The proof uses killed Brownian motion, percolation-type path constructions, and second-moment arguments. No machine-checked statement of BEC for an interacting system is known.

Difficulty

Energy estimates alone cannot detect occupation of the constant orbital, because the cost of moving particles out of it is of order $L^{-2}$ per particle and vanishes in the limit. One must show directly that a typical ground state correlates distant parts of the box. The preprint compares a tagged particle's position in distant cells by moving trajectories along random lattice routes; multiplying local comparison costs along a route loses a factor at every step, so instead it averages over random routes and bounds the second moment of the averaged likelihood, where exact cancellation of normalizers leaves a cost depending only on mutual encounters of two routes (Introduction, pp. 4–5; Section 8). A separate phase argument passes from $|\Psi|$ to complex $\Psi$ (Lemma 2.3, p. 9).

Formalization scope

• Configurations are Fin N → Fin 3 → AddCircle L; the allowed set uses the Euclidean torus distance with strict inequality a < dist.
• The form domain dirichletDomain is the closure, in $L^2\times(L^2)^{3N}$, of jets of smooth compactly supported test functions with support in the allowed set; energy is the sum of squared $L^2$ norms of the partial derivatives. IsGroundVector means: in the domain, bosonic (a.e. permutation invariant), normalized, and of minimal energy among such vectors.
• occupation is exactly $B(\Psi)$; mixedOccupation T is the trace of $T$ compressed by the bounded map $\Psi\mapsto L^{-3/2}\int\Psi(x,\cdot)\,dx$. GroundSupported T says every unit vector in $(\ker T)^\perp$ is (the first component of) a ground vector.
• Density operators are positive bounded operators with trace one, computed in a fixed Hilbert basis.
• Hypotheses on the sequences are only those of the source; the ground-vector hypothesis is required for every index $k$, which loses nothing since $\liminf$ depends only on tails.

Selected references

• OpenAI, Ground-state condensation in the dilute hard-sphere gas, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Ground-state-condensation-in-the-dilute-hard-sphere-gas-September-24-2026/paper.pdf
• O. Penrose, L. Onsager, Bose–Einstein condensation and liquid helium, Phys. Rev. 104 (1956). https://doi.org/10.1103/PhysRev.104.576
• F. J. Dyson, Ground-state energy of a hard-sphere gas, Phys. Rev. 106 (1957). https://doi.org/10.1103/PhysRev.106.20
• T. D. Lee, K. Huang, C. N. Yang, Eigenvalues and eigenfunctions of a Bose system of hard spheres and its low-temperature properties, Phys. Rev. 106 (1957). https://doi.org/10.1103/PhysRev.106.1135
• E. H. Lieb, J. Yngvason, Ground state energy of the low density Bose gas, Phys. Rev. Lett. 80 (1998). https://doi.org/10.1103/PhysRevLett.80.2504
• E. H. Lieb, R. Seiringer, Proof of Bose–Einstein condensation for dilute trapped gases, Phys. Rev. Lett. 88 (2002). https://doi.org/10.1103/PhysRevLett.88.170409
• S. Fournais, J. P. Solovej, The energy of dilute Bose gases II: the general case, Invent. Math. (2023). https://doi.org/10.1007/s00222-022-01175-0
• A. Deuchert, R. Seiringer, Gross–Pitaevskii limit of a homogeneous Bose gas at positive temperature, Arch. Ration. Mech. Anal. (2020). https://doi.org/10.1007/s00205-020-01489-4
• J. P. Solovej, Mathematical physics of dilute Bose gases, C. R. Physique (2025). https://doi.org/10.5802/crphys.247
• G. Basti, M. Brooks, S. Cenatiempo, A. Olgiati, B. Schlein, The Lee–Huang–Yang energy for a dilute gas of hard spheres: an upper bound, arXiv:2603.13084 (2026). https://arxiv.org/abs/2603.13084v2

Motivation: Banach's simple Lebesgue-spectrum problem

A measure-preserving transformation $T$ of a probability space acts on square-integrable functions by the Koopman operator $U_Tg=g\circ T$, a unitary operator. Its spectral type (discrete, singular continuous, absolutely continuous) and its multiplicity are basic invariants of ergodic theory. The Lebesgue spectrum is the spectral type of the shift on $\ell^2(\mathbb Z)$, the type of Bernoulli shifts and other strongly chaotic systems, where it occurs with infinite multiplicity. Banach's problem asks whether Lebesgue spectrum can occur with multiplicity one: is there a transformation whose Koopman operator on the orthogonal complement of the constants is unitarily equivalent to multiplication by $w$ on $L^2(S^1)$? Equivalently, is there a single function whose bilateral orbit under $U_T$ is an orthonormal basis of the mean-zero space? The problem combines spectral theory with the construction of explicit dynamics, and a smooth example would show this spectral behavior is compatible with the regularity of differentiable dynamics.

Timeline

• 1949 — Rokhlin asks for ergodic automorphisms with simple, or at least finite-multiplicity, Lebesgue spectrum (Uspekhi Mat. Nauk 1949, §4, no. 7).
• 1960 — Ulam records a real-line form of the question attributed to Banach (A Collection of Mathematical Problems, Interscience, 1960, §6, p. 76).
• 1970 — Anosov and Katok introduce approximation-by-conjugation constructions of smooth ergodic diffeomorphisms (Trudy MMO 1970).
• 1978 — Helson and Parry construct cocycles over aperiodic transformations with associated Lebesgue spectrum (Ark. Mat. 1978).
• 1984 — Mathew and Nadkarni construct a transformation with a Lebesgue component of multiplicity two (Bull. LMS 1984).
• 1999 — Guenais connects Morse cocycles with flat polynomials and constructs a group action with simple spectrum of mixed type (ETDS 1999).
• 2001 — Fayad constructs $C^\infty$ volume-preserving torus diffeomorphisms with simple (not Lebesgue) spectrum (J. LMS 2001).
• 2020–2023 — Prikhod'ko constructs a finite-measure flow with simple Lebesgue spectrum (Sb. Math. 2020); Fayad–Forni–Kanigowski (JAMS 2021) and Abdedou–Fayad–Kessi (DCDS 2023) obtain smooth flows with countable Lebesgue multiplicity; el Abdalaoui presents an infinite-measure conservative example (arXiv:1508.06439). None of these gives a probability-preserving map with simple Lebesgue spectrum on the whole mean-zero space.
• 2026 — The OpenAI preprint A smooth three-torus diffeomorphism with simple Lebesgue spectrum (OpenAI Math Release, September 23, 2026) claims a $C^\infty$ volume-preserving diffeomorphism of $\mathbb T^3$ with this property. It has not been peer reviewed and its theorem is not formally verified.

Setting

Let $\mathbb T=\mathbb R/\mathbb Z$ and let $\mu$ be normalized Lebesgue (Haar) measure on $\mathbb T^3$. A bijection $T:\mathbb T^3\to\mathbb T^3$ is a $C^\infty$ diffeomorphism if $T$ and $T^{-1}$ lift locally to $C^\infty$ maps of $\mathbb R^3$. It is volume preserving if $\mu(T^{-1}A)=\mu(A)$ for every measurable $A$. Let $L^2_0(\mathbb T^3,\mu)$ be the closed subspace of complex square-integrable functions with integral zero, and $U_Tg=g\circ T$. Let $m$ be Haar measure on the circle and $w(z)=e^{2\pi i z}$ the first Fourier character.

In Lean (namespace OAI.ThreeTorus), the torus is Fin 3 → UnitAddCircle with the product Haar measure, smoothness is local smooth lifting on Fin 3 → ℝ, $L^2_0$ is the subspace meanZero of Lp ℂ 2 μ, and MainConclusion packages the theorem below.

Formalization targets

Goal: smooth simple Lebesgue spectrum (Theorem 1.1)

There exist a $C^\infty$ volume-preserving diffeomorphism $T$ of $\mathbb T^3$ and a real-valued $f\in L^2_0(\mathbb T^3,\mu)$ such that

$$\{\,f\circ T^n : n\in\mathbb Z\,\}\ \text{is an orthonormal basis of } L^2_0(\mathbb T^3,\mu);$$

moreover $T$ is ergodic, and there is a unitary $W:L^2_0(\mathbb T^3,\mu)\to L^2(S^1,m)$ with

$$W(g\circ T)=w\cdot W(g)\qquad\text{for all } g\in L^2_0 .$$

The goal is published on the platform with status Open.

Significance

The result itself. The theorem answers the probability-preserving form of Banach's problem, with the strongest kind of example: the invariant measure is the standard smooth volume on a compact manifold, the map is $C^\infty$, and the conclusion covers the whole mean-zero space, both spectral type and multiplicity. Earlier work produced Lebesgue components, Lebesgue spectrum of higher multiplicity, simple spectrum of other types, flows, or infinite-measure examples; time-$t$ maps of simple-Lebesgue flows have infinite multiplicity, so they do not answer the question. The source also derives from it mixing (of all orders, using a separate companion multiple-mixing theorem), zero Kolmogorov–Sinai entropy (via Rokhlin's finite-multiplicity entropy theorem) and vanishing Lyapunov exponents (Corollary 6.1, p. 28).

Formalizing it. The statement exercises Mathlib's $L^p$ spaces, Haar measure on the additive circle, ergodicity and Fourier characters together. A formal proof would certify a long quantitative construction (successive smooth passages, stationary-phase estimates, Fourier signals) whose convergence must be checked simultaneously in the $C^\infty$ topology and in spectral norms.

Difficulty

Smooth constructions by successive conjugation (Anosov–Katok type) naturally produce maps with singular or discrete spectral behavior, because each approximating map is close to a rotation or an integrable twist with pure point or very structured spectrum. Lebesgue spectral type requires the spectral measure of every function to be absolutely continuous with the right density, and simplicity requires a single orbit to span the whole space. Making both hold in the limit, while keeping the limit map $C^\infty$, requires controlling spectral densities at every scale and approximating every target function by translates of one fixed vector — the step where generic perturbation arguments give no control.

Formalization scope

• The torus is Fin 3 → UnitAddCircle with Measure.pi of AddCircle.haarAddCircle; $T$ is an Equiv.Perm with Smooth T and Smooth T.symm (local $C^\infty$ lifts), and MeasurePreserving T μ μ.
• $L^2_0$ is the complex subspace of Lp ℂ 2 μ with zero integral; $f$ is real-valued almost everywhere. The orbit $v_n=f\circ T^n$ is required to be orthonormal with dense span, i.e. a Hilbert basis indexed by $\mathbb Z$.
• The spectral model is stated with an explicit linear isometric equivalence W : H₀ ≃ₗᵢ[ℂ] CircleH intertwining composition with $T$ and multiplication by fourier 1. Ergodicity is Mathlib's Ergodic T μ.
• Mixing, zero entropy and Lyapunov exponents (Section 6) are not part of the goal.
• Needed infrastructure: stationary-phase estimates, spectral measures of Koopman operators, smooth volume-preserving changes of coordinates on the torus. Spectral-theory infrastructure for Koopman operators is reusable throughout ergodic theory.

Selected references

• V. A. Rokhlin, Selected topics from the metric theory of dynamical systems, Uspekhi Mat. Nauk 4 (1949). https://www.mathnet.ru/eng/rm8607
• S. M. Ulam, A Collection of Mathematical Problems, Interscience Tracts in Pure and Applied Mathematics 8, 1960.
• D. V. Anosov and A. B. Katok, New examples in smooth ergodic theory. Ergodic diffeomorphisms, Trudy Moskov. Mat. Obshch. 23 (1970). https://www.mathnet.ru/eng/mmo237
• H. Helson and W. Parry, Cocycles and spectra, Ark. Mat. 16 (1978). https://doi.org/10.1007/BF02385994
• J. Mathew and M. G. Nadkarni, A measure preserving transformation whose spectrum has Lebesgue component of multiplicity two, Bull. London Math. Soc. 16 (1984). https://doi.org/10.1112/blms/16.4.402
• M. Guenais, Morse cocycles and simple Lebesgue spectrum, Ergodic Theory Dynam. Systems 19 (1999). https://doi.org/10.1017/S0143385799126579
• B. R. Fayad, Partially mixing and locally rank one smooth transformations and flows on the torus $\mathbb T^d$, $d\ge3$, J. London Math. Soc. 64 (2001). https://doi.org/10.1112/S0024610701002447
• A. A. Prikhod'ko, On ergodic flows with simple Lebesgue spectrum, Sb. Math. 211 (2020). https://doi.org/10.1070/SM8147
• B. Fayad, G. Forni and A. Kanigowski, Lebesgue spectrum of countable multiplicity for conservative flows on the torus, J. Amer. Math. Soc. 34 (2021). https://doi.org/10.1090/jams/970
• OpenAI, A smooth three-torus diffeomorphism with simple Lebesgue spectrum, OpenAI Math Release preprint, September 23, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-smooth-three-torus-diffeomorphism-with-simple-Lebesgue-spectrum-September-23-2026/paper.pdf

Motivation

Edit distance $\mathrm{ED}(x,y)$ is the least number of single-symbol insertions, deletions and substitutions transforming a string $x$ into $y$. It is the basic similarity measure for strings, but it is expensive to compute and awkward to index. A standard way around this is to embed strings into $\ell_1$ so that $\ell_1$ distances approximate edit distances; the quality of such a map is its distortion. Low-distortion embeddings give fast approximate nearest-neighbour search and sketching for edit distance, so the best possible distortion has been studied for two decades.

This preprint determines the exponential scale of the optimal distortion: for strings of length at most $d$, it is $\exp(\Theta(\sqrt{\log d\,\log\log d}))$, uniformly over finite alphabets.

Background

• 1966. Levenshtein studies codes correcting insertions, deletions and substitutions.
• 1974. Wagner and Fischer describe edit scripts through increasing traces (alignments).
• 1995. Linial, London and Rabinovich develop the geometry of finite metric embeddings into $\ell_1$.
• 2003. Andoni, Deza, Gupta, Indyk and Raskhodnikova give binary subsets with $\ell_1$ distortion approaching $3/2$.
• 2006. Khot and Naor prove an $\Omega(\sqrt{\log d/\log\log d})$ lower bound via cuts and Fourier analysis of noisy shifts.
• 2007. Ostrovsky and Rabani prove the upper bound $\exp(O(\sqrt{\log d\log\log d}))$ for binary strings of length $d$.
• 2009. Krauthgamer and Rabani prove an $\Omega(\log d)$ lower bound for binary strings of length $d$.
• 2026. The OpenAI preprint Edit Distance in $\ell_1$: Matching Bounds up to Constants in the Exponent (dated September 27, 2026) proves a matching lower bound $\exp(\Omega(\sqrt{\log d\log\log d}))$. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

For a finite alphabet $\Sigma$ and $d \ge 1$, let $\Sigma^{\le d}$ be the set of strings of length at most $d$, including the empty string. Edit scripts may pass through strings of any length. Let $\ell_1$ be the space of absolutely summable real sequences. Define

$$E_\Sigma(d) = \inf_{f:\Sigma^{\le d}\hookrightarrow \ell_1}\Big(\max_{x\ne y}\frac{\|f(x)-f(y)\|_1}{\mathrm{ED}(x,y)}\Big)\Big(\max_{x\ne y}\frac{\mathrm{ED}(x,y)}{\|f(x)-f(y)\|_1}\Big),$$

the infimum over injective maps with no restriction on dimension or computability.

In Lean (OAI.EditDistortion), edit x y is the least length of a Script true n x y of unit insertions, deletions and substitutions on List Alpha; L1 = lp (fun _ : ℕ => ℝ) 1; distortion ρ f is the product of the two maximal ratios for an embedding f : X ↪ L1; leastDistortion is the infimum over embeddings; E Alpha d applies this to {x : List Alpha // x.length ≤ d}; exponentScale c d = exp(c·sqrt(log d · log log d)).

Formalization targets

Goal: Theorem 1.1

There are absolute $c, C > 0$ and $d_0$ such that for every $d \ge d_0$ and every finite alphabet with $|\Sigma| \ge 2$,

$$\exp\big(c\sqrt{\log d\,\log\log d}\big) \le E_\Sigma(d) \le \exp\big(C\sqrt{\log d\,\log\log d}\big).$$

The lower bound is witnessed by a finite set of binary strings of one common length at most $d$, and the same two bounds hold for $\sup_{2 \le |\Sigma| < \infty} E_\Sigma(d)$.

Significance

The result. Theorem 1.1 shows that the Ostrovsky–Rabani embedding is optimal up to the constant in the exponent, closing the gap between $\Omega(\log d)$ (Krauthgamer–Rabani) and $\exp(O(\sqrt{\log d\log\log d}))$. It rules out any $\ell_1$ embedding of edit distance with distortion $\exp(o(\sqrt{\log d\log\log d}))$, which limits $\ell_1$-based approaches to approximate edit-distance search.

Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. The upper bound relies on Ostrovsky and Rabani's fixed-length theorem (Theorem 5.1 in the preprint, taken from the literature) plus reductions proved in the preprint, so a full formalization also requires formalizing the Ostrovsky–Rabani embedding. The lower bound (Sections 2–4) is the new contribution.

Difficulty

Any lower bound must control every alignment of two strings, including matchings that cross the boundaries of the blocks used to build them, because an insertion or deletion shifts an entire suffix. Earlier Fourier-analytic arguments (Khot–Naor) and recursive constructions (Krauthgamer–Rabani) lose too much to reach the $\sqrt{\log d\log\log d}$ exponent; reaching it requires a construction whose combinatorial separation and an $\ell_1$ displacement inequality match at that scale.

Formalization scope

• Strings are List Alpha with Fintype Alpha, 2 ≤ card Alpha; the domain includes the empty string and all lengths up to $d$.
• Edit distance includes substitutions; edit is an sInf over script lengths, which is attained since scripts always exist.
• distortion uses sSup over finitely many ratios (the domain is finite), so no default values arise; leastDistortion is sInf over all injective maps into $\ell_1(\mathbb{N})$.
• BinaryWitness c d asks for a finite nonempty set of Boolean lists of common length $n \le d$ whose least distortion is at least exponentScale c d; a singleton has least distortion $0$, so the witness must be nontrivial.

The statement cannot be met trivially: both bounds are required with constants uniform in the alphabet.

Needed infrastructure: cut decompositions of finite $\ell_1$ metrics, Fourier analysis on finite abelian groups, prime-number estimates (Rosser–Schoenfeld), and the Ostrovsky–Rabani construction. Contributions toward the displacement inequality (Proposition 2.2) or the recursive construction (Proposition 3.1) are welcome.

Selected references

• OpenAI, Edit Distance in $\ell_1$: Matching Bounds up to Constants in the Exponent, OpenAI Math Release preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Edit-Distance-in-l1-Matching-Bounds-up-to-Constants-in-the-Exponent-September-27-2026/paper.pdf
• R. Ostrovsky, Y. Rabani, Low distortion embeddings for edit distance, J. ACM 54(5), Article 23, 2007. https://doi.org/10.1145/1284320.1284322
• R. Krauthgamer, Y. Rabani, Improved lower bounds for embeddings into $L_1$, SIAM J. Comput. 38(6), 2009.
• S. Khot, A. Naor, Nonembeddability theorems via Fourier analysis, Math. Ann. 334(4), 2006. https://doi.org/10.1007/s00208-005-0745-0
• A. Andoni, M. Deza, A. Gupta, P. Indyk, S. Raskhodnikova, Lower bounds for embedding edit distance into normed spaces, SODA 2003.
• N. Linial, E. London, Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2), 1995. https://doi.org/10.1007/BF01200757
• V. I. Levenshtein, Binary codes capable of correcting deletions, insertions, and reversals, Soviet Physics Doklady 10(8), 1966.
• R. A. Wagner, M. J. Fischer, The string-to-string correction problem, J. ACM 21(1), 1974. https://doi.org/10.1145/321796.321811

Motivation

The volume product of a convex body measures how large a body and its polar can simultaneously be. For a body without a distinguished centre, the polar is taken about the point that makes it smallest, the Santaló point, so the product is invariant under all invertible affine maps. The Blaschke–Santaló inequality identifies ellipsoids as the maximizers. Mahler's conjecture for general convex bodies asks for the minimizers and predicts simplices, with minimum value $(n+1)^{n+1}/(n!)^2$. The question arose from Mahler's work on polarity and the geometry of numbers, and it is the sharp form of the Bourgain–Milman reverse Santaló inequality.

This mission asks for a formal proof of the general Mahler conjecture with its equality case, as stated in an OpenAI preprint dated September 22, 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.

Timeline

• 1938–1939 — Mahler proves the planar inequality among polygons with triangles as equality cases (Ein Minimalproblem für konvexe Polygone, Mathematica (Zutphen) B, 1938) and formulates the higher-dimensional problem (Časopis 1939).
• 1949 — Santaló's affine invariant and the centre now named after him (Portugaliae Math., 1949).
• 1987 — Bourgain and Milman prove an inverse Santaló inequality with an exponential constant (Invent. Math. 1987).
• 1991 — Meyer completes the planar case for arbitrary convex bodies: triangles are exactly the minimizers (Monatsh. Math. 1991).
• 2006 — Meyer and Reisner use shadow systems to prove the sharp inequality for polytopes with at most $n+3$ vertices (Mathematika 2006).
• 2008–2012 — Kuperberg's explicit lower bounds via Gauss linking integrals (GAFA 2008); Nazarov's complex-analytic proof of Bourgain–Milman (GAFA seminar 2012).
• 2011 — Kim and Reisner prove strict local minimality at every simplex (Mathematika 2011).
• 2018 — Klartag's cone/Laplace-transform formulation of Mahler volumes (Adv. Math. 2018).
• 2024 — Mastrantonis and Rubinstein extend Nazarov's method to nonsymmetric bodies (arXiv:2206.06188).
• 2026 — Chen, Li, Xi and Xu prove the three-dimensional general case with tetrahedra as minimizers (arXiv:2605.09334).
• September 2026 — The OpenAI preprint claims the general conjecture in every dimension (Theorem 1.1, p. 1).

Setting

A convex body $K\subset\mathbb R^n$ is a compact convex set with nonempty interior; $|\cdot|$ is Lebesgue measure and $\langle\cdot,\cdot\rangle$ the Euclidean inner product. For an interior point $z$, the polar of $K$ about $z$ is

$$(K-z)^\circ=\{y\in\mathbb R^n:\ \langle y,x-z\rangle\le1\ \text{for all }x\in K\},$$

and the volume product is

$$P(K)=\inf_{z\in\operatorname{int}K}|K|\,|(K-z)^\circ|.$$

The infimum is attained at the unique Santaló point $s(K)$. A simplex is the convex hull of $n+1$ affinely independent points.

Formalization targets

Goal: the general Mahler conjecture (Theorem 1.1, p. 1)

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

$$P(K)\ \ge\ \frac{(n+1)^{n+1}}{(n!)^2},$$

with equality if and only if $K$ is a simplex.

Significance

The result itself. It is the exact form of a problem open since the 1930s and previously settled only in dimensions $2$ and $3$ and for polytopes with few vertices. Because the infimum over centres is taken, it gives the same lower bound for $|K||(K-z)^\circ|$ at every interior point $z$. Via the known geometric-to-functional implication, the preprint derives the sharp functional Mahler inequality for log-concave functions and an entropy–transport inequality (Corollary 1.2, p. 4; Corollary 8.1, p. 41). The symmetric conjecture, with the larger constant $4^n/n!$, is a different statement treated in a companion preprint.

Formalizing it. The proof combines convex cones and their Laplace transforms, Gaussian Sobolev calculus, Moreau's decomposition, matrix divided differences, and certified one-variable inequalities. A formal proof would provide checked versions of these tools and of the Santaló point's existence and uniqueness. No machine-checked proof of the conjecture in any dimension $n\ge2$ is known.

Difficulty

Symmetrization does not apply, the volume product is not convex along natural deformations except in restricted families (shadow systems), and local minimality at simplices says nothing about distant bodies. In the preprint's route the main obstacle (Introduction, pp. 2–3) is that the Jacobian matrices $P_z=D\Pi_C(Z+\xi_z)$ of the Gaussian-averaged cone projections neither commute nor increase in $z$: bounding them separately loses both the sharp constant and the equality case. Controlling them jointly requires comparing the whole family with spectral thresholds of a linear Gaussian matrix (Sections 5–7), and equality must then force the cone to split into half-lines.

Formalization scope

• Bodies are subsets of EuclideanSpace ℝ (Fin n) with IsCompact, Convex ℝ and nonempty interior, and $n\ge1$.
• polarAt K z is the polar about $z$; volumeProduct K is the sInf over interior K of (volume K).toReal * (volume (polarAt K z)).toReal. For an interior $z$ the polar is bounded, so toReal reads the true volume; the index set is nonempty because the interior is.
• The goal is a conjunction: the inequality, and volumeProduct K = (n+1)^(n+1)/(n!)^2 iff K = convexHull ℝ (range v) for some affinely independent v : Fin (n+1) → _.
• The Santaló point is not named in Lean; using the infimum over interior points is equivalent to evaluating at $s(K)$ because the infimum is attained there (Section 2 of the preprint).

Welcome contributions: polar bodies and their volumes in Mathlib, the Santaló point, Laplace transforms of convex cones, and Gaussian integration by parts.

Selected references

• OpenAI, The Mahler Conjecture for General Convex Bodies, OpenAI Math Release preprint, September 22, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Mahler-Conjecture-for-General-Convex-Bodies-September-22-2026/paper.pdf
• OpenAI, The symmetric Mahler conjecture and its equality cases, OpenAI Math Release preprint, September 22, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-symmetric-Mahler-conjecture-and-its-equality-cases-September-22-2026/paper.pdf
• K. Mahler, Ein Übertragungsprinzip für konvexe Körper, Časopis Pěst. Mat. Fys. 68 (1939). https://doi.org/10.21136/CPMF.1939.109441
• M. Meyer, Convex bodies with minimal volume product in $\mathbb R^2$, Monatsh. Math. (1991). https://doi.org/10.1007/BF01351770
• J. Bourgain, V. Milman, New volume ratio properties for convex symmetric bodies in $\mathbb R^n$, Invent. Math. (1987). https://doi.org/10.1007/BF01388911
• G. Kuperberg, From the Mahler conjecture to Gauss linking integrals, GAFA (2008). https://doi.org/10.1007/s00039-008-0669-4
• M. Meyer, S. Reisner, Shadow systems and volumes of polar convex bodies, Mathematika (2006). https://doi.org/10.1112/S0025579300000061
• J. Kim, S. Reisner, Local minimality of the volume-product at the simplex, Mathematika (2011). https://doi.org/10.1112/S0025579310001555
• B. Klartag, Isotropic constants and Mahler volumes, Adv. Math. (2018). https://doi.org/10.1016/j.aim.2018.03.009
• V. Mastrantonis, Y. A. Rubinstein, The Nazarov proof of the non-symmetric Bourgain–Milman inequality, Indiana Univ. Math. J. (2024). https://arxiv.org/abs/2206.06188
• S. Chen, Y. Li, D. Xi, Z. Xu, The Mahler Conjecture in Three Dimensions, preprint (2026). https://arxiv.org/abs/2605.09334v3

Motivation

Matrix-valued affine processes on the cone of positive semidefinite matrices are used in finance as models of stochastic covariance: multi-asset option pricing with stochastic volatility and correlation, and fixed-income models with stochastically correlated risk factors and default intensities. The best-known example is the Wishart process of Bru (1991). What makes these models tractable is that the Laplace transform of the state is exponential-affine in the initial state, with exponents that solve ordinary differential equations of Riccati type.

Cuchiero, Filipović, Mayerhofer and Teichmann (2011) give the mathematical foundation: a complete characterization of stochastically continuous affine processes on $S_d^+$ through an admissible parameter set. Their Theorem 2.4 has two halves. This mission formalizes the first, necessity, half: every affine process on $S_d^+$ is regular and Feller, and its generator and Riccati equations are given by an admissible parameter set.

Timeline. Duffie, Filipović and Schachermayer (2003) characterized regular affine processes on the canonical state space $\mathbb R_+^m \times \mathbb R^n$, assuming regularity. Keller-Ressel, Schachermayer and Teichmann showed that on that state space stochastic continuity already implies regularity. The 2011 paper carries both the characterization and the regularity result over to $S_d^+$, a non-polyhedral cone with a curved boundary, on which the drift must satisfy the new condition $b \succeq (d-1)\alpha$.

Setting

Let $S_d$ be the space of real symmetric $d\times d$ matrices with scalar product $\langle x,y\rangle = \mathrm{Tr}(xy)$ and norm $\|x\| = \langle x,x\rangle^{1/2}$. Let $S_d^+$ be the cone of positive semidefinite matrices and $S_d^{++}$ its interior, and write $x \preceq y$ when $y - x \in S_d^+$.

A time-homogeneous Markov process $X$ on $S_d^+$ is described by sub-stochastic transition kernels $p_t(x,d\xi)$, $t\ge 0$. Mass that is lost goes to a cemetery state $\Delta$. The kernels satisfy the Chapman–Kolmogorov equations, and the semigroup is $P_tf(x) = \int f(\xi)\,p_t(x,d\xi)$. The process is affine (Definition 2.1) if it is stochastically continuous, i.e. $p_s(x,\cdot) \to p_t(x,\cdot)$ weakly as $s \to t$, and if there are $\varphi : \mathbb R_+ \times S_d^+ \to \mathbb R_+$ and $\psi : \mathbb R_+\times S_d^+ \to S_d^+$ with

$$\int_{S_d^+} e^{-\langle u,\xi\rangle}\,p_t(x,d\xi) = e^{-\varphi(t,u) - \langle\psi(t,u),x\rangle}, \qquad t\ge0,\ u,x\in S_d^+.$$

It is regular (Definition 2.2) if $F(u) = \partial_t\varphi(t,u)|_{t=0+}$ and $R(u) = \partial_t\psi(t,u)|_{t=0+}$ exist and are continuous at $u=0$.

An admissible parameter set $(\alpha, b, \beta^{ij}, c, \gamma, m, \mu)$, associated with a bounded continuous truncation function $\chi$ (equal to the identity near $0$), consists of:

• a diffusion coefficient $\alpha \in S_d^+$ and a constant drift $b \succeq (d-1)\alpha$;
• killing rates $c \ge 0$ and $\gamma \in S_d^+$;
• a jump measure $m$ with $\int(\|\xi\|\wedge1)\,m(d\xi)<\infty$;
• a matrix $\mu$ of finite signed measures with $\mu(E) \in S_d^+$, defining $M(x,d\xi) = \langle x,\mu(d\xi)\rangle/(\|\xi\|^2\wedge1)$;
• a linear drift $B(x) = \sum_{i,j}\beta^{ij}x_{ij}$.

These are subject to the boundary conditions (2.9) and (2.11) for $x,u \in S_d^+$ with $\langle x,u\rangle = 0$. The space $\mathcal S_+$ consists of restrictions to $S_d^+$ of rapidly decreasing smooth functions on $S_d$.

Formalization targets

Goal: Theorem 2.4, first part

If $X$ is affine on $S_d^+$, then $X$ is regular and Feller, $\mathcal S_+$ lies in the domain of its generator $\mathcal A$ on $C_0(S_d^+)$, and there is an admissible parameter set such that for $f \in \mathcal S_+$

$$\mathcal Af(x) = \tfrac12\sum A_{ijkl}(x)\,\partial_{ij}\partial_{kl}f(x) + \sum (b_{ij}+B_{ij}(x))\,\partial_{ij}f(x) - (c+\langle\gamma,x\rangle)f(x) + \int (f(x+\xi)-f(x))\,m(d\xi) + \int \big(f(x+\xi)-f(x)-\langle\chi(\xi),\nabla f(x)\rangle\big)\,M(x,d\xi),$$

with $A_{ijkl}(x) = x_{ik}\alpha_{jl}+x_{il}\alpha_{jk}+x_{jk}\alpha_{il}+x_{jl}\alpha_{ik}$. In addition, $\varphi,\psi$ solve $\partial_t\varphi = F(\psi)$, $\varphi(0,u)=0$, $\partial_t\psi = R(\psi)$, $\psi(0,u) = u$, with

$$F(u) = \langle b,u\rangle + c - \int (e^{-\langle u,\xi\rangle}-1)\,m(d\xi),\qquad R(u) = -2u\alpha u + B^\top(u) + \gamma - \int \frac{e^{-\langle u,\xi\rangle}-1+\langle\chi(\xi),u\rangle}{\|\xi\|^2\wedge1}\,\mu(d\xi).$$

Milestones, in attack order

1. Lemma 3.1 and Lemma 3.3: order-preserving, continuous, analytic semiflows map $S_d^{++}$ into $S_d^{++}$.
2. Lemma 3.2: semiflow identities, monotonicity, continuity and analyticity of $\varphi,\psi$.
3. Proposition 3.4: Feller and regular.
4. Lemmas 4.1 and 4.4: zero divisors in the cone, and linear extension of additive maps.
5. Proposition 4.9: $F,R$ have the form (2.16)–(2.17) with $b\in S_d^+$.
6. Lemma B.2 and Theorem B.3: exponentials lie in $\mathcal S_+$ and span a dense subspace.
7. Proposition 4.12: the generator formula (2.12) on $\mathcal S_+$.
8. Lemma 4.17 and Proposition 4.18: derivatives of $\det$ at diagonal matrices, and the drift condition $b\succeq(d-1)\alpha$.

Significance

The result. Theorem 2.4 reduces the study of affine processes on $S_d^+$ to finitely many parameters. Any such process, a priori specified only through its Laplace transform, has the Lévy–Khintchine-type generator (2.12), its Laplace exponents solve the Riccati system, and its parameters obey the admissibility conditions. The drift condition $b\succeq(d-1)\alpha$ is the matrix analogue of the Feller condition, and for $d\ge2$ it excludes affine diffusions on $S_d^+$ with zero constant drift. The Feller property yields càdlàg versions, and the generator formula is the starting point for the semimartingale description and for the converse existence result.

Formalizing it. The theorem is proved in the paper, and this mission produces a machine-checked version of the necessity direction. Along the way it builds reusable infrastructure: a Lean model of Markov transition families on a cone, Feller semigroups on $C_0$ of a closed cone, generators on Schwartz-type test spaces with the symmetric-matrix derivative convention, and the positive semidefinite cone's order and boundary facts. No machine-checked proof of this theorem, or of its $\mathbb R_+^m\times\mathbb R^n$ predecessor, is known to exist.

Difficulty

The definition assumes only stochastic continuity and the exponential-affine form of the Laplace transform; differentiability in time is not given. Obtaining regularity, and hence the Riccati equations, needs the positivity statement of Lemma 3.3. Its proof uses analyticity in $u$ and the boundary geometry of $S_d^+$. Identifying $F$ and $R$ requires Lévy–Khintchine representations on cones and on $S_d$, and a convergence theorem for Laplace transforms. The admissibility conditions on the boundary come from support considerations at each boundary point. The drift condition (2.4) is not captured by the conditions read off from Laplace exponents at boundary points along single directions; it is a genuinely matrix-valued constraint coupling $b$ and $\alpha$. Extending the generator formula from exponentials to all of $\mathcal S_+$ needs a density result in a Fréchet topology and the closedness of the generator.

Formalization scope

• Matrices are Fin d → Fin d → ℝ, with $\langle x,y\rangle=\sum x_{ij}y_{ji}$ and $\|x\|=\langle x,x\rangle^{1/2}$. Mathlib's positive semidefiniteness, which includes symmetry over $\mathbb R$, defines $S_d^+$. The state space is the subtype $S_d^+$ with its subspace topology and Borel $\sigma$-algebra.
• Transition families are Mathlib kernels indexed by $t\in\mathbb R$ and constrained only for $t\ge0$. Sub-stochasticity encodes the cemetery. Stochastic continuity is convergence of integrals of bounded continuous functions as $s\to t$ within $[0,\infty)$.
• The exponents $\varphi,\psi$ are functions on $\mathbb R\times M_d$, used at $t\ge0$ and positive semidefinite arguments. Analyticity on $S_d^{++}$ is analyticity of $y\mapsto\psi(t,(y+y^\top)/2)$ on an open subset of $M_d$.
• The matrix measure $\mu$ is encoded as $H\,d\nu$ with $\nu$ finite and $H$ positive semidefinite and integrable. This loses nothing, since $\nu = \sum_i\mu_{ii}$ dominates every $\mu_{ij}$.
• $\mathcal S_+$ is the set of restrictions of Schwartz functions on $M_d$. Partial derivatives $\partial/\partial x_{ij}$ of functions on $S_d$ are taken in the direction $\tfrac12(E^{ij}+E^{ji})$, per §1.2 of the paper. Lemma 4.17 alone uses raw entry derivatives of $\det$ on $M_d$, as its proof does.
• The Feller property uses the platform definition EthierKurtz.IsStronglyContinuousContractionSemigroup on $C_0(S_d^+)$. "$f\in D(\mathcal A)$ and $\mathcal Af=g$" is uniform convergence of $(P_tf-f)/t$ to $g$ on $S_d^+$.
• Lean assigns the value $0$ to the integral of a non-integrable function. Wherever a statement concludes a formula containing an integral, it therefore also concludes integrability of the integrand, so the formula cannot hold through this default value. Regularity and the Feller property are conclusions, never hypotheses, of the goal. The drift condition (2.4) is part of admissibility in the goal; Propositions 4.9, 4.12 and 4.18 use admissibility without (2.4) and $b\in S_d^+$, as in the paper.
• Contributions are welcome on any milestone. The matrix lemmas (3.1, 3.3, 4.1, 4.4, 4.17) are self-contained, and Lemma B.2 and Theorem B.3 concern only Schwartz functions.

Selected references

• C. Cuchiero, D. Filipović, E. Mayerhofer, J. Teichmann, Affine processes on positive semidefinite matrices, Ann. Appl. Probab. 21 (2011) 397–463; cited as arXiv:0910.0137v3. https://arxiv.org/abs/0910.0137
• D. Duffie, D. Filipović, W. Schachermayer, Affine processes and applications in finance, Ann. Appl. Probab. 13 (2003) 984–1053. https://doi.org/10.1214/aoap/1060202833
• M. Keller-Ressel, W. Schachermayer, J. Teichmann, Affine processes are regular, Probab. Theory Related Fields 151 (2011) 591–611. https://arxiv.org/abs/0906.3392
• M.-F. Bru, Wishart processes, J. Theoret. Probab. 4 (1991) 725–751. https://doi.org/10.1007/BF01259552

Motivation

Optimal control problems with pointwise bounds on the control, such as

$$\min_u \tfrac12\|y - z\|_{L^2}^2 + \tfrac{\beta}{2}\|u\|_{L^2}^2 \quad\text{subject to } -\Delta y = u \text{ in } \Omega,\ y = 0 \text{ on } \partial\Omega,\ u \le \psi,$$

reduce, after eliminating the state, to a quadratic program in $L^2(\Omega)$ with a pointwise upper bound. The primal-dual active set strategy solves such problems by guessing the set where the bound is active, solving one linear system on that guess, and updating the guess from the new primal and dual values. It is used routinely in PDE-constrained optimization because each iteration costs one linear solve and, in practice, very few iterations are needed.

Hintermüller, Ito and Kunisch (SIAM J. Optim. 13 (2002) 865–888; authors' version hal-01660511) showed that this strategy is a semismooth Newton method for a nonsmooth reformulation of the optimality system, built on the notion of slant differentiability of Chen, Nashed and Qi (SIAM J. Numer. Anal. 38 (2000) 1200–1216). In finite dimension this gives local superlinear convergence (missions I–IV of this series). This mission concerns the paper's function-space result, Theorem 4.1: in $L^2(\Omega)$, under a norm gap on the operator, the method still converges locally superlinearly. Ulbrich (SIAM J. Optim. 13 (2003) 805–841) developed a related semismooth Newton theory for superposition operators in function spaces, which also requires a norm gap.

Setting

Let $(\Omega, \mu)$ be a finite measure space (the paper takes a bounded domain $\Omega \subset \mathbb{R}^n$ with Lebesgue measure) and $L^p = L^p(\Omega)$ the real Lebesgue spaces, with inner product $(\cdot,\cdot)$ on $L^2$. The paper writes $A$ for an operator and calligraphic $\mathcal{A}$, $\mathcal{I}$ for active and inactive sets.

Slant differentiability (Definition 1). For Banach spaces $X$, $Z$, a map $F : X \to Z$ is slantly differentiable in an open set $U$ if there is $G : U \to \mathcal{L}(X, Z)$, a slanting function, with

$$\lim_{h\to 0}\frac{1}{\|h\|}\,\|F(x+h) - F(x) - G(x+h)h\| = 0 \qquad (x \in U). \tag{A}$$

For $\delta \in \mathbb{R}$, the candidate slanting function of the pointwise max is $G_m(y)(x) = 1$ if $y(x) > 0$, $0$ if $y(x) < 0$, $\delta$ if $y(x) = 0$ (4.1).

The problem. Given $f, \psi \in L^2$ and a self-adjoint $A \in \mathcal{L}(L^2)$ with

$$(Ay, y) \ge \gamma\|y\|^2 \quad (\gamma > 0), \tag{H1}$$

minimize $\tfrac12(y, Ay) - (f, y)$ subject to $y \le \psi$. The solution $y^*$ and its multiplier $\lambda^*$ are the unique solution of

$$Ay^* + \lambda^* = f, \qquad \lambda^* - \max(0, \lambda^* + c(y^* - \psi)) = 0 \ \text{a.e.}, \tag{4.2}$$

for any fixed $c > 0$. The norm gap hypothesis is

$$A = C + \beta I, \qquad C \in \mathcal{L}(L^2, L^q),\quad \beta > 0,\quad q > 2. \tag{H2}$$

The algorithm. From $(y^0, \lambda^0) \in L^2 \times L^2$, set $\mathcal{A}_k = \{x : \lambda^k(x) + c(y^k(x) - \psi(x)) > 0\}$, $\mathcal{I}_k = \Omega\setminus\mathcal{A}_k$, and solve

$$Ay^{k+1} + \lambda^{k+1} = f, \qquad y^{k+1} = \psi \text{ on } \mathcal{A}_k, \qquad \lambda^{k+1} = 0 \text{ on } \mathcal{I}_k.$$

A sequence obeying this rule for every $k$ is a run. Superlinear convergence of $x^k \to x^*$ means $x^k \to x^*$ and, for every $\eta > 0$, eventually $\|x^{k+1} - x^*\| \le \eta\|x^k - x^*\|$.

Formalization targets

Goal: Theorem 4.1 (p. 15)

The page reads: "Assume that (H1), (H2) hold and that ψ and f are in L^q(Ω). Then the primal-dual active set strategy or, equivalently, the semismooth Newton method converge superlinearly if ‖y⁰ − y*‖ is sufficiently small and λ⁰ = β(y⁰ − ψ)." The formalized goal is the statement the proof establishes: with $c = \beta$, there is $\rho > 0$ such that every run with

$$\|y^0 - y^*\|_{L^2} < \rho, \qquad \lambda^0 = f - Ay^0$$

converges superlinearly to $(y^*, \lambda^*)$ in $L^2 \times L^2$. The initialization differs from the printed one; see Formalization scope.

Milestones

1. Theorem 1.1 (Chen–Nashed–Qi): slant differentiability near a zero $x^*$ with uniformly bounded $G(x)^{-1}$ gives local superlinear convergence of $x^{k+1} = x^k - G(x^k)^{-1}F(x^k)$.
2. Proposition 4.1(ii): for $1 \le p < q \le \infty$, $\max(0,\cdot) : L^q \to L^p$ is slantly differentiable with slanting function $G_m$.
3. (4.9)–(4.10): for $c = \beta$, (4.2) is equivalent to $\beta y^* - \beta\psi + \max(0, Cy^* - f + \beta\psi) = 0$ and $\lambda^* = f - Cy^* - \beta y^*$.
4. Equivalence of the algorithms: along a run with $c = \beta$ and $\lambda^0 = f - Ay^0$, $\lambda^k + \beta(y^k - \psi) = f - Cy^k - \beta\psi$ for all $k$, so the active sets are those of the reduced algorithm.
5. Slant differentiability of the reduced map $F(y) = \beta y - \beta\psi + \max(0, Cy - f + \beta\psi)$ on $L^2$, with $G_F(y+h) = \beta I + G_m(Cy - f + \beta\psi + Ch)C$, $\delta = 1$.
6. Bounded inverses: $G_F(z)$ is invertible on $L^2$, with $\|G_F(z)^{-1}\|$ bounded uniformly in $z$.

Two companion items accompany the goal: existence of a run from every $y^0$, and Proposition 4.1(i), the paper's counterexamples showing that $G_m$ fails to be a slanting function from $L^p$ to $L^p$.

Significance

Theorem 4.1 is the infinite-dimensional justification of a method used throughout control-constrained optimal control: it shows that the method converges locally superlinearly for the continuous problem itself, not only for each discretization. Example 1 of the paper shows that distributed control of the Poisson equation, and boundary control with Sobolev embeddings, satisfy (H2). Proposition 4.1 isolates the structural reason: the pointwise max is a Newton-differentiable map only between spaces with a norm gap.

None of these results is known to be machine-checked. A complete development would provide slant differentiability in Banach spaces, the Chen–Nashed–Qi local convergence theorem, the norm-gap differentiability of $\max(0,\cdot)$ between Lebesgue spaces, and invertibility of block operators on $L^2$ of a measurable partition. Each of these is reusable for other semismooth Newton analyses in function space.

Difficulty

The obvious argument fails at the max. In finite dimension, $\max(0,\cdot)$ is slantly differentiable with $G_m$ because a small perturbation does not change the sign of any nonzero component. In $L^2$, a perturbation $h$ of small norm can flip the sign of $y$ on a set of positive measure, and on that set the error $\max(0, y+h) - \max(0, y) - G_m(y+h)h$ is as large as $|y|$. Proposition 4.1(i) shows that this error is not $o(\|h\|_{L^p})$ in $L^p$ for any $p$. Superlinear convergence in $L^2$ therefore needs the argument of the max to be controlled in a stronger norm than the error is measured in, which is what (H2) and $f, \psi \in L^q$ provide. A second difficulty is that the two-variable algorithm is not literally a Newton method for a map of $y$ alone; it must be identified with the reduced algorithm, and that identification depends on the initialization.

Formalization scope

• Spaces. $L^p$ is Mathlib's Lp ℝ p μ on an arbitrary finite measure space; $q \in (2, \infty]$ is an extended real with 2 < q. The paper's bounded Lipschitz domain is replaced by a finite measure space: the proofs use only $|\Omega| < \infty$, and Mathlib has no notion of Lipschitz boundary.
• Pointwise statements on $L^p$ classes are almost everywhere statements about representatives. (H2) is stated as $Ay = Cy + \beta y$ a.e. for every $y \in L^2$, which avoids building the inclusion $L^q \subseteq L^2$.
• Hypotheses kept: self-adjointness of $A$, (H1) with explicit $\gamma > 0$, (H2) with $\beta > 0$ and $q > 2$, $f, \psi \in L^q$. The solution $(y^*, \lambda^*)$ of (4.2) is a hypothesis; it exists and is unique under (H1), as the paper states on p. 12.
• The initialization. The printed $\lambda^0 = \beta(y^0 - \psi)$ does not support the proof, which uses "$\lambda^0 + \beta(y^0 - \psi) = f - Cy^0 - \beta\psi$" and $c = \beta$. That identity holds exactly for $\lambda^0 = f - Ay^0$. The goal uses $\lambda^0 = f - Ay^0$ and $c = \beta$. With the printed initialization the first active set is $\{y^0 > \psi\}$, and for $y^0$ slightly below $y^*$ the first iterate solves the unconstrained problem, which can be far from $y^*$.
• Superlinear convergence is stated for the pair $(y^k, \lambda^k)$ in the product norm $\max(\|y\|, \|\lambda\|)$, without dividing by $\|x^k - x^*\|$, so finite termination qualifies. "Sufficiently small" is an $\exists\rho > 0$ chosen before the run, on $\|y^0 - y^*\|$ only.
• No trivialization. The goal mentions neither the reduced algorithm, nor $G_F$, nor Proposition 4.1; the norm gap $q > 2$ is not weakened to $C \in \mathcal{L}(L^2)$, under which Proposition 4.1(i) shows that $G_m$ need not be a slanting function; and the companion run_exists shows that the runs the goal quantifies over exist.
• Definitions (PDASNewton.FunSpace.Setting): slanting functions, superlinear convergence, $G_m$, property (A) for $\max(0,\cdot) : L^q \to L^p$, system (4.2), one step and runs of the algorithm. These duplicate the finite-dimensional definitions of the other missions of the series in a separate namespace.

Proofs of any milestone are welcome, as are reusable lemmas on Lebesgue spaces (Hölder on sets of small measure, multiplication operators, Lax–Milgram on $L^2$ of a measurable subset).

Selected references

• M. Hintermüller, K. Ito, K. Kunisch, The primal-dual active set strategy as a semismooth Newton method, SIAM J. Optim. 13(3) (2002) 865–888. https://doi.org/10.1137/S1052623401383558 ; authors' version https://hal.science/hal-01660511
• X. Chen, Z. Nashed, L. Qi, Smoothing methods and semismooth methods for nondifferentiable operator equations, SIAM J. Numer. Anal. 38 (2000) 1200–1216. https://doi.org/10.1137/S0036142999356719
• M. Ulbrich, Semismooth Newton methods for operator equations in function spaces, SIAM J. Optim. 13 (2003) 805–841. https://doi.org/10.1137/S1052623400371569
• L. Qi, J. Sun, A nonsmooth version of Newton's method, Math. Programming 58 (1993) 353–367. https://doi.org/10.1007/BF01581275

Motivation

A convex minimization problem comes with a dual maximization problem, and the dual value never exceeds the primal value. When the two values differ, a duality gap occurs. Dual bounds, Lagrangian relaxations and optimality certificates are then weaker than hoped. Conditions that rule the gap out are constraint qualifications such as Slater's condition and Rockafellar's notion of a stably set problem. Such conditions say when the gap vanishes, but not what the dual value is when it does not.

R. T. Rockafellar's 1967 paper answers that question for the Fenchel-type pair of problems built from a convex function, a concave function and a continuous linear map between infinite-dimensional spaces. Its Theorem 6 (§6, "Weak duality theorems", pp. 179–180) "explains the exact way in which inf (P) and sup (P*) can fail to be equal", by expressing the dual value through the primal problem alone: the dual supremum is the lower limit of the optimal values of slightly perturbed primal problems. This perturbational view of duality was later developed in Rockafellar's Conjugate Duality and Optimization (1974). It underlies the modern treatment of value functions in convex optimization.

Setting

Two real vector spaces $E$ and $E^*$ are topologically paired when each carries a locally convex Hausdorff topology, they are in duality under a bilinear form $\langle x,x^*\rangle$ that is continuous in each variable, and every continuous linear functional on either space is the pairing with exactly one element of the other. Let $(E,E^*)$ and $(F,F^*)$ be two such pairs. Let $A:E\to F$ be continuous linear and $A^*:F^*\to E^*$ its adjoint, the continuous linear map with $\langle Ax,y^*\rangle=\langle x,A^*y^*\rangle$.

A function $f:E\to[-\infty,+\infty]$ is convex when its epigraph $\{(x,\mu)\mid\mu\in\mathbb R,\ \mu\ge f(x)\}$ is convex in $E\times\mathbb R$. It is proper when it never takes $-\infty$ and is finite somewhere. A function $g$ is proper concave when $-g$ is convex, $g$ never takes $+\infty$, and $g$ is finite somewhere. The standing hypotheses are that $f$ is lower semicontinuous proper convex on $E$ and $g$ is upper semicontinuous proper concave on $F$. Their conjugates are

$$f^*(x^*)=\sup_{x}\{\langle x,x^*\rangle-f(x)\},\qquad g^*(y^*)=\inf_{y}\{\langle y,y^*\rangle-g(y)\}.$$

The primal problem (P) is to minimize $f(x)-g(Ax)$ over $x\in E$. The dual problem (P*) is to maximize $g^*(y^*)-f^*(A^*y^*)$ over $y^*\in F^*$. For $z\in F$ the perturbed problem (P($z$)) is to minimize $f(x)-g(Ax-z)$. Its value defines the perturbation function

$$h(z)=\inf(\mathrm P(z))=\inf_{x\in E}\{f(x)-g(Ax-z)\},\qquad h(0)=\inf(\mathrm P).$$

The lower semicontinuous hull of $h$ is $\bar h(y)=\liminf_{z\to y}h(z)$, where $z=y$ is allowed, so that $\bar h\le h$. All infima and suprema are taken in $[-\infty,+\infty]$.

Formalization targets

Goal: Theorem 6

$$\sup(\mathrm P^*)=\liminf_{z\to 0}\,[\inf(\mathrm P(z))],$$

valid except in the trivial case where the left side is $-\infty$ and the right side is $+\infty$. No consistency, constraint qualification or attainment is assumed, and neither side need be finite. The exception is exactly the stated conjunction. A version assuming (P) consistent would be weaker, since an inconsistent (P), with $h(0)=+\infty$, may still have a finite lower limit.

Milestones: the four claims of the proof (p. 180)

1. $\bar h$ is a lower semicontinuous convex function on $F$.
2. For every $y^*\in F^*$, with $\bar h^*(y^*)=\sup_y\{\langle y,y^*\rangle-\bar h(y)\}$,

$$-\bar h^*(y^*)=\inf_y\{\bar h(y)-\langle y,y^*\rangle\}=\inf_z\{h(z)-\langle z,y^*\rangle\}=g^*(y^*)-f^*(A^*y^*).$$

3. (6.2): if $\bar h$ is proper, then $\bar h(0)=\sup_{y^*}\{\langle 0,y^*\rangle-\bar h^*(y^*)\}$.
4. If $\bar h$ is not proper, the maximand $g^*(y^*)-f^*(A^*y^*)$ of (P*) is identically $-\infty$.

The paper's Lemma 2 (convexity of $h$) is used by the first claim. It is a milestone of the companion mission on Theorem 3 of the same paper and is not restated here.

Significance

Theorem 6 reduces every question about the dual value to a question about the primal value function near the origin. Strong duality $\inf(\mathrm P)=\sup(\mathrm P^*)$ holds exactly when $h$ is lower semicontinuous at $0$ (outside the trivial case). A duality gap is exactly a downward jump of $h$ at $0$. The dual of (P*) obeys the same formula, which the paper uses to derive Theorem 7 on normal problems. An integer-lattice analogue appears in discrete convex analysis (Murota, Theorem 8.53, whose duality relation is already stated on Prove2Me as DiscreteConvex.ConjugacyDualityD.general_duality_relations). That statement has no topology and is not the same theorem.

The result is classical and its proof is published. As far as the platform's index shows, no machine-checked statement of it exists in the paper's generality, nor a statement of extended-real biconjugation on general paired locally convex spaces. The value of the mission is a formal proof in the paper's setting: arbitrary topologically paired spaces, extended-real-valued functions, and both the proper and the improper case of the hull. The biconjugation milestone (6.2) and the hull lemma are reusable for other perturbational duality results.

Difficulty

The obvious argument compares $h(0)$ with the dual objective directly. It cannot give the theorem, because $h$ may jump at $0$, and the dual objective does not detect the value of $h$ at a single point: the target is a lower limit, not a value. In infinite dimensions, conjugacy recovers a function only when it is lower semicontinuous and convex for a topology compatible with the pairing, so the statement depends on the full compatibility of the pairing on $F$, not on a norm. The usual statements of biconjugation cover proper functions only, whereas here the lower limit may take both values $\pm\infty$, and both cases of the theorem must be covered. Finally, extended-real arithmetic must be tracked so that the dual objective, defined from $f^*$, $g^*$ and $A^*$, is matched in every infinite case.

Formalization scope

Values lie in EReal. Infima and suprema are complete-lattice ⨅ and ⨆, so an empty or unbounded family gives $\pm\infty$ as in the paper. The lower limit is Filter.liminf h (nhds y) over the full neighbourhood filter: a punctured limit would change the theorem. Convexity is epigraph convexity in $E\times\mathbb R$, and properness is the paper's two-sided condition. A topological pairing is a structure holding a bilinear map, separate continuity, and existence and uniqueness of representing elements in both directions. No norm, inner product or finite dimension is assumed. The adjoint $A^*$ is continuous linear data satisfying the adjoint identity. The conjugates $f^*$, $g^*$ are defined by the paper's formulas from $f$, $g$, so their regularity is a consequence, not a hypothesis. Properness of $f$ and $g$ excludes the form $(+\infty)-(+\infty)$ from $f(x)-g(Ax-z)$ and from $g^*(y^*)-f^*(A^*y^*)$. No statement is repaired relative to the page.

The dual value is the supremum of the maximand built from $f^*$, $g^*$ and $A^*$ as on p. 172. Defining $\sup(\mathrm P^*)$ through $\bar h$ (for instance as the biconjugate of $\bar h$ at $0$) would make Theorem 6 true by definition and is ruled out.

A complete development needs extended-real conjugates on paired spaces, the lower semicontinuous hull and the closure of a convex epigraph, and Fenchel–Moreau for proper lower semicontinuous convex functions on a locally convex space. All of these are reusable beyond this mission. Proofs of the milestones, and lemmas toward Fenchel–Moreau in this generality, are welcome contributions.

Selected references

• R. T. Rockafellar, Duality and Stability in Extremum Problems Involving Convex Functions, Pacific J. Math. 21 (1967), 167–187. https://doi.org/10.2140/pjm.1967.21.167
• W. Fenchel, On conjugate convex functions, Canad. J. Math. 1 (1949), 73–77. https://doi.org/10.4153/CJM-1949-007-x
• A. Brøndsted, Conjugate convex functions in topological vector spaces, Mat.-Fys. Medd. Dansk. Vid. Selsk. 34 (1964) (reference [2] of the paper; no DOI).
• J.-J. Moreau, Fonctions convexes en dualité, multigraph, Séminaires de Mathématique, Faculté des Sciences, Université de Montpellier, 1962 (reference [12] of the paper; no DOI).
• R. T. Rockafellar, Conjugate Duality and Optimization, CBMS-NSF Regional Conference Series in Applied Mathematics 16, SIAM, 1974. https://doi.org/10.1137/1.9781611970524
• K. Murota, Discrete Convex Analysis, SIAM, 2003, Theorem 8.53. https://doi.org/10.1137/1.9780898718508