All missions

Motivation: the classical capacity of a thermal qubit channel

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

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

Background timeline

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

Setting

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

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

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

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

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

Formalization targets

Goal: additivity and capacity formula (Theorem 1.1)

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

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

Background

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

This mission asks for a formal proof of the parity lower bound stated as Theorem 1 of an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Setting

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

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

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

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

Formalization targets

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

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

Timeline

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

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

Setting

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

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 1.1

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

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

This mission asks for a formal proof of ground-state condensation for the dilute three-dimensional hard-sphere Bose gas, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

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

Setting

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

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

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

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

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

Formalization targets

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

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

Timeline

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 1.1

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

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

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

Significance

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

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. A formal proof would certify a proof whose key step is a finite-interval action inequality established by a continuation and degree argument for matrix fields.

Difficulty

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

Formalization scope

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

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

Selected references

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

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

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.

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

Motivation

The word problem for a group with a finite generating set asks whether a given word in the generators and their inverses represents the identity; it is decidable if one algorithm answers this for every word. Since Higman's embedding theorem (1961), a recurring theme in combinatorial group theory has been to characterize algorithmic properties of groups by embeddings into groups with good algebraic properties. Boone and Higman (1974) proved that a finitely generated group has decidable word problem if and only if it embeds in a simple subgroup of a finitely presented group, and asked whether the simple group can itself be taken finitely presented. This is the Boone–Higman conjecture.

This preprint states a proof of the conjecture: a finitely generated group has decidable word problem if and only if it embeds in a finitely presented simple group.

Background

• 1961. Higman characterizes finitely generated subgroups of finitely presented groups as the recursively presented groups.
• 1974. Boone and Higman prove the characterization $G \le H \le K$ with $H$ simple and $K$ finitely presented, and ask whether $H$ can be finitely presented.
• 1980. Thompson embeds every finitely generated group with decidable word problem into a finitely generated simple group with decidable word problem; a later proof is given by Darbinyan and Steenbock (2022).
• 2022. Belk and Zaremsky introduce twisted Brin–Thompson groups, which embed an acting group in a simple group; Zaremsky (2024) gives a finite-presentation criterion requiring a finitely presented acting group with finitely generated point stabilizers and finitely many orbits on unordered pairs.
• 2023–2026. The conjecture is verified for hyperbolic groups and contracting self-similar groups (Belk, Bleak, Matucci, Zaremsky), Baumslag–Solitar and free-by-cyclic groups (Bux, Llosa Isenrich, Wu), and $\mathrm{Aut}(F_n)$ and mapping class groups of punctured surfaces (Belk, Fournier-Facio, Hyde, Zaremsky); see the survey of Belk, Bleak, Matucci and Zaremsky.
• 2026. The OpenAI preprint Finite algebraic envelopes and the Boone–Higman conjecture (dated September 23, 2026) states a proof of the conjecture in general. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

A group $G$ is finitely generated if some finite tuple $g_1, \dots, g_n$ generates it. A word is a finite list of letters $g_i^{\pm1}$; $G$ has decidable word problem if for some finite generating tuple the set of words evaluating to $1$ is computable. A group is finitely presented if it has a presentation with finitely many generators and relations, and simple if it is nontrivial with no normal subgroups other than $1$ and itself. An embedding is an injective homomorphism.

In Lean (OAI.FiniteAlgebraicEnvelopes, definitions BooneHigman), words are List (Fin n × Bool), evalWord multiplies generators or their inverses, HasDecidableWordProblem G asserts a generating tuple whose identity predicate is ComputablePred, and EmbedsInFinitelyPresentedSimpleGroup G asserts a group in the same universe that is Group.IsFinitelyPresented and IsSimpleGroup, with an injective homomorphism from $G$.

Formalization targets

Goal: Theorem 1.1 (Boone–Higman conjecture)

For every finitely generated group $G$,

$$G \text{ has decidable word problem} \iff G \text{ embeds in a finitely presented simple group.}$$

The implication from right to left is classical (a finitely presented simple group has decidable word problem, and the property passes to finitely generated subgroups); the content is the forward implication.

Significance

The result. Theorem 1.1 gives a purely algebraic characterization of decidability of the word problem and settles a question open since 1974. Its intermediate result, Theorem 1.2, embeds every finitely generated group with decidable word problem in a finitely presented group with a faithful two-transitive action on a countably infinite set with finitely generated point stabilizers, which feeds Zaremsky's criterion for twisted Brin–Thompson groups.

Formalizing it. No machine-checked proof exists, and the source is an unrefereed preprint. Formalizing it requires computability of word problems, finite presentations (available in Mathlib as Group.IsFinitelyPresented), Steinberg groups over noncommutative rings, and twisted Brin–Thompson groups, which are not in Mathlib. The proof also uses Zaremsky's finite-presentation theorem (Theorem 2.3) from the literature, which a complete formalization must include.

Difficulty

Finite presentation does not pass to subgroups, so Boone and Higman's simple group $H$ and finitely presented group $K$ cannot simply be merged. Thompson's construction gives a finitely generated simple overgroup but provides no finite presentation. The new route needs a finitely presented group acting faithfully and two-transitively, built from a finitely presented algebra whose simplicity appears only after passing to a direct limit, and an exact calculation removing the kernel of the Steinberg group without assuming it is central.

Formalization scope

• GroupType : Type u with [Group GroupType] [Group.FG GroupType]; the target group lives in the same universe.
• Decidability is ComputablePred on words over a specified finite generating tuple (Subgroup.closure (range generators) = ⊤); since the word problem's decidability is independent of the finite generating set, this matches the source.
• IsSimpleGroup includes nontriviality, matching the paper's convention.

The statement is not trivially true: both directions are required for every finitely generated group, including infinitely presented ones.

Needed infrastructure: computable group presentations, Steinberg groups, mapping tori of endomorphisms, twisted Brin–Thompson groups and Zaremsky's criterion. Contributions toward the classical backward implication, or toward Theorem 1.2, are welcome.

Selected references

• OpenAI, Finite algebraic envelopes and the Boone–Higman conjecture, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/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, North-Holland, 1980. https://doi.org/10.1016/S0049-237X(08)71348-X
• J. Belk, M. C. B. Zaremsky, Twisted Brin–Thompson groups, Geom. Topol. 26 (2022). https://doi.org/10.2140/gt.2022.26.1189
• M. C. B. Zaremsky, Finite presentability of twisted Brin–Thompson groups, Proc. Roy. Soc. Edinburgh Sect. A (2024). https://doi.org/10.1017/prm.2024.131
• 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, C. Bleak, F. Matucci, M. C. B. Zaremsky, Progress around the Boone–Higman conjecture, 2025. https://arxiv.org/abs/2306.16356
• K.-U. Bux, C. Llosa Isenrich, X. Wu, On the Boone–Higman conjecture for groups acting on locally finite trees, 2025. https://arxiv.org/abs/2408.05673
• J. Belk, F. Fournier-Facio, J. Hyde, M. C. B. Zaremsky, Boone–Higman embeddings of Aut(F_n) and mapping class groups of punctured surfaces, 2026. https://arxiv.org/abs/2503.21882
• A. Darbinyan, M. Steenbock, Embeddings into left-orderable simple groups, J. London Math. Soc. 105 (2022). https://doi.org/10.1112/jlms.12552

Motivation: algebraic versus geometric dimension of groups

Two numbers measure how "large" a discrete group $\Gamma$ is. The cohomological dimension $\operatorname{cd}\Gamma$ is algebraic: the length of the shortest projective resolution of the trivial module $\mathbb Z$ over the group ring $\mathbb Z[\Gamma]$. The geometric dimension $\operatorname{gd}\Gamma$ is topological: the least dimension of a CW complex with fundamental group $\Gamma$ and contractible universal cover (a classifying space or $K(\Gamma,1)$). Cellular chains of a classifying space give a free resolution, so $\operatorname{cd}\Gamma\le\operatorname{gd}\Gamma$. Eilenberg and Ganea proved in 1957 that equality holds whenever $\operatorname{cd}\Gamma\ge3$, and Stallings and Swan settled dimension one. The remaining case — must a group of cohomological dimension two have a two-dimensional classifying space? — is the Eilenberg–Ganea conjecture, closely tied to Whitehead's asphericity conjecture in low-dimensional topology.

Background

• 1941 — Whitehead asks whether every connected subcomplex of an aspherical 2-complex is aspherical (Ann. of Math. 1941).
• 1957 — Eilenberg and Ganea prove $\operatorname{cd}=\operatorname{gd}$ for $\operatorname{cd}\ge3$ and pose the dimension-two question (Ann. of Math. 1957).
• 1968–1969 — Stallings proves that finitely generated groups of cohomological dimension one are free (Ann. of Math. 1968); Swan removes finite generation (J. Algebra 1969).
• 1997 — Bestvina and Brady introduce height kernels of right-angled Artin groups and show that for suitable flag triangulations of a spine of the Poincaré homology sphere at least one of the Eilenberg–Ganea and Whitehead conjectures fails (Invent. Math. 1997, Thm 8.7).
• 1999 — Dicks and Leary give presentations of these kernels (Proc. AMS 1999); Howie studies them via plus constructions (Math. Proc. Camb. Phil. Soc. 1999).
• 2026 — Leary and Petrosyan compare Coxeter and Bestvina–Brady candidates for the problem (arXiv:2605.07853).
• 2026 — An OpenAI preprint, A finitely generated counterexample to the Eilenberg–Ganea conjecture (OpenAI Math Release, September 23, 2026), claims a finitely generated residually finite group with $\operatorname{cd}=2$ and $\operatorname{gd}=3$. The preprint has not been peer reviewed and its theorem is not formally verified.

Setting

For a finite simplicial graph $\Delta$ with vertex set $V$, the right-angled Artin group is

$$A_\Delta=\bigl\langle a_q\ (q\in V)\ \bigm|\ a_qa_ra_q^{-1}a_r^{-1}=1\ \text{whenever } q,r \text{ are adjacent}\bigr\rangle ,$$

and the height homomorphism $\lambda:A_\Delta\to\mathbb Z$ sends every $a_q$ to $1$. Its kernel is a Bestvina–Brady group.

The specific graph comes from the presentation complex $K$ of $\langle x,y\mid x^2y^{-5},\ x^2(yx^{-1})^{3}\rangle$, which is integrally acyclic and has a nontrivial representation of its fundamental group into $\mathrm{SU}(2)$. Subdivide each of the two loops of $K$ into three edges, cone the boundary of each relator polygon to a new interior vertex (keeping one radial edge per boundary occurrence), and take the order complex of the resulting regular cell structure (7 vertices, 51 edges, 45 triangular sectors). This is a flag triangulation $L$ of $K$; $\Delta$ is its 1-skeleton, i.e. the comparability graph of the cells. The group is $G=\ker\lambda\le A_\Delta$.

A group is residually finite if every nontrivial element survives in some finite quotient.

Formalization targets

Goal: the counterexample (Theorem 1.1)

For the group $G$ above,

$$G\ \text{is finitely generated and residually finite},\qquad \operatorname{cd}G=2,\qquad G \text{ has a 3-dimensional } K(G,1),\qquad G \text{ has no 2-dimensional } K(G,1).$$

In particular $\operatorname{gd}G=3\ne2=\operatorname{cd}G$. The non-existence clause holds for classifying spaces with any number of cells. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The theorem disproves the Eilenberg–Ganea conjecture with a finitely generated (indeed type $\mathrm{FL}$, but not finitely presented) residually finite group, so the conjecture fails even for countable groups with strong finiteness properties. By Bestvina–Brady's dichotomy the Whitehead conjecture is not directly decided by this example, but the gap between the algebraic and geometric dimensions in dimension two is now exhibited concretely.

Formalizing it. The statement is concrete: an explicit finite graph, its Artin group and height kernel, a projective dimension, and existence/non-existence of CW models. The non-existence clause ranges over all CW complexes of arbitrary cardinality, which is exactly the kind of universally quantified topological claim where a machine check is valuable. Groundwork includes classifying spaces in Mathlib's CW-complex framework, projective dimension over group rings, and Bestvina–Brady Morse theory.

Difficulty

The kernel acts freely on an acyclic 2-complex, which gives $\operatorname{cd}G\le2$, but an acyclic complex need not be contractible, and showing that one particular 2-dimensional model fails to be a $K(G,1)$ says nothing about other models. The obstacle is to rule out every hypothetical two-dimensional classifying space, with arbitrarily many cells, and to do so for a group that is not finitely presented. Homological invariants cannot see the difference, since they agree with those of a genuine 2-dimensional model.

Formalization scope

• The seed complex is encoded combinatorially: signed relator words seedWord, rose vertices, circle edges and sectors; seedGraph is the comparability graph of the cell face relation. ArtinGroup is a PresentedGroup on commutators of adjacent vertices, height sends each generator to $1$ in Multiplicative ℤ, and SourceGroup is its kernel.
• cohomologicalDimension is the categorical projective dimension (in WithBot ℕ∞) of the trivial $\mathbb Z[G]$-module in ModuleCat.
• HasClassifyingSpace G n asks for a Hausdorff, path-connected CW complex with no cells above dimension $n$, fundamental group isomorphic to $G$, and a surjective covering map from a contractible space. The positive clause is stated in universe 0; the negative clause is universe-polymorphic, so no restriction on the cardinality of cells is imposed.
• Needed infrastructure: Bestvina–Brady level complexes, presentations of height kernels, residual finiteness of RAAG subgroups, $\mathrm{SU}(2)$ representations and degree arguments.

Selected references

• S. Eilenberg and T. Ganea, On the Lusternik–Schnirelmann category of abstract groups, Ann. of Math. 65 (1957). https://doi.org/10.2307/1970062
• J. H. C. Whitehead, On adding relations to homotopy groups, Ann. of Math. 42 (1941). https://doi.org/10.2307/1968907
• J. R. Stallings, On torsion-free groups with infinitely many ends, Ann. of Math. 88 (1968). https://doi.org/10.2307/1970577
• R. G. Swan, Groups of cohomological dimension one, J. Algebra 12 (1969). https://doi.org/10.1016/0021-8693(69)90030-1
• M. Bestvina and N. Brady, Morse theory and finiteness properties of groups, Invent. Math. 129 (1997). https://doi.org/10.1007/s002220050168
• W. Dicks and I. J. Leary, Presentations for subgroups of Artin groups, Proc. Amer. Math. Soc. 127 (1999). https://doi.org/10.1090/S0002-9939-99-04873-X
• J. Howie, Bestvina–Brady groups and the plus construction, Math. Proc. Cambridge Philos. Soc. 127 (1999). https://doi.org/10.1017/S0305004199003928
• I. J. Leary and N. Petrosyan, Universal structure of graph product kernels, preprint, 2026. https://arxiv.org/abs/2605.07853v1
• OpenAI, A finitely generated counterexample to the Eilenberg–Ganea conjecture, OpenAI Math Release preprint, September 23, 2026 (source of the goal; Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-finitely-generated-counterexample-to-the-Eilenberg-Ganea-conjecture-September-23-2026/paper.pdf

Motivation

Thompson's group $F$ consists of the increasing piecewise linear homeomorphisms of $[0,1]$ with finitely many pieces, dyadic rational breakpoints, and slopes that are integer powers of $2$. It is finitely presented, has strong topological finiteness properties, and appears across group theory, dynamics and logic. Whether $F$ is amenable, i.e. whether its bounded functions admit a translation-invariant mean, is one of the best-known open questions about a single explicit group. It is a natural test case because the two classical routes to deciding amenability both fail: $F$ contains no nonabelian free subgroup (Brin–Squier 1985), so the free-subgroup obstruction is unavailable, yet $F$ is not elementary amenable (Cannon–Floyd–Parry 1996, Theorem 4.10). Geoghegan conjectured in 1979 that $F$ is nonamenable. The problem has attracted claimed resolutions in both directions, several later withdrawn or found to contain errors.

This mission asks for a formal proof of nonamenability as stated in an OpenAI preprint dated September 23, 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

• 1929–1957 — Von Neumann and Day develop invariant means and amenability (Fund. Math. 1929; Illinois J. Math. 1957); Følner's criterion (Math. Scand. 1955).
• 1965–1973 — Thompson introduces $F$; an early published construction is McKenzie–Thompson (1973).
• 1979 — Geoghegan conjectures that $F$ is nonamenable (recorded in Cannon–Floyd–Parry 1996, p. 227).
• 1984–1985 — Brown and Geoghegan: $F$ is $\mathrm{FP}_\infty$ (Invent. Math. 1984); Brin and Squier: no nonabelian free subgroups (Invent. Math. 1985).
• 2009–2013 — Shavgulidze's amenability claim (arXiv:0906.0107) and Moore's identification of its errors (arXiv:1102.0747); Moore's tower lower bounds for Følner functions (GGD 2013) and Ramsey characterization of amenability (Fund. Math. 2013); Moore's later amenability manuscript is withdrawn (arXiv:1209.2063).
• 2017 — Haagerup and Olesen: $C^*$-simplicity of $T$ would imply nonamenability of $F$ (JFA 2017).
• 2021–2026 — Akhmedov's nonamenability claim via height functions (arXiv:1310.4395v3); Guba's density estimates (J. Comb. Algebra 2025; J. Algebra 2026).

Setting

A homeomorphism $f$ of $[0,1]$ is a dyadic PL map if there are dyadic rationals $0=x_0<x_1<\dots<x_k=1$ and integers $e_i$ such that on each $[x_{i-1},x_i]$, $f(x)=f(x_{i-1})+2^{e_i}(x-x_{i-1})$. The group $F$ is the set of increasing dyadic PL homeomorphisms of $[0,1]$, with multiplication $hg=h\circ g$, regarded as a discrete group. Let $\ell^\infty(F;\mathbb R)$ be the bounded real functions on $F$. A left-invariant mean is a linear functional $M:\ell^\infty(F;\mathbb R)\to\mathbb R$ with $M(\mathbf 1)=1$, $M(\varphi)\ge0$ whenever $\varphi\ge0$, and $M(g\mapsto\varphi(hg))=M(\varphi)$ for every $h\in F$. $F$ is amenable if such a mean exists.

Formalization targets

Goal: Theorem 1.1 (p. 1)

Thompson's group $F$ is not amenable: there is no positive, normalized, left-invariant mean on $\ell^\infty(F;\mathbb R)$.

Significance

The result itself. It settles Geoghegan's conjecture and the amenability problem for $F$. Because $F$ has no free subgroups, $F$ becomes a finitely presented, torsion-free example of a nonamenable group without free subgroups. Through companion results the preprint derives that $F$ has uniformly bounded representations that are not unitarizable (Corollary 3.1, p. 7) and that Bernoulli percolation on every Cayley graph of $F$ has a nonuniqueness phase (Corollary 3.2, p. 8). The proof is short (Section 2) and uses an infinite-dimensional fixed-point phenomenon: the Benyamini–Sternfeld theorem that the unit ball of an infinite-dimensional Hilbert space admits a Lipschitz self-map moving every point by at least a fixed $\delta>0$ (Lemma 1.2, p. 2; Proc. AMS 1983).

Formalizing it. Given the length of the published argument, this is a realistic target for a complete formal proof of a result that had been open for over forty years. It needs the dyadic-partition model of $F$, the Følner criterion (forward direction), and a Lipschitz map on a Hilbert ball with no approximate fixed points (Appendix A of the preprint constructs one on $L^2([0,1];\mathbb R^2)$ with $\delta=1/2$). The Følner direction from invariant means to Følner sets is reusable infrastructure for amenability in Mathlib.

Difficulty

Neither standard obstruction applies: there is no free subgroup to produce a paradoxical decomposition, and no structural closure property shows amenability. Følner sets, if they existed, would have to grow extremely fast (Moore's tower bounds), so explicit counting is ineffective. The preprint's argument converts approximate invariance of a finite set $A\subset F$ into an approximate fixed point of a Lipschitz map on a Hilbert ball, via recursively defined Hilbert-valued colours of dyadic partitions. The delicate points are exact covariance of normalized restrictions under the group action (equation (2.2), p. 4) and controlling the diagonal and nested pairs in the correlation expansion, which yields a uniform lower bound on the relative boundary of every finite set (Proposition 2.3, p. 5).

Formalization scope

• UnitInterval is Set.Icc (0:ℝ) 1; an element of F is a homeomorphism of it that is StrictMono and has a DyadicPLWitness: finitely many strictly increasing dyadic knots from $0$ to $1$ and integer exponents with the affine formula on each piece.
• The goal asserts that some group structure on F exists whose multiplication is composition ((h * g) x = h (g x)); since multiplication is fixed, this structure is unique.
• InvariantMean F is a real-linear functional on lp (fun _ : F => ℝ) ∞ that is positive, sends the constant $1$ to $1$, and is invariant under leftPull h, $\varphi\mapsto(g\mapsto\varphi(hg))$; the goal is ¬ Nonempty (InvariantMean F).
• No generating set, Følner constant or boundary bound is fixed in the statement, so the goal is stable under improved constants.

Selected references

• OpenAI, Thompson's group F is nonamenable, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Thompsons-group-F-is-nonamenable-September-23-2026/paper.pdf
• J. W. Cannon, W. J. Floyd, W. R. Parry, Introductory notes on Richard Thompson's groups, Enseign. Math. (2) 42 (1996), 215–256. https://www.imo.universite-paris-saclay.fr/~emmanuel.breuillard/Cannon.pdf
• M. G. Brin, C. C. Squier, Groups of piecewise linear homeomorphisms of the real line, Invent. Math. 79 (1985), 485–498. https://doi.org/10.1007/BF01388519
• K. S. Brown, R. Geoghegan, An infinite-dimensional torsion-free $\mathrm{FP}_\infty$ group, Invent. Math. 77 (1984), 367–381. https://doi.org/10.1007/BF01388451
• Y. Benyamini, Y. Sternfeld, Spheres in infinite-dimensional normed spaces are Lipschitz contractible, Proc. Amer. Math. Soc. 88 (1983), 439–445. https://doi.org/10.1090/S0002-9939-1983-0699410-7
• E. Følner, On groups with full Banach mean value, Math. Scand. 3 (1955), 243–254. https://doi.org/10.7146/math.scand.a-10442
• J. T. Moore, Amenability and Ramsey theory, Fund. Math. 220 (2013), 263–280. https://doi.org/10.4064/fm220-3-6
• J. T. Moore, Fast growth in the Følner function for Thompson's group F, Groups Geom. Dyn. 7 (2013), 633–651. https://doi.org/10.4171/GGD/201
• U. Haagerup, K. K. Olesen, Non-inner amenability of the Thompson groups T and V, J. Funct. Anal. 272 (2017), 4838–4852. https://doi.org/10.1016/j.jfa.2017.02.003
• M. M. Day, Amenable semigroups, Illinois J. Math. 1 (1957), 509–544. https://doi.org/10.1215/ijm/1255380675

Motivation

A finitely generated group is (word-)hyperbolic if the geodesic triangles in its Cayley graph are uniformly thin, as in the hyperbolic plane. Such a group has a boundary at infinity $\partial G$, a compact space of asymptotic directions. The fundamental group of a closed hyperbolic 3-manifold is hyperbolic with boundary the 2-sphere. Cannon's conjecture asks for the converse: if a hyperbolic group has boundary homeomorphic to $S^2$, does it act geometrically on hyperbolic three-space $\mathbb H^3$? An affirmative answer characterizes, purely in terms of coarse geometry, which groups arise from closed hyperbolic 3-manifolds; it is one of the central problems of geometric group theory and is closely tied to the geometrization program for 3-manifolds.

Timeline

• 1981, 1980. Sullivan and Tukia show that groups of uniformly quasiconformal maps of the sphere are conjugate to Möbius groups (Sullivan, Stony Brook 1978 proceedings; Tukia, doi:10.5186/aasfm.1980.0530).
• 1989. Pansu introduces conformal dimension of boundaries (doi:10.5186/aasfm.1989.1424).
• 1994. Cannon's combinatorial Riemann mapping theorem recovers quasiconformal coordinates from discrete moduli (doi:10.1007/BF02398434).
• 1998. Cannon and Swenson state the group-boundary conjecture and relate geometric actions to conformality of boundary coverings (doi:10.1090/S0002-9947-98-02107-2).
• 1999. Cannon, Floyd and Parry reduce the problem to bounded discrete moduli of annuli at small scales (Ann. Acad. Sci. Fenn. Math., 1999).
• 2002, 2005. Bonk and Kleiner develop quasisymmetric uniformization of metric spheres and prove the conjecture when the Ahlfors-regular conformal dimension is attained (doi:10.1007/s00222-002-0233-z, doi:10.2140/gt.2005.9.219).
• 2012–2013. Kahn–Marković, Bergeron–Wise, Agol and Marković connect surface subgroups, cubulation and Kleinian realizations (doi:10.4007/annals.2012.175.3.4, doi:10.4171/DM/421, doi:10.1007/s00039-013-0228-5). Bourdon and Kleiner give a combinatorial-modulus criterion for uniformization (doi:10.4171/GGD/177).
• 2015. Haïssinsky proves a virtual Kleinian criterion for cubulated hyperbolic groups with planar boundary (doi:10.1007/s00222-014-0552-x).
• 2026. Groves, Haïssinsky, Manning, Osajda, Sisto and Walsh reduce the residually finite case to the Toral Relative Cannon conjecture (arXiv:2406.14667).

The source of this mission, an OpenAI preprint dated September 23, 2026, follows the analytic route and proves the conjecture.

Setting

Let $G$ be a group with a finite symmetric generating set $S$ and Cayley graph $\Gamma(G,S)$ with graph distance $d$. $G$ is hyperbolic if there is $\delta$ such that every point on a side of a geodesic triangle lies within $d\le\delta$ of the union of the other two sides. A geodesic ray based at $1$ is a sequence $r_0=1,r_1,\dots$ with $d(r_i,r_j)=|i-j|$; two rays are equivalent if $d(r_n,s_n)$ stays bounded. The boundary $\partial G$ is the set of equivalence classes with the quotient of the topology of pointwise convergence.

$\mathbb H^3$ is the upper half-space $\{x\in\mathbb R^3: x_3>0\}$ with distance $\operatorname{arcosh}\bigl(1+|x-y|^2/(2x_3y_3)\bigr)$, and $\operatorname{Isom}(\mathbb H^3)$ is its full isometry group, including orientation-reversing isometries. A homomorphism $\rho:G\to\operatorname{Isom}(\mathbb H^3)$ gives a proper action if $\{g:\rho(g)K\cap K\ne\varnothing\}$ is finite for every compact $K$, and a cocompact action if translates of one compact set cover $\mathbb H^3$.

Formalization targets

Goal: Theorem 1.1

$$G\ \text{hyperbolic},\ \partial G\cong S^2\ \Longrightarrow\ \exists\,\rho:G\to\operatorname{Isom}(\mathbb H^3)\ \text{proper, cocompact, with }\ker\rho\ \text{finite}.$$

The Lean statement OAI.CannonRelease.cannon is open on the platform.

Significance

The theorem identifies hyperbolic groups with 2-sphere boundary, up to finite kernels, with uniform lattices in $\operatorname{Isom}(\mathbb H^3)$. For torsion-free $G$, the quotient $\mathbb H^3/G$ is a closed hyperbolic 3-manifold, possibly nonorientable (Corollary 8.1), and the work of Kahn–Marković, Bergeron–Wise and Agol then gives virtual structure results (Corollary 8.2). It also settles the hypotheses of the reductions of Marković and of Groves et al. in full generality.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. A formal proof would require formal infrastructure for hyperbolic groups and their boundaries, quasiconformal analysis and combinatorial modulus, very little of which is currently in Mathlib.

Difficulty

By the Cannon–Floyd–Parry and Bourdon–Kleiner criteria, the theorem reduces to a uniform upper bound on the combinatorial 2-modulus of curve families at all scales of the boundary. The bound is easy to state but there is no a priori reason why moduli of coverings of a topological sphere should stay bounded; Bonk–Kleiner needed the extra hypothesis that the conformal dimension is attained. A proof must extract analytic control (a nonconstant limit function with controlled oscillation) from a hypothetical sequence of coverings with unbounded modulus and contradict it using only hyperbolicity and the topology of the boundary.

Formalization scope

• CayleyData G is a finite symmetric generating set with connected SimpleGraph.mulCayley; ThinTriangles asks for one natural number $\delta$ working for all geodesic triangles given as walks of length equal to graph distance.
• Rays are ℕ → G with r 0 = 1 and dist (r i) (r j) = |i-j|; the boundary is the quotient by bounded synchronous distance. $G$ carries the discrete topology, rays the subspace product topology, and the boundary the quotient topology, which coincides with the visual topology for hyperbolic groups.
• $S^2$ is the unit sphere in EuclideanSpace ℝ (Fin 3); $\mathbb H^3$ is the upper half-space with the explicit arcosh distance and subspace topology; isometries are self-homeomorphisms preserving that distance.
• The kernel is only required to be finite, and orientation-reversing elements are allowed, matching the paper.

A complete development needs Gromov hyperbolic groups and visual metrics, approximately self-similar spheres, combinatorial modulus and the Bonk–Kleiner/Bourdon–Kleiner uniformization criterion, and the Sullivan–Tukia straightening of uniformly quasiconformal groups. Contributions formalizing Proposition 2.6 (from a round boundary action to a geometric action on $\mathbb H^3$) or Theorem 2.5 (the uniformization criterion) are welcome.

Selected references

• OpenAI, A Modulus Proof of Cannon's Conjecture, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Modulus-Proof-of-Cannons-Conjecture-September-23-2026/paper.pdf
• J. W. Cannon, The combinatorial Riemann mapping theorem, Acta Math., 1994. https://doi.org/10.1007/BF02398434
• J. W. Cannon, E. L. Swenson, Recognizing constant curvature discrete groups in dimension 3, Trans. Amer. Math. Soc., 1998. https://doi.org/10.1090/S0002-9947-98-02107-2
• J. W. Cannon, W. J. Floyd, W. R. Parry, Sufficiently rich families of planar rings, Ann. Acad. Sci. Fenn. Math., 1999. https://www.acadsci.fi/mathematica/Vol24/cannon.pdf
• M. Bonk, B. Kleiner, Quasisymmetric parametrizations of two-dimensional metric spheres, Invent. Math., 2002. https://doi.org/10.1007/s00222-002-0233-z
• M. Bonk, B. Kleiner, Conformal dimension and Gromov hyperbolic groups with 2-sphere boundary, Geom. Topol., 2005. https://doi.org/10.2140/gt.2005.9.219
• M. Bourdon, B. Kleiner, Combinatorial modulus, the combinatorial Loewner property, and Coxeter groups, Groups Geom. Dyn., 2013. https://doi.org/10.4171/GGD/177
• V. Marković, Criterion for Cannon's conjecture, Geom. Funct. Anal., 2013. https://doi.org/10.1007/s00039-013-0228-5
• P. Haïssinsky, Hyperbolic groups with planar boundaries, Invent. Math., 2015. https://doi.org/10.1007/s00222-014-0552-x
• D. Groves, P. Haïssinsky, J. F. Manning, D. Osajda, A. Sisto, G. S. Walsh, Drilling hyperbolic groups, preprint, 2026. https://arxiv.org/abs/2406.14667

Motivation: does having a normal form imply termination?

Pure type systems (PTSs) are a uniform framework covering the simply typed λ-calculus, System F, the calculus of constructions and the type theories behind proof assistants such as Coq and Lean. A system is specified by its sorts (like $\ast$ and $\square$), axioms ($\ast:\square$) and product rules (which dependent function types may be formed). Normalization is the key metatheoretic property: it underlies logical consistency and decidability of type checking. There are two versions. A term is weakly normalizing if some sequence of β-reductions reaches a normal form, and strongly normalizing if every reduction sequence is finite. Strong normalization is what implementations need (any evaluation strategy terminates) but it is much harder to prove. The Barendregt–Geuvers–Klop conjecture asserts that, for pure type systems, the system-wide weak property already implies the strong one.

Timeline

• 1989 — Girard's Proofs and Types presents the Tait–Girard reducibility method for strong normalization (book).
• 1993 — Geuvers states the system-wide conjecture for β and βη reduction in his thesis (Logics and Type Systems, Nijmegen, Conjecture 8.1.2) (thesis).
• 1997 — Sørensen proves the implication for generalized nondependent, clean, negatable systems via continuation-passing translations (thesis, Copenhagen, Theorem 3.5.20).
• 2001 — Barthe, Hatcliff and Sørensen prove a uniform nondependent version (TCS 2001).
• 2006 — Barthe and Coquand show that erasing λ-domain annotations can identify non-convertible terms in non-normalizing PTSs (JFP 2006), a constraint on erasure-based approaches.
• 2014 — Roux and van Doorn develop a structural theory of PTSs, preserving weak normalization under sums and added rules (RTA–TLCA 2014).
• 2023 — Mull reduces the conjecture within tiered systems to an irrelevance-eliminating translation (TYPES 2022, LIPIcs 2023) and extends the nondependent results in his thesis (Chicago, 2023).
• 2025 — Roux proposes internal strong-normalization proofs for specific systems (TYPES 2025 abstract).
• 2026 — An OpenAI preprint, Weak and strong normalization in pure type systems (OpenAI Math Release, September 25, 2026), claims the β-version of the conjecture for every PTS, with no functionality assumption. The preprint has not been peer reviewed and its theorem is not formally verified.

Setting

A specification consists of a type $S$ of sorts, an axiom relation $\mathcal A\subseteq S^2$ and a rule relation $\mathcal R\subseteq S^3$; neither is assumed functional. Expressions are

$$M,N,A,B ::= x\mid s\mid MN\mid \lambda x{:}A.\,M\mid \Pi x{:}A.\,B,\qquad s\in S,$$

up to renaming of bound variables. β-reduction is the compatible closure of $(\lambda x{:}A.M)N\to_\beta M[x:=N]$, with steps allowed everywhere, including inside the annotation $A$ of a λ and both parts of a Π. Typing $\Gamma\vdash M:A$ is generated by the seven standard PTS rules (axiom, variable, weakening, product, abstraction, application, conversion up to $=_\beta$). A context is valid if each declared type is typed by a sort in the preceding prefix, and $M$ is legal in $\Gamma$ if $\Gamma\vdash M:A$ or $\Gamma\vdash A:M$ for some $A$.

The system is weakly (strongly) normalizing if every legal expression in every valid context is weakly (strongly) normalizing.

Formalization targets

Goal: β-Barendregt–Geuvers–Klop (Theorem 1)

For every specification $\mathcal P=(S,\mathcal A,\mathcal R)$,

$$\bigl(\forall \Gamma\ \text{valid},\ \forall M\ \text{legal in }\Gamma:\ M\ \text{is weakly }\beta\text{-normalizing}\bigr) \ \Longrightarrow\ \bigl(\forall \Gamma\ \text{valid},\ \forall M\ \text{legal in }\Gamma:\ M\ \text{is strongly }\beta\text{-normalizing}\bigr).$$

Both quantifiers range over the whole system; the theorem does not claim that an individual weakly normalizing term is strongly normalizing, and it says nothing about η-reduction. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. For any PTS, a proof that every legal term has a normal form now yields termination of every β-reduction strategy, including reductions inside types and annotations that may continue after the computational body is normal. Earlier results needed nondependent products, cleanliness, negatability, a tiered sort hierarchy, or a translation requiring extra product rules; the general case — arbitrary sorts and nonfunctional rules — was not covered by any earlier result since Geuvers' 1993 formulation.

Formalizing it. The statement is entirely syntactic and finitary, so it is a natural target for a proof assistant, and the relevant objects (de Bruijn syntax, substitution, typing derivations) are standard formalization material. The proof in the source is long (over 70 pages) and combines reducibility candidates with a fixed-point construction over sort profiles; a machine check would substantially raise confidence. A formal PTS metatheory library (substitution lemmas, confluence, subject reduction) would be reusable for other type-theory formalizations.

Difficulty

The obvious route — reducibility candidates à la Tait–Girard — needs a model of types built by recursion on sorts, which fails for impredicative or nonfunctional specifications where a type can have several sorts and no hierarchy is available. Translation methods (CPS or irrelevance elimination) need specific product rules to preserve typing, which a general specification may lack. Weak normalization of one term cannot be used alone; the argument must exploit normal forms of other open expressions. Annotations add a further complication: erasing them can change the equational theory (Barthe–Coquand), so reduction inside annotations must be tracked rather than erased.

Formalization scope

• Expressions use de Bruijn indices (Expr S with var, sort, app, lam, pi), so α-equivalence is syntactic; substitution is parallel substitution with lifting.
• Beta is full compatible closure, including lam_domain, pi_domain and pi_body steps; conversion is Relation.EqvGen Beta.
• HasType has exactly the seven PTS rules; contexts are lists stored newest-first, each declaration typed in its prefix (ValidContext). Legal includes expressions occurring as types.
• Weak normalization is reduction to a normal form; strong normalization is accessibility for the converse of Beta.
• The sort type S is arbitrary (any universe), and axioms and rules are arbitrary relations: no functionality, finiteness or hierarchy assumptions.
• Needed infrastructure: renaming/substitution lemmas, confluence of β, subject reduction for PTSs, reducibility candidates. All are reusable for any PTS formalization.

Selected references

• J. H. Geuvers, Logics and Type Systems, PhD thesis, Katholieke Universiteit Nijmegen, 1993. https://www.cs.ru.nl/~herman/PUBS/Proefschrift.pdf
• J.-Y. Girard, Proofs and Types, Cambridge University Press, 1989. https://www.paultaylor.eu/stable/prot.pdf
• M. H. B. Sørensen, Normalization in λ-Calculus and Type Theory, PhD thesis, University of Copenhagen, 1997. https://di.ku.dk/forskning/Publikationer/tekniske_rapporter/tekniske-rapporter-1997/97-27.pdf
• G. Barthe, J. Hatcliff and M. H. Sørensen, Weak normalization implies strong normalization in a class of non-dependent pure type systems, Theoret. Comput. Sci. (2001). https://doi.org/10.1016/S0304-3975(01)00012-3
• G. Barthe and T. Coquand, Remarks on the equational theory of non-normalizing pure type systems, J. Funct. Programming (2006). https://doi.org/10.1017/S0956796803004726
• C. Roux and F. van Doorn, The structural theory of pure type systems, RTA–TLCA 2014. https://doi.org/10.1007/978-3-319-08918-8_25
• N. Mull, An irrelevancy-eliminating translation of pure type systems, TYPES 2022, LIPIcs, 2023. https://doi.org/10.4230/LIPIcs.TYPES.2022.7
• OpenAI, Weak and strong normalization in pure type systems, OpenAI Math Release preprint, September 25, 2026 (source of the goal; Theorem 1, p. 3). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Weak-and-strong-normalization-in-pure-type-systems-September-25-2026/paper.pdf