Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Computing the ground-state energy of electrons in the Coulomb field of fixed nuclei is the basic problem of quantum chemistry. In quantum complexity theory, a problem is QMA-hard if every problem with polynomial-time quantum verification of a quantum witness (the quantum analogue of NP) reduces to it. Hardness was previously known for lattice models with magnetic fields, for continuum models with freely designed potentials, and for electronic structure restricted to a supplied finite orbital basis. None of these is the exact problem in which the external field comes only from point nuclei of charge one — hydrogen-like nuclei — and the energy is minimized over every antisymmetric many-electron wavefunction in the continuum. Two obstacles separate the known results from this problem: a designed potential need not be a sum of unit Coulomb wells, and a projected (finite-basis) energy only bounds the continuum infimum from above.
An instance consists of pairwise distinct positions of nuclei of charge one, an electron number encoded in unary, and rational thresholds (signed binary numerators, positive binary denominators). The electronic Hamiltonian is
on , defined through its closed form on . Antisymmetry exchanges position and spin together and no spin sector is selected. equals the infimum of the form over normalized vectors of . YES: ; NO: . Nuclear repulsion is omitted.
In Lean, unitGroundEnergy is that infimum (as an EReal) over normalized antisymmetric states with explicit square-integrable weak gradients; InQMA is defined by polynomial-time uniform circuit families with completeness and soundness ; QMAHard requires a deterministic polynomial-time (Turing-machine computable) many-one reduction from every QMA promise problem.
for the promise problem whose valid instances have threshold separation . This is Theorem 1 of the source in the form produced by its reduction ("threshold separation at least one"), which implies the stated precision . The goal is published on the platform with status Open.
The result itself. The theorem shows that the exact clamped-nucleus electronic ground-energy problem is QMA-hard even when all nuclei are protons (charge one), with no supplied basis, magnetic field, or extra potential, and with constant threshold separation. It makes no claim of membership in QMA, of a molecular spectral gap, or of a ground eigenvector. It implies the companion binary-charge theorem, whose input class is larger, while the companion's proof gives independent tools.
Formalizing it. The Lean statement fixes the input encoding, the variational ground energy, and the notion of QMA precisely. Its proof would need the QMA-completeness source (an external theorem), finite spin and Hubbard reductions, and continuum estimates for Coulomb operators (localization, complement gaps, Hardy-type form bounds), most of which is absent from Mathlib. The definitions are shared with the binary-charge mission.
Unit nuclei offer no independently adjustable charges, so the wells needed for a Hubbard model must be produced by the geometry of many nuclei alone; the construction first builds a nonnegative continuous charge density and then replaces it by equal-mass point charges via a measure-transport flow and cubature, with rational rounding. The replacement error is not small on arbitrary states; only its compression to smooth localized modes is small. The lower bound must hold for every antisymmetric state in every spin sector, which requires a uniform gap on the one-particle complement and careful handling of the long-range direct Coulomb repulsion.
UnitCoulomb records (a list of rational positions, unary electron count, two binary rationals) with a self-delimiting bit encoding; validity requires , distinct positions, positive denominators and . Lowest-terms encoding of rationals is not required in Lean, a harmless relaxation.unitGroundEnergy is computed by toNuclearData with every charge equal to one, using the same Coulomb form as the binary-charge definitions.Turing.TM2ComputableInPolyTime, and a polynomial size bound; the reduction must be polynomial-time computable on the encodings.Computing the ground-state energy of a molecule — electrons moving in the Coulomb field of fixed nuclei — is the central task of quantum chemistry. Quantum complexity theory asks whether it is hard even for a quantum computer: a problem is QMA-hard if every problem verifiable by a polynomial-time quantum verifier with a quantum witness reduces to it (QMA is the quantum analogue of NP). Many lattice and finite-basis versions of electronic structure are known to be QMA-complete, but those results either allow magnetic fields and designed potentials, or restrict the electrons to a supplied finite orbital basis. The exact problem — external field generated only by positive point nuclei, minimization over the full continuum of antisymmetric many-electron wavefunctions — needs a lower bound excluding every state outside any chosen orbital set, which projection arguments do not provide.
An instance consists of pairwise distinct nuclear positions , positive integer charges (encoded in binary), an electron number (encoded in unary), and rational thresholds . The electronic Hamiltonian, in atomic units, is
on the antisymmetric space (positions and spins permuted together), defined through its closed quadratic form on . Let . YES instances have ; NO instances have . Nuclear repulsion is omitted (clamped-nucleus electronic energy) and all spin sectors are included.
In Lean, groundEnergy is the infimum (in EReal) of the Coulomb form over normalized antisymmetric states, given by explicit square-integrable values and weak gradients; QMA is defined through polynomial-time uniform families of circuits with acceptance / ; QMAHard asks for a deterministic polynomial-time many-one reduction (as a Turing-machine-computable map on bit strings) from every QMA promise problem.
for the promise problem whose valid instances satisfy . This is Theorem 1.1 of the source in its stronger form ("the reduction can produce instances with "), which implies the stated precision . The goal is published on the platform with status Open.
The result itself. The theorem places the exact clamped-nuclei electronic ground-energy problem, with no supplied basis, field, or designed potential, among QMA-hard problems at inverse-polynomial (indeed constant) precision. It makes no claim of membership in QMA, of a spectral gap, or of hardness under bounded charges. The companion unit-charge theorem implies this one for the larger binary-charge input class; the present proof is independent and contributes certified exponential-accuracy eigenvalue computation and relative tunneling calibration for widely separated hydrogenic wells.
Formalizing it. A complete formalization would combine a QMA-completeness source theorem (Heisenberg models), finite spin and Hubbard reductions, and continuum many-body spectral estimates (Hardy inequality, localization, complement gaps) — a large but well-delimited body of mathematics, much of it absent from Mathlib. The precise Lean encoding of inputs and of QMA itself is reusable for other Hamiltonian-complexity missions.
Projecting onto chosen orbitals gives an upper bound on but says nothing about states outside the projection, so finite-basis hardness does not transfer NO instances. The construction must realize prescribed, exponentially small Hubbard hoppings using only point nuclei, with relative (not absolute) precision, and must certify one-well energies to exponential accuracy using polynomially many bits. Finally a lower bound for the full many-electron spectral infimum must hold for every fermionic state, in every spin sector.
BinaryCoulomb records (list of rational positions with natural charges, unary electron count, two binary rationals) with an explicit self-delimiting bit encoding; validity requires , distinct positions, positive denominators, positive charges, and . Lowest-terms encoding is not required in Lean, a harmless relaxation.H1Vector n with antisymmetry under simultaneous permutation of positions and spins; groundEnergy is an EReal infimum over normalized states, which is the variational characterization of .Turing.TM2ComputableInPolyTime); the reduction must also be TM2ComputableInPolyTime.Parity, , 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 () 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 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 . Because fanout makes constant-depth quantum circuits very powerful (Høyer–Špalek, ToC 2005), whether has been a central question about shallow quantum computation.
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.
A circuit acts on qubits, with state space and computational basis indexed by bit strings . The allowed gates are arbitrary one-qubit unitaries and generalized Toffoli gates on distinct control and target qubits. A layer is a set of gates with pairwise disjoint supports, and a depth- circuit is a product of at most layers. Gates and their complex entries may depend on but not on the input.
On input with , the circuit starts in . 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 is
A circuit computes parity with worst-case advantage if this probability is at least for every .
Fix an integer , a real and . Then for all sufficiently large , for every with , every circuit of depth at most on qubits and every choice of output qubit, there is an input with
With this is the usual bounded-error statement in the measured-output model.
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.
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 . The preprint's route controls transitions from a product condition to states with many mismatches, for all fixed (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.
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 (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 with zeros; successProbability W out x sums over all whose output bit equals the parity of , so final garbage is unrestricted.out : Fin N is arbitrary, including an input qubit. The quantifier order is: depth, size bound and advantage fixed first; then a threshold ; then every , every in range, every circuit and every output qubit.ParityStatement takes the size bound as a real exponent: with real, , and depth layers.length ≤ d with , exactly as in Theorem 1. Its conclusion is the negation of "for every , success ".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).
Shannon's entropy power inequality bounds the entropy of a sum of independent random vectors below by the entropies of the summands; it is a basic tool for classical Gaussian channel capacities. In optical communication, addition is replaced by passive mixing of bosonic modes at a beam splitter. Guha, Erkmen and Shapiro conjectured the sharp bosonic analogue, the entropy photon-number inequality (EPnI), stated in terms of the photon number of the thermal state with the same entropy (ITA 2008). If true, it settles the minimum output entropy of thermal attenuators at fixed input entropy and the capacity regions of bosonic broadcast and wiretap channels, which had been reduced to this inequality (PRA 2007).
This mission asks for a formal proof of the EPnI for finite-energy inputs in any finite number of modes, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
An -mode bosonic system has Fock space with number basis , . A state is a positive trace-one operator ; it has finite energy if . The von Neumann entropy is (natural log). The thermal entropy per mode is
increasing from to , and the entropy photon number of is , the mean photon number per mode of the product thermal state with the same entropy. For independent inputs and transmissivity , the beam-splitter output is the reduced state of the modes after passive mixing of . No independence among the modes within either input is assumed.
For every finite , every pair of finite-energy -mode states and every ,
Thermal inputs with a common mean photon number within each port give equality.
The result itself. The EPnI is sharper than the exponential quantum entropy power inequality when the two input entropies differ, which is exactly the regime needed for constrained minimum output entropy. The preprint derives the exact minimum output entropy at fixed input entropy for every tensor power of an identical thermal attenuator, with inputs entangled across modes (Corollary 1.2, p. 2), and the exact capacity region of the degraded two-receiver pure-loss broadcast channel (Corollary 7.1, p. 26), completing the converse of Guha, Shapiro and Erkmen.
Formalizing it. The statement involves infinite-dimensional Fock space, trace-class positive operators, continuous functional calculus for the entropy, and the partial trace after a passive unitary. The Lean development builds these concretely in the number basis. A formal proof would give machine-checked infrastructure for quantum entropy on infinite-dimensional spaces, which Mathlib currently lacks. No machine-checked version of any quantum entropy power inequality is known.
Heat-flow (quantum Fisher information) proofs give the linear and exponential bounds, but these are attained only for equal entropies and do not recover the thermal comparison at unequal entropy levels. The preprint instead minimizes a regularized functional over pairs of inputs and must show that minimizers are thermal. This requires an interpolation theorem for diagonal form comparisons (Theorem 3.1, p. 8), attainment and Gibbs regularity of minimizers in infinite dimensions (Lemma 4.1, Proposition 4.2, pp. 15–16), a component entropy-Hessian estimate, and a stationarity identity whose cancellation forces convergence to thermal inputs (Section 6). Compactness relies on the finite-energy hypothesis; without it entropies can be infinite.
Fock n is lp (fun _ : Fin n → ℕ => ℂ) 2. A State is a positive bounded operator whose diagonal in the number basis sums (HasSum) to .FiniteEnergy ρ is summability of .entropy ρ is the sum of diagonal entries of ; for finite-energy states it is finite, so the tsum is the true entropy.gInv s = sInf {t ≥ 0 | s ≤ g t}, the inverse of on .IsBeamSplitterOutput η ρA ρB ρC requires every number-basis entry of to be the (convergent) partial-trace sum of the explicitly given beam-splitter coefficients applied to ; the inputs are arbitrary density matrices, so internal entanglement is allowed.The quantum Heisenberg ferromagnet is the basic quantum model of a magnet: a quantum spin sits at each site of the lattice 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 it has been a standard open problem of mathematical physics, recorded by Lieb in 1999 and again by Seiringer in 2025.
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 .
Fix and a spin ; write . Each site carries with basis and
, . For finite the free-boundary Hamiltonian is
each unordered edge counted once. The quasi-local algebra is the norm completion of the local matrix algebras . The dynamics is along the boxes .
A state is a positive linear functional on with . It is -KMS if for all there is a bounded function , continuous on and analytic inside, with
It is translation invariant if for all .
The Lean statement OAI.Heisenberg.spontaneous_magnetization also asserts that the box limits defining converge for every and (the standing fact the theorem relies on). The goal is open on the platform.
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 . 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 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.
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 , 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.
Fin d → ℤ; a spin level is Fin (ℓ+1) with magnetic quantum number . The Hilbert space is 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 ( distance one) with one orientation per edge; box d n is ; dynamics is the limUnder of the box dynamics, and DynamicsConverges asserts that these limits exist.State packages a continuous linear functional with and ; IsKMS β ω requires and, for every , a bounded continuous on the closed strip, complex-differentiable on the open strip, with the two boundary identities.A complete development needs quantum spin systems on , 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.
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.
Let be the flat torus with torus distance . For particles and exclusion distance , the allowed configurations are
The hard-sphere Hamiltonian is the operator of the Dirichlet form on restricted to symmetric (bosonic) functions; wave functions vanish on forbidden configurations, and is the scattering length. A ground vector is a normalized bosonic minimizer of . For a normalized bosonic , the condensate fraction in the constant orbital is
and for a density operator it is defined by linearity. The gas parameter is with the density.
There are absolute constants such that, for all with and every sequence , with :
The constant does not depend on the gas parameter in this range.
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.
Energy estimates alone cannot detect occupation of the constant orbital, because the cost of moving particles out of it is of order 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 to complex (Lemma 2.3, p. 9).
Fin N → Fin 3 → AddCircle L; the allowed set uses the Euclidean torus distance with strict inequality a < dist.dirichletDomain is the closure, in , of jets of smooth compactly supported test functions with support in the allowed set; energy is the sum of squared 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 ; mixedOccupation T is the trace of compressed by the bounded map . GroundSupported T says every unit vector in is (the first component of) a ground vector.Lieb–Thirring inequalities bound the negative eigenvalues of a Schrödinger operator 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 : for it should be the constant of the best potential with a single bound state, given by an explicit profile.
The source of this mission, an OpenAI preprint dated September 23, 2026, proves the conjectured sharp constant for every .
For , let be the self-adjoint operator of the quadratic form
For its negative spectrum is discrete; write with multiplicity, possibly a priori. The optimal constant is
is the same supremum with only the lowest eigenvalue retained, and the semiclassical constant is
For and every ,
the constant equals , and with equality holds for . The Lean statement OAI.SharpLiebThirring.sharp_lieb_thirring is open on the platform.
The theorem settles the one-dimensional Lieb–Thirring conjecture on the whole interval , extending the case of Read and Schulz: allowing many bound states never beats a single optimally shaped well. Combined with the known endpoint results ( and ), 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.
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 (where the inequality is dual to a kinetic-energy bound for orthonormal families) do not directly apply at other exponents, since the moment is not linear in the density matrix. The proof must keep track of the individual eigenvalue scales.
H1 packages with a weak derivative in , tested against smooth compactly supported functions.negativeMoment γ W is the supremum, in , over all finite orthonormal families of such eigenfunctions of ; this counts multiplicity and does not presuppose finiteness. oneStateMoment retains one eigenfunction.Admissible γ W is a.e. and ; potentialMass is the lower Lebesgue integral of ; the optimal constants are suprema over admissible with positive mass.A complete development needs Sobolev space and form methods, the variational characterization of negative eigenvalues, Gamma-function identities for , the explicit eigenvalue computation, and the paper's action inequality. Contributions formalizing Theorem 2.1 (action inequality) and the equality computation for the potential are welcome.
Given a group , adjoin one new generator and impose one relation , where is a word in and elements of . Can the result collapse to the trivial group when is nontrivial? The Kervaire conjecture says no. It arose from Kervaire's 1965 characterization of high-dimensional knot groups, which involves groups normally generated by a single element, and it is one of the best-known problems about equations over groups: when does an equation with coefficients in have a solution in some group containing ?
The source of this mission, an OpenAI preprint dated September 24, 2026, proves unimodular coefficient injectivity for every group by a route through spectral phase and a fixed-space theorem for unitary matrices.
Let be a group, , and the free product. Let be the homomorphism that kills and sends to ; is the exponent sum of in . A word is unimodular if . Write for the normal closure of in . The coefficient map is the composite
Its injectivity is equivalent to solvability of over : there is an overgroup and with .
The Lean statement OAI.Kervaire.coefficient_injective is open on the platform.
Theorem 1.1 immediately gives the Kervaire conjecture (Corollary 1.2): if then for every , since for the quotient maps onto . It proves the unimodular case of the stronger Kervaire–Laudenbach conjecture with no hypothesis on : no torsion-freeness, residual finiteness, hyperlinearity or countability. The paper's companion work extends the method to nonsingular systems of equations (Howie's conjecture).
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. The statement is short and entirely algebraic, which makes it an attractive formalization target; Mathlib already provides free products and normal closures.
The classical Gerstenhaber–Rothaus argument solves the equation in a unitary group and needs to embed in (an ultraproduct of) unitary groups, which is not known for arbitrary groups. Torsion in blocks the diagrammatic and topological arguments that work in the torsion-free case. A proof for every group therefore needs a representation available for all groups (the left regular representation, with its faithful finite trace) together with an argument that does not rely on finite-dimensional approximation of .
Monoid.Coprod A (Multiplicative ℤ); the exponent sum is Multiplicative.toAdd (Monoid.Coprod.snd w).Unimodular w is exponentSum w = 1 ∨ exponentSum w = -1.Subgroup.normalClosure {w}, and coefficientMap w is the quotient map composed with Monoid.Coprod.inl.A complete development needs the group von Neumann algebra of (or at least its trace), the spectral phase of unitaries and its subadditivity, a degree computation on a compact manifold of unitaries with fixed -planes, and corner-labelled planar diagrams with Euler-characteristic estimates. Contributions formalizing Corollary 1.2 from Theorem 1.1, Lemma 2.1 (subadditivity of spectral phase) and Lemma 3.1 (fixed-space lemma) are welcome.
Geometric group theory studies finitely generated groups through their word metrics, which are well defined up to quasi-isometry. A basic question is which algebraic properties are quasi-isometry invariants: if a group "looks like" a group from far away, must share 's algebraic structure? Gromov's polynomial-growth theorem (1981) answers this for virtually nilpotent groups. The next natural class is the virtually polycyclic groups — groups with a finite-index subgroup admitting a finite subnormal series with cyclic factors — which are exactly, up to finite index, the lattices in connected simply connected solvable Lie groups. Eskin, Fisher and Whyte conjectured that this class is quasi-isometrically rigid, and the question had been settled only for special families such as and certain abelian-by-abelian groups.
For finitely generated groups with word metrics, a -quasi-isometry satisfies and has -dense image. For finitely generated groups this is equivalent to a coarse equivalence: maps , sending pairs at bounded distance (differences in a fixed finite set) to pairs at bounded distance, with and at bounded distance from the identities. A uniform lattice in a locally compact group is a discrete subgroup with for a compact ; a lattice is a discrete subgroup whose coset space carries an -invariant probability measure.
For the height theorem: a connected simply connected Lie group is real-triangulable if the adjoint representation of its Lie algebra is simultaneously upper triangular in some real basis, with diagonal characters . Put and ; the exponential height map is the homomorphism whose differential is the quotient map. is unimodular if its left Haar measure is right invariant.
Let be connected, simply connected, real-triangulable and unimodular, with a proper left-invariant metric and a norm on . There is a finite subgroup such that for all , there is with: every self quasi-isometry of has some with
If a finitely generated group is quasi-isometric to a lattice in a connected simply connected solvable Lie group, then a finite-index subgroup of is a uniform lattice in some (possibly different) connected simply connected solvable Lie group.
Let be finitely generated and virtually polycyclic and finitely generated. If is quasi-isometric to , then
The second clause is the classical lattice realization of virtually polycyclic groups (Dekimpe's theorem, used in the source's proof of Corollary 1.2), recorded in the same formal statement. All three statements are published on the platform with status Open: no machine-checked proofs exist yet.
The result itself. Virtual polycyclicity becomes a quasi-isometry invariant among finitely generated groups, extending Gromov's theorem from nilpotent to solvable lattices and resolving the Eskin–Fisher–Whyte conjecture in its lattice form, where the ambient Lie group may change. The bounded-height theorem is a rigidity statement for quasi-isometries of an entire class of solvable Lie groups: up to bounded error and a finite group of linear symmetries, every quasi-isometry preserves height. This is the kind of control that previously required case-by-case coarse differentiation.
Formalizing it. The proof combines Lie theory, measured couplings, reduced cohomology, volume growth, Gromov's theorem and finiteness/duality results for elementary amenable groups — a long chain in which a machine check would add real confidence. Basic objects (coarse equivalences of groups, polycyclic series, uniform lattices, Lie groups with exponential maps) are reusable across geometric group theory.
Quasi-isometries carry no algebraic structure and can be wild at bounded scales, so the comparison group cannot be assumed solvable or even amenable a priori. Shalom's argument yields only a nontrivial homomorphism to , not full structure. The geometric core is height rigidity: one must show that a quasi-isometry cannot mix "up" and "down" directions of different exponential rates, uniformly over all quasi-isometries with given constants, and with a bounded (not merely sublinear) error, which is exactly what the later group-theoretic deduction needs.
GroupCoarseEquivalence, with bornologous maps and errors in finite sets — equivalent to quasi-isometry of word metrics.SimplyConnectedSolvableLieModel (finite-dimensional charted Lie group, Hausdorff, second countable, simply connected, solvable). Uniform lattices are discrete subgroups with a compact fundamental cover; finite-covolume lattices carry an invariant probability measure on the coset space.TriangularAdjoint basis, is any normed space linearly isomorphic to the canonical quotient, and is characterized through an exponential map. The metric is any compatible proper left-invariant metric with linear chain bounds — a quasi-isometric generalization of the source's fixed left-invariant Riemannian metric. The finite group is chosen before .A representation of a group by bounded invertible operators on a Hilbert space is uniformly bounded if , and unitarizable if after a change of inner product it becomes unitary, i.e. some bounded invertible makes every 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, -invariants and measured group theory for seven decades.
The source of this mission, an OpenAI preprint dated September 23, 2026, answers Dixmier's question affirmatively for all discrete groups.
Let be a discrete group. is amenable if there is a linear functional on the bounded functions with , for , and , where .
A representation is a homomorphism into bounded operators on a complex Hilbert space (each is then invertible). It is similar to a unitary representation if there is a bounded invertible with unitary for every . 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.
Every countable nonamenable has a representation on a separable Hilbert space with that is not similar to a unitary representation.
and for nonamenable and every there is with not similar to a unitary representation, on a separable space when is countable. The Lean statement OAI.Dixmier.current_main_theorem is open on the platform.
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 . Earlier results produced witnesses for groups with free subgroups, for residually finite groups with positive -Betti number, or for wreath-product extensions of ; the theorem gives a witness for every nonamenable 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.
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 -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.
G with the discrete topology, using G →ᵇ ℂ for ; positivity is required on functions with nonnegative real values.G →* (H →L[ℂ] H) with [InnerProductSpace ℂ H] [CompleteSpace H]; SimilarToUnitary π asks for S : H ≃L[ℂ] H with for all .max u v, and the witness is built there; since the theorem holds for every v, this covers all Hilbert spaces.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.
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 .
This preprint constructs a single group of type , i.e. with a classifying space having finitely many cells in every dimension, that contains every finitely presented group. This answers the form of the higher-dimensional Higman embedding question posed by Fournier-Facio and Zaremsky.
A classifying complex for a group is a connected CW complex with fundamental group isomorphic to and contractible universal cover; it may be infinite-dimensional. has type if some classifying complex has finite -skeleton, and type if some classifying complex has finitely many cells in every dimension. Type 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 with a CW structure on Set.univ having finitely many -cells for every , a basepoint with , and a surjective covering map from a contractible space. Finite presentation is Mathlib's Group.IsFinitelyPresented.
There exists a group of type such that every finitely presented group admits an injective homomorphism into :
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 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 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.
Higman's universal group is only finitely presented; type 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 , 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.
Type u; finitely presented groups are countable, so this loses nothing.Finite (cw.cell n) for every , , and a contractible covering space; no finite-dimensionality is required.Group.IsFinitelyPresented group, not a chosen list of presentations.The statement cannot be met trivially: a trivial or finite cannot contain all finitely presented groups, and the type requirement is substantive.
Needed infrastructure: CW complexes of finite type, spaces, HNN extensions, Higman's embedding theorem. Contributions toward Theorem 5.1 (ascending-torus theorem) or Proposition 6.2 are welcome.
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 , i.e. one with a classifying space having finitely many cells in each dimension. Since type implies finite presentation, this implies the Boone–Higman conjecture.
A classifying space is a connected CW complex with fundamental group and contractible universal cover. has type if some has finite -skeleton and type if some has finitely many cells in each dimension. Type is finite generation and type is finite presentation. A group is simple if it is nontrivial and has no normal subgroups besides 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 with a CW structure of finite type (Topology.CWComplex.FiniteType), a basepoint with , and a surjective covering map from a contractible space.
Every finitely generated group with decidable word problem admits an injective homomorphism into a nontrivial simple group of type .
The input need not be finitely presented and its word-problem algorithm may have arbitrary running time; the classifying space of may be infinite-dimensional.
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 .
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).
Finite presentation already fails to pass to subgroups; higher finiteness additionally requires controlling relations among relations in every dimension. Known families of simple 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 with stabilizers of type , built from an algebraic envelope whose Steinberg-group kernel must be annihilated exactly (Theorem 4.6).
Type u; carries [Group.FG G].IsSimpleGroup H together with Nontrivial H encodes simplicity.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 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.
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.
A group is finitely generated if some finite tuple generates it. A word is a finite list of letters ; has decidable word problem if for some finite generating tuple the set of words evaluating to 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 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 .
For every finitely generated 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.
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.
Finite presentation does not pass to subgroups, so Boone and Higman's simple group and finitely presented group 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.
GroupType : Type u with [Group GroupType] [Group.FG GroupType]; the target group lives in the same universe.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.
Two numbers measure how "large" a discrete group is. The cohomological dimension is algebraic: the length of the shortest projective resolution of the trivial module over the group ring . The geometric dimension is topological: the least dimension of a CW complex with fundamental group and contractible universal cover (a classifying space or ). Cellular chains of a classifying space give a free resolution, so . Eilenberg and Ganea proved in 1957 that equality holds whenever , 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.
For a finite simplicial graph with vertex set , the right-angled Artin group is
and the height homomorphism sends every to . Its kernel is a Bestvina–Brady group.
The specific graph comes from the presentation complex of , which is integrally acyclic and has a nontrivial representation of its fundamental group into . Subdivide each of the two loops of 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 of ; is its 1-skeleton, i.e. the comparability graph of the cells. The group is .
A group is residually finite if every nontrivial element survives in some finite quotient.
For the group above,
In particular . 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.
The result itself. The theorem disproves the Eilenberg–Ganea conjecture with a finitely generated (indeed type , 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.
The kernel acts freely on an acyclic 2-complex, which gives , but an acyclic complex need not be contractible, and showing that one particular 2-dimensional model fails to be a 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.
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 in Multiplicative ℤ, and SourceGroup is its kernel.cohomologicalDimension is the categorical projective dimension (in WithBot ℕ∞) of the trivial -module in ModuleCat.HasClassifyingSpace G n asks for a Hausdorff, path-connected CW complex with no cells above dimension , fundamental group isomorphic to , 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.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 , 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 , does it act geometrically on hyperbolic three-space ? 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.
The source of this mission, an OpenAI preprint dated September 23, 2026, follows the analytic route and proves the conjecture.
Let be a group with a finite symmetric generating set and Cayley graph with graph distance . is hyperbolic if there is such that every point on a side of a geodesic triangle lies within of the union of the other two sides. A geodesic ray based at is a sequence with ; two rays are equivalent if stays bounded. The boundary is the set of equivalence classes with the quotient of the topology of pointwise convergence.
is the upper half-space with distance , and is its full isometry group, including orientation-reversing isometries. A homomorphism gives a proper action if is finite for every compact , and a cocompact action if translates of one compact set cover .
The Lean statement OAI.CannonRelease.cannon is open on the platform.
The theorem identifies hyperbolic groups with 2-sphere boundary, up to finite kernels, with uniform lattices in . For torsion-free , the quotient 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.
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.
CayleyData G is a finite symmetric generating set with connected SimpleGraph.mulCayley; ThinTriangles asks for one natural number working for all geodesic triangles given as walks of length equal to graph distance.ℕ → G with r 0 = 1 and dist (r i) (r j) = |i-j|; the boundary is the quotient by bounded synchronous distance. carries the discrete topology, rays the subspace product topology, and the boundary the quotient topology, which coincides with the visual topology for hyperbolic groups.EuclideanSpace ℝ (Fin 3); is the upper half-space with the explicit arcosh distance and subspace topology; isometries are self-homeomorphisms preserving that distance.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 ) or Theorem 2.5 (the uniformization criterion) are welcome.
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 and ), axioms () 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.
A specification consists of a type of sorts, an axiom relation and a rule relation ; neither is assumed functional. Expressions are
up to renaming of bound variables. β-reduction is the compatible closure of , with steps allowed everywhere, including inside the annotation of a λ and both parts of a Π. Typing is generated by the seven standard PTS rules (axiom, variable, weakening, product, abstraction, application, conversion up to ). A context is valid if each declared type is typed by a sort in the preceding prefix, and is legal in if or for some .
The system is weakly (strongly) normalizing if every legal expression in every valid context is weakly (strongly) normalizing.
For every specification ,
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.
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.
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.
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.Beta.S is arbitrary (any universe), and axioms and rules are arbitrary relations: no functionality, finiteness or hierarchy assumptions.A logic for unordered finite structures (graphs, databases, relational inputs given up to isomorphism) must give answers that do not depend on how the input elements are named. Many polynomial-time algorithms nevertheless make arbitrary intermediate choices, for example the pivot in Gaussian elimination, without changing their final answer. Choiceless polynomial time with counting (CPT), introduced by Blass, Gurevich and Shelah (1999), forbids such choices entirely: it computes with hereditarily finite sets over the input elements and can count, but can never pick one element from a set merely because the set is nonempty.
Witnessed symmetric choice (WSC), in the form of Lichter and Schweitzer (2022, arXiv version 3), adds a controlled form of choice: the logic may pick an element of a set provided it also constructs automorphisms of the input showing that all elements of that set are interchangeable, so the answer cannot depend on which one was picked. Lichter and Schweitzer asked whether CPT + WSC is strictly more expressive than CPT. This mission concerns a proof that it is.
The source of this mission is an OpenAI preprint dated September 24, 2026; its companion preprint (September 23, 2026) proves that CPT does not capture polynomial time.
Let be a finite set of atoms and the hereditarily finite sets over . CPT terms are built from variables, , , , , (the member of a singleton, else ), (the von Neumann ordinal ), comprehensions and iteration from ; formulas use input relations, equality and Boolean connectives. A sentence pairs a closed formula with a polynomial that bounds the number of iteration steps and the hereditary size of all intermediate objects on inputs with atoms; exceeding the bounds yields a default or a failure value .
A WSC operator iterates a step term in which, at each stage, a choice term proposes a nonempty set ; one element is chosen, and a witness term must produce automorphisms of the entire input that fix the parameters and all earlier stages and map any element of to any other. If the witnesses are valid along every possible choice sequence, the output formula's value on the terminal state is returned; otherwise the value is .
The true-model class of a sentence is the set of finite structures on which it returns true; false and are both outside it.
For the fixed vocabulary of eight binary relations there is a CPT + WSC sentence with exactly one WSC occurrence such that
The Lean statement OAI.WitnessedChoice.main (via BGS.MainStatement) is open on the platform.
Since every CPT sentence is a CPT + WSC sentence, Theorem 1.1 gives a strict inclusion of definable Boolean queries and answers the expressiveness question posed by Lichter and Schweitzer in the true-model sense. The separation holds against CPT with counting and sets of arbitrary finite rank, not a rank-restricted fragment. It leaves open whether CPT + WSC captures polynomial time and the effect of nesting WSC operators.
The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists.
Two different tasks must be done. The upper bound requires a legal WSC definition on all inputs, not only on the intended grid structures: witnesses must be genuine automorphisms of the whole input fixing the full history, which the sentence must check, with a fallback when the input is not of the intended shape. The lower bound must defeat every CPT sentence, including those that build nested sets of large rank; rank-sensitive support arguments (Dawar–Richerby–Rossman) do not suffice. The paper uses a nonabelian automorphism group whose central subgroup has rank-independent small supports, then a counting equivalence and a bounded-width description of complete CPT evaluations.
Term n / Formula n with de Bruijn-style Fin n variables, including iterate and the wsc formula; wscCount counts WSC occurrences.Option (none is ). resource p n = ⌊p(n)⌋ bounds iteration length and transitive-closure size.GoodWSC) quantifies over all choice prefixes; witnesses are permutationGraph g for permutations g that are input automorphisms, fix the free parameters and every earlier stage, and act transitively on the choice set.FiniteInput packs any finite carrier type with the eight-symbol relations (Ed, Cf, EB, VB, I, Z δ, δ : ZMod 3). Sentence.isCPT means wscCount = 0.A complete development needs hereditarily finite sets with permutation actions, support and counting-equivalence theory, and the grid structures; much of this is shared with the companion CPT noncapture mission. Contributions formalizing Proposition 4.4 (a total all-input definition), Proposition 5.3 (transitivity for every parameter tree), Theorem 5.5 (opposite grid answers), Proposition 6.3 (small-orbit support bound), Theorem 8.1 (transfer through small supports) and Theorem 9.3 (eventual equality for every CPT sentence) are welcome.
Descriptive complexity asks whether complexity classes can be characterized by logics, without reference to machines. Immerman and Vardi (1982) showed that on ordered finite structures, first-order logic with a least fixed-point operator expresses exactly the polynomial-time queries. On unordered structures, such as graphs given only up to isomorphism, an algorithm must not depend on an arbitrary ordering of the input, and whether some logic captures polynomial time there is a central open question (Chandra–Harel 1982, Gurevich 1988).
Choiceless polynomial time with counting (CPT), introduced by Blass, Gurevich and Shelah (1999), was for decades the strongest candidate: it computes with hereditarily finite sets built over the input elements, can count, and is invariant under automorphisms by construction. Blass, Gurevich and Shelah conjectured that CPT is still a proper fragment of polynomial time. This mission concerns a proof of that conjecture.
The source of this mission is an OpenAI preprint dated September 23, 2026.
Fix the field and the vocabulary of eight binary relation symbols . For a finite -structure put
With unknowns and (separate families), the system consists of
for every such that some and satisfy and . The query says this system is consistent over . No promise is imposed on the input.
A CPT program is a fixed finite set of rules that updates dynamic functions whose values are hereditarily finite sets over the atoms of , using pairing, union, comprehension, equality, membership, the input relations, and the cardinality operation (which returns a von Neumann ordinal). A program defines if for fixed polynomials , on every input of size it halts within steps, touches at most hereditarily finite objects, and accepts exactly when holds. No bound on set rank is imposed.
The Lean statement OAI.CPTSeparation.main is the conjunction of these three clauses. It is open on the platform.
The theorem confirms the Blass–Gurevich–Shelah noncapture conjecture for the full counting formalism: CPT does not capture polynomial time on unordered structures. It removes the leading candidate logic from Gurevich's question, which itself remains open. Because is expressible in fixed-point logic with a solvability or rank operator over (Corollary 3, p. 3), it also shows that neither of those logics is contained in CPT. The lower bound holds for programs of arbitrary set rank, unlike the bounded-rank lower bounds of Dawar–Richerby–Rossman.
The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists.
The polynomial-time upper bound is Gaussian elimination. The obstacle is the lower bound against every CPT program, including those that build sets of unbounded rank. Bounded-variable counting games handle fixed-point logic with counting but do not by themselves control CPT, which is strictly stronger (it decides CFI queries over ordered base graphs). Rank-dependent support arguments give lower bounds only for each fixed rank. The paper needs support bounds independent of rank, for which it uses a nonabelian automorphism group acting on grid structures, then a counting equivalence for all supported objects, and finally a transfer to complete computations via an interpretation characterization of CPT.
Input A gives a Boolean-valued binary relation for each Symbol (Ed, Cf, EB, VB, I, Z δ with δ : ZMod 3). Input.query is the existence of λ, μ satisfying the normalization and consistency equations exactly as above; an empty system is consistent.OrdinaryPolynomialTime asks for a function on ordered tables and a Turing.TM2ComputableInPolyTime machine with finite alphabets computing it from the cell-by-cell table encoding, agreeing with the query for every ordering of every structure.FullCPT defines terms and rules over hereditarily finite sets (Lists quotient), a state of finitely many nonempty locations, synchronous consistent updates, halt/accept flags, and the set of occurring objects (active elements plus roots of evaluated terms). EvaluationDefinable Q asks for one program and polynomials time, space that accept exactly the inputs satisfying Q, halting within time and with at most space occurring objects.A complete development needs: hereditarily finite sets and automorphism actions on them, support theory, counting equivalence games, the grid structures with their automorphism group, and a CPT-to-interpretation translation. Contributions formalizing Proposition 2 (polynomial-time decidability), Proposition 8 (small-orbit support bound), Proposition 13 (quantitative homogeneity) and Theorem 14 (transfer through small supports) are welcome.
Turing reducibility compares sets of natural numbers by their information content: if an oracle Turing machine with oracle computes the characteristic function of . Identifying mutually reducible sets gives the Turing degrees , partially ordered by . A central question of computability theory since the 1970s is how much of the underlying computational structure the abstract order remembers. The strongest possible answer is rigidity: the order has no nontrivial automorphisms, so every degree is determined by its position in the order.
After these results the remaining problem was rigidity at degrees outside the known fixed cone. The source of this mission, an OpenAI preprint dated September 24, 2026, proves full rigidity.
An oracle is a function (a set of natural numbers). means that the characteristic function of is partial recursive relative to . This is a preorder; its quotient by is the set of Turing degrees, partially ordered by . An automorphism of is a bijection with
No definability, Borel or continuity hypothesis is imposed on .
The Lean statement OAI.TuringRigidity.ManuscriptMain.rigidity is open on the platform.
Rigidity says that the order alone determines every Turing degree. By the theorem of Slaman and Woodin, it is equivalent to their biinterpretability conjecture: the degrees are biinterpretable without parameters with full second-order arithmetic (Corollary 5.1). Consequently every relation on degrees that is definable in second-order arithmetic and invariant under Turing equivalence is definable in the degree order, which settles a family of definability questions at once.
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. Its proof relies on the Slaman–Woodin representation theorem, whose cited source is an unpublished 2005 manuscript; a formalization would either need to formalize that input as well or isolate it as an explicit hypothesis, and would make the dependence fully transparent.
Earlier methods fix cones of degrees: coding arguments work above a sufficiently high base such as , where enough information can be coded and decoded. Below that base the coding machinery is not available, and an arbitrary automorphism carries no a priori regularity. The proof must turn the arithmetic (hence Borel) representation of an automorphism into recovery of every individual real, using a category argument that works for every irrational parameter, not only generic ones.
ℕ → Bool; reducibility is Mathlib's TuringReducible between the characteristic functions viewed as partial functions ℕ →. ℕ (values and ).Degree is Antisymmetrization Oracle Reduces with the induced partial order; automorphisms are order isomorphisms Degree ≃o Degree, i.e. bijections preserving and reflecting .A complete development needs relativized computability (oracle machines, joins, the jump), Borel and Baire-category arguments on and , and the Slaman–Woodin representation theorem (Theorem 3.1). Formalizing that theorem would itself be a substantial and reusable contribution. Contributions formalizing Proposition 4.1 (recovery of an irrational from four values of a Borel subadditive map with countable fibers) are welcome.
A class of structures is categorical in a cardinal if it has exactly one model of size up to isomorphism. Morley's theorem (1965) says that a complete first-order theory in a countable language categorical in one uncountable cardinal is categorical in all of them. Abstract elementary classes (AECs), introduced by Shelah in the 1970s, axiomatize classes of structures with a well-behaved notion of strong substructure (closure under isomorphism, coherence, unions of chains, a Löwenheim–Skolem number) without requiring first-order axiomatizability; they cover classes defined in infinitary logics and many classes of modules. Shelah's categoricity conjecture for AECs, in its eventual form, asks whether categoricity in one sufficiently large cardinal transfers to all sufficiently large cardinals. A sharper, prescribed-threshold form names the threshold explicitly: with (the Hanf number for existence of arbitrarily large models), categoricity in some should imply categoricity in every . Deciding which form holds is a central question in non-elementary model theory.
Work with relational structures in a finitary relational language (a set of relation symbols, each with a finite arity). An abstract elementary class is a class of -structures with a relation ("strong substructure") such that: is a partial order on refining substructure; and are closed under isomorphism; coherence holds (, , imply ); unions of -chains are in , are -extensions of each member, and are -below any common strong extension (Tarski–Vaught chain axioms); and there is a Löwenheim–Skolem number , the least such that every subset of a model lies in some with .
is categorical in if it has a model of size and any two models of size are isomorphic. The beth numbers are , and suprema at limits. CH is .
Assume CH. There is a countable finitary relational language and an AEC in such that
has two nonisomorphic models of cardinality , and, with ,
Hence is a categoricity cardinal from which downward transfer to fails, while eventual categoricity holds for this . The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. Combined with Gödel's relative consistency of CH, the theorem shows that, if ZFC is consistent, the prescribed-threshold form of Shelah's categoricity conjecture is not provable in ZFC (Corollary 6.1 of the source). The example has no amalgamation or joint embedding, which explains why transfer theorems that assume these properties are unaffected, and it is compatible with qualitative eventual categoricity. It also bears directly on a published claim of transfer at the prescribed bound for arbitrary AECs.
Formalizing it. Because the result contradicts a claimed theorem in the literature, an independent machine check is especially valuable. The formal statement verifies every AEC axiom explicitly, not just the two cardinal-arithmetic conclusions. Mathlib has cardinal and ordinal arithmetic, beth numbers and ZFC sets; the AEC framework built here would be reusable for further formal work in non-elementary model theory.
Most known non-transfer examples (Hart–Shelah) fail categoricity at small cardinals; here the failure must happen exactly at the Hanf-type bound while categoricity holds on a tail, with . One must build two nonisomorphic models at and simultaneously rule out any two nonisomorphic models above , without appealing to a general eventual-categoricity theorem. All AEC axioms — in particular coherence and smoothness of unions of arbitrary directed chains — must survive the exceptional sets used to separate models, which is where naive constructions break.
RelModel L with carrier a ZFSet (so cardinalities are cardinals of genuine sets in universe u) and relations indexed by arity; Type with countable.ClassData packages a predicate of objects and a strong-substructure relation; IsAEC lists the axioms above, including invariance under isomorphisms compatible with inclusion, coherence, and the union axioms for chains indexed by any nonzero ordinal.HasLSNumber ℵ₀ asserts both that is a Löwenheim–Skolem bound and that it is the least one.hanf κ = beth (succ (2^κ)).ord, endpoint = beth (ω_2), tailThreshold = beth (succ (2^{ℵ₁})).ord. The equality endpoint = hanf ℵ₀ is part of the goal (it follows from CH).Categorical μ includes existence of a model of size ; TwoModels asks for two nonisomorphic models of the given size.The Thorp shuffle cuts a deck in half, pairs cards in corresponding positions, and lets an independent fair coin order each pair before the pairs are interleaved. On cards, removing the deterministic rotation of coordinates turns physical shuffles into one binary coordinate sweep: in each coordinate direction, in order, every pair of positions differing in that coordinate is independently swapped with probability . After one sweep each card is uniform, but the joint permutation retains dependence because cards share switches.
By finite-group Fourier analysis (Diaconis–Shahshahani 1981), fast mixing of the whole deck follows from a power saving for the sweep in every irreducible representation of . The source obtains this saving by first controlling a perturbed sweep, in which each line permutation is mostly uniform, conditionally on prescribed trajectories of some cards, and then transferring the estimate analytically to the binary sweep.
Positions are binary strings , (Lean: Slot d := Fin d → Bool). For a coordinate , a layer flips bit of a position according to a fair coin attached to the edge ; the binary sweep applies the layers for in order, with all coins independent (Lean: binarySweep, binaryLaw d its law on ). For an irreducible unitary representation of of dimension , the sweep operator is
Write for the law of independent sweeps and .
For the conditional estimate, an ordered product grid is with each a power of two in ; a sweep permutes the lines parallel to coordinate , then coordinate , and so on, each line independently with law . A family of prescribed trajectories (disjoint at every layer) is conditioned on; the remaining random bijection of the free slots has average in each irreducible , with line cost .
There are a power of two , an integer and such that for every grid, every feasible family , every and every irreducible ,
with , , , and .
There are absolute constants and such that for all and every irreducible unitary representation of of dimension ,
the sign representation is annihilated, ; and there is an absolute integer such that
The goal is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. Since one binary sweep is exactly physical shuffles, the goal gives physical shuffles for mixing from every starting deck, and the support obstruction (Proposition 1.2: shuffles reach at most permutations) gives the matching lower bound ; thus , improving Morris 2013. The power saving in every irreducible representation is a stronger, reusable statement: it controls any number of further sweeps and any function of the permutation through Fourier analysis.
Formalizing it. The goal is stated for explicit finite objects (coins, sweeps, Fourier operators on ), with existential constants only. A formal proof would certify optimal-order mixing for the Thorp sweep. The conditional estimate (Theorem 3.1) is formalized separately and is the natural intermediate milestone.
The obvious induction—split the coordinates and multiply child bounds—breaks because revealing card paths changes the conditional law of the line permutations, and the induction must be stable when more paths are revealed. The source handles this with the line cost , which records the exact cost of prescribing positions without replacement. A second obstacle is that the conditional estimate is only available for mostly-uniform lines ( small), while the Thorp sweep is the binary case ; for a fixed grid the sweep operator is a matrix polynomial in whose behavior at is not controlled by real-segment bounds alone. Representations of very small "level" (first appearing on few tracked cards) need a separate sparse estimate.
binary_sweep_contraction_and_mixing): three conjuncts. BinaryContractionTarget: and every irreducible representation of Equiv.Perm (Slot d) on EuclideanSpace ℂ (Fin D) preserving norms, the operator norm of is at most (real power). Sign: for every , . UniformSweepMixingTarget: , total variation of the -fold convolution power translated by from uniform is at most . Physical shuffles are not modelled; the statement is about sweeps.conditional_main): grids are Grid with coordinates of (); trajectories are Holes with disjointness at every layer and coordinate-respecting steps; feasibility means some line choices realize them; the residual bijection is identified with the stabilizer of the input holes via a fixed reference completion; representations are UnitaryIrrep of that stabilizer; the Schatten moment is ; .all_grid_moment is a parameter-explicit form of the same induction under numerical largeness hypotheses and a small-perturbation hypothesis, kept as a plain item.The Thorp shuffle is a simple card-shuffling rule: cut a deck of cards into two equal halves, pair cards in corresponding positions, and let an independent fair coin decide the order within each pair when the pairs are interleaved. It is a standard test case for mixing-time methods and a building block in small-domain enciphering schemes. For every individual card is uniform after shuffles, but the joint order of all cards is much harder to control. Determining whether shuffles suffice to make the full permutation close to uniform was a long-standing question.
Index the positions by binary strings (in Lean, Card d := Fin d → Bool). One physical shuffle sends
with independent fair bits (Lean: step d ξ = rotate * pairSwitch ξ). After physical shuffles the rotations cancel, and the result is a coordinate sweep: one random matching switch in each coordinate direction. Write for the law on of physical shuffles (Lean: law d t, the fraction of coin sequences producing a given permutation).
For a partition let be the Specht module (the irreducible representation of indexed by ), of dimension , and let be the average of the sweep in . For an operator , and traces are unnormalized. The regular trace of the -th power is
in which the trivial representation contributes exactly . Total variation is .
There is an absolute real such that for every (so )
and for every integer with and every initial deck ,
The constant is not specified; only its existence and uniformity in are asserted. The goal is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. Since one sweep is physical shuffles, the second clause shows that Thorp shuffles bring the full permutation within of uniform from every starting deck. A counting argument on coin strings (Proposition 5.1 of the source) shows that at least physical shuffles are needed, so this order is optimal, improving the bound of Morris 2013. The regular-trace bound is stronger than an operator-norm bound for each irreducible: it controls all singular values with their multiplicities, which is what yields polynomially small total-variation distance.
Formalizing it. The statement is fully finite and explicit: an existential over one real constant followed by inequalities for each . A formal proof would certify an optimal-order mixing bound for a widely studied shuffle. Specht modules, Schatten-type traces via continuous functional calculus, and the shuffle law are all defined in the mission's definition file and can be reused for related shuffling problems.
Single-card and few-card statistics mix after one sweep, but the full permutation involves all bits of information, and the coin choices of a sweep interact across coordinates. The natural route—bounding the operator norm of separately in each irreducible representation—does not suffice, because the regular trace weights each representation by its dimension , and the number of partitions grows like . A uniform power must work simultaneously for representations of tiny dimension (very long first row), intermediate dimension, and dimension close to , and splitting the coordinates into row and column groups produces two symmetry decompositions that do not commute.
Fin d → Bool; permutations are Equiv.Perm (Card d); partitions of are Young diagrams of cardinality (Shapes (2^d)).Q d μ is the average over all coin sequences of length of the representation of run d d.absoluteTrace A P is the real part of the trace of CFC.rpow (CFC.sqrt (A⋆A)) P, i.e. ; regularTrace multiplies by finrank.sweepDistance d v σ is total variation of the law of physical shuffles, right-translated by , from the uniform weight . The integer is converted with Int.toNat; since and , and no truncation occurs.Many random permutations are analysed through what they do to a few labels at a time: the joint positions of chosen cards in a shuffle, or the images of a list of inputs under a block cipher built from a shuffle. Such partial information does not by itself control the whole permutation. The uniform law on the alternating group already has uniform images on every set of at most labels, yet it is at total-variation distance from uniform on . Converting partial-permutation estimates into full-permutation estimates therefore needs an additional argument, and this is the bottleneck in recent work on the Thorp shuffle, where fixed fractions of the deck were known to randomize quickly (Czumaj–Vöcking 2014; Czumaj 2015) long before the full deck was.
Let be a finite set of labels and , acting as maps from initial labels to final positions. For , let be the block subgroup of permutations that fix every label outside . Two permutations have the same images on exactly when they lie in the same left coset , so a bound on the law of those images is a bound on coset masses.
For a nonnegative weight on and a unitary representation of on a finite-dimensional complex inner-product space , the Fourier transform is , with . The Hilbert–Schmidt norm is unnormalized, . For the symmetric degree constant is
where ranges over the degrees of the irreducible complex representations of .
Partition into nonempty blocks and put . Let on have total mass at most one and satisfy
Then for every and every irreducible unitary of degree ,
No restriction is placed on the block sizes or on multiplicities in the restriction of to . The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. Theorem 1.1 is a quantitative transfer principle: a single law whose complementary partial images are never much heavier than uniform has a power saving in every irreducible representation of . With and it gives , which is enough for the principal application in the source (Corollary 3.6, p. 9): if the images of a uniformly chosen set of labels are close to uniform in average total variation and the sign mean tends to zero, then the product of just two independent copies of the permutation converges to uniform. This is the step used by the companion Thorp-shuffle preprints to turn fixed-list estimates into full-deck mixing in shuffles. The statement concerns arbitrary laws on and does not depend on any shuffle.
Formalizing it. The theorem is a finite inequality with explicit constants, so it is a natural target for machine checking. A proof would certify the partial-to-full transfer used by the Thorp mixing arguments, and would require reusable infrastructure: isotypic decompositions of restrictions to products of subgroups, Schur averaging, Hilbert–Schmidt and operator norms of group-algebra elements, and uniform bounds on symmetric-group Witten zeta sums. None of this is formalized yet.
The natural approach decomposes restricted to into tensor products of irreducibles of the blocks and bounds on each piece. This fails when a block type occurs with large multiplicity: a dimension count that pays for every copy gives no decay in . The bound must count each irreducible type of a block subgroup once, regardless of multiplicity, and must hold uniformly over all block sizes, which is why the constant is a supremum over every symmetric group. The Hilbert–Schmidt bound is harder than the operator bound, because it must control the whole Fourier matrix rather than its action on one vector.
Fintype with decidable equality; blocks are M : Fin b → Set X, nonempty, pairwise disjoint and covering. The block subgroup is blockSubgroup (M i), the permutations fixing each point outside M i.LeftCosetCap f H B: for every , , with the index H.index.complexFourier ρ f; hsNormSq is ; the operator norm is that of the associated continuous linear map; is Module.finrank ℂ V and the exponent is a real power.Equiv.Perm (Fin m), and is symmetricDegreeConstant u, an sSup over . The supremum is finite for every ; a solver must prove this boundedness, since sSup of an unbounded real set would be .At its critical weight, a self-avoiding path on the honeycomb lattice can make long excursions without paying an exponential cost. A basic quantitative question is how much of its total weight reaches the far side of a strip of height . Physics heuristics (Nienhuis's Coulomb gas and the conjectured scaling limit with boundary exponent ) predict that this crossing mass decays like . Rigorous results so far showed only that it tends to zero, with a polynomial upper bound with a tiny exponent.
The OpenAI preprint behind this mission, dated September 26, 2026 (source), claims the predicted power with bounded-factor constants: the crossing mass is comparable to , and the first horizontal-displacement moment of paths returning to the starting side is comparable to (Theorem 1.1, p. 2). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Use the honeycomb lattice dual to the equilateral triangular tiling of side one, with one edge direction horizontal; its vertices are the triangles up i j and down i j, where indexes the horizontal band. Let be the strip of bands. A path starts in the triangle up 0 0 (just above bottom port ), visits distinct triangles, moves between adjacent ones, and stays in bands . Its length is the number of visited triangles and its critical weight is with . An arch ends at up k 0 with (bottom port ); a bridge ends at a down triangle of the top band. Put and
Write if for all with fixed constants .
For every all sums above are finite, and with constants independent of ,
and is nonincreasing in .
The result itself. It establishes the predicted crossing power with uniform multiplicative constants, not just a logarithmic exponent, improving the qualitative decay of Beaton et al. and the polynomial upper bound of Krachun and Panagiotis. It is an input for the bridge-length and spatial-exponent results of companion preprints. The exponent of concerns an unnormalized displacement moment summed over all lengths; the fixed-length displacement conjecture and the scaling limit are different questions.
Formalizing it. The proof combines an exact boundary identity of Duminil-Copin–Smirnov type, finite-strip transfer matrices with integrable local relations, a Pfaffian that makes the stationary vector polynomial, and a comparison of the resulting positive integral with Bures–Laguerre ensembles. A formal proof would include the honeycomb boundary identity, the core of the connective-constant proof, which is itself a natural formalization target. No machine-checked honeycomb walk result of this kind is known.
The boundary identity (Lemma 4.2, p. 15) does not determine the power: it only gives between orders and . The preprint's route computes the arch moment first, as one coefficient of a ratio of Pfaffians (Proposition 4.1, p. 13), converts it into a positive -fold integral with Bures-type interaction (Section 5), and estimates that integral uniformly in by comparison with Laguerre laws (Section 6). The crossing power then follows from monotonicity and . A degree bound on the polynomial vacuum (Lemma 3.2, p. 10) is essential, because it turns interpolation into an identity argument.
ℤ × ℕ × Bool (column, band, up/down); adjacency joins an up triangle to the down triangles sharing an edge. Paths are Lists with Nodup, IsChain adjacent, head up 0 0, a prescribed last triangle, and all bands < N.rho ^ p.length on paths satisfying IsPath, and 0 otherwise; all masses are tsums over lists. The goal includes summability of each family, so the tsums are genuine sums.moment N = ∑' k : ℕ, (k+1) * K N (k+1), i.e. .Comparable f g asks for constants with for every ; powers are real rpow.Reusable contributions: the honeycomb boundary (parafermionic) identity in finite domains, and summability of critical walk weights in strips.
A random configuration on the vertices of a graph is a factor of IID if it can be produced by a measurable rule from independent uniform labels at the vertices, where the rule commutes with the graph's automorphisms. On trees this notion connects ergodic theory (which invariant processes are "Bernoulli-like"), local algorithms on sparse random graphs (factors of IID are limits of what local algorithms can produce), and statistical mechanics. The free Ising state on the -regular tree is the basic test case. It is easy to sample from a chosen root by broadcasting spins outward, but a factor rule may not use a root. Lyons asked for which inverse temperatures it is a factor of IID (Lyons 2017), and Nam, Sly and Zhang conjectured the answer after proving it for large below a non-explicit constant (Nam–Sly–Zhang 2022).
This mission asks for a formal proof of the exact threshold, including equality, as stated in an OpenAI preprint dated September 26, 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.
Let be the infinite -regular tree with vertex set ; concretely, is the set of finite words over with no two equal consecutive letters, and is adjacent to . Put for . The free zero-field Ising law on is determined by its marginals on finite connected subtrees :
Equivalently, a fair spin at one vertex is broadcast along edges, each child agreeing with its parent with probability . A spin law is a factor of IID if it is the law of for i.i.d. uniform labels and a measurable such that, for each fixed automorphism , almost surely, where .
For every integer and every ,
The result itself. It answers the ferromagnetic case of Lyons's question and proves the Nam–Sly–Zhang conjecture for every . The threshold coincides with the reconstruction (extremality) threshold of the free state, and the result holds at equality, where non-reconstruction alone gives no factor rule (a weak limit of factors need not be a factor). The preprint also shows that, in this range, the factor can be chosen to commute with every automorphism on every input (Lemma 8.5, p. 46). The converse direction ( excludes a factor) is known from Sly's obstruction via the Backhausz–Szegedy–Virág bound and is reproved on p. 2.
Formalizing it. The preprint's construction uses Brownian observation processes, stochastic localization, innovation equations of nonlinear filtering, and conditional-copy coupling arguments. Mathlib has Brownian motion only in early form and no stochastic calculus for infinitely many coupled SDEs; a formal proof would build reusable stochastic-analysis infrastructure. The converse needs the BSV correlation bound for factors of IID. No machine-checked factor-of-IID result for a non-trivial Gibbs measure is known.
Rooted sampling is easy; the obstacle is to remove the root while keeping the output a measurable function of the labels. Finite-cluster constructions only work in the uniqueness range . The Nam–Sly–Zhang approach observes and expresses the posterior through innovations , which are independent Brownian motions; but being Brownian does not make a function of , and that is the central step (pp. 2–3). At criticality the field-response sums in the innovation equation are only borderline integrable near time zero, so infinite sums must be justified with an exact covariance-energy identity rather than with a contraction estimate (Section 1.2, p. 3).
TreeVertex d is the set of words in Fin d with distinct consecutive letters, treeAdj appends or removes one letter, and TreeAut d is the group of adjacency-preserving bijections.Measure.infinitePi of Lebesgue measure on ; spins take values in a two-element type with the discrete σ-algebra, and configurations carry the product σ-algebra.HasFreeIsingLaw θ μ prescribes on every cylinder over a finite connected Finset by the product formula above; these cylinders determine the law.IsFactorOfIID d θ asks for a measurable Phi with pushforward law HasFreeIsingLaw θ and, for each automorphism g, Phi (relabel g U) = relabel g (Phi U) for almost every U (null set may depend on g), matching (1.1).θ = Real.tanh β with and ; at both sides hold trivially (i.i.d. spins), which is consistent with the source. The stronger everywhere-equivariant version is not part of the goal.