All missions

Motivation

A von Neumann algebra is a unital algebra of bounded operators on a Hilbert space that is closed under adjoints and in the weak operator topology. For a set $S$ of operators, $W^*(S)$ denotes the smallest von Neumann algebra containing $S$. The generator problem, going back to Kadison's 1967 list of problems, asks whether every von Neumann algebra with separable predual is singly generated, $M=W^*(x)$ for a single bounded operator $x$; equivalently, whether two self-adjoint operators always suffice. It is one of the oldest structural questions about von Neumann algebras, and by classical reductions everything comes down to type II$_1$ factors.

Timeline

• 1962–1969. Pearcy proves single generation for type I algebras (doi:10.2307/2034069); Suzuki and Saitô for hyperfinite algebras (1963, doi:10.2748/tmj/1178243811); Wogen for properly infinite algebras (1969, doi:10.1090/S0002-9904-1969-12157-9); Douglas and Pearcy develop matrix-generation techniques (1969, doi:10.1307/mmj/1029000161).
• 1972. Behncke treats tensor products of two II$_1$ factors (doi:10.2748/tmj/1178241478).
• 1974. Willig's direct-integral theorem reduces the general problem to II$_1$ factors (doi:10.2748/tmj/1178241231).
• 1981. Popa constructs irreducible hyperfinite subfactors (doi:10.1007/BF01389015).
• 1985–2002. Popa treats factors with Cartan subalgebras (doi:10.7146/math.scand.a-12110); Ge and Popa treat property $\Gamma$ factors (1998, doi:10.1215/S0012-7094-98-09405-4); Ge and Shen treat certain property (T) factors (2002, doi:10.1073/pnas.022593699).
• 2008–2009. Dykema, Sinclair, Smith and White study generator invariants and their amplification formula (arXiv:0706.1953); Shen's generator invariant unifies the positive classes (arXiv:math/0511327).
• 2012. Sherman shows that finite generation of every countably generated II$_1$ factor would suffice (arXiv:0908.4565).
• 2021. Popa studies tight decompositions and stable single generation (arXiv:1910.14653).
• 2025. Gao, Kunnawalkam Elayavalli, Patchell and Tan prove single generation under an internal sequential-commutation hypothesis (arXiv:2404.12380).

The source of this mission is an OpenAI preprint dated September 23, 2026, which claims single generation for every II$_1$ factor with separable predual.

Setting

Let $H$ be a complex Hilbert space and $M\subseteq B(H)$ a unital $*$-subalgebra closed in the weak operator topology. $M$ is a factor if its centre is $\mathbb C1$; it is finite if every isometry $v\in M$ ($v^*v=1$) is unitary; it is diffuse if every nonzero projection has a proper nonzero subprojection. A nonzero finite diffuse factor is a type II$_1$ factor; it carries a unique faithful normal tracial state $\tau$, with $\|x\|_2=\tau(x^*x)^{1/2}$. $M$ has separable predual if $M$ is isometrically the dual of a separable Banach space; this does not require $H$ or $M$ to be norm-separable.

An inclusion of factors $P\subseteq M$ is irreducible if $P'\cap M=\mathbb C1$. $\mathcal U(M)$ denotes the unitary group.

Formalization targets

Milestone: Theorem 1.1 (relative generation)

For an irreducible inclusion $P\subset M$ of II$_1$ factors with $M$ of separable predual,

$$\{u\in\mathcal U(M):\ W^*(P,u)=M\}\ \text{ is a dense }G_\delta\text{ in }(\mathcal U(M),\|\cdot\|_2).$$

Goal: Theorem 1.2 (single generation)

$$M\ \text{a II}_1\text{ factor with separable predual}\ \Longrightarrow\ \exists\,x\in M:\quad W^*(x)=M.$$

The Lean statement OAI.Generator.single_generation_of_II1_separable_predual is open on the platform.

Significance

Combined with Willig's reduction and the known type I and properly infinite cases, Theorem 1.2 gives single generation of every von Neumann algebra with separable predual, an affirmative answer to the generator problem. The paper also deduces that the generator invariants $G$ and $G_{\mathrm{sa}}$ of Dykema–Sinclair–Smith–White vanish for every such factor, and that Voiculescu's free entropy dimensions $\delta,\delta_0$ are not invariants of the generated algebra (Corollary 6.1), since $L(\mathbb F_n)$ has both a free semicircular $n$-tuple and a self-adjoint pair as generators. Theorem 1.1 is of independent interest: it shows that relative generators are generic, not merely existent.

These results are stated in an OpenAI preprint; they have not been peer reviewed, and no machine-checked proofs exist.

Difficulty

Earlier positive results all relied on extra structure (Cartan subalgebras, property $\Gamma$, tensor decompositions, sequential commutation) to build a generator. Without such structure one must show that a unitary $u$ generates $M$ over $P$, which requires detecting every vector of $L^2(M)$ through words in $P$ and $u$. Perturbing $u$ along a long word changes it many times, and operator-norm bounds on the accumulated perturbation grow with the word length; a length-uniform estimate is needed. The Baire-category step also needs the projection onto $L^2(W^*(P,u))$ to vary semicontinuously in $u$.

Formalization scope

• Algebras are concrete StarSubalgebra ℂ (H →L[ℂ] H); WOTClosed uses Mathlib's weak operator topology, and wstar s is the infimum of WOT-closed star-subalgebras containing $s$ (unital by construction).
• IsII1Factor = nonzero Hilbert space, WOT-closed, trivial centre, finite (isometries are unitary), diffuse. No trace is assumed.
• HasSeparablePredual asks for a separable Banach space $X$ in the same universe with a conjugate-linear isometric equivalence between its dual and the algebra; this is equivalent to the usual condition.
• For Theorem 1.1, the trace is part of the conclusion (IsNormalizedTrace: normalized, positive, faithful, tracial, ultraweakly continuous), the topology on unitary large is generated by trace 2-distance balls, and the locus is $\{u: \mathrm{wstar}(P\cup\{u\})=M\}$.

A complete development needs the standard theory of II$_1$ factors (trace, $L^2(M)$, conditional expectations, ultrapowers), Popa's free independence in ultraproducts and irreducible hyperfinite subfactors, Haagerup's inequality for free groups, and the Baire category theorem on the unitary group. This infrastructure is reusable across operator-algebra missions. Contributions formalizing Proposition 3.2 (perturbation bounds) and Popa's irreducible hyperfinite embedding (Theorem 5.1) are welcome.

Selected references

• OpenAI, Relative generation and the generator problem for finite factors, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Relative-generation-and-the-generator-problem-for-finite-factors-September-23-2026/paper.pdf
• P. Willig, Generators and direct integral decompositions of $W^*$-algebras, Tohoku Math. J., 1974. https://doi.org/10.2748/tmj/1178241231
• D. Sherman, On cardinal invariants and generators for von Neumann algebras, Canad. J. Math., 2012. https://arxiv.org/abs/0908.4565
• K. Dykema, A. Sinclair, R. Smith, S. White, Generators of II$_1$ factors, Oper. Matrices, 2008. https://arxiv.org/abs/0706.1953
• L. Ge, S. Popa, On some decomposition properties for factors of type II$_1$, Duke Math. J., 1998. https://doi.org/10.1215/S0012-7094-98-09405-4
• J. Shen, Type II$_1$ factors with a single generator, J. Operator Theory, 2009. https://arxiv.org/abs/math/0511327
• S. Popa, Independence properties in subalgebras of ultraproduct II$_1$ factors, J. Funct. Anal., 2014. https://arxiv.org/abs/1308.3982
• U. Haagerup, An example of a non nuclear $C^*$-algebra, which has the metric approximation property, Invent. Math., 1979. https://doi.org/10.1007/BF01410082
• D. Gao, S. Kunnawalkam Elayavalli, G. Patchell, H. Tan, Internal sequential commutation and single generation, IMRN, 2025. https://arxiv.org/abs/2404.12380

Motivation

The classification programme for simple nuclear $C^*$-algebras identifies a class of algebras that are determined by K-theory and traces. Membership in that class is governed by regularity properties: finite nuclear dimension, absorption of the Jiang–Su algebra $\mathcal Z$, and strict comparison. Uniform property $\Gamma$, introduced by Castillejos, Evington, Tikuisis, White and Winter, is a central divisibility condition: it asks for projections in a central sequence algebra that cut every trace exactly in half, uniformly across the whole trace space, while preserving trace values against fixed coefficients. Together with strict comparison it is equivalent to $\mathcal Z$-stability for simple separable unital nuclear algebras (Castillejos–Evington–Tikuisis–White). Schafhauser, Tikuisis and White asked (Problem XXI of their problem list) whether real rank zero of the uniform tracial ultrapower of the tracial completion already forces uniform property $\Gamma$.

Timeline

• 1943, 1969, 1970. Murray and von Neumann introduce property $\Gamma$ for II$_1$ factors (doi:10.2307/1969107); Dixmier gives its central-projection formulation (doi:10.1007/BF01404306); McDuff studies central sequences and absorption of the hyperfinite factor (doi:10.1112/plms/s3-21.3.443).
• 1976. Connes classifies injective factors (doi:10.2307/1971057).
• 1991. Brown and Pedersen introduce real rank zero (doi:10.1016/0022-1236(91)90056-B).
• 1999. Jiang and Su construct the algebra $\mathcal Z$ (doi:10.1353/ajm.1999.0012).
• 2010–2012. Winter and Zacharias define nuclear dimension and the Toms–Winter conjecture is formulated (doi:10.1016/j.aim.2009.12.005); Winter proves finite nuclear dimension implies $\mathcal Z$-stability (doi:10.1007/s00222-011-0334-7); Matui and Sato prove strict comparison implies $\mathcal Z$-stability with finitely many extremal traces (doi:10.1007/s11511-012-0084-4).
• 2013. Ozawa introduces uniform tracial completions (J. Math. Sci. Univ. Tokyo).
• 2021–2022. Castillejos, Evington, Tikuisis, White and Winter introduce uniform property $\Gamma$ and prove $\mathcal Z$-stability implies finite nuclear dimension (doi:10.1007/s00222-020-01013-1); CETW develop it systematically (doi:10.1093/imrn/rnaa282).
• 2023. Carrión et al. develop tracially complete $C^*$-algebras (arXiv:2310.20594).
• 2025–2026. Schafhauser, Tikuisis and White list Problem XXI (arXiv:2506.10902); Vaccaro, Kessinger–Toms and Fu obtain related implications (arXiv:2604.24682, arXiv:2607.23817, arXiv:2605.21655); Toms constructs a simple separable unital AH algebra without uniform property $\Gamma$ (arXiv:2606.12188).

The source of this mission is an OpenAI preprint dated September 23, 2026, which answers Problem XXI affirmatively (and, by separate arguments, also treats the unital Toms–Winter conjecture).

Setting

Let $A$ be a unital $C^*$-algebra with nonempty set $T(A)$ of tracial states. The uniform 2-seminorm is

$$\|a\|_{2,T(A)}=\sup_{\tau\in T(A)}\tau(a^*a)^{1/2}.$$

The uniform tracial completion $B=\overline A^{T(A)}$ consists of bounded sequences in $A$ that are Cauchy for $\|\cdot\|_{2,T(A)}$, modulo those tending to zero; each $\tau\in T(A)$ extends to a designated trace $\bar\tau$ on $B$. For a free ultrafilter $\omega$ on $\mathbb N$, the uniform tracial ultrapower $B^\omega$ is the algebra of bounded sequences in $B$ modulo those whose uniform 2-norm tends to zero along $\omega$. Its limit traces are

$$\lambda([(b_j)])=\lim_{j\to\omega}\bar\tau_j(b_j),\qquad \tau_j\in T(A),$$

and $\Lambda_\omega$ denotes the set of these. $B$ embeds in $B^\omega$ as constant sequences.

A unital $C^*$-algebra has real rank zero if every self-adjoint element is a norm limit of self-adjoint elements with finite spectrum. $A$ is stably finite if every isometry in every matrix algebra over $A$ is unitary, and nuclear if its algebraic tensor product with any $C^*$-algebra carries a unique $C^*$-norm.

Formalization targets

Goal: Theorem 1.1

Let $A$ be unital, separable, simple, infinite-dimensional, nuclear and stably finite with $T(A)\neq\varnothing$, and let $\omega$ be a free ultrafilter. If $B^\omega$ has real rank zero, then there is a projection $p\in B^\omega\cap B'$ with

$$\lambda(px)=\tfrac12\,\lambda(x)\qquad(x\in B,\ \lambda\in\Lambda_\omega).$$

This is the halving formulation of uniform property $\Gamma$ used in Problem XXI. The Lean statement OAI.ComparatorModel.CurrentMain.main is open on the platform.

Significance

The theorem shows that real rank zero at the level of the tracial ultrapower is enough to produce uniform property $\Gamma$, with no restriction on the trace space; the paper also deduces that every trace on $B$ is a designated extension (Corollary 1.2). Since uniform property $\Gamma$ plus strict comparison gives $\mathcal Z$-stability, this links projection structure in tracial ultrapowers to the Toms–Winter regularity theory. The equivalence between the halving formulation and the usual all-$m$ formulation is due to Carrión et al.

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

Difficulty

Real rank zero supplies many projections in $B^\omega$, but nothing makes them central, and halving must hold simultaneously for every limit trace and every coefficient $x\in B$. Divisibility results derived from real rank zero (Vaccaro) give tracially large order-zero maps without centrality; uniform property $\Gamma$ needs commutation with all of $B$ and exact coefficient identities. Equality of the scalar traces $\lambda(p)$ alone is not enough. Nuclearity by itself does not suffice either, as Toms' AH example shows, so the real rank zero hypothesis must be used in an essential way.

Formalization scope

• TracialState A is a positive linear functional with $\tau(1)=1$ and $\tau(ab)=\tau(ba)$; the order on $A$ is the $C^*$ order (StarOrderedRing).
• The uniform tracial completion is the quotient of the star-subalgebra of uniformly 2-Cauchy elements of $\ell^\infty(\mathbb N,A)$ by uniformly 2-null sequences; the ultrapower is the quotient of $\ell^\infty(\mathbb N,B)$ by sequences 2-null along U, computed with the designated traces $\bar\tau$.
• TopologicallySimple, StablyFinite (via CStarMatrix), IsNuclear (subsingleton of $C^*$-norms on algebraic tensor products, in a fixed universe) and RealRankZero (finite-spectrum self-adjoint approximation) are defined directly.
• UniformPropertyGammaAt A U asserts a star projection $p$ commuting with the image of $B$ and halving familyLimitTrace … s for every sequence of traces s : ℕ → TracialState A.
• MainClaim existentially packages five auxiliary Prop classes (quotient $C^*$-norm, closure properties of null and Cauchy sequences, existence of ultralimits, and vanishing of limit traces on null sequences). They are true general facts that a proof must establish; they are not assumptions.

A complete development needs ultrapowers and tracial completions of $C^*$-algebras, nuclearity and completely positive approximation, and real rank zero; all of this is reusable for the other regularity missions of this family. Contributions formalizing Theorem 1.3 (finite-set central splitting) and Corollary 1.2 are welcome.

Selected references

• OpenAI, Tracial projection methods and uniform property $\Gamma$, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Tracial-projection-methods-and-uniform-property-Gamma-September-23-2026/paper.pdf
• J. Castillejos, S. Evington, A. Tikuisis, S. White, Uniform property $\Gamma$, Int. Math. Res. Not., 2022. https://doi.org/10.1093/imrn/rnaa282
• J. Castillejos, S. Evington, A. Tikuisis, S. White, W. Winter, Nuclear dimension of simple $C^*$-algebras, Invent. Math., 2021. https://doi.org/10.1007/s00222-020-01013-1
• C. Schafhauser, A. Tikuisis, S. White, Nuclear $C^*$-algebras: 99 problems, 2026. https://arxiv.org/abs/2506.10902
• J. R. Carrión et al., Tracially Complete $C^*$-Algebras, 2023. https://arxiv.org/abs/2310.20594
• L. G. Brown, G. K. Pedersen, $C^*$-algebras of real rank zero, J. Funct. Anal., 1991. https://doi.org/10.1016/0022-1236(91)90056-B
• W. Winter, J. Zacharias, The nuclear dimension of $C^*$-algebras, Adv. Math., 2010. https://doi.org/10.1016/j.aim.2009.12.005
• H. Matui, Y. Sato, Strict comparison and $\mathcal Z$-absorption of nuclear $C^*$-algebras, Acta Math., 2012. https://doi.org/10.1007/s11511-012-0084-4
• A. Vaccaro, Stable rank one, tracial local homogeneity and uniform property $\Gamma$, 2026. https://arxiv.org/abs/2604.24682

Motivation: the classical capacity of a thermal qubit channel

A quantum channel models how a physical system, used to carry information, is corrupted by its environment. The classical capacity of a channel is the largest rate, in bits per use, at which classical messages can be sent with vanishing error when the sender may encode into arbitrary — possibly entangled — states of many uses and the receiver may measure all outputs jointly. The Holevo–Schumacher–Westmoreland coding theorem (Holevo 1998; Schumacher–Westmoreland 1997) expresses this capacity as a regularized limit of the Holevo information over ever larger blocks of uses. Since Holevo information is not additive in general (Hastings 2009), computing the capacity of any specific channel requires a channel-specific additivity argument, and exact formulas are known only for a few families.

Generalized amplitude damping is the standard model of a qubit relaxing toward a thermal state: it loses or gains an excitation with probabilities set by a damping strength $\gamma$ and a stationary excited population $\nu$, and its coherences decay. It is one of the basic noise models of quantum information theory.

Background timeline

• 1996–1998 — Coding theorems for pure and mixed signals establish the regularized capacity formula (Hausladen et al. 1996; Schumacher–Westmoreland 1997; Holevo 1998).
• 2002 — Additivity for unital qubit channels (King 2002) and for entanglement-breaking channels (Shor 2002) settles some parameter regions of the family; Bennett, Shor, Smolin and Thapliyal describe the two-signal optimization for ordinary amplitude damping (BSST 2002).
• 2005 — Giovannetti and Fazio derive the optimized one-use expression for ordinary amplitude damping (Giovannetti–Fazio 2005); Berry studies qubit channels achieving capacity with two states (Berry 2005).
• 2007 — Hou and Fang characterize the one-use Holevo optimum of the generalized channel (Hou–Fang 2007).
• 2009 — Hastings shows that Holevo information is not additive in general (Hastings 2009).
• 2018 — Leditzky, Kaur, Datta and Wilde note that the unrestricted classical capacity of amplitude damping had not been determined (LKDW 2018).
• 2020 — Khatri, Sharma and Wilde collect upper bounds for the generalized family (KSW 2020).
• 2026 — Tang, Zhu, Bai and Wang prove additivity for qubit channels with a pure output, including ordinary amplitude damping (arXiv:2609.28592); Fang gives a close converse bound for the generalized family (arXiv:2609.14621).
• 2026 — An OpenAI preprint, Classical capacity and entropy inequalities for generalized amplitude damping (OpenAI Math Release, September 24, 2026), claims the capacity for all $(\gamma,\nu)\in[0,1]^2$. The preprint has not been peer reviewed, and its results are not formally verified.

Setting

For $\gamma,\nu\in[0,1]$ the generalized amplitude-damping channel acts on a qubit density matrix by

$$\mathcal A_{\gamma,\nu}\begin{pmatrix}1-q&z\\\bar z&q\end{pmatrix}=\begin{pmatrix}1-t&\sqrt{1-\gamma}\,z\\\sqrt{1-\gamma}\,\bar z&t\end{pmatrix},\qquad t=(1-\gamma)q+\gamma\nu,$$

and $n$ independent uses act as $\mathcal A_{\gamma,\nu}^{\otimes n}$ on $2^n\times2^n$ matrices. With $S(P)=-\operatorname{Tr}P\ln P$, the Holevo information in bits is

$$\chi(\mathcal N)=\frac1{\ln2}\sup_{\{q_a,\rho_a\}}\Bigl\{S\Bigl(\sum_aq_a\mathcal N(\rho_a)\Bigr)-\sum_aq_aS(\mathcal N(\rho_a))\Bigr\},$$

over all finite ensembles of input states (entangled across uses when $\mathcal N=\mathcal A^{\otimes n}$). The classical capacity $C(\mathcal N)$ is the supremum of rates $R$ for which there are $n$-use codes — arbitrary input states for each of $M_n$ equiprobable messages and one joint measurement of all outputs — with average error tending to zero and $\liminf_n n^{-1}\log_2M_n\ge R$; there is no shared entanglement or feedback. Write $h$ for binary entropy in nats, $g(u)=h\bigl((1+\sqrt{1-4u})/2\bigr)$ and $v_{\gamma,\nu}(p)=\gamma\nu(1-\nu)+\gamma(1-\gamma)(p-\nu)^2$.

Formalization targets

Goal: additivity and capacity formula (Theorem 1.1)

For all $\gamma,\nu\in[0,1]$ and every $n\ge1$,

$$\chi(\mathcal A_{\gamma,\nu}^{\otimes n})=n\,\chi(\mathcal A_{\gamma,\nu})=\frac n{\ln 2}\max_{0\le p\le1}\bigl\{h((1-\gamma)p+\gamma\nu)-g(v_{\gamma,\nu}(p))\bigr\},$$

the maximum is attained, $C(\mathcal A_{\gamma,\nu})=\chi(\mathcal A_{\gamma,\nu})$, and for every maximizer $p$ the equiprobable independent products of the two signals $\phi_\pm=\sqrt{1-p}\,|0\rangle\pm\sqrt p\,|1\rangle$ attain $\chi(\mathcal A_{\gamma,\nu}^{\otimes n})$ at every block length. The goal is published on the platform with status Open.

Significance

The result itself. The theorem gives a closed one-variable formula for the classical capacity of every generalized amplitude-damping channel, removing the regularization over block lengths: entangled input signals across uses give no advantage, and a simple product code with two signals per use is optimal. This settles the ordinary amplitude-damping case listed as open by LKDW 2018 and extends beyond the pure-output criterion of Tang et al. to the thermal regime, where the channel has no pure output. The source further proves additivity of Holevo capacity, minimum output entropy and classical capacity when the channel is used in parallel with any finite-dimensional partner channel (Corollary 1.2); that corollary is not part of this goal.

Formalizing it. The goal ties together an operational capacity (codes and error probabilities), an entropic quantity (a supremum over unrestricted ensembles on $2^n$-dimensional matrices), and a scalar optimization. A machine-checked proof would certify both the matrix entropy inequality at the heart of the argument and the converse direction of the coding theorem. Mathlib does not currently contain quantum channel capacity theory, so the definitions here are new infrastructure.

Difficulty

Optimizing a single use gives a lower bound on capacity; the difficulty is the matching upper bound for all $n$ simultaneously, where an input may be entangled across all uses. Holevo additivity is false for general channels, so no abstract argument applies, and for interior thermal occupation $0<\nu<1$ with $\gamma>0$ the channel has no pure output, which rules out the recent pure-output criterion. The proof needs a lower bound on the entropy of the output of an arbitrary entangled block input, i.e. a matrix entropy inequality for $2\times2$ block-structured states that is tight on product inputs. Identifying the capacity with the regularized Holevo quantity also requires the full coding theorem and a Fano-type converse.

Formalization scope

• Matrices are indexed by Fin n → Fin 2; the $n$-use channel is given by tensor products of the four standard Kraus operators of generalized amplitude damping, which reproduce the displayed action exactly.
• Entropy is Tr (cfc negMulLog P) (nats, $0\ln0=0$); Holevo values are divided by $\ln 2$ (bits). holevo γ ν n is the sSup over all finite ensembles of arbitrary $2^n$-dimensional states, with no product or purity restriction.
• capacity is the sSup of operationally achievable rates: codes with any positive number of messages, arbitrary state encodings, an arbitrary POVM decoder, average error tending to $0$, and the liminf rate condition. It is defined operationally, not by regularization, so the identity $C=\chi$ includes the coding theorem.
• The scalar objective uses Real.binEntropy (nats); the maximizer is over $p\in[0,1]$. The final clause also asserts that the phase-product signals are states.
• Parameters range over the closed square $[0,1]^2$, including boundary cases (identity channel at $\gamma=0$, full replacement at $\gamma=1$).
• Needed infrastructure: matrix entropy and its concavity, CPTP maps and Kraus representations, Holevo's bound, Fano's inequality, the HSW coding theorem for finite ensembles, and Fekete-type superadditivity. These are reusable for any quantum Shannon-theory mission.

Selected references

• P. Hausladen, R. Jozsa, B. Schumacher, M. Westmoreland, W. K. Wootters, Classical information capacity of a quantum channel, Phys. Rev. A 54 (1996), 1869–1876. https://doi.org/10.1103/PhysRevA.54.1869
• B. Schumacher and M. D. Westmoreland, Sending classical information via noisy quantum channels, Phys. Rev. A 56 (1997), 131–138. https://doi.org/10.1103/PhysRevA.56.131
• A. S. Holevo, The capacity of the quantum channel with general signal states, IEEE Trans. Inf. Theory 44 (1998), 269–273. https://doi.org/10.1109/18.651037
• C. King, Additivity for unital qubit channels, J. Math. Phys. 43 (2002), 4641–4653. https://doi.org/10.1063/1.1500791
• P. W. Shor, Additivity of the classical capacity of entanglement-breaking quantum channels, J. Math. Phys. 43 (2002), 4334–4340. https://doi.org/10.1063/1.1498000
• C. H. Bennett, P. W. Shor, J. A. Smolin, A. V. Thapliyal, Entanglement-assisted capacity of a quantum channel and the reverse Shannon theorem, IEEE Trans. Inf. Theory 48 (2002), 2637–2655. https://doi.org/10.1109/TIT.2002.802612
• V. Giovannetti and R. Fazio, Information-capacity description of spin-chain correlations, Phys. Rev. A 71 (2005), 032314. https://doi.org/10.1103/PhysRevA.71.032314
• D. W. Berry, Qubit channels that achieve capacity with two states, Phys. Rev. A 71 (2005), 032334. https://doi.org/10.1103/PhysRevA.71.032334
• L.-Z. Hou and M.-F. Fang, The Holevo capacity of a generalized amplitude-damping channel, Chinese Physics 16 (2007), 1843–1847. https://doi.org/10.1088/1009-1963/16/7/006
• M. B. Hastings, Superadditivity of communication capacity using entangled inputs, Nature Physics 5 (2009), 255–257. https://doi.org/10.1038/nphys1224
• F. Leditzky, E. Kaur, N. Datta, M. M. Wilde, Approaches for approximate additivity of the Holevo information of quantum channels, Phys. Rev. A 97 (2018), 012332. https://doi.org/10.1103/PhysRevA.97.012332
• S. Khatri, K. Sharma, M. M. Wilde, Information-theoretic aspects of the generalized amplitude-damping channel, Phys. Rev. A 102 (2020), 012401. https://doi.org/10.1103/PhysRevA.102.012401
• Z. Tang, C. Zhu, G. Bai, X. Wang, Classical capacity and entanglement cost of the amplitude damping channel, arXiv:2609.28592 (2026). https://arxiv.org/abs/2609.28592v1
• K. Fang, A pretty-tight converse on the classical capacity of generalized amplitude-damping channels, arXiv:2609.14621 (2026). https://arxiv.org/abs/2609.14621v1
• OpenAI, Classical capacity and entropy inequalities for generalized amplitude damping, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 3). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Classical-capacity-and-entropy-inequalities-for-generalized-amplitude-damping-September-24-2026/paper.pdf

Motivation: hardness of the molecular ground-state energy with ordinary nuclei

Computing the ground-state energy of electrons in the Coulomb field of fixed nuclei is the basic problem of quantum chemistry. In quantum complexity theory, a problem is QMA-hard if every problem with polynomial-time quantum verification of a quantum witness (the quantum analogue of NP) reduces to it. Hardness was previously known for lattice models with magnetic fields, for continuum models with freely designed potentials, and for electronic structure restricted to a supplied finite orbital basis. None of these is the exact problem in which the external field comes only from point nuclei of charge one — hydrogen-like nuclei — and the energy is minimized over every antisymmetric many-electron wavefunction in the continuum. Two obstacles separate the known results from this problem: a designed potential need not be a sum of unit Coulomb wells, and a projected (finite-basis) energy only bounds the continuum infimum from above.

Timeline

• 1959 — Anderson's superexchange mechanism: virtual hopping through double occupancy produces Heisenberg exchange (Anderson 1959).
• 1965 / 1990 — Moser and Dacorogna–Moser: transporting volume forms by flows, later used here to place equal-mass nuclei (Moser 1965, Dacorogna–Moser 1990).
• 2009 — Schuch and Verstraete: QMA-completeness of a Hubbard model with local magnetic fields and a continuum realization with designed scalar and spin-dependent potentials (Nature Phys. 2009).
• 2017 — Piddock and Montanaro: singlet-pair mediators turning signed into positive (antiferromagnetic) exchange, and 2D lattice hardness (QIC 2017).
• 2018/2019 — Cubitt, Montanaro and Piddock: universal quantum Hamiltonians, including spatially sparse QMA-hard Heisenberg models with polynomial interaction scales (PNAS 2018, arXiv:1701.05182v4).
• 2022 — O'Gorman, Irani, Whitfield and Fefferman: QMA-completeness of electronic structure in a supplied finite basis, including a unit-point-charge construction; the complete-space question is left open (PRX Quantum 2022).
• 2026 — Two OpenAI preprints (OpenAI Math Release, September 24, 2026) claim QMA-hardness of the full continuum problem: one with binary-encoded nuclear charges, and QMA-hardness of continuum Coulomb energy with unit nuclear charges (this mission). Neither is peer reviewed, and the theorem is not formally verified.

Setting

An instance consists of $M\ge1$ pairwise distinct positions $R_\alpha\in\mathbb Q^3$ of nuclei of charge one, an electron number $N\ge1$ encoded in unary, and rational thresholds $a<b$ (signed binary numerators, positive binary denominators). The electronic Hamiltonian is

$$H=-\frac12\sum_{i=1}^N\Delta_{x_i}-\sum_{i=1}^N\sum_{\alpha=1}^M\frac1{|x_i-R_\alpha|}+\sum_{1\le i<j\le N}\frac1{|x_i-x_j|}$$

on $\mathcal H_N=\bigwedge^N\big(L^2(\mathbb R^3)\otimes\mathbb C^2\big)$, defined through its closed form on $\mathcal Q_N=H^1(\mathbb R^{3N};(\mathbb C^2)^{\otimes N})\cap\mathcal H_N$. Antisymmetry exchanges position and spin together and no spin sector is selected. $E_0=\inf\operatorname{spec}H$ equals the infimum of the form over normalized vectors of $\mathcal Q_N$. YES: $E_0\le a$; NO: $E_0\ge b$. Nuclear repulsion is omitted.

In Lean, unitGroundEnergy is that infimum (as an EReal) over normalized antisymmetric $H^1$ states with explicit square-integrable weak gradients; InQMA is defined by polynomial-time uniform $\{H,T,\mathrm{CNOT}\}$ circuit families with completeness $2/3$ and soundness $1/3$; QMAHard requires a deterministic polynomial-time (Turing-machine computable) many-one reduction from every QMA promise problem.

Formalization targets

Goal: QMA-hardness with unit nuclear charges

$$\textsf{UnitCoulomb}\ \text{is QMA-hard under deterministic polynomial-time many-one reductions},$$

for the promise problem whose valid instances have threshold separation $b-a\ge1$. This is Theorem 1 of the source in the form produced by its reduction ("threshold separation at least one"), which implies the stated precision $b-a\ge L^{-1}$. The goal is published on the platform with status Open.

Significance

The result itself. The theorem shows that the exact clamped-nucleus electronic ground-energy problem is QMA-hard even when all nuclei are protons (charge one), with no supplied basis, magnetic field, or extra potential, and with constant threshold separation. It makes no claim of membership in QMA, of a molecular spectral gap, or of a ground eigenvector. It implies the companion binary-charge theorem, whose input class is larger, while the companion's proof gives independent tools.

Formalizing it. The Lean statement fixes the input encoding, the variational ground energy, and the notion of QMA precisely. Its proof would need the QMA-completeness source (an external theorem), finite spin and Hubbard reductions, and continuum estimates for Coulomb operators (localization, complement gaps, Hardy-type form bounds), most of which is absent from Mathlib. The definitions are shared with the binary-charge mission.

Difficulty

Unit nuclei offer no independently adjustable charges, so the wells needed for a Hubbard model must be produced by the geometry of many nuclei alone; the construction first builds a nonnegative continuous charge density and then replaces it by equal-mass point charges via a measure-transport flow and cubature, with rational rounding. The replacement error is not small on arbitrary states; only its compression to smooth localized modes is small. The lower bound must hold for every antisymmetric state in every spin sector, which requires a uniform gap on the one-particle complement and careful handling of the long-range direct Coulomb repulsion.

Formalization scope

• Inputs are UnitCoulomb records (a list of rational positions, unary electron count, two binary rationals) with a self-delimiting bit encoding; validity requires $M,N\ge1$, distinct positions, positive denominators and $b-a\ge1$. Lowest-terms encoding of rationals is not required in Lean, a harmless relaxation.
• unitGroundEnergy is computed by toNuclearData with every charge equal to one, using the same Coulomb form as the binary-charge definitions.
• QMA verifiers use the gate set $\{H,T,\mathrm{CNOT}\}$, uniform generation by Turing.TM2ComputableInPolyTime, and a polynomial size bound; the reduction must be polynomial-time computable on the encodings.
• Needed infrastructure: a formal QMA-completeness source for Heisenberg models, perturbative reductions, Sobolev/Hardy and quadratic-form methods for Coulomb operators, measure transport (Moser flow), and cubature error bounds.

Selected references

• P. W. Anderson, New approach to the theory of superexchange interactions, Phys. Rev. 115 (1959), 2–13. https://doi.org/10.1103/PhysRev.115.2
• J. Moser, On the volume elements on a manifold, Trans. Amer. Math. Soc. 120 (1965), 286–294. https://doi.org/10.1090/S0002-9947-1965-0182927-5
• B. Dacorogna and J. Moser, On a partial differential equation involving the Jacobian determinant, Ann. Inst. H. Poincaré C 7 (1990), 1–26. https://www.numdam.org/item/AIHPC_1990__7_1_1_0/
• N. Schuch and F. Verstraete, Computational complexity of interacting electrons and fundamental limitations of density functional theory, Nature Phys. 5 (2009), 732–735. https://doi.org/10.1038/nphys1370
• S. Piddock and A. Montanaro, The complexity of antiferromagnetic interactions and 2D lattices, Quantum Inf. Comput. 17 (2017), 636–672. https://www.rintonpress.com/xxqic17/qic-17-78/0636-0672.pdf
• T. S. Cubitt, A. Montanaro and S. Piddock, Universal quantum Hamiltonians, Proc. Natl. Acad. Sci. USA 115 (2018), 9497–9502. https://doi.org/10.1073/pnas.1804949115
• B. O'Gorman, S. Irani, J. Whitfield and B. Fefferman, Intractability of electronic structure in a fixed basis, PRX Quantum 3 (2022), 020322. https://doi.org/10.1103/PRXQuantum.3.020322
• G. Teschl, Mathematical Methods in Quantum Mechanics, Graduate Studies in Mathematics 99, AMS, 2009. https://www.mat.univie.ac.at/~gerald/ftp/book-schroe/schroe.pdf
• OpenAI, Continuum Coulomb hardness with binary nuclear charges, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Continuum-Coulomb-hardness-with-binary-nuclear-charges-September-24-2026/Continuum-Coulomb-hardness-with-binary-nuclear-charges-September-24-2026.pdf
• OpenAI, QMA-hardness of continuum Coulomb energy with unit nuclear charges, OpenAI Math Release preprint, September 24, 2026 (Theorem 1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/QMA-hardness-of-continuum-Coulomb-energy-with-unit-nuclear-charges-September-24-2026/QMA-hardness-of-continuum-Coulomb-energy-with-unit-nuclear-charges-September-24-2026.pdf

Motivation: how hard is the molecular ground-state energy?

Computing the ground-state energy of a molecule — electrons moving in the Coulomb field of fixed nuclei — is the central task of quantum chemistry. Quantum complexity theory asks whether it is hard even for a quantum computer: a problem is QMA-hard if every problem verifiable by a polynomial-time quantum verifier with a quantum witness reduces to it (QMA is the quantum analogue of NP). Many lattice and finite-basis versions of electronic structure are known to be QMA-complete, but those results either allow magnetic fields and designed potentials, or restrict the electrons to a supplied finite orbital basis. The exact problem — external field generated only by positive point nuclei, minimization over the full continuum of antisymmetric many-electron wavefunctions — needs a lower bound excluding every state outside any chosen orbital set, which projection arguments do not provide.

Timeline

• 1959 — Anderson's theory of superexchange: virtual double occupancy produces Heisenberg exchange between localized spins (Anderson 1959).
• 2007 — Liu, Christandl and Verstraete: QMA-completeness of $N$-representability (finite modes, Turing reductions) (PRL 2007).
• 2009 — Schuch and Verstraete: QMA-completeness of a Hubbard model with local magnetic fields, with a continuum realization using designed scalar and spin-dependent potentials (Nature Phys. 2009).
• 2013 — Whitfield, Love and Aspuru-Guzik survey complexity in electronic structure and the role of magnetic fields (PCCP 2013).
• 2017–2018 — Piddock and Montanaro: complexity of antiferromagnetic interactions on 2D lattices (QIC 17, 2017); Cubitt, Montanaro and Piddock: universal quantum Hamiltonians, including QMA-hard field-free Heisenberg models (PNAS 2018).
• 2022 — O'Gorman, Irani, Whitfield and Fefferman: QMA-completeness of electronic structure in a supplied finite basis, explicitly raising the complete-space question (PRX Quantum 2022).
• 2026 — Two OpenAI preprints (OpenAI Math Release, September 24, 2026) claim QMA-hardness of the exact continuum problem: Continuum Coulomb hardness with binary nuclear charges (this mission) and a companion with unit nuclear charges. Neither is peer reviewed, and the theorem is not formally verified.

Setting

An instance consists of $M\ge1$ pairwise distinct nuclear positions $R_\alpha\in\mathbb Q^3$, positive integer charges $Z_\alpha$ (encoded in binary), an electron number $N\ge1$ (encoded in unary), and rational thresholds $a<b$. The electronic Hamiltonian, in atomic units, is

$$H=-\frac12\sum_{\ell=1}^N\Delta_{x_\ell}-\sum_{\ell=1}^N\sum_{\alpha=1}^M\frac{Z_\alpha}{|x_\ell-R_\alpha|}+\sum_{1\le\ell<k\le N}\frac1{|x_\ell-x_k|}$$

on the antisymmetric space $\bigwedge^N L^2(\mathbb R^3;\mathbb C^2)$ (positions and spins permuted together), defined through its closed quadratic form on $H^1\cap\bigwedge^N L^2$. Let $E_0=\inf\operatorname{Spec}H$. YES instances have $E_0\le a$; NO instances have $E_0\ge b$. Nuclear repulsion is omitted (clamped-nucleus electronic energy) and all spin sectors are included.

In Lean, groundEnergy is the infimum (in EReal) of the Coulomb form over normalized antisymmetric $H^1$ states, given by explicit square-integrable values and weak gradients; QMA is defined through polynomial-time uniform families of $\{H, T, \mathrm{CNOT}\}$ circuits with acceptance $\ge2/3$ / $\le1/3$; QMAHard asks for a deterministic polynomial-time many-one reduction (as a Turing-machine-computable map on bit strings) from every QMA promise problem.

Formalization targets

Goal: QMA-hardness with binary charges

$$\textsf{BinaryCoulomb}\ \text{is QMA-hard under deterministic polynomial-time many-one reductions},$$

for the promise problem whose valid instances satisfy $b-a\ge1$. This is Theorem 1.1 of the source in its stronger form ("the reduction can produce instances with $b-a\ge1$"), which implies the stated precision $b-a\ge L^{-1}$. The goal is published on the platform with status Open.

Significance

The result itself. The theorem places the exact clamped-nuclei electronic ground-energy problem, with no supplied basis, field, or designed potential, among QMA-hard problems at inverse-polynomial (indeed constant) precision. It makes no claim of membership in QMA, of a spectral gap, or of hardness under bounded charges. The companion unit-charge theorem implies this one for the larger binary-charge input class; the present proof is independent and contributes certified exponential-accuracy eigenvalue computation and relative tunneling calibration for widely separated hydrogenic wells.

Formalizing it. A complete formalization would combine a QMA-completeness source theorem (Heisenberg models), finite spin and Hubbard reductions, and continuum many-body spectral estimates (Hardy inequality, localization, complement gaps) — a large but well-delimited body of mathematics, much of it absent from Mathlib. The precise Lean encoding of inputs and of QMA itself is reusable for other Hamiltonian-complexity missions.

Difficulty

Projecting $H$ onto chosen orbitals gives an upper bound on $E_0$ but says nothing about states outside the projection, so finite-basis hardness does not transfer NO instances. The construction must realize prescribed, exponentially small Hubbard hoppings using only point nuclei, with relative (not absolute) precision, and must certify one-well energies to exponential accuracy using polynomially many bits. Finally a lower bound for the full many-electron spectral infimum must hold for every fermionic state, in every spin sector.

Formalization scope

• Inputs are BinaryCoulomb records (list of rational positions with natural charges, unary electron count, two binary rationals) with an explicit self-delimiting bit encoding; validity requires $M,N\ge1$, distinct positions, positive denominators, positive charges, and $b-a\ge1$. Lowest-terms encoding is not required in Lean, a harmless relaxation.
• The state space is H1Vector n with antisymmetry under simultaneous permutation of positions and spins; groundEnergy is an EReal infimum over normalized states, which is the variational characterization of $\inf\operatorname{Spec}H$.
• QMA uses a fixed universal gate set $\{H,T,\mathrm{CNOT}\}$ and polynomial-time Turing-machine uniformity (Turing.TM2ComputableInPolyTime); the reduction must also be TM2ComputableInPolyTime.
• A trivial proof is excluded: YES/NO sets are disjoint by construction and the reduction must preserve both promises for every QMA problem.
• Needed infrastructure: a QMA-complete source (Kitaev-type local Hamiltonian / Heisenberg problem), perturbative gadgets, Hardy inequality, quadratic-form methods for Coulomb operators, and certified numerical analysis.

Selected references

• P. W. Anderson, New approach to the theory of superexchange interactions, Phys. Rev. 115 (1959), 2–13. https://doi.org/10.1103/PhysRev.115.2
• Y.-K. Liu, M. Christandl and F. Verstraete, Quantum computational complexity of the N-representability problem: QMA complete, Phys. Rev. Lett. 98 (2007), 110503. https://doi.org/10.1103/PhysRevLett.98.110503
• N. Schuch and F. Verstraete, Computational complexity of interacting electrons and fundamental limitations of density functional theory, Nature Phys. 5 (2009), 732–735. https://doi.org/10.1038/nphys1370
• J. D. Whitfield, P. J. Love and A. Aspuru-Guzik, Computational complexity in electronic structure, Phys. Chem. Chem. Phys. 15 (2013), 397–411. https://doi.org/10.1039/C2CP42695A
• S. Piddock and A. Montanaro, The complexity of antiferromagnetic interactions and 2D lattices, Quantum Inf. Comput. 17 (2017), 636–672.
• T. S. Cubitt, A. Montanaro and S. Piddock, Universal quantum Hamiltonians, Proc. Natl. Acad. Sci. USA 115 (2018), 9497–9502. https://doi.org/10.1073/pnas.1804949115
• B. O'Gorman, S. Irani, J. Whitfield and B. Fefferman, Intractability of electronic structure in a fixed basis, PRX Quantum 3 (2022), 020322. https://doi.org/10.1103/PRXQuantum.3.020322
• OpenAI, QMA-hardness of continuum Coulomb energy with unit nuclear charges, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/QMA-hardness-of-continuum-Coulomb-energy-with-unit-nuclear-charges-September-24-2026/QMA-hardness-of-continuum-Coulomb-energy-with-unit-nuclear-charges-September-24-2026.pdf
• OpenAI, Continuum Coulomb hardness with binary nuclear charges, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Continuum-Coulomb-hardness-with-binary-nuclear-charges-September-24-2026/Continuum-Coulomb-hardness-with-binary-nuclear-charges-September-24-2026.pdf

Motivation

Parity, $\mathrm{PARITY}_n(x)=x_1\oplus\cdots\oplus x_n$, is the standard test of whether a shallow circuit can aggregate information from all of its inputs. Classically, constant-depth circuits with unbounded fan-in AND/OR gates ($\mathsf{AC}^0$) cannot compute it: Furst, Saxe and Sipser (Math. Systems Theory 1984) and Ajtai (APAL 1983) proved superpolynomial lower bounds, and Håstad's switching lemma gave nearly optimal exponential ones (STOC 1986). The quantum analogue $\mathsf{QAC}^0$ allows arbitrary one-qubit unitaries and Toffoli gates of unbounded arity, but gates in one layer must act on disjoint qubits, so a wire cannot control many simultaneous gates. Moore (arXiv:quant-ph/9903046, 1999) showed that coherent parity and quantum fanout are equivalent under Hadamard conjugation, and conjectured that neither is in $\mathsf{QAC}^0$. Because fanout makes constant-depth quantum circuits very powerful (Høyer–Špalek, ToC 2005), whether $\mathrm{PARITY}\notin\mathsf{QAC}^0$ has been a central question about shallow quantum computation.

Background

• 1999 — Moore introduces the quantum circuit classes and the parity/fanout conjecture.
• 2002 — Green, Homer, Moore and Pollett develop quantum counting classes and modular-gate equivalences (QIC 2002).
• 2006 — Fang, Fenner, Green, Homer and Zhang: depth $\Omega(\log(n/(a+1)))$ for exact clean parity with $a$ ancillas (QIC 2006).
• 2020–2021 — Padé, Fenner, Grier and Thierauf rule out exact clean parity at entangling depth two (arXiv:2005.12169); Rosenthal bounds approximate parity unitaries (ITCS 2021).
• 2024–2025 — Pauli-spectrum lower bounds with restricted ancillas (Nadimpalli, Parham, Vasconcelos, Yuen, STOC 2024); no fixed parity advantage with barely superlinear ancillas (Anshu, Dong, Ou, Yao, STOC 2025), extended by Dong, Ou and Yao (arXiv:2510.00593).
• 2026 — Joshi, Tal, Vasconcelos and Wright: exact parity lower bounds at entangling depth three without size restriction (STOC 2026); Gretta, Gupta and Joshi relate the question to Fourier concentration (arXiv:2604.02793).
• September 2026 — Two OpenAI preprints claim the lower bound for every fixed depth and every polynomial number of qubits, by independent arguments: product-projection localization (source) and regular trajectories with pruning (source).

This mission asks for a formal proof of the parity lower bound stated as Theorem 1 of 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.

Setting

A circuit acts on $N$ qubits, with state space $(\mathbb C^2)^{\otimes N}$ and computational basis indexed by bit strings $y\in\{0,1\}^N$. The allowed gates are arbitrary one-qubit unitaries and generalized Toffoli gates $|z_1,\dots,z_t,b\rangle\mapsto|z_1,\dots,z_t,b\oplus z_1\cdots z_t\rangle$ on distinct control and target qubits. A layer is a set of gates with pairwise disjoint supports, and a depth-$d$ circuit is a product $W=L_d\cdots L_1$ of at most $d$ layers. Gates and their complex entries may depend on $n$ but not on the input.

On input $x\in\{0,1\}^n$ with $n\le N$, the circuit starts in $|x\rangle\otimes|0\rangle^{\otimes(N-n)}$. One designated output qubit is measured in the computational basis; all other qubits are discarded in arbitrary states, and the input need not be preserved. The success probability on $x$ is

$$\Pr[\text{output}=\mathrm{PARITY}_n(x)]=\sum_{y:\ y_{\mathrm{out}}=\mathrm{PARITY}_n(x)}\bigl|\langle y|W|x,0\rangle\bigr|^2 .$$

A circuit computes parity with worst-case advantage $\varepsilon$ if this probability is at least $1/2+\varepsilon$ for every $x$.

Formalization targets

Goal: the parity lower bound (Theorem 1, p. 1)

Fix an integer $d\ge0$, a real $c\ge1$ and $0<\varepsilon\le1/2$. Then for all sufficiently large $n$, for every $N$ with $n\le N\le n^c$, every circuit of depth at most $d$ on $N$ qubits and every choice of output qubit, there is an input $x\in\{0,1\}^n$ with

$$\Pr[\text{output}=\mathrm{PARITY}_n(x)]<\tfrac12+\varepsilon .$$

With $\varepsilon=1/6$ this is the usual bounded-error statement $\mathrm{PARITY}\notin\mathsf{QAC}^0$ in the measured-output model.

Significance

The result itself. It answers Moore's question for every fixed depth and every polynomial bound on the total number of qubits, with arbitrary final garbage and any fixed positive advantage, whereas earlier results fixed the entangling depth or restricted the number of ancillas. Through Hadamard conjugation it also excludes constant-depth polynomial-size coherent fanout. The preprint derives further consequences (Section 7): state-preparation obstructions (Corollary 8, p. 14), a qualitative quantum LMN-type Fourier tail bound (Corollary 9, p. 16), and, via reductions of Xu and Li, lower bounds for majority and other symmetric functions (Corollaries 10–11, pp. 17–18). The structural Theorem 2 (p. 5), localization of conjugated product projections, is of independent interest.

Formalizing it. The statement is elementary (finite matrices, Born probabilities) while the proof is a two-level induction with polynomial approximation, so a formal proof would give a fully checked circuit lower bound in quantum complexity, an area with few machine-checked results. A companion OpenAI preprint gives an independent proof by regular trajectories and pruning.

Difficulty

Light-cone arguments fail at once: a single Toffoli gate may touch every qubit, so after one layer an output can depend on all inputs. Spectral and Pauli-weight methods previously needed ancilla bounds such as $\tilde O(n^{1+2^{-d}})$. The preprint's route controls transitions from a product condition to states with many mismatches, $\bigl\|[M\ge N^t]\,U\,[D=0]\,U^\dagger\,[M=0]\bigr\|\le e^{-N^s}$ for all fixed $0\le s<t$ (Theorem 2, p. 5). The obstacle is that reflection expansions cost exponentially in the projection's support, and low-degree polynomial surrogates for a product projection are accurate only at low mismatch counts; the uncontrolled high-count error is handled by a second induction on thresholds that exchanges the roles of the two counts.

Formalization scope

• Word N := Fin N → Fin 2; operators are complex matrices indexed by words. Gate.local q u is a one-qubit unitary tensored with identities; Gate.toffoli controls target is the permutation matrix flipping the target when all controls are $1$ (an empty control set gives a NOT gate, itself a one-qubit unitary).
• PhysicalLayer N is a list of gates whose supports are pairwise disjoint; its matrix is the product of the gate matrices. physicalCircuitMatrix layers applies the layers in list order (rightmost matrix acts first).
• inputWord x pads $x$ with zeros; successProbability W out x sums $|W_{y,(x,0)}|^2$ over all $y$ whose output bit equals the parity of $x$, so final garbage is unrestricted.
• The output qubit out : Fin N is arbitrary, including an input qubit. The quantifier order is: depth, size bound and advantage fixed first; then a threshold $n_0$; then every $n\ge n_0$, every $N$ in range, every circuit and every output qubit.
• No intermediate measurement, postselection or fanout gate is in the model; the statement is a pure statement about unitary matrices, with no complexity-class machinery.
• ParityStatement takes the size bound as a real exponent: $N\le n^c$ with $c\ge1$ real, $n\le N$, and depth layers.length ≤ d with $d\ge0$, exactly as in Theorem 1. Its conclusion is the negation of "for every $x$, success $\ge 1/2+\varepsilon$".

Welcome contributions: a reusable Lean model of unitary circuits on qubits, spectral projections of commuting count operators, and Chebyshev-type polynomial approximation with coefficient bounds (Lemma 3, p. 6).

Selected references

• OpenAI, Product-projection localization and the QAC0 parity lower bound, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Product-projection-localization-and-the-QAC0-parity-lower-bound-September-24-2026/paper.pdf
• OpenAI, Regular trajectories, pruning and quantum parity, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Regular-trajectories-pruning-and-quantum-parity-September-24-2026/paper.pdf
• C. Moore, Quantum circuits: fanout, parity, and counting, arXiv:quant-ph/9903046 (1999). https://arxiv.org/abs/quant-ph/9903046v3
• M. Furst, J. B. Saxe, M. Sipser, Parity, circuits, and the polynomial-time hierarchy, Math. Systems Theory 17 (1984), 13–27. https://doi.org/10.1007/BF01744431
• M. Ajtai, $\Sigma^1_1$-formulae on finite structures, Ann. Pure Appl. Logic 24 (1983), 1–48. https://doi.org/10.1016/0168-0072(83)90038-6
• J. Håstad, Almost optimal lower bounds for small depth circuits, STOC 1986. https://doi.org/10.1145/12130.12132
• F. Green, S. Homer, C. Moore, C. Pollett, Counting, fanout and the complexity of quantum ACC, QIC 2 (2002). https://doi.org/10.26421/QIC2.1-3
• P. Høyer, R. Špalek, Quantum fan-out is powerful, Theory of Computing 1 (2005). https://doi.org/10.4086/toc.2005.v001a005
• M. Fang, S. Fenner, F. Green, S. Homer, Y. Zhang, Quantum lower bounds for fanout, QIC 6 (2006). https://doi.org/10.26421/QIC6.1-3
• G. Rosenthal, Bounds on the QAC0 complexity of approximating parity, ITCS 2021. https://doi.org/10.4230/LIPIcs.ITCS.2021.32
• S. Nadimpalli, N. Parham, F. Vasconcelos, H. Yuen, On the Pauli spectrum of QAC0, STOC 2024. https://doi.org/10.1145/3618260.3649662
• M. R. Joshi, A. Tal, F. Vasconcelos, J. Wright, Improved lower bounds for QAC0, STOC 2026. https://doi.org/10.1145/3798129.3800922
• L. Gretta, M. Gupta, M. R. Joshi, Parity ∉ QAC0 ⟺ QAC0 is Fourier-concentrated, arXiv:2604.02793 (2026). https://arxiv.org/abs/2604.02793v2

Motivation

The quantum Heisenberg ferromagnet is the basic quantum model of a magnet: a quantum spin sits at each site of the lattice $\mathbb Z^d$ and neighbouring spins prefer to align. Its Hamiltonian is invariant under simultaneous rotation of all spins, so at zero external field no direction is preferred. Spontaneous magnetization asks whether an infinite-volume equilibrium state at positive temperature can nevertheless choose a direction, giving a nonzero expected spin at a single site. For classical spins and for quantum antiferromagnets this was settled decades ago; for the quantum ferromagnet in $d\ge3$ it has been a standard open problem of mathematical physics, recorded by Lieb in 1999 and again by Seiringer in 2025.

Timeline

• 1928–1930. Heisenberg proposes the exchange model of ferromagnetism (doi:10.1007/BF01328601); Bloch's spin-wave picture predicts the low-temperature reduction of magnetization (doi:10.1007/BF01339661).
• 1956. Dyson develops the theory of interacting spin waves and its thermodynamics (doi:10.1103/PhysRev.102.1217, doi:10.1103/PhysRev.102.1230).
• 1966. Mermin and Wagner exclude positive-temperature ferro- and antiferromagnetism for finite-range isotropic Heisenberg models in $d=1,2$ (doi:10.1103/PhysRevLett.17.1133).
• 1967. Haag, Hugenholtz and Winnink formulate equilibrium of infinite systems through the KMS condition (doi:10.1007/BF01646342).
• 1976. Fröhlich, Simon and Spencer prove low-temperature ordering for classical continuous-spin models in $d\ge3$ via infrared bounds (doi:10.1007/BF01608557); Powers relates the Heisenberg model to random walks on the permutation group (doi:10.1007/BF00398374).
• 1978. Dyson, Lieb and Simon prove ordering for quantum antiferromagnets (spin $\ge1$ in $d\ge3$, spin $\tfrac12$ in high dimension) and explain why reflection positivity gives no ferromagnetic infrared bound (doi:10.1007/BF01106729).
• 1988. Kennedy, Lieb and Shastry prove ground-state Néel order for the spin-$\tfrac12$ antiferromagnet on $\mathbb Z^3$ (doi:10.1007/BF01023854).
• 1991–1994. Conlon–Solovej random-walk representations and free-energy upper bound (doi:10.1007/BF01057876); Tóth's improved pressure bound (1993, doi:10.1007/BF00739568); Nachtergaele's general-spin stochastic-geometric representations (1994, doi:10.1007/978-94-015-8326-8_14).
• 1999. Lieb poses ferromagnetic long-range order as Problem A of the Mathematical Physics Open Problems list.
• 2015. Correggi, Giuliani and Seiringer prove the spin-wave free-energy asymptotics in $d=3$ (arXiv:1312.7873).
• 2020. Björnberg, Fröhlich and Ueltschi analyse the loop representation on the complete graph (arXiv:1811.12834).
• 2025–2026. Seiringer records the ordering problem in an Oberwolfach report; Klippel proves the free-energy asymptotics in $d=2$ (arXiv:2608.25506).

The source of this mission is an OpenAI preprint dated September 24, 2026, which claims a proof of spontaneous magnetization for every spin and every $d\ge3$.

Setting

Fix $d\ge3$ and a spin $S\in\{\tfrac12,1,\tfrac32,\dots\}$; write $\ell=2S$. Each site carries $\mathbb C^{2S+1}$ with basis $(e_m)_{m=-S}^{S}$ and

$$S^ze_m=me_m,\qquad S^+e_m=\sqrt{S(S+1)-m(m+1)}\,e_{m+1},\qquad S^-=(S^+)^*,$$

$S^x=(S^++S^-)/2$, $S^y=(S^+-S^-)/(2i)$. For finite $\Lambda\subset\mathbb Z^d$ the free-boundary Hamiltonian is

$$H_\Lambda=-\sum_{\{x,y\}\subset\Lambda,\ |x-y|_1=1}\ \bigl(S^x_xS^x_y+S^y_xS^y_y+S^z_xS^z_y\bigr),$$

each unordered edge counted once. The quasi-local algebra $\mathcal A$ is the norm completion of the local matrix algebras $\bigotimes_{x\in F}M_{2S+1}(\mathbb C)$. The dynamics is $\tau_t(A)=\lim_n e^{itH_{\Lambda_n}}Ae^{-itH_{\Lambda_n}}$ along the boxes $\Lambda_n=[-n,n]^d$.

A state is a positive linear functional $\omega$ on $\mathcal A$ with $\omega(1)=1$. It is $\beta$-KMS if for all $A,B\in\mathcal A$ there is a bounded function $F$, continuous on $\{0\le\operatorname{Im}z\le\beta\}$ and analytic inside, with

$$F(t)=\omega(A\,\tau_t(B)),\qquad F(t+i\beta)=\omega(\tau_t(B)\,A)\qquad(t\in\mathbb R).$$

It is translation invariant if $\omega\circ T_x=\omega$ for all $x\in\mathbb Z^d$.

Formalization targets

Goal: Theorem 1.1

$$\exists\,\beta_0>0\ \ \forall\,\beta\ge\beta_0\ \ \exists\,\omega\ \text{translation invariant, }\beta\text{-KMS for }\tau,\quad \omega(S_0^z)\ \ge\ \frac S4.$$

The Lean statement OAI.Heisenberg.spontaneous_magnetization also asserts that the box limits defining $\tau_t(A)$ converge for every $t$ and $A$ (the standing fact the theorem relies on). The goal is open on the platform.

Significance

The theorem gives an equilibrium state of the zero-field model, at every sufficiently low positive temperature, that breaks the rotation symmetry: a translation-invariant KMS state with one-site magnetization at least $S/4$. It addresses the ordering problem in its spontaneous-magnetization formulation; the volume-averaged finite-volume two-point criterion in Seiringer's account is a different formulation that the paper does not use. For $S=\tfrac12$ the Matsubara–Matsuda correspondence turns the ordered state into a hard-core boson state with off-diagonal long-range order, a lattice analogue of Bose–Einstein condensation.

The result is stated in an OpenAI preprint; it has not been peer reviewed, and there is no machine-checked proof. A formal proof would certify a long argument (loop representation, stable-polynomial pin test, Markov-walk return estimates, flow constructions and the KMS limit) whose individual steps are each delicate.

Difficulty

The classical route to continuous-symmetry breaking, infrared bounds from reflection positivity, fails for the quantum ferromagnet: as Dyson, Lieb and Simon explained, it does not yield the needed Duhamel bound. Spin-wave free-energy asymptotics, now known in $d=2,3$, control correlations only on a temperature-dependent finite length scale, not at all scales at a fixed temperature. Loop representations give positive weights, but positivity alone does not imply ordering: one must show that an interior cycle rarely avoids pins placed on the boundary, uniformly in the volume. Finally, a KMS state must be produced for the zero-field dynamics itself, so the symmetry-breaking field used in finite volume has to be removed while both KMS boundary conditions survive.

Formalization scope

• Sites are Fin d → ℤ; a spin level is Fin (ℓ+1) with magnetic quantum number $k-\ell/2$. The Hilbert space is $\ell^2$ of finitely supported configurations Site d →₀ Fin (ℓ+1), and the quasi-local algebra is the norm closure of the star-algebra generated by single-site matrix units on it (a faithful copy of the abstract quasi-local algebra).
• hamiltonian d ℓ Λ sums over nearest-neighbour pairs ($\ell^1$ distance one) with one orientation per edge; box d n is $[-n,n]^d$; dynamics is the limUnder of the box dynamics, and DynamicsConverges asserts that these limits exist.
• State packages a continuous linear functional with $\omega(1)=1$ and $\omega(A^*A)\ge0$; IsKMS β ω requires $0<\beta$ and, for every $A,B$, a bounded $F$ continuous on the closed strip, complex-differentiable on the open strip, with the two boundary identities.
• The conclusion reads $\operatorname{Im}\omega(S^z_0)=0$ and $\operatorname{Re}\omega(S^z_0)\ge\ell/8$.

A complete development needs quantum spin systems on $\mathbb Z^d$, Lieb–Robinson-type existence of infinite-volume dynamics, KMS states, and the probabilistic loop machinery. The quantum-spin and KMS infrastructure is reusable for other lattice models (including the Bloch-law missions of this family). Contributions formalizing the existence of the dynamics, Proposition 2.2 (spin-to-loop representation), Proposition 3.1 (simultaneous pin test) and Proposition 8.2 (vanishing-field limit) are welcome.

Selected references

• OpenAI, Spontaneous magnetization in the quantum Heisenberg ferromagnet, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Spontaneous-magnetization-in-the-quantum-Heisenberg-ferromagnet-September-24-2026/paper.pdf
• E. H. Lieb, Long Range Order for the Quantum Heisenberg Model, Mathematical Physics Open Problems, Problem A, 1999. https://web.math.princeton.edu/~aizenman/OpenProblems_MathPhys/9901.HeisenbergFerr.html
• R. Seiringer, The Heisenberg Ferromagnet: A Dilute Bose Gas in Disguise, Oberwolfach Report 7/2025. https://doi.org/10.4171/OWR/2025/7
• N. D. Mermin, H. Wagner, Absence of Ferromagnetism or Antiferromagnetism in One- or Two-Dimensional Isotropic Heisenberg Models, Phys. Rev. Lett., 1966. https://doi.org/10.1103/PhysRevLett.17.1133
• J. Fröhlich, B. Simon, T. Spencer, Infrared Bounds, Phase Transitions and Continuous Symmetry Breaking, Comm. Math. Phys., 1976. https://doi.org/10.1007/BF01608557
• F. J. Dyson, E. H. Lieb, B. Simon, Phase Transitions in Quantum Spin Systems with Isotropic and Nonisotropic Interactions, J. Stat. Phys., 1978. https://doi.org/10.1007/BF01106729
• M. Correggi, A. Giuliani, R. Seiringer, Validity of the Spin-Wave Approximation for the Free Energy of the Heisenberg Ferromagnet, Comm. Math. Phys., 2015. https://arxiv.org/abs/1312.7873
• B. Nachtergaele, Y. Ogata, R. Sims, Propagation of Correlations in Quantum Lattice Systems, J. Stat. Phys., 2006. https://arxiv.org/abs/math-ph/0603064
• J. Borcea, P. Brändén, T. M. Liggett, Negative Dependence and the Geometry of Polynomials, J. Amer. Math. Soc., 2009. https://arxiv.org/abs/0707.2340
• R. Haag, N. M. Hugenholtz, M. Winnink, On the equilibrium states in quantum statistical mechanics, Comm. Math. Phys., 1967. https://doi.org/10.1007/BF01646342

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

Lieb–Thirring inequalities bound the negative eigenvalues of a Schrödinger operator $-\Delta-W$ by an integral of the potential. Lieb and Thirring introduced them in 1975 to give a short proof of the stability of matter, and they remain basic tools in mathematical physics, spectral theory and the analysis of many-fermion systems. The sharp constants are known only in a few cases. In one dimension, the Lieb–Thirring conjecture predicts the sharp constant for every exponent $\gamma$: for $1/2<\gamma<3/2$ it should be the constant of the best potential with a single bound state, given by an explicit $\operatorname{sech}^2$ profile.

Timeline

• 1961. Keller solves the one-bound-state variational problem (doi:10.1063/1.1703708).
• 1971, 1974. Inverse-scattering trace identities for the KdV equation give the sharp value $L_{3/2,1}=3/16$ (Zakharov–Faddeev, doi:10.1007/BF01086739; Gardner–Greene–Kruskal–Miura, doi:10.1002/cpa.3160270108).
• 1975–1976. Lieb and Thirring prove their inequalities and state the one-dimensional conjecture (doi:10.1103/PhysRevLett.35.687).
• 1978. Aizenman and Lieb extend semiclassical equality to all $\gamma\ge3/2$ (doi:10.1016/0375-9601(78)90385-7).
• 1996, 1998. Weidl proves finiteness of $L_{1/2,1}$ (doi:10.1007/BF02104912); Hundertmark, Lieb and Thomas obtain its sharp value $1/2$ (doi:10.4310/ATMP.1998.v2.n4.a2).
• 2000. Laptev and Weidl prove sharp semiclassical constants in all dimensions for $\gamma\ge3/2$ (doi:10.1007/BF02392782); Hundertmark, Laptev and Weidl prove $L_{\gamma,1}\le2L^{\rm cl}_{\gamma,1}$ for $1/2\le\gamma<3/2$ (doi:10.1007/s002220000077).
• 2008–2025. Improved constants at $\gamma=1$ by Dolbeault–Laptev–Loss (doi:10.4171/JEMS/142), Frank–Hundertmark–Jex–Nam (doi:10.4171/JEMS/1062) and Corso–Ried (doi:10.1007/s00220-024-05216-y); Levitt's numerics support the conjectured value (doi:10.4171/JST/65).
• 2026. Read and Schulz prove the sharp case $\gamma=1$ (arXiv:2609.10478).

The source of this mission, an OpenAI preprint dated September 23, 2026, proves the conjectured sharp constant for every $1/2<\gamma<3/2$.

Setting

For $0\le W\in L^{\gamma+1/2}(\mathbb R)$, let $H_{-W}$ be the self-adjoint operator of the quadratic form

$$h_{-W}[v]=\int_{\mathbb R}|v'|^2\,dx-\int_{\mathbb R}W|v|^2\,dx,\qquad v\in H^1(\mathbb R).$$

For $\gamma>1/2$ its negative spectrum is discrete; write $\operatorname{Tr}(H_{-W})_-^\gamma=\sum_{\lambda_j<0}|\lambda_j|^\gamma$ with multiplicity, possibly $+\infty$ a priori. The optimal constant is

$$L_{\gamma,1}=\sup_{0\le W\in L^{\gamma+1/2},\ W\not\equiv0}\frac{\operatorname{Tr}(H_{-W})_-^\gamma}{\int W^{\gamma+1/2}},$$

$L^{(1)}_{\gamma,1}$ is the same supremum with only the lowest eigenvalue retained, and the semiclassical constant is

$$L^{\rm cl}_{\gamma,1}=\frac{\Gamma(\gamma+1)}{2\sqrt\pi\,\Gamma(\gamma+3/2)}.$$

Formalization targets

Goal: Theorem 1.1

For $1/2<\gamma<3/2$ and every $0\le W\in L^{\gamma+1/2}(\mathbb R)$,

$$\operatorname{Tr}(H_{-W})_-^\gamma\ \le\ 2\Bigl(\frac{\gamma-1/2}{\gamma+1/2}\Bigr)^{\gamma-1/2}L^{\rm cl}_{\gamma,1}\int_{\mathbb R}W^{\gamma+1/2};$$

the constant equals $L_{\gamma,1}=L^{(1)}_{\gamma,1}$, and with $r=(\gamma-1/2)^{-1}$ equality holds for $W(x)=(r+1)\operatorname{sech}^2(rx)$. The Lean statement OAI.SharpLiebThirring.sharp_lieb_thirring is open on the platform.

Significance

The theorem settles the one-dimensional Lieb–Thirring conjecture on the whole interval $1/2<\gamma<3/2$, extending the case $\gamma=1$ of Read and Schulz: allowing many bound states never beats a single optimally shaped well. Combined with the known endpoint results ($\gamma=1/2$ and $\gamma\ge3/2$), it completes the sharp one-dimensional constants. It also gives the corresponding bound for signed potentials (Corollary 7.3), and through the Laptev–Weidl lifting method one-dimensional sharp constants feed into higher-dimensional estimates.

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 a proof whose key step is a finite-interval action inequality established by a continuation and degree argument for matrix fields.

Difficulty

Single-state bounds and numerical evidence say nothing about potentials with many bound states, and the conjecture requires a bound uniform over all orthonormal families of eigenfunctions. Methods that work at $\gamma=1$ (where the inequality is dual to a kinetic-energy bound for orthonormal families) do not directly apply at other exponents, since the moment $\sum|\lambda_j|^\gamma$ is not linear in the density matrix. The proof must keep track of the individual eigenvalue scales.

Formalization scope

• H1 packages $u\in L^2(\mathbb R;\mathbb C)$ with a weak derivative in $L^2$, tested against smooth compactly supported functions.
• A negative eigenvalue $-k^2$ ($k>0$) is a weak eigenvalue of the form: $h_{-W}(v,u)=-k^2\langle v,u\rangle$ for all $v\in H^1$.
• negativeMoment γ W is the supremum, in $[0,\infty]$, over all finite orthonormal families of such eigenfunctions of $\sum_ik_i^{2\gamma}$; this counts multiplicity and does not presuppose finiteness. oneStateMoment retains one eigenfunction.
• Admissible γ W is $W\ge0$ a.e. and $W\in L^{\gamma+1/2}$; potentialMass is the lower Lebesgue integral of $W^{\gamma+1/2}$; the optimal constants are suprema over admissible $W$ with positive mass.
• For admissible $W$ the integral $\int W\bar uv$ converges for $u,v\in H^1$, so the form is correctly defined.

A complete development needs Sobolev space $H^1(\mathbb R)$ and form methods, the variational characterization of negative eigenvalues, Gamma-function identities for $L^{\rm cl}_{\gamma,1}$, the explicit $\operatorname{sech}^2$ eigenvalue computation, and the paper's action inequality. Contributions formalizing Theorem 2.1 (action inequality) and the equality computation for the $\operatorname{sech}^2$ potential are welcome.

Selected references

• OpenAI, Sharp one-dimensional Lieb–Thirring constants, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Sharp-One-Dimensional-Lieb-Thirring-Constants-September-23-2026/paper.pdf
• E. H. Lieb, W. E. Thirring, Bound for the kinetic energy of fermions which proves the stability of matter, Phys. Rev. Lett., 1975. https://doi.org/10.1103/PhysRevLett.35.687
• J. B. Keller, Lower bounds and isoperimetric inequalities for eigenvalues of the Schrödinger equation, J. Math. Phys., 1961. https://doi.org/10.1063/1.1703708
• D. Hundertmark, E. H. Lieb, L. E. Thomas, A sharp bound for an eigenvalue moment of the one-dimensional Schrödinger operator, Adv. Theor. Math. Phys., 1998. https://doi.org/10.4310/ATMP.1998.v2.n4.a2
• A. Laptev, T. Weidl, Sharp Lieb–Thirring inequalities in high dimensions, Acta Math., 2000. https://doi.org/10.1007/BF02392782
• D. Hundertmark, A. Laptev, T. Weidl, New bounds on the Lieb–Thirring constants, Invent. Math., 2000. https://doi.org/10.1007/s002220000077
• R. L. Frank, D. Hundertmark, M. Jex, P. T. Nam, The Lieb–Thirring inequality revisited, J. Eur. Math. Soc., 2021. https://doi.org/10.4171/JEMS/1062
• A. Levitt, Best constants in Lieb–Thirring inequalities: a numerical investigation, J. Spectr. Theory, 2014. https://doi.org/10.4171/JST/65
• L. Read, M. R. Schulz, The sharp one-dimensional Lieb–Thirring inequality for the sum of eigenvalues, preprint, 2026. https://arxiv.org/abs/2609.10478