OAI Math

All of openAI's results.

317 missions

Missions

141–160 of 317

Algebraic Topology Group Theory Mathematical Logic·Captain: wurtle

Simple F∞ overgroups of groups with decidable word problemResearch Paper

Motivation

A finitely generated group has decidable word problem if an algorithm decides, for every word in a fixed finite generating set and its inverses, whether it represents the identity. Embedding theorems translate this algorithmic property into algebra: Higman (1961) characterized subgroups of finitely presented groups, and Boone and Higman (1974) showed that decidable word problem is equivalent to embedding in a simple subgroup of a finitely presented group, asking whether the simple group can be finitely presented (the Boone–Higman conjecture).

This preprint proves a stronger statement in the direction of higher finiteness: every finitely generated group with decidable word problem embeds in a simple group of type $F_\infty$ , i.e. one with a classifying space having finitely many cells in each dimension. Since type $F_\infty$ implies finite presentation, this implies the Boone–Higman conjecture.

Background

1961. Higman's embedding theorem: finitely generated subgroups of finitely presented groups are exactly the recursively presented groups.
1974. Boone and Higman characterize decidable word problem by embeddings into simple subgroups of finitely presented groups and pose the conjecture.
1975, 1987. Brown gives homological criteria for finiteness and establishes type $F_\infty$ for the Thompson–Higman groups.
1980. Thompson shows the simple overgroup can be chosen finitely generated with decidable word problem.
2022. Belk and Zaremsky introduce twisted Brin–Thompson groups and construct a simple group of type $F_\infty$ containing all finitely generated right-angled Artin groups.
2024–2026. Belk, Hyde and Matucci construct a simple $F_\infty$ group containing every countable abelian group; the Boone–Higman conjecture is verified for hyperbolic groups (Belk, Bleak, Matucci, Zaremsky) and for $\mathrm{Aut}(F_n)$ and mapping class groups (Belk, Fournier-Facio, Hyde, Zaremsky). The survey of Belk, Bleak, Matucci and Zaremsky raises the higher-finiteness question.
2026. The OpenAI preprint Simple $F_\infty$ overgroups of groups with decidable word problem (dated September 23, 2026) proves the theorem below, building on the companion preprint Finite algebraic envelopes and the Boone–Higman conjecture. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

A classifying space $K(H,1)$ is a connected CW complex with fundamental group $H$ and contractible universal cover. $H$ has type $F_n$ if some $K(H,1)$ has finite $n$ -skeleton and type $F_\infty$ if some $K(H,1)$ has finitely many cells in each dimension. Type $F_1$ is finite generation and type $F_2$ is finite presentation. A group is simple if it is nontrivial and has no normal subgroups besides $1$ and itself.

In Lean (OAI.SimpleFInftyOvergroups, definitions SimpleOvergroups), HasDecidableWordProblem G asks for a finite generating tuple with a ComputablePred identity predicate on words; HasTypeFInfty H asks for a Hausdorff connected space $X$ with a CW structure of finite type (Topology.CWComplex.FiniteType), a basepoint with $H \simeq \pi_1(X, x)$ , and a surjective covering map from a contractible space.

Formalization targets

Goal: Theorem 1.1

Every finitely generated group $G$ with decidable word problem admits an injective homomorphism $G \hookrightarrow H$ into a nontrivial simple group $H$ of type $F_\infty$ .

The input need not be finitely presented and its word-problem algorithm may have arbitrary running time; the classifying space of $H$ may be infinite-dimensional.

Significance

The result. Theorem 1.1 answers the higher-finiteness strengthening of the Boone–Higman conjecture and implies the conjecture itself. With the classical converse (finitely presented simple groups have decidable word problem), it characterizes groups with decidable word problem as the finitely generated subgroups of simple groups of type $F_\infty$ .

Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. A formalization requires CW complexes of finite type, classifying spaces and covering theory (partially in Mathlib), Brown's homological finiteness criterion, Steinberg groups, and twisted Brin–Thompson groups with the Belk–Zaremsky finiteness theorem (Theorem 5.1 in the preprint, from the literature).

Difficulty

Finite presentation already fails to pass to subgroups; higher finiteness additionally requires controlling relations among relations in every dimension. Known families of simple $F_\infty$ groups contain large classes of groups but give no general construction from a word-problem algorithm. The proof needs an oligomorphic faithful action of a group of type $F_\infty$ with stabilizers of type $F_\infty$ , built from an algebraic envelope whose Steinberg-group kernel must be annihilated exactly (Theorem 4.6).

Formalization scope

$G$ and $H$ live in the same universe Type u; $G$ carries [Group.FG G].
IsSimpleGroup H together with Nontrivial H encodes simplicity.
Type $F_\infty$ is encoded topologically via a finite-type CW structure on a connected Hausdorff space whose universal cover (a surjective covering with contractible total space) witnesses asphericity.
The word problem uses ComputablePred on lists of (generator, sign) pairs for a specified generating tuple.

The statement is not vacuous: the hypothesis holds for many groups (e.g. all finitely presented residually finite groups), and the conclusion requires a genuine embedding.

Needed infrastructure: finite-type CW complexes and $K(\pi,1)$ spaces, Brown's criterion, group actions with finiteness properties, Steinberg groups over noncommutative algebras, and twisted Brin–Thompson groups. Contributions toward any of these are welcome.

Selected references

OpenAI, Simple $F_\infty$ overgroups of groups with decidable word problem, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem-September-23-2026/paper.pdf
OpenAI, Finite algebraic envelopes and the Boone–Higman conjecture, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/main/preprints/Finite-algebraic-envelopes-and-the-Boone-Higman-conjecture-September-23-2026/paper.pdf
W. W. Boone, G. Higman, An algebraic characterization of groups with soluble word problem, J. Austral. Math. Soc. 18 (1974). https://doi.org/10.1017/S1446788700019108
G. Higman, Subgroups of finitely presented groups, Proc. Roy. Soc. London Ser. A 262 (1961). https://doi.org/10.1098/rspa.1961.0132
R. J. Thompson, Embeddings into finitely generated simple groups which preserve the word problem, in Word Problems II, 1980. https://doi.org/10.1016/S0049-237X(08)71348-X
K. S. Brown, Homological criteria for finiteness, Comment. Math. Helv. 50 (1975). https://doi.org/10.1007/BF02565740
K. S. Brown, Finiteness properties of groups, J. Pure Appl. Algebra 44 (1987). https://doi.org/10.1016/0022-4049(87)90015-6
J. Belk, M. C. B. Zaremsky, Twisted Brin–Thompson groups, Geom. Topol. 26 (2022). https://doi.org/10.2140/gt.2022.26.1189
J. Belk, C. Bleak, F. Matucci, M. C. B. Zaremsky, Progress around the Boone–Higman conjecture, 2025. https://arxiv.org/abs/2306.16356
J. Belk, C. Bleak, F. Matucci, M. C. B. Zaremsky, Hyperbolic groups satisfy the Boone–Higman conjecture, Duke Math. J. 175 (2026). https://doi.org/10.1215/00127094-2025-0055
J. Belk, J. Hyde, F. Matucci, Finite germ extensions, 2024. https://arxiv.org/abs/2407.03149

2 thms1 active userReviewed

Completed

Algebraic Topology Group Theory·Captain: wurtle

A universal group of type F∞Research Paper

Motivation

Higman's embedding theorem (1961) says that a finitely generated group embeds in a finitely presented group exactly when it is recursively presented, i.e. has a presentation with finitely many generators and a recursively enumerable set of relators. A consequence is that there is a single universal finitely presented group containing every finitely presented group. A natural higher-dimensional question asks whether finiteness can be pushed beyond presentations: finite presentability is the dimension-two case of the topological finiteness properties $F_n$ .

This preprint constructs a single group $H$ of type $F_\infty$ , i.e. with a classifying space having finitely many cells in every dimension, that contains every finitely presented group. This answers the $F_\infty$ form of the higher-dimensional Higman embedding question posed by Fournier-Facio and Zaremsky.

Background

1949. Higman, Neumann and Neumann introduce HNN extensions and embedding theorems for groups.
1961. Higman proves his embedding theorem.
1974–1975. Bieri and Eckmann, and Brown, develop finiteness properties of groups and homological criteria for them.
2018. Leary proves every countable group embeds in a group of type $FP_2$ .
2026. Fournier-Facio and Zaremsky show that embedding theorems into recursively presented groups of type $FP_n$ would yield embeddings of finitely presented groups into groups of type $F_n$ , show that their rope-trick groups fail $FP_3(\mathbb{Q})$ in general, and ask the higher-dimensional Higman embedding question (Question 1.3).
2026. The OpenAI preprint A universal group of type $F_\infty$ (dated September 23, 2026) proves the theorem below. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

A classifying complex for a group $G$ is a connected CW complex with fundamental group isomorphic to $G$ and contractible universal cover; it may be infinite-dimensional. $G$ has type $F_n$ if some classifying complex has finite $n$ -skeleton, and type $F_\infty$ if some classifying complex has finitely many cells in every dimension. Type $F_2$ is equivalent to finite presentability. A group is finitely presented if it has a presentation with finitely many generators and relators.

In Lean (OAI.UniversalFInfinity), HasTypeFInfinity G asks for a Hausdorff connected space $X$ with a CW structure on Set.univ having finitely many $n$ -cells for every $n$ , a basepoint with $\pi_1(X, x) \simeq G$ , and a surjective covering map from a contractible space. Finite presentation is Mathlib's Group.IsFinitelyPresented.

Formalization targets

Goal: Theorem 1.1

There exists a group $H$ of type $F_\infty$ such that every finitely presented group admits an injective homomorphism into $H$ :

\exists H \text{ of type } F_\infty\ \ \forall G \text{ finitely presented}\ \ \exists\, \varphi : G \hookrightarrow H .

Significance

The result. Theorem 1.1 gives a universal group with the strongest standard topological finiteness property. Corollary 1.2 follows: the finitely generated subgroups of $H$ are exactly the finitely generated recursively presented groups. No word-problem hypothesis is imposed on the inputs, in contrast with the companion result on simple $F_\infty$ overgroups.

Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. A formalization requires finite-type CW complexes, classifying spaces and covering theory, Brown's criterion or a direct cell-count argument, Higman's universal finitely presented group, HNN extensions and an ascending-torus theorem (Theorem 5.1), none of which is fully in Mathlib.

Difficulty

Higman's universal group is only finitely presented; type $F_\infty$ requires finite control of relations among relations in every dimension, which is typically destroyed by the embeddings and amalgams used in Higman-type arguments. Fournier-Facio and Zaremsky show that the rope-trick construction fails $FP_3(\mathbb{Q})$ , so a different route is needed. The preprint constructs a finitely presented envelope with two families of homomorphisms from the universal group and an ascending HNN-type mapping torus whose finiteness properties can be verified.

Formalization scope

Universes: $H$ and the quantified finitely presented $G$ live in the same universe Type u; finitely presented groups are countable, so this loses nothing.
Type $F_\infty$ : a CW structure with Finite (cw.cell n) for every $n$ , $\pi_1 \simeq H$ , and a contractible covering space; no finite-dimensionality is required.
The universal quantifier is over every Group.IsFinitelyPresented group, not a chosen list of presentations.

The statement cannot be met trivially: a trivial or finite $H$ cannot contain all finitely presented groups, and the type $F_\infty$ requirement is substantive.

Needed infrastructure: CW complexes of finite type, $K(\pi,1)$ spaces, HNN extensions, Higman's embedding theorem. Contributions toward Theorem 5.1 (ascending-torus theorem) or Proposition 6.2 are welcome.

Selected references

OpenAI, A universal group of type $F_\infty$ , OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-universal-group-of-type-F-infinity-September-23-2026/paper.pdf
OpenAI, Simple $F_\infty$ overgroups of groups with decidable word problem, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/main/preprints/Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem-September-23-2026/paper.pdf
G. Higman, Subgroups of finitely presented groups, Proc. Roy. Soc. London Ser. A 262 (1961). https://doi.org/10.1098/rspa.1961.0132
G. Higman, B. H. Neumann, H. Neumann, Embedding theorems for groups, J. London Math. Soc. 24 (1949).
R. Bieri, B. Eckmann, Finiteness properties of duality groups, Comment. Math. Helv. 49 (1974). https://doi.org/10.1007/BF02566720
K. S. Brown, Homological criteria for finiteness, Comment. Math. Helv. 50 (1975). https://doi.org/10.1007/BF02565740
I. J. Leary, Subgroups of almost finitely presented groups, Math. Ann. 372 (2018).
F. Fournier-Facio, M. C. B. Zaremsky, Finiteness properties and Higman's rope trick, preprint, 2026. https://arxiv.org/abs/2607.21727
A. Hatcher, Algebraic Topology, Cambridge University Press, 2002.

6 thms2 active usersReviewed

Completed

Functional Analysis Group Theory Harmonic Analysis·Captain: wurtle

Unitarizability implies amenability for discrete groupsResearch Paper

Motivation

A representation $\pi$ of a group $G$ by bounded invertible operators on a Hilbert space is uniformly bounded if $\sup_g\|\pi(g)\|<\infty$ , and unitarizable if after a change of inner product it becomes unitary, i.e. some bounded invertible $S$ makes every $S\pi(g)S^{-1}$ unitary. Unitary representations are the ones harmonic analysis knows how to decompose, so it matters which groups have only unitarizable uniformly bounded representations. Day and Dixmier showed in 1950 that every amenable group (one with an invariant mean) has this property, and Dixmier asked whether the converse holds. Dixmier's unitarizability problem has driven work in operator algebras, $\ell^2$ -invariants and measured group theory for seven decades.

Timeline

1947. Sz.-Nagy proves that an invertible operator with uniformly bounded powers is similar to a unitary.
1950. Day and Dixmier prove that amenable groups are unitarizable; Dixmier asks whether the converse holds (doi:10.2307/1990358).
1955. Ehrenpreis and Mautner give nonunitarizable uniformly bounded representations of $\mathrm{SL}_2(\mathbb R)$ (doi:10.1073/pnas.41.4.231); Følner gives his finite-set criterion for amenability (doi:10.7146/math.scand.a-10442).
1986. Pytlik and Szwarc construct explicit nonunitarizable families for free groups, settling all groups containing $F_2$ (doi:10.1007/BF02392596).
1998. Pisier characterizes amenability by a quantitative similarity bound with exponent $<3$ (The similarity degree of an operator algebra, Algebra i Analiz, 1998).
2009. Epstein and Monod use invariant random forests to prove nonunitarizability for residually finite groups with positive first $\ell^2$ -Betti number (doi:10.1093/imrn/rnp090); Osin obtains nonunitarizable groups without free subgroups.
2010. Monod and Ozawa prove that the wreath products $A\wr G$ with $A$ infinite abelian are unitarizable exactly when $G$ is amenable (doi:10.1016/j.jfa.2009.06.029), using the Gaboriau–Lyons theorem (doi:10.1007/s00222-009-0187-5).
2018–2025. Gerasimova, Gruber, Monod and Thom relate unitarizability to Cheeger constants (doi:10.1016/j.jfa.2019.108457); Alpeev and Vergara obtain further cases.

The source of this mission, an OpenAI preprint dated September 23, 2026, answers Dixmier's question affirmatively for all discrete groups.

Setting

Let $G$ be a discrete group. $G$ is amenable if there is a linear functional $m$ on the bounded functions $G\to\mathbb C$ with $m(1)=1$ , $m(f)\ge0$ for $f\ge0$ , and $m(L_gf)=m(f)$ , where $(L_gf)(x)=f(g^{-1}x)$ .

A representation is a homomorphism $\pi:G\to\mathcal B(\mathcal K)$ into bounded operators on a complex Hilbert space $\mathcal K$ (each $\pi(g)$ is then invertible). It is similar to a unitary representation if there is a bounded invertible $S$ with $S\pi(g)S^{-1}$ unitary for every $g$ . $G$ is unitarizable if every uniformly bounded representation on every complex Hilbert space is similar to a unitary representation; the similarity may depend on the representation.

Formalization targets

Milestone: countable case

Every countable nonamenable $G$ has a representation on a separable Hilbert space with $\sup_g\|\pi(g)\|\le101$ that is not similar to a unitary representation.

Goal: Theorem 1.1

G\ \text{amenable}\iff G\ \text{unitarizable},

and for nonamenable $G$ and every $\varepsilon>0$ there is $\pi$ with $\sup_g\|\pi(g)\|\le1+\varepsilon$ not similar to a unitary representation, on a separable space when $G$ is countable. The Lean statement OAI.Dixmier.current_main_theorem is open on the platform.

Significance

Theorem 1.1 characterizes amenability of discrete groups by a purely Hilbert-space property, without any quantitative bound on similarities, and shows that nonunitarizable representations can be chosen with uniform bound arbitrarily close to $1$ . Earlier results produced witnesses for groups with free subgroups, for residually finite groups with positive $\ell^2$ -Betti number, or for wreath-product extensions of $G$ ; the theorem gives a witness for every nonamenable $G$ itself. The paper also derives a consequence for group C $^*$ -algebras using a companion similarity result.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. The amenable direction (Day–Dixmier averaging) is classical and a natural first formalization step; the converse needs the paper's new operator construction.

Difficulty

A witness must be one representation for which no similarity exists, with no a priori control of the condition number of a putative unitarizer; quantitative criteria such as Pisier's do not apply. Nonamenable groups need not contain free subgroups and need not be residually finite, so the earlier free-group, random-forest and $\ell^2$ -Betti routes do not cover them. The paper builds bounded operator cocycles with no bounded implementer, which requires operators whose conjugation differences under translation are uniformly bounded while their distance from the translation commutant tends to infinity.

Formalization scope

Amenability is stated for G with the discrete topology, using G →ᵇ ℂ for $\ell^\infty(G)$ ; positivity is required on functions with nonnegative real values.
Representations are monoid homomorphisms G →* (H →L[ℂ] H) with [InnerProductSpace ℂ H] [CompleteSpace H]; SimilarToUnitary π asks for S : H ≃L[ℂ] H with $\|S\pi(g)S^{-1}x\|=\|x\|$ for all $g,x$ .
Unitarizability quantifies over Hilbert spaces in universe max u v, and the witness is built there; since the theorem holds for every v, this covers all Hilbert spaces.
Separability of the witness is required only for countable G, as in the paper.

A complete development needs bounded operator cocycles and triangular representations, Hilbert direct sums, Hilbert–Schmidt estimates, Følner's criterion, induction of representations from subgroups, and invariant means. Contributions formalizing the Day–Dixmier direction, Proposition 2.2 (direct-sum obstruction) and Lemma 5.1 (induction from a subgroup) are welcome.

Selected references

OpenAI, Unitarizability implies amenability for discrete groups, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Unitarizability-Implies-Amenability-for-Countable-Groups-September-23-2026/paper.pdf
M. M. Day, Means for the bounded functions and ergodicity of the bounded representations of semi-groups, Trans. Amer. Math. Soc., 1950. https://doi.org/10.2307/1990358
J. Dixmier, Les moyennes invariantes dans les semi-groupes et leurs applications, Acta Sci. Math. (Szeged), 1950.
G. Pisier, Are unitarizable groups amenable?, preprint, 2004. https://arxiv.org/abs/math/0405282
I. Epstein, N. Monod, Nonunitarizable representations and random forests, IMRN, 2009. https://doi.org/10.1093/imrn/rnp090
N. Monod, N. Ozawa, The Dixmier problem, lamplighters and Burnside groups, J. Funct. Anal., 2010. https://doi.org/10.1016/j.jfa.2009.06.029
D. Gaboriau, R. Lyons, A measurable-group-theoretic solution to von Neumann's problem, Invent. Math., 2009. https://doi.org/10.1007/s00222-009-0187-5
T. Pytlik, R. Szwarc, An analytic family of uniformly bounded representations of free groups, Acta Math., 1986. https://doi.org/10.1007/BF02392596
M. Gerasimova, D. Gruber, N. Monod, A. Thom, Asymptotics of Cheeger constants and unitarisability of groups, J. Funct. Anal., 2020. https://doi.org/10.1016/j.jfa.2019.108457

30 thms2 active usersReviewed

Geometry & Topology Group Theory·Captain: wurtle

Quasi-isometric recognition of virtually polycyclic groupsResearch Paper

Motivation: recognizing a group from its large-scale geometry

Geometric group theory studies finitely generated groups through their word metrics, which are well defined up to quasi-isometry. A basic question is which algebraic properties are quasi-isometry invariants: if a group $H$ "looks like" a group $P$ from far away, must $H$ share $P$ 's algebraic structure? Gromov's polynomial-growth theorem (1981) answers this for virtually nilpotent groups. The next natural class is the virtually polycyclic groups — groups with a finite-index subgroup admitting a finite subnormal series with cyclic factors — which are exactly, up to finite index, the lattices in connected simply connected solvable Lie groups. Eskin, Fisher and Whyte conjectured that this class is quasi-isometrically rigid, and the question had been settled only for special families such as $\mathrm{Sol}$ and certain abelian-by-abelian groups.

Background

1981 — Gromov: groups of polynomial growth are virtually nilpotent, which settles the virtually nilpotent case (Publ. IHÉS 1981).
2000 — Farb and Mosher pose horizontal-preservation and recognition problems for solvable groups (arXiv:math/0005184).
2004 — Shalom proves that a finitely generated group quasi-isometric to an infinite polycyclic group has a finite-index subgroup with infinite abelianization (Acta Math. 2004).
2007 — Eskin, Fisher and Whyte formulate the lattice-recognition conjecture and its polycyclic form (Conjecture 1.2) (PAMQ 2007).
2010–2013 — Dymarz treats certain diagonalizable models (GAFA 2010); Peng handles nondegenerate unimodular split abelian-by-abelian Lie groups (G&T 2011); Eskin–Fisher–Whyte prove recognition for $\mathrm{Sol}$ by coarse differentiation (Ann. of Math. 2013).
2025 — Dymarz, Fisher and Xie prove a Tukia-type theorem and rigidity for SOL-like groups (Adv. Math. 2025); Le Boudec proves recognition under commability (arXiv:2510.24581); Grayevsky and Pallier treat $\mathrm{Sol}_5$ (arXiv:2509.12823).
2026 — An OpenAI preprint, Quasi-isometric recognition of virtually polycyclic groups (OpenAI Math Release, September 24, 2026), claims recognition for the full class. The preprint has not been peer reviewed and its theorems are not formally verified.

Setting

For finitely generated groups $P,H$ with word metrics, a $(K,C)$ -quasi-isometry $F:P\to H$ satisfies $K^{-1}d(x,x')-C\le d(Fx,Fx')\le Kd(x,x')+C$ and has $C$ -dense image. For finitely generated groups this is equivalent to a coarse equivalence: maps $f:P\to H$ , $g:H\to P$ sending pairs at bounded distance (differences in a fixed finite set) to pairs at bounded distance, with $g\circ f$ and $f\circ g$ at bounded distance from the identities. A uniform lattice in a locally compact group $S$ is a discrete subgroup $\Lambda$ with $S=\Lambda K$ for a compact $K$ ; a lattice is a discrete subgroup whose coset space carries an $S$ -invariant probability measure.

For the height theorem: a connected simply connected Lie group $G$ is real-triangulable if the adjoint representation of its Lie algebra $\mathfrak g$ is simultaneously upper triangular in some real basis, with diagonal characters $\chi_1,\dots,\chi_s$ . Put $\mathfrak k=\bigcap_j\ker\chi_j$ and $W=\mathfrak g/\mathfrak k$ ; the exponential height map $\pi:G\to(W,+)$ is the homomorphism whose differential is the quotient map. $G$ is unimodular if its left Haar measure is right invariant.

Formalization targets

Milestone: uniform bounded height (Theorem 1.4)

Let $G$ be connected, simply connected, real-triangulable and unimodular, with a proper left-invariant metric and a norm on $W$ . There is a finite subgroup $\mathcal A_G\le\mathrm{GL}(W)$ such that for all $K\ge1$ , $C\ge0$ there is $B$ with: every $(K,C)$ self quasi-isometry $F$ of $G$ has some $A_F\in\mathcal A_G$ with

\bigl\|\pi F(g)-\pi F(1)-A_F\,\pi(g)\bigr\|\le B\qquad(g\in G).

Milestone: lattice recognition (Corollary 1.2)

If a finitely generated group $H$ is quasi-isometric to a lattice in a connected simply connected solvable Lie group, then a finite-index subgroup of $H$ is a uniform lattice in some (possibly different) connected simply connected solvable Lie group.

Goal: quasi-isometric recognition (Theorem 1.1)

Let $P$ be finitely generated and virtually polycyclic and $H$ finitely generated. If $H$ is quasi-isometric to $P$ , then

H\ \text{is virtually polycyclic},\quad\text{and some finite-index } \Gamma\le H \text{ is isomorphic to a uniform lattice in a connected simply connected solvable Lie group.}

The second clause is the classical lattice realization of virtually polycyclic groups (Dekimpe's theorem, used in the source's proof of Corollary 1.2), recorded in the same formal statement. All three statements are published on the platform with status Open: no machine-checked proofs exist yet.

Significance

The result itself. Virtual polycyclicity becomes a quasi-isometry invariant among finitely generated groups, extending Gromov's theorem from nilpotent to solvable lattices and resolving the Eskin–Fisher–Whyte conjecture in its lattice form, where the ambient Lie group may change. The bounded-height theorem is a rigidity statement for quasi-isometries of an entire class of solvable Lie groups: up to bounded error and a finite group of linear symmetries, every quasi-isometry preserves height. This is the kind of control that previously required case-by-case coarse differentiation.

Formalizing it. The proof combines Lie theory, measured couplings, reduced cohomology, volume growth, Gromov's theorem and finiteness/duality results for elementary amenable groups — a long chain in which a machine check would add real confidence. Basic objects (coarse equivalences of groups, polycyclic series, uniform lattices, Lie groups with exponential maps) are reusable across geometric group theory.

Difficulty

Quasi-isometries carry no algebraic structure and can be wild at bounded scales, so the comparison group $H$ cannot be assumed solvable or even amenable a priori. Shalom's argument yields only a nontrivial homomorphism to $\mathbb Z$ , not full structure. The geometric core is height rigidity: one must show that a quasi-isometry cannot mix "up" and "down" directions of different exponential rates, uniformly over all quasi-isometries with given constants, and with a bounded (not merely sublinear) error, which is exactly what the later group-theoretic deduction needs.

Formalization scope

Polycyclicity is encoded by an explicit finite cyclic subnormal series; virtual polycyclicity by a finite-index polycyclic subgroup. Quasi-isometry of finitely generated groups is encoded as GroupCoarseEquivalence, with bornologous maps and errors in finite sets — equivalent to quasi-isometry of word metrics.
Simply connected solvable Lie groups are bundled as SimplyConnectedSolvableLieModel (finite-dimensional charted Lie group, Hausdorff, second countable, simply connected, solvable). Uniform lattices are discrete subgroups with a compact fundamental cover; finite-covolume lattices carry an invariant probability measure on the coset space.
In the height theorem, real-triangulability is a TriangularAdjoint basis, $W$ is any normed space linearly isomorphic to the canonical quotient, and $\pi$ is characterized through an exponential map. The metric is any compatible proper left-invariant metric with linear chain bounds — a quasi-isometric generalization of the source's fixed left-invariant Riemannian metric. The finite group $\mathcal A$ is chosen before $K,C$ .
Needed infrastructure: Lie algebras of Lie groups and exponential maps, Haar measure, quasi-isometries, Gromov's theorem, and the theory of elementary amenable groups.

Selected references

M. Gromov, Groups of polynomial growth and expanding maps, Publ. Math. IHÉS 53 (1981), 53–78. https://doi.org/10.1007/BF02698687
Y. Shalom, Harmonic analysis, cohomology, and the large-scale geometry of amenable groups, Acta Math. 192 (2004), 119–185. https://doi.org/10.1007/BF02392739
A. Eskin, D. Fisher and K. Whyte, Quasi-isometries and rigidity of solvable groups, Pure Appl. Math. Q. 3 (2007), 927–947. https://doi.org/10.4310/PAMQ.2007.v3.n4.a3
A. Eskin, D. Fisher and K. Whyte, Coarse differentiation of quasi-isometries II: Rigidity for Sol and lamplighter groups, Ann. of Math. 177 (2013), 869–910. https://doi.org/10.4007/annals.2013.177.3.2
I. Peng, Coarse differentiation and quasi-isometries of a class of solvable Lie groups II, Geom. Topol. 15 (2011), 1927–1981. https://doi.org/10.2140/gt.2011.15.1927
T. Dymarz, Large scale geometry of certain solvable groups, Geom. Funct. Anal. 19 (2010), 1650–1687. https://doi.org/10.1007/s00039-010-0046-y
T. Dymarz, D. Fisher and X. Xie, A Tukia-type theorem for nilpotent Lie groups and quasi-isometric rigidity of solvable groups, Adv. Math. 468 (2025). https://doi.org/10.1016/j.aim.2025.110202
K. Dekimpe, Solvable Lie algebras, Lie groups and polynomial structures, Compos. Math. 121 (2000), 183–204. https://doi.org/10.1023/A:1001738932743
Y. Cornulier and R. Tessera, On the vanishing of reduced 1-cohomology for Banach representations, Ann. Inst. Fourier 70 (2020), 1951–2003. https://doi.org/10.5802/aif.3363
OpenAI, Quasi-isometric recognition of virtually polycyclic groups, OpenAI Math Release preprint, September 24, 2026 (source of the goal; Theorem 1.1 and Corollary 1.2, p. 2; Theorem 1.4, p. 4). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/quasi-isometric-recognition-of-virtually-polycyclic-groups-September-24-2026/paper.pdf

4 thms1 active userReviewed

Completed

Algebra Group Theory·Captain: wurtle

The Kervaire theorem for groupsResearch Paper

Motivation

Given a group $A$ , adjoin one new generator $t$ and impose one relation $w=1$ , where $w$ is a word in $t$ and elements of $A$ . Can the result collapse to the trivial group when $A$ is nontrivial? The Kervaire conjecture says no. It arose from Kervaire's 1965 characterization of high-dimensional knot groups, which involves groups normally generated by a single element, and it is one of the best-known problems about equations over groups: when does an equation $w(t)=1$ with coefficients in $A$ have a solution in some group containing $A$ ?

Timeline

1962. Gerstenhaber and Rothaus prove that nonsingular systems of equations over finite groups are solvable in finite overgroups, using unitary groups and degree theory (doi:10.1073/pnas.48.9.1531); this gives the result for residually finite groups.
1965. Kervaire characterizes high-dimensional knot groups (doi:10.24033/bsmf.1624); the group-theoretic Kervaire problem is traced to this setting.
1983. Howie studies equations of length three over groups (doi:10.1017/S0013091500028108).
1993. Klyachko proves unimodular injectivity for torsion-free groups (doi:10.1080/00927879308824692).
2005. Klyachko records the reduction showing that universal nontriviality is equivalent to unimodular injectivity (doi:10.1007/s10469-005-0023-y).
2008. Pestov records the extension to hyperlinear groups (doi:10.2178/bsl/1231081461).
2012. Klyachko and Lurye prove injectivity for arbitrary coefficient groups after imposing $w^m=1$ , $m\ge2$ (doi:10.1016/j.jpaa.2011.06.020).
2017. Klyachko and Thom develop new topological methods for equations over groups (doi:10.2140/agt.2017.17.331).
2024–2026. Kawauchi publishes a proposed resolution via ribbon sphere-links; Chen gives a new proof of the torsion-free case via the complexity of surfaces (arXiv:2302.09811).

The source of this mission, an OpenAI preprint dated September 24, 2026, proves unimodular coefficient injectivity for every group by a route through spectral phase and a fixed-space theorem for unitary matrices.

Setting

Let $A$ be a group, $\langle t\rangle\cong\mathbb Z$ , and $H=A*\langle t\rangle$ the free product. Let $p:H\to\mathbb Z$ be the homomorphism that kills $A$ and sends $t$ to $1$ ; $p(w)$ is the exponent sum of $t$ in $w$ . A word $w\in H$ is unimodular if $p(w)=\pm1$ . Write $\langle\!\langle w\rangle\!\rangle_H$ for the normal closure of $w$ in $H$ . The coefficient map is the composite

A\hookrightarrow H\twoheadrightarrow H/\langle\!\langle w\rangle\!\rangle_H.

Its injectivity is equivalent to solvability of $w(t)=1$ over $A$ : there is an overgroup $B\supseteq A$ and $b\in B$ with $w(b)=1$ .

Formalization targets

Goal: Theorem 1.1

\forall A,\ \forall w\in A*\langle t\rangle\ \text{with}\ p(w)=\pm1:\qquad A\longrightarrow (A*\langle t\rangle)/\langle\!\langle w\rangle\!\rangle_H\ \text{is injective}.

The Lean statement OAI.Kervaire.coefficient_injective is open on the platform.

Significance

Theorem 1.1 immediately gives the Kervaire conjecture (Corollary 1.2): if $A\ne1$ then $(A*\langle t\rangle)/\langle\!\langle w\rangle\!\rangle\ne1$ for every $w$ , since for $p(w)=d\ne\pm1$ the quotient maps onto $\mathbb Z/d\mathbb Z$ . It proves the unimodular case of the stronger Kervaire–Laudenbach conjecture with no hypothesis on $A$ : no torsion-freeness, residual finiteness, hyperlinearity or countability. The paper's companion work extends the method to nonsingular systems of equations (Howie's conjecture).

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. The statement is short and entirely algebraic, which makes it an attractive formalization target; Mathlib already provides free products and normal closures.

Difficulty

The classical Gerstenhaber–Rothaus argument solves the equation in a unitary group and needs $A$ to embed in (an ultraproduct of) unitary groups, which is not known for arbitrary groups. Torsion in $A$ blocks the diagrammatic and topological arguments that work in the torsion-free case. A proof for every group therefore needs a representation available for all groups (the left regular representation, with its faithful finite trace) together with an argument that does not rely on finite-dimensional approximation of $A$ .

Formalization scope

The free product is Monoid.Coprod A (Multiplicative ℤ); the exponent sum is Multiplicative.toAdd (Monoid.Coprod.snd w).
Unimodular w is exponentSum w = 1 ∨ exponentSum w = -1.
The quotient is by Subgroup.normalClosure {w}, and coefficientMap w is the quotient map composed with Monoid.Coprod.inl.
No hypothesis is placed on $A$ ; the group may live in any universe.

A complete development needs the group von Neumann algebra of $A$ (or at least its trace), the spectral phase of unitaries and its subadditivity, a degree computation on a compact manifold of unitaries with fixed $k$ -planes, and corner-labelled planar diagrams with Euler-characteristic estimates. Contributions formalizing Corollary 1.2 from Theorem 1.1, Lemma 2.1 (subadditivity of spectral phase) and Lemma 3.1 (fixed-space lemma) are welcome.

Selected references

OpenAI, The Kervaire theorem for groups, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Kervaire-Theorem-for-Groups-September-24-2026/The-Kervaire-Theorem-for-Groups-September-24-2026.pdf
M. A. Kervaire, Les nœuds de dimensions supérieures, Bull. Soc. Math. France, 1965. https://doi.org/10.24033/bsmf.1624
M. Gerstenhaber, O. S. Rothaus, The solution of sets of equations in groups, Proc. Natl. Acad. Sci. USA, 1962. https://doi.org/10.1073/pnas.48.9.1531
A. A. Klyachko, A funny property of sphere and equations over groups, Comm. Algebra, 1993. https://doi.org/10.1080/00927879308824692
A. A. Klyachko, The Kervaire–Laudenbach conjecture and presentations of simple groups, Algebra and Logic, 2005. https://doi.org/10.1007/s10469-005-0023-y
A. A. Klyachko, D. E. Lurye, Relative hyperbolicity and similar properties of one-generator one-relator relative presentations with powered unimodular relator, J. Pure Appl. Algebra, 2012. https://doi.org/10.1016/j.jpaa.2011.06.020
V. G. Pestov, Hyperlinear and sofic groups: a brief guide, Bull. Symb. Log., 2008. https://doi.org/10.2178/bsl/1231081461
A. Klyachko, A. Thom, New topological methods to solve equations over groups, Algebr. Geom. Topol., 2017. https://doi.org/10.2140/agt.2017.17.331
L. Chen, The Kervaire conjecture and the minimal complexity of surfaces, Trans. Amer. Math. Soc., 2026. https://arxiv.org/abs/2302.09811

48 thms3 active usersReviewed

Completed

Analysis Mathematical Physics Partial Differential Equations·Captain: wurtle

Sharp one-dimensional Lieb–Thirring constantsResearch Paper

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

5 thms2 active usersReviewed

Functional Analysis Mathematical Physics Probability·Captain: wurtle

Ground-state condensation in the dilute hard-sphere gasResearch Paper

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$ :

for every choice of (possibly complex) bosonic ground vectors $\Psi_k$ , $\ \liminf_k B(\Psi_k)\ge c_0$ ;
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

2 thms1 active userReviewed

Mathematical Physics Probability·Captain: wurtle

Spontaneous magnetization in the quantum Heisenberg ferromagnetResearch Paper

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

2 thms1 active userReviewed

Completed

Information Theory Mathematical Physics Quantum Information·Captain: wurtle

The entropy photon-number inequalityResearch Paper

Motivation

Shannon's entropy power inequality bounds the entropy of a sum of independent random vectors below by the entropies of the summands; it is a basic tool for classical Gaussian channel capacities. In optical communication, addition is replaced by passive mixing of bosonic modes at a beam splitter. Guha, Erkmen and Shapiro conjectured the sharp bosonic analogue, the entropy photon-number inequality (EPnI), stated in terms of the photon number of the thermal state with the same entropy (ITA 2008). If true, it settles the minimum output entropy of thermal attenuators at fixed input entropy and the capacity regions of bosonic broadcast and wiretap channels, which had been reduced to this inequality (PRA 2007).

This mission asks for a formal proof of the EPnI for finite-energy inputs in any finite number of modes, 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

1948–1965 — Shannon introduces entropy power; Stam (1959) and Blachman (IEEE IT 1965) prove the entropy power inequality.
2004 — Capacity of the pure-loss bosonic channel (PRL 2004) and the minimum-output-entropy conjecture (PRA 2004).
2007–2008 — Guha, Shapiro and Erkmen relate broadcast capacity to a minimum-output-entropy conjecture; Guha, Erkmen and Shapiro state the EPnI.
2011 — Special cases (one-mode number-diagonal inputs) by Das, Sharma and Muthukrishnan (arXiv:1107.2365).
2014 — König and Smith prove a quantum entropy power inequality, including $S(\rho_C)\ge\eta S(\rho_A)+(1-\eta)S(\rho_B)$ (IEEE IT 2014); De Palma, Mari and Giovannetti prove the exponential form $e^{S(\rho_C)/n}\ge\eta e^{S(\rho_A)/n}+(1-\eta)e^{S(\rho_B)/n}$ (Nat. Photonics 2014).
2015 — Giovannetti, Holevo and García-Patrón solve the Gaussian optimizer conjecture for unconstrained minimum output entropy (CMP 2015).
2016–2018 — De Palma, Trevisan and Giovannetti settle one-mode constrained problems (IEEE IT 2017; PRL 2017); De Palma and Trevisan give a rigorous finite-energy conditional EPI (CMP 2018).
September 2026 — The OpenAI preprint claims the two-input EPnI for all finite-energy inputs (Theorem 1.1, p. 2).

Setting

An $n$ -mode bosonic system has Fock space $\ell^2(\mathbb N^n)$ with number basis $|k\rangle$ , $k\in\mathbb N^n$ . A state is a positive trace-one operator $\rho$ ; it has finite energy if $\operatorname{Tr}\rho\sum_ja_j^\dagger a_j=\sum_k(k_1+\dots+k_n)\langle k|\rho|k\rangle<\infty$ . The von Neumann entropy is $S(\rho)=-\operatorname{Tr}\rho\log\rho$ (natural log). The thermal entropy per mode is

g(t)=(t+1)\log(t+1)-t\log t,\qquad t\ge0,

increasing from $0$ to $\infty$ , and the entropy photon number of $\rho$ is $N(\rho)=g^{-1}(S(\rho)/n)$ , the mean photon number per mode of the product thermal state with the same entropy. For independent inputs $\rho_A,\rho_B$ and transmissivity $0\le\eta\le1$ , the beam-splitter output $\rho_C$ is the reduced state of the modes $c_j=\sqrt\eta\,a_j+\sqrt{1-\eta}\,b_j$ after passive mixing of $\rho_A\otimes\rho_B$ . No independence among the modes within either input is assumed.

Formalization targets

Goal: Theorem 1.1 (p. 2)

For every finite $n\ge1$ , every pair of finite-energy $n$ -mode states $\rho_A,\rho_B$ and every $0\le\eta\le1$ ,

g^{-1}\!\Bigl(\frac{S(\rho_C)}n\Bigr)\ \ge\ \eta\,g^{-1}\!\Bigl(\frac{S(\rho_A)}n\Bigr)+(1-\eta)\,g^{-1}\!\Bigl(\frac{S(\rho_B)}n\Bigr).

Thermal inputs with a common mean photon number within each port give equality.

Significance

The result itself. The EPnI is sharper than the exponential quantum entropy power inequality when the two input entropies differ, which is exactly the regime needed for constrained minimum output entropy. The preprint derives the exact minimum output entropy at fixed input entropy for every tensor power of an identical thermal attenuator, with inputs entangled across modes (Corollary 1.2, p. 2), and the exact capacity region of the degraded two-receiver pure-loss broadcast channel (Corollary 7.1, p. 26), completing the converse of Guha, Shapiro and Erkmen.

Formalizing it. The statement involves infinite-dimensional Fock space, trace-class positive operators, continuous functional calculus for the entropy, and the partial trace after a passive unitary. The Lean development builds these concretely in the number basis. A formal proof would give machine-checked infrastructure for quantum entropy on infinite-dimensional spaces, which Mathlib currently lacks. No machine-checked version of any quantum entropy power inequality is known.

Difficulty

Heat-flow (quantum Fisher information) proofs give the linear and exponential bounds, but these are attained only for equal entropies and do not recover the thermal comparison at unequal entropy levels. The preprint instead minimizes a regularized functional over pairs of inputs and must show that minimizers are thermal. This requires an interpolation theorem for diagonal form comparisons (Theorem 3.1, p. 8), attainment and Gibbs regularity of minimizers in infinite dimensions (Lemma 4.1, Proposition 4.2, pp. 15–16), a component entropy-Hessian estimate, and a stationarity identity whose cancellation forces convergence to thermal inputs (Section 6). Compactness relies on the finite-energy hypothesis; without it entropies can be infinite.

Formalization scope

Fock n is lp (fun _ : Fin n → ℕ => ℂ) 2. A State is a positive bounded operator whose diagonal in the number basis sums (HasSum) to $1$ .
FiniteEnergy ρ is summability of $\sum_k|k|\,\langle k|\rho|k\rangle$ .
entropy ρ is the sum of diagonal entries of $\mathrm{cfc}(-t\log t)(\rho)$ ; for finite-energy states it is finite, so the tsum is the true entropy.
gInv s = sInf {t ≥ 0 | s ≤ g t}, the inverse of $g$ on $[0,\infty)$ .
IsBeamSplitterOutput η ρA ρB ρC requires every number-basis entry of $\rho_C$ to be the (convergent) partial-trace sum of the explicitly given beam-splitter coefficients applied to $\rho_A\otimes\rho_B$ ; the inputs are arbitrary density matrices, so internal entanglement is allowed.
The hypotheses are satisfiable (e.g. vacuum or thermal inputs) and the conclusion is the inequality as stated.

Selected references

OpenAI, The entropy photon-number inequality, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-entropy-photon-number-inequality-September-24-2026/paper.pdf
S. Guha, B. I. Erkmen, J. H. Shapiro, The entropy photon-number inequality and its consequences, ITA Workshop 2008, 128–130. https://doi.org/10.1109/ITA.2008.4601037
S. Guha, J. H. Shapiro, B. I. Erkmen, Classical capacity of bosonic broadcast communication and a minimum output entropy conjecture, Phys. Rev. A 76 (2007), 032303. https://doi.org/10.1103/PhysRevA.76.032303
R. König, G. Smith, The entropy power inequality for quantum systems, IEEE Trans. Inf. Theory 60 (2014), 1536–1548. https://doi.org/10.1109/TIT.2014.2298436
G. De Palma, A. Mari, V. Giovannetti, A generalization of the entropy power inequality to bosonic quantum systems, Nat. Photonics 8 (2014), 958–964. https://doi.org/10.1038/nphoton.2014.252
G. De Palma, D. Trevisan, The conditional entropy power inequality for bosonic quantum systems, Comm. Math. Phys. 360 (2018), 639–662. https://doi.org/10.1007/s00220-017-3082-8
V. Giovannetti, A. S. Holevo, R. García-Patrón, A solution of Gaussian optimizer conjecture for quantum channels, Comm. Math. Phys. 334 (2015), 1553–1571. https://doi.org/10.1007/s00220-014-2150-6
V. Giovannetti, S. Guha, S. Lloyd, L. Maccone, J. H. Shapiro, H. P. Yuen, Classical capacity of the lossy bosonic channel: the exact solution, Phys. Rev. Lett. 92 (2004), 027902. https://doi.org/10.1103/PhysRevLett.92.027902
C. E. Shannon, A mathematical theory of communication, Bell Syst. Tech. J. 27 (1948). https://doi.org/10.1002/j.1538-7305.1948.tb00917.x

61 thms3 active usersReviewed

Completed

Complexity Theory Quantum Information Theoretical Computer Science·Captain: wurtle

Product-projection localization and the QAC0 parity lower boundResearch Paper

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

32 thms2 active usersReviewed

Complexity Theory Mathematical Physics Quantum Information·Captain: wurtle

Continuum Coulomb hardness with binary nuclear chargesResearch Paper

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

2 thms1 active userReviewed

Complexity Theory Mathematical Physics Quantum Information·Captain: wurtle

QMA-hardness of continuum Coulomb energy with unit nuclear chargesResearch Paper

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

2 thms1 active userReviewed

Completed

Information Theory Quantum Information·Captain: wurtle

Classical capacity and entropy inequalities for generalized amplitude dampingResearch Paper

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

37 thms2 active usersReviewed

Analysis Functional Analysis·Captain: wurtle

Universal strong Kadison–Kastler stabilityResearch Paper

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

2 thms1 active userReviewed

Completed

Functional Analysis·Captain: wurtle

Tracial projection methods and uniform property GammaResearch Paper

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

4 thms2 active usersReviewed

Dynamical Systems Functional Analysis·Captain: wurtle

Invariant-projection counterexamples for every irrational rotationResearch Paper

Motivation

The invariant subspace problem asks whether every bounded operator on a separable infinite-dimensional complex Hilbert space has a nontrivial closed invariant subspace. Inside a finite von Neumann algebra there is a sharper, algebra-relative version: given $T$ in a type $\mathrm{II}_1$ factor $M$ , is there a projection $p\in M$ with $0<\tau(p)<1$ and $(1-p)Tp=0$ , i.e. a nontrivial $T$ -invariant subspace whose projection lies in $M$ ? The Brown measure, built from the Fuglede–Kadison determinant, gives such projections whenever it is not a point mass (Haagerup–Schultz). The open territory is therefore operators whose Brown measure is a point mass, in particular quasinilpotent ones.

Zhu, Fang and Shi (2017) studied the weighted irrational rotations $T_f=Uf(V)$ in the hyperfinite $\mathrm{II}_1$ factor and asked whether $T_f$ must have a nontrivial invariant projection when $f$ is nonzero almost everywhere, $|f|$ is nonconstant and the determinant of $f(V)$ is zero. This mission formalizes a negative answer for every prescribed irrational angle.

Timeline

1952. Fuglede and Kadison introduce the determinant on finite factors (doi:10.2307/1969645).
1986. Brown defines the spectral distribution (Brown measure) of an operator in a $\mathrm{II}_1$ factor.
2004. Dykema and Haagerup construct nontrivial hyperinvariant subspaces for the quasinilpotent DT-operator, whose Brown measure is a point mass (doi:10.1016/S0022-1236(03)00167-8).
2008. Tucci constructs quasinilpotent generators of the hyperfinite factor that do have nontrivial invariant projections (doi:10.1016/j.jfa.2008.03.012).
2009. Haagerup and Schultz attach a hyperinvariant projection to each Borel set, with trace equal to its Brown mass (doi:10.1007/s10240-009-0018-7). Dykema and Schultz identify the Brown measure of weighted rotations as uniform measure on a circle of radius the determinant (arXiv:math/0512197).
2017. Zhu, Fang and Shi give a direct proof of that Brown-measure formula, exhibit continuous weights with one zero and determinant zero, and pose the question above (doi:10.7146/math.scand.a-25625).

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

Setting

Fix an irrational $\theta\in(0,1)$ . Let $R_\theta$ be the von Neumann algebra generated by unitaries $U,V$ with $VU=e^{2\pi i\theta}UV$ and trace $\tau(U^mV^n)=0$ for $(m,n)\ne(0,0)$ , $\tau(1)=1$ ; it is the hyperfinite $\mathrm{II}_1$ factor. Concretely, on $\mathcal H=L^2(\mathbb R/\mathbb Z;\ell^2(\mathbb Z))$ , $U$ shifts the $\ell^2(\mathbb Z)$ coordinate and $V$ multiplies the $k$ -th coordinate at $x$ by $e^{2\pi i(x+k\theta)}$ . For a continuous $f:\mathbb T\to[0,1]$ set $T_f=Uf(V)$ . A projection $p\in R_\theta$ is invariant for $T_f$ if $(1-p)T_fp=0$ ; it is nontrivial if $p\ne0,1$ . The Fuglede–Kadison determinant of $f(V)$ is $\exp\int_{\mathbb T}\log f\,dm$ , with $m$ the normalized Haar measure.

Formalization targets

Goal: Theorem 1.1 (with Corollary 6.2)

For every irrational $\theta\in(0,1)$ there is a continuous $f:\mathbb T\to[0,1]$ with

f^{-1}(0)=\{1\},\qquad \int_{\mathbb T}\log f\,dm=-\infty,

such that every projection $p\in R_\theta$ with $(1-p)\,Uf(V)\,p=0$ equals $0$ or $1$ ; moreover $T_f\ne0$ , $\|T_f^n\|^{1/n}\to0$ , and $\Delta(T_f)=0$ .

Milestones

Theorem 1.1 at some angle. The same conclusion for one irrational angle, in the abstract tracial model on $\ell^2(\mathbb Z^2)$ .
Theorem A.1 (product realization). A second model on $\mathbb T^{\mathbb N}$ : angles $\theta_i$ with $\sum\theta_i<\infty$ , rationally independent with $1$ , and $f(x)=\exp(-\sum c_i\lfloor x_i+\theta_i\rfloor)$ , giving a nonzero quasinilpotent $T=U\pi(f)$ in a $\mathrm{II}_1$ factor with only trivial invariant projections and the stated polar structure.
Abstract consequence. Some $\mathrm{II}_1$ factor with separable predual contains a nonzero quasinilpotent operator with no nontrivial invariant projection.

The goal OAI.Invariant233.Results.prescribed_irrational_counterexample is open on the platform.

Significance

Theorem 1.1 answers the Zhu–Fang–Shi question negatively, with the angle fixed in advance and no Diophantine condition. Combined with Dykema's observation that hyperinvariant subspaces of $T\in M$ have projections in $M$ , it yields (Corollary 1.4) a nonzero quasinilpotent operator on every separable infinite-dimensional Hilbert space with no nontrivial hyperinvariant subspace, so its commutant is a proper, strongly closed, transitive unital algebra. It also shows that, at determinant zero, the Haagerup–Schultz method cannot be supplemented by any invariant projection in the factor for these operators. The conclusion concerns projections in $R_\theta$ ; ordinary invariant subspaces of the Hilbert-space representation are not excluded.

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

Difficulty

Brown-measure methods give nothing here: at determinant zero the Brown measure is $\delta_0$ , so Haagerup–Schultz projections are trivial, and point-mass Brown measure does not by itself exclude invariant projections (Dykema–Haagerup, Tucci). One must show directly that a hypothetical invariant projection, viewed as a measurable field of projections, contradicts weighted orthogonality identities along rotation orbits. The weight's logarithmic drops must be rare enough to keep a finite window under control yet strong enough to suppress the infinite tail, and this must work at an arbitrary prescribed angle, which forces large divisible frequencies. Passing from a measurable weight to a continuous one with a single zero requires an intertwining multiplier that may be unbounded.

Formalization scope

The circle is AddCircle (1:ℝ) with Haar probability; the zero of $f$ is at $0\in\mathbb R/\mathbb Z$ , which corresponds to $1\in\mathbb T$ .
The Hilbert space is Lp (lp (fun _ : ℤ => ℂ) 2) 2 circleMeasure; Rotation.U is the fibrewise shift and Rotation.V θ multiplies by $e^{2\pi i(x+k\theta)}$ ; Rotation.algebra θ is the double commutant of $\{U,V\}$ .
HasOnlyTrivialInvariantProjections M T quantifies over self-adjoint idempotents $p\in M$ with $(1-p)Tp=0$ ; no commutation with $T$ is required.
NormQuasinilpotent T is $\|T^n\|^{1/n}\to0$ ; the determinant is the vector-state Fuglede–Kadison determinant $\inf_{\varepsilon>0}\exp\frac12\tau\log(T^*T+\varepsilon)$ , avoiding $\log0$ .

A complete development needs crossed-product (group-measure-space) von Neumann algebras, measurable fields of projections, the Fuglede–Kadison determinant, and uniform averaging under irrational rotation. Contributions formalizing Theorem 5.2 (the measurable-weight obstruction), Lemma 5.1 (conditional convolution obstruction), Corollary 6.2 (quasinilpotence) and Lemma A.4 (the product algebra is a $\mathrm{II}_1$ factor) are welcome.

Selected references

OpenAI, Invariant-projection counterexamples for every irrational rotation, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Invariant-projection-counterexamples-for-every-irrational-rotation-September-27-2026/paper.pdf
Z. Zhu, J. Fang, R. Shi, On a class of operators in the hyperfinite II $_1$ factor, Math. Scand., 2017. https://doi.org/10.7146/math.scand.a-25625
B. Fuglede, R. V. Kadison, Determinant theory in finite factors, Ann. of Math., 1952. https://doi.org/10.2307/1969645
U. Haagerup, H. Schultz, Invariant subspaces for operators in a general II $_1$ -factor, Publ. Math. IHÉS, 2009. https://doi.org/10.1007/s10240-009-0018-7
K. Dykema, H. Schultz, Brown measure and iterates of the Aluthge transform for some operators arising from measurable actions, Trans. Amer. Math. Soc., 2009. https://doi.org/10.1090/S0002-9947-09-04762-X
K. Dykema, U. Haagerup, Invariant subspaces of the quasinilpotent DT-operator, J. Funct. Anal., 2004. https://doi.org/10.1016/S0022-1236(03)00167-8
G. H. Tucci, Some quasinilpotent generators of the hyperfinite II $_1$ factor, J. Funct. Anal., 2008. https://doi.org/10.1016/j.jfa.2008.03.012
K. Dykema, Hyperinvariant subspaces for some B-circular operators, Math. Ann., 2005. https://doi.org/10.1007/s00208-005-0669-8

9 thms1 active userReviewed

Completed

Analysis Functional Analysis·Captain: wurtle

Backward intertwiners and a transitive commutantResearch Paper

Motivation

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

Timeline

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

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

Setting

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

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

Formalization targets

Goal: Corollary 1.2

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

23 thms2 active usersReviewed

Functional Analysis·Captain: wurtle

Relative generation and the generator problem for finite factorsResearch Paper

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

4 thms1 active userReviewed

Completed

Functional Analysis Probability Random Matrix Theory·Captain: wurtle

A finite-entropy separation of microstates and nonmicrostates free entropyResearch Paper

Motivation

Free probability treats bounded self-adjoint operators $X_1,\dots,X_n$ in a tracial von Neumann algebra as noncommuting random variables, and the free analogue of independence is freeness. Voiculescu introduced two candidate analogues of Shannon entropy for such tuples. The microstates free entropy $\chi(X)$ measures how large the set of matrix tuples imitating the joint moments of $X$ is (Voiculescu 1994). The nonmicrostates free entropy $\chi^*(X)$ is built instead from free Fisher information, by integrating along the addition of free semicircular noise (Voiculescu 1998). The two agree for a single variable, and whether they agree in general is part of Voiculescu's unification problem (Voiculescu 2002, Sections 3.5 and 3.8). Guionnet stated the finite-entropy formulation explicitly: does $\chi(X)>-\infty$ imply $\chi(X)=\chi^*(X)$ ? (Guionnet 2004, Conjecture 7.1).

The question matters because $\chi$ carries the strongest structural consequences for von Neumann algebras (it is the tool behind results such as Ge's theorem that free group factors are prime, Ge 1996), while $\chi^*$ is far more computable. Equality would let analytic computations of $\chi^*$ transfer to $\chi$ .

This mission asks for a machine-checked proof of Theorem 1.1 of an OpenAI preprint dated September 25, 2026 (source), which claims a tuple with $-\infty<\chi(X)\le\chi^*(X)-\tfrac12<\infty$ . The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.

Timeline

1991 — Voiculescu proves asymptotic freeness of independent GUE matrices (Invent. Math. 1991), the random-matrix input behind microstates.
1994 — Voiculescu defines the microstates free entropy $\chi$ (Invent. Math. 1994); Speicher develops the noncrossing cumulant calculus (Math. Ann. 1994).
1996 — Ge uses microstates entropy to prove that $L(F_2)$ is prime (PNAS 1996).
1998 — Voiculescu defines free Fisher information via conjugate variables and the nonmicrostates entropy $\chi^*$ (Invent. Math. 1998).
2002–2004 — Voiculescu's survey lists the unification problem (Bull. LMS 2002); Guionnet states the finite-entropy equality conjecture (Probab. Surv. 2004).
2003 — Biane, Capitaine and Guionnet prove $\chi\le\chi^*$ in general (Invent. Math. 2003).
2017–2020 — Equality is established for regular convex potentials by Dabrowski (arXiv:1604.06420) and Jekel (Anal. PDE 2020).
2024 — Jekel and Pi give an elementary proof of $\chi\le\chi^*$ , including the conditional version (Doc. Math. 2024).
2026 — The OpenAI preprint claims a strict gap with both entropies finite (Theorem 1.1, p. 2).

Setting

Let $M$ be a von Neumann algebra with a faithful normal tracial state $\tau$ , and $X=(X_1,\dots,X_n)$ a tuple of self-adjoint elements of $M$ .

Microstates. For $R>0$ , $m\in\mathbb N$ , $\varepsilon>0$ and a matrix size $d$ , let $\Gamma_R(X;m,d,\varepsilon)$ be the set of $n$ -tuples of self-adjoint $d\times d$ complex matrices with operator norms at most $R$ whose normalized traces $d^{-1}\mathrm{Tr}$ of all words of length $\le m$ are within $\varepsilon$ of the corresponding $\tau$ -moments of $X$ . Volume is Lebesgue measure for the unnormalized Hilbert–Schmidt inner product. Then

\chi_R(X)=\inf_{m,\varepsilon}\ \limsup_{d\to\infty}\Bigl[d^{-2}\log\mathrm{Vol}\,\Gamma_R(X;m,d,\varepsilon)+\tfrac n2\log d\Bigr],\qquad \chi(X)=\sup_{R>0}\chi_R(X).

Free Fisher information. Vectors $\xi_1,\dots,\xi_n$ in the $L^2(\tau)$ -closure of polynomials in $X$ are conjugate variables if $\tau(\xi_i P(X))=(\tau\otimes\tau)((\partial_iP)(X))$ for every noncommutative polynomial $P$ , where $\partial_i$ is the free difference quotient. Then $\Phi^*(X)=\sum_i\|\xi_i\|_2^2$ , or $+\infty$ if no conjugate variables exist.

Nonmicrostates entropy. With $S=(S_1,\dots,S_n)$ a standard free semicircular family free from $X$ ,

\chi^*(X)=\frac n2\log(2\pi e)+\frac12\int_0^\infty\Bigl(\frac n{1+s}-\Phi^*(X+\sqrt s\,S)\Bigr)\,ds .

Formalization targets

Goal: Theorem 1.1 (p. 2)

There exist $n\ge2$ and a bounded self-adjoint tuple $X$ in a von Neumann algebra with faithful normal tracial state such that

-\infty<\chi(X)\le\chi^*(X)-\tfrac12<\infty .

The Lean goal OAI.FiniteEntropySeparation.main asserts exactly this, with the semicircular family $S$ required to lie in the same algebra.

Significance

The result itself. The theorem answers the finite-entropy equality question negatively: finiteness of $\chi$ does not force $\chi=\chi^*$ , so the matrix-approximation and Fisher-information definitions are genuinely different invariants even in the finite regime. Known equality results therefore cannot be extended by finiteness alone; any equality theorem must use structure such as convexity of a potential. The preprint notes that it does not settle the question for each fixed small number of variables.

Formalizing it. No formal definitions of free entropy, free Fisher information or free semicircular systems are known to exist in a proof assistant. A complete development would formalize both entropies, the comparison $\chi\le\chi^*$ in the form needed, Gaussian asymptotic freeness, cumulant calculus and matrix-volume estimates, all reusable across free probability.

Difficulty

Both entropies are hard to compute for any non-free tuple, and the gap must survive two limits that interact badly: the $\limsup$ over matrix size in $\chi$ and the integral over noise time in $\chi^*$ . The preprint's tuple couples free semicirculars with a commuting discrete variable $Y$ that creates spectral blocks; after perturbing by small semicircular noise, $\chi$ is finite (Lemma 4.2, p. 9). The analytic side needs a Fisher-information bound in terms of higher cumulants (Proposition 3.2, p. 6), which makes $\chi^*$ nearly Gaussian at a suitable noise scale, while the matrix side must show that microstates, after GUE evolution, retain detectable block structure that independent GUE matrices of the same variances lack (Lemma 6.1, p. 12). Matching the two requires a finite-time entropy-production comparison along one fixed sequence of matrix laws (Lemma 5.1, p. 10); a naive application of $\chi\le\chi^*$ loses exactly the deficit being sought.

Formalization scope

The algebra is a VonNeumannAlgebra H on a complex Hilbert space $H$ ; the trace is a vector state given by a unit vector that is tracial on $M$ and separating for $M$ (so the state is faithful and normal).
$X$ and $S$ are Fin n-indexed self-adjoint elements of $M$ . FreeStandardNoise requires each $S_i$ to have the semicircle moments (Catalan numbers) and the unital algebras generated by $X$ and by each $S_i$ to be free.
Conjugate systems are vectors in the closed span of word vectors satisfying the derivative-moment identities; free Fisher information is an infimum in ℝ≥0∞, equal to $\infty$ when no conjugate system exists.
$\chi^*$ is an EReal built from the positive and negative parts of the integrand as lower Lebesgue integrals over $(0,\infty)$ .
$\chi$ uses explicit real coordinates for Hermitian matrices that make the Euclidean volume equal to Hilbert–Schmidt volume, matrix sizes $d+1$ to avoid $d=0$ , and EReal logarithms (volume zero gives $-\infty$ ).
The finiteness conditions are part of the conclusion, so a degenerate witness with $\chi=-\infty$ or $\chi^*=\infty$ does not satisfy the goal.

Selected references

OpenAI, A finite-entropy separation of microstates and nonmicrostates free entropy, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-finite-entropy-separation-of-microstates-and-nonmicrostates-free-entropy-September-25-2026/paper.pdf
D. Voiculescu, The analogues of entropy and of Fisher's information measure in free probability theory. II, Invent. Math. 118 (1994), 411–440. https://doi.org/10.1007/BF01231539
D. Voiculescu, The analogues of entropy and of Fisher's information measure in free probability theory. V, Invent. Math. 132 (1998), 189–227. https://doi.org/10.1007/s002220050222
D. Voiculescu, Free entropy, Bull. London Math. Soc. 34 (2002), 257–278. https://doi.org/10.1112/S0024609301008992
A. Guionnet, Large deviations and stochastic calculus for large random matrices, Probab. Surv. 1 (2004), 72–172. https://doi.org/10.1214/154957804100000033
P. Biane, M. Capitaine, A. Guionnet, Large deviation bounds for matrix Brownian motion, Invent. Math. 152 (2003), 433–459. https://doi.org/10.1007/s00222-002-0281-4
D. Jekel, J. Pi, An elementary proof of the inequality χ ≤ χ for conditional free entropy*, Doc. Math. 29 (2024), 1085–1124. https://doi.org/10.4171/DM/969
D. Jekel, An elementary approach to free entropy theory for convex potentials, Anal. PDE 13 (2020), 2289–2374. https://doi.org/10.2140/apde.2020.13.2289
D. Voiculescu, Limit laws for random matrices and free products, Invent. Math. 104 (1991), 201–220. https://doi.org/10.1007/BF01245072

6 thms2 active usersReviewed

Functional Analysis·Captain: wurtle

Weak pure infiniteness and O-infinity absorptionResearch Paper

Motivation

Purely infinite $C^*$ -algebras are the infinite counterpart of the finite, tracial algebras: every positive element can absorb copies of itself. In the simple case they are the Kirchberg algebras, classified by K-theory. For non-simple algebras, Kirchberg and Rørdam introduced three versions of pure infiniteness (weak, ordinary, strong) and showed that the strongest one is equivalent, for separable nuclear algebras, to absorbing the Cuntz algebra $\mathcal O_\infty$ tensorially, the regularity property that underlies Kirchberg's classification of non-simple purely infinite algebras. Whether the three notions coincide is Kirchberg–Rørdam's Question 9.5, listed as Problem LXXII by Schafhauser, Tikuisis and White.

Timeline

1978. Cuntz introduces the comparison relation $\precsim$ on positive elements (doi:10.1007/BF01421922).
2000. Kirchberg and Rørdam define pure infiniteness for non-simple algebras (doi:10.1353/ajm.2000.0021).
2002. Kirchberg and Rørdam introduce weak and strong pure infiniteness, prove $\mathcal O_\infty$ -absorption equivalences, settle the simple, real-rank-zero and approximately divisible cases, and pose Question 9.5 (doi:10.1006/aima.2001.2041).
2004. Blanchard and Kirchberg prove ordinary implies strong when the primitive ideal space is Hausdorff (doi:10.1016/j.jfa.2003.06.008); Rørdam treats $\mathcal Z$ -absorbing algebras (arXiv:math/0408020).
2006. Kirchberg's central-sequence results extend absorption to general nonunital separable nuclear algebras (doi:10.1007/978-3-540-34197-0_10).
2007. Pasnicu and Rørdam settle algebras with the ideal property (arXiv:math/0606378).
2016. Kirchberg and Sierakowski give the formulation of strong pure infiniteness used here (arXiv:1503.08519).
2023. Thiel and Vilalta study the Global Glimm Property (doi:10.1090/tran/8880); Elliott and Rouzbehani prove weak implies ordinary in topological dimension zero.
2025–2026. Pasnicu and Rouzbehani prove ordinary implies strong in topological dimension zero (doi:10.5565/PUBLMAT6922506); Ng, Thiel and Vilalta recover weak-to-ordinary via the Global Glimm Property (arXiv:2507.16261); Schafhauser, Tikuisis and White record Problem LXXII (arXiv:2506.10902).

The source of this mission is an OpenAI preprint dated September 25, 2026, which proves ordinary $\Rightarrow$ strong in general and weak $\Rightarrow$ ordinary for exact algebras.

Setting

All $C^*$ -algebras are complex and may be nonunital or nonseparable. For positive $u,v$ in matrices over $C$ (or in $C\otimes\mathcal K$ ), write $u\precsim v$ (Cuntz subequivalence) if there are $x_j$ with $x_j^*vx_j\to u$ in norm; matrices of different sizes are compared after zero padding. A positive $h$ is properly infinite if $h\oplus h\precsim h$ (zero counts as properly infinite). The paper uses two conditions:

(P) every $h\in C_+$ is properly infinite (ordinary pure infiniteness, by Kirchberg–Rørdam);
( $F_n$ ) for one fixed $n\ge1$ , $h^{\oplus n}$ is properly infinite for every $h\in C_+$ (weak pure infiniteness).

$C$ is strongly purely infinite if for all $x,y\in C_+$ and $\varepsilon>0$ there are $s,t\in C$ with

\|s^*x^2s-x^2\|<\varepsilon,\qquad \|t^*y^2t-y^2\|<\varepsilon,\qquad \|s^*xyt\|<\varepsilon.

$C$ is exact if $C\otimes_{\min}-$ preserves short exact sequences of $C^*$ -algebras.

Formalization targets

Milestone: Theorem 1.1

If $C$ satisfies (P), then for all $a,b\in C_+$ , $c\in C$ , $\varepsilon>0$ there are $s,t$ with

\|s^*as-a\|<\varepsilon,\quad\|t^*bt-b\|<\varepsilon,\quad\|s^*ct\|<\varepsilon;

in particular $C$ is strongly purely infinite.

Milestone: Theorem 1.2, first conclusion

C\ \text{exact and }(F_n)\ \Longrightarrow\ (P).

Goal: Theorem 1.2

C\ \text{exact and }(F_n)\ \text{for some }n\ge1\ \Longrightarrow\ C\ \text{strongly purely infinite}.

The Lean statement OAI.WeakPureInfiniteness.exact_weaklyPurelyInfinite_stronglyPurelyInfinite is open on the platform.

Significance

Theorem 1.1 answers the ordinary-to-strong part of Problem LXXII for arbitrary algebras, and Theorem 1.2 answers the whole comparison question for exact (hence for nuclear) algebras. With Kirchberg's results, every separable nuclear algebra satisfying ( $F_n$ ) absorbs $\mathcal O_\infty$ (Corollary 1.3), with no unitality or simplicity assumption: a single finite amplification test characterizes this tensorial regularity. The weak-to-ordinary implication for non-exact algebras remains open.

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

Difficulty

For non-simple algebras, comparing one positive element with itself and comparing two elements simultaneously are different demands: strong pure infiniteness must also kill a mixed entry $s^*xyt$ , and earlier proofs needed control of the ideal structure (Hausdorff primitive spectrum, ideal property, topological dimension zero). Removing a fixed amplification similarly needs enough orthogonal equivalent pieces in hereditary subalgebras, which earlier work extracted from Global Glimm-type hypotheses. The difficulty is to obtain this uniformly over primitive quotients when $\mathrm{Prim}(C)$ is not Hausdorff.

Formalization scope

Algebras are NonUnitalCStarAlgebra with the $C^*$ order (StarOrderedRing); no unit, separability or simplicity is assumed.
In the exact group, Cuntz subequivalence is between CStarMatrix blocks, witnessed by rectangular matrices $v$ with $\|v^*bv-a\|<\varepsilon$ for every $\varepsilon$ ; $h^{\oplus n}$ is diagonalCopies n h; WeaklyPurelyInfinite fixes one $n\ge1$ before quantifying over nonzero positives.
Exact is stated with minimal tensor products realized inside $\ell^\infty$ over all pairs of Hilbert-space representations, and tests surjections $q:C\to D$ in the same universe.
In the Theorem 1.1 group, Cuntz comparison is in the stabilization (completion of the union of matrix algebras, i.e. $C\otimes\mathcal K$ ), and PropertyP is (P).
StronglyPurelyInfinite is the three-inequality condition above, with no norm bound on $s,t$ .

A complete development needs Cuntz comparison, stabilizations, minimal tensor products and exactness, primitive ideal spaces and hereditary subalgebras; this is reusable for other regularity missions. Contributions formalizing Proposition 2.2-style transport lemmas and Corollary 1.3 (via Kirchberg's absorption theorem) are welcome.

Selected references

OpenAI, Weak pure infiniteness and $\mathcal O_\infty$ absorption, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Weak-pure-infiniteness-and-O-infinity-absorption-September-25-2026/paper.pdf
E. Kirchberg, M. Rørdam, Non-simple purely infinite $C^*$ -algebras, Amer. J. Math., 2000. https://doi.org/10.1353/ajm.2000.0021
E. Kirchberg, M. Rørdam, Infinite non-simple $C^*$ -algebras: absorbing the Cuntz algebra $\mathcal O_\infty$ , Adv. Math., 2002. https://doi.org/10.1006/aima.2001.2041
E. Kirchberg, A. Sierakowski, Filling families and strong pure infiniteness, 2016. https://arxiv.org/abs/1503.08519
E. Blanchard, E. Kirchberg, Non-simple purely infinite $C^*$ -algebras: the Hausdorff case, J. Funct. Anal., 2004. https://doi.org/10.1016/j.jfa.2003.06.008
C. Pasnicu, M. Rørdam, Purely infinite $C^*$ -algebras of real rank zero, J. Reine Angew. Math., 2007. https://doi.org/10.1515/CRELLE.2007.091
E. Kirchberg, Central sequences in $C^*$ -algebras and strongly purely infinite algebras, Abel Symposium, 2006. https://doi.org/10.1007/978-3-540-34197-0_10
C. Schafhauser, A. Tikuisis, S. White, Nuclear $C^*$ -algebras: 99 problems, 2026. https://arxiv.org/abs/2506.10902

30 thms2 active usersReviewed

Top contributors

Rank	Contributor	Accepted solutions	Submitted problems
1	Eyal1990	1081	1564
2	Shuze Chen	822	3136
3	dbenbenn	382	331
4	fizzyinc3	349	0
5	polylog	44	8
6	marwahaha	30	36
7	Ethan Cheung	28	15
8	WillR	20	2
9	Yuxuan Xu	18	34
10	SamenHossain	11	19