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.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
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?
A model structure on a category specifies weak equivalences, fibrations and cofibrations so that the category carries a homotopy theory. Thomason showed that the category of small categories carries a model structure Quillen equivalent to simplicial sets, so that ordinary categories model all homotopy types of spaces (Thomason 1980). Its weak equivalences are the functors whose nerves are weak homotopy equivalences.
Strict higher categories have a nerve too: Street's orientals give the Street nerve of a strict -category (Street 1987). The higher-dimensional Thomason model-structure conjecture of Ara and Maltsiniotis asks for the analogue of Thomason's theorem for strict globular -categories for every (Ara–Maltsiniotis 2014; Ara 2023, §§9.2.5–9.2.6; Guetta–Maltsiniotis 2024). Strict higher categories are already known to describe the homotopy category of spaces after localization (Gagna, below); the conjecture asks for the full model structure, with lifting and factorization on all strict -categories.
This mission asks for a machine-checked proof of Theorem 1.1 of an OpenAI preprint dated September 25, 2026 (source), which claims the conjecture in every dimension. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
A strict globular -category has a set of cells, source and target operations in each dimension, and associative, unital compositions along -dimensional boundaries satisfying the interchange law; every cell has finite dimension. A strict -category is one whose cells above dimension are identities; denotes the category of small strict -categories and strict functors ( means ). No invertibility is assumed.
The Street nerve has , with left adjoint . With barycentric subdivision set
Let and be the weak homotopy equivalences and Kan fibrations, and . Define
: a functor of strict -categories is a weak equivalence exactly when its Street nerve is a weak homotopy equivalence. This follows from being a natural weak equivalence.
For every , is a proper combinatorial model structure on , cofibrantly generated by , and
is a Quillen equivalence.
The result itself. The theorem says that strict higher categories, in every dimension, model the homotopy theory of spaces through a genuine model structure, not only after localization. It provides functorial factorizations and lifting on arbitrary strict -categories, including those that are not freely generated, which is what the small-object argument needs. The key new input is a couniversality theorem: pushouts of along sieves with a right adjoint retraction are Street weak equivalences (Theorem 5.2, p. 18), which is the remaining sufficient condition of Ara–Maltsiniotis.
Formalizing it. Mathlib has simplicial sets and model-category foundations but no strict -categories, orientals or Street nerve. A complete development adds these, Steiner's directed complexes, Gray cylinders and local presentability of , all reusable in higher category theory.
The transfer theorem reduces the model structure to a pushout condition, and that is the hard part: categorical pushouts of strict -categories can create many new composites, so the nerve of a pushout is not the pushout of nerves. Thomason controlled this in dimension 1 with Dwyer maps, but that method does not extend directly. The preprint builds explicit stationary directed prisms (Lemma 3.1, p. 10) that are constant on the old part, so contractions glue across any attachment, and then reduces general posets to finite ones via sieve covers (Corollary 4.5, p. 16; Lemma 4.6, p. 17). Properness (Proposition 7.3, p. 26) and the unit comparison after two subdivisions (Proposition 7.4, p. 27) are separate arguments.
OmegaCategory is a structure with a type of cells, source/target maps indexed by ℕ, partial compositions, the globular, unit, associativity and interchange laws, and finite dimension of each cell. Finite uses a full subcategory NCategory n.FullMain asserts: the Kan–Quillen model structure on SSet exists with the standard classes; and, for and every finite , an ExactModelEndpoint for : a ModelCategory whose weak equivalences, fibrations and cofibrations are exactly ; and ; both weak factorization systems; completeness, cocompleteness and local presentability; left and right properness; left Quillen; and the Quillen-equivalence criterion at fibrant targets.n : ℕ, including , which the source does not consider; the identity holds there by the same argument.Free probability treats bounded self-adjoint operators in a tracial von Neumann algebra as noncommuting random variables, and the free analogue of independence is freeness. Voiculescu introduced two candidate analogues of Shannon entropy for such tuples. The microstates free entropy measures how large the set of matrix tuples imitating the joint moments of is (Voiculescu 1994). The nonmicrostates free entropy is built instead from free Fisher information, by integrating along the addition of free semicircular noise (Voiculescu 1998). The two agree for a single variable, and whether they agree in general is part of Voiculescu's unification problem (Voiculescu 2002, Sections 3.5 and 3.8). Guionnet stated the finite-entropy formulation explicitly: does imply ? (Guionnet 2004, Conjecture 7.1).
The question matters because carries the strongest structural consequences for von Neumann algebras (it is the tool behind results such as Ge's theorem that free group factors are prime, Ge 1996), while is far more computable. Equality would let analytic computations of transfer to .
This mission asks for a machine-checked proof of Theorem 1.1 of an OpenAI preprint dated September 25, 2026 (source), which claims a tuple with . The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.
Let be a von Neumann algebra with a faithful normal tracial state , and a tuple of self-adjoint elements of .
Microstates. For , , and a matrix size , let be the set of -tuples of self-adjoint complex matrices with operator norms at most whose normalized traces of all words of length are within of the corresponding -moments of . Volume is Lebesgue measure for the unnormalized Hilbert–Schmidt inner product. Then
Free Fisher information. Vectors in the -closure of polynomials in are conjugate variables if for every noncommutative polynomial , where is the free difference quotient. Then , or if no conjugate variables exist.
Nonmicrostates entropy. With a standard free semicircular family free from ,
There exist and a bounded self-adjoint tuple in a von Neumann algebra with faithful normal tracial state such that
The Lean goal OAI.FiniteEntropySeparation.main asserts exactly this, with the semicircular family required to lie in the same algebra.
The result itself. The theorem answers the finite-entropy equality question negatively: finiteness of does not force , so the matrix-approximation and Fisher-information definitions are genuinely different invariants even in the finite regime. Known equality results therefore cannot be extended by finiteness alone; any equality theorem must use structure such as convexity of a potential. The preprint notes that it does not settle the question for each fixed small number of variables.
Formalizing it. No formal definitions of free entropy, free Fisher information or free semicircular systems are known to exist in a proof assistant. A complete development would formalize both entropies, the comparison in the form needed, Gaussian asymptotic freeness, cumulant calculus and matrix-volume estimates, all reusable across free probability.
Both entropies are hard to compute for any non-free tuple, and the gap must survive two limits that interact badly: the over matrix size in and the integral over noise time in . The preprint's tuple couples free semicirculars with a commuting discrete variable that creates spectral blocks; after perturbing by small semicircular noise, is finite (Lemma 4.2, p. 9). The analytic side needs a Fisher-information bound in terms of higher cumulants (Proposition 3.2, p. 6), which makes nearly Gaussian at a suitable noise scale, while the matrix side must show that microstates, after GUE evolution, retain detectable block structure that independent GUE matrices of the same variances lack (Lemma 6.1, p. 12). Matching the two requires a finite-time entropy-production comparison along one fixed sequence of matrix laws (Lemma 5.1, p. 10); a naive application of loses exactly the deficit being sought.
VonNeumannAlgebra H on a complex Hilbert space ; the trace is a vector state given by a unit vector that is tracial on and separating for (so the state is faithful and normal).Fin n-indexed self-adjoint elements of . FreeStandardNoise requires each to have the semicircle moments (Catalan numbers) and the unital algebras generated by and by each to be free.ℝ≥0∞, equal to when no conjugate system exists.EReal built from the positive and negative parts of the integrand as lower Lebesgue integrals over .EReal logarithms (volume zero gives ).The classification programme for simple nuclear -algebras identifies a class of algebras that are determined by K-theory and traces. Membership in that class is governed by regularity properties: finite nuclear dimension, absorption of the Jiang–Su algebra , and strict comparison. Uniform property , introduced by Castillejos, Evington, Tikuisis, White and Winter, is a central divisibility condition: it asks for projections in a central sequence algebra that cut every trace exactly in half, uniformly across the whole trace space, while preserving trace values against fixed coefficients. Together with strict comparison it is equivalent to -stability for simple separable unital nuclear algebras (Castillejos–Evington–Tikuisis–White). Schafhauser, Tikuisis and White asked (Problem XXI of their problem list) whether real rank zero of the uniform tracial ultrapower of the tracial completion already forces uniform property .
The source of this mission is an OpenAI preprint dated September 23, 2026, which answers Problem XXI affirmatively (and, by separate arguments, also treats the unital Toms–Winter conjecture).
Let be a unital -algebra with nonempty set of tracial states. The uniform 2-seminorm is
The uniform tracial completion consists of bounded sequences in that are Cauchy for , modulo those tending to zero; each extends to a designated trace on . For a free ultrafilter on , the uniform tracial ultrapower is the algebra of bounded sequences in modulo those whose uniform 2-norm tends to zero along . Its limit traces are
and denotes the set of these. embeds in as constant sequences.
A unital -algebra has real rank zero if every self-adjoint element is a norm limit of self-adjoint elements with finite spectrum. is stably finite if every isometry in every matrix algebra over is unitary, and nuclear if its algebraic tensor product with any -algebra carries a unique -norm.
Let be unital, separable, simple, infinite-dimensional, nuclear and stably finite with , and let be a free ultrafilter. If has real rank zero, then there is a projection with
This is the halving formulation of uniform property used in Problem XXI. The Lean statement OAI.ComparatorModel.CurrentMain.main is open on the platform.
The theorem shows that real rank zero at the level of the tracial ultrapower is enough to produce uniform property , with no restriction on the trace space; the paper also deduces that every trace on is a designated extension (Corollary 1.2). Since uniform property plus strict comparison gives -stability, this links projection structure in tracial ultrapowers to the Toms–Winter regularity theory. The equivalence between the halving formulation and the usual all- formulation is due to Carrión et al.
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.
Real rank zero supplies many projections in , but nothing makes them central, and halving must hold simultaneously for every limit trace and every coefficient . Divisibility results derived from real rank zero (Vaccaro) give tracially large order-zero maps without centrality; uniform property needs commutation with all of and exact coefficient identities. Equality of the scalar traces alone is not enough. Nuclearity by itself does not suffice either, as Toms' AH example shows, so the real rank zero hypothesis must be used in an essential way.
TracialState A is a positive linear functional with and ; the order on is the order (StarOrderedRing).U, computed with the designated traces .TopologicallySimple, StablyFinite (via CStarMatrix), IsNuclear (subsingleton of -norms on algebraic tensor products, in a fixed universe) and RealRankZero (finite-spectrum self-adjoint approximation) are defined directly.UniformPropertyGammaAt A U asserts a star projection commuting with the image of and halving familyLimitTrace … s for every sequence of traces s : ℕ → TracialState A.MainClaim existentially packages five auxiliary Prop classes (quotient -norm, closure properties of null and Cauchy sequences, existence of ultralimits, and vanishing of limit traces on null sequences). They are true general facts that a proof must establish; they are not assumptions.A complete development needs ultrapowers and tracial completions of -algebras, nuclearity and completely positive approximation, and real rank zero; all of this is reusable for the other regularity missions of this family. Contributions formalizing Theorem 1.3 (finite-set central splitting) and Corollary 1.2 are welcome.
A quantum channel models how a physical system, used to carry information, is corrupted by its environment. The classical capacity of a channel is the largest rate, in bits per use, at which classical messages can be sent with vanishing error when the sender may encode into arbitrary — possibly entangled — states of many uses and the receiver may measure all outputs jointly. The Holevo–Schumacher–Westmoreland coding theorem (Holevo 1998; Schumacher–Westmoreland 1997) expresses this capacity as a regularized limit of the Holevo information over ever larger blocks of uses. Since Holevo information is not additive in general (Hastings 2009), computing the capacity of any specific channel requires a channel-specific additivity argument, and exact formulas are known only for a few families.
Generalized amplitude damping is the standard model of a qubit relaxing toward a thermal state: it loses or gains an excitation with probabilities set by a damping strength and a stationary excited population , and its coherences decay. It is one of the basic noise models of quantum information theory.
For the generalized amplitude-damping channel acts on a qubit density matrix by
and independent uses act as on matrices. With , the Holevo information in bits is
over all finite ensembles of input states (entangled across uses when ). The classical capacity is the supremum of rates for which there are -use codes — arbitrary input states for each of equiprobable messages and one joint measurement of all outputs — with average error tending to zero and ; there is no shared entanglement or feedback. Write for binary entropy in nats, and .
For all and every ,
the maximum is attained, , and for every maximizer the equiprobable independent products of the two signals attain at every block length. The goal is published on the platform with status Open.
The result itself. The theorem gives a closed one-variable formula for the classical capacity of every generalized amplitude-damping channel, removing the regularization over block lengths: entangled input signals across uses give no advantage, and a simple product code with two signals per use is optimal. This settles the ordinary amplitude-damping case listed as open by LKDW 2018 and extends beyond the pure-output criterion of Tang et al. to the thermal regime, where the channel has no pure output. The source further proves additivity of Holevo capacity, minimum output entropy and classical capacity when the channel is used in parallel with any finite-dimensional partner channel (Corollary 1.2); that corollary is not part of this goal.
Formalizing it. The goal ties together an operational capacity (codes and error probabilities), an entropic quantity (a supremum over unrestricted ensembles on -dimensional matrices), and a scalar optimization. A machine-checked proof would certify both the matrix entropy inequality at the heart of the argument and the converse direction of the coding theorem. Mathlib does not currently contain quantum channel capacity theory, so the definitions here are new infrastructure.
Optimizing a single use gives a lower bound on capacity; the difficulty is the matching upper bound for all simultaneously, where an input may be entangled across all uses. Holevo additivity is false for general channels, so no abstract argument applies, and for interior thermal occupation with the channel has no pure output, which rules out the recent pure-output criterion. The proof needs a lower bound on the entropy of the output of an arbitrary entangled block input, i.e. a matrix entropy inequality for block-structured states that is tight on product inputs. Identifying the capacity with the regularized Holevo quantity also requires the full coding theorem and a Fano-type converse.
Fin n → Fin 2; the -use channel is given by tensor products of the four standard Kraus operators of generalized amplitude damping, which reproduce the displayed action exactly.Tr (cfc negMulLog P) (nats, ); Holevo values are divided by (bits). holevo γ ν n is the sSup over all finite ensembles of arbitrary -dimensional states, with no product or purity restriction.capacity is the sSup of operationally achievable rates: codes with any positive number of messages, arbitrary state encodings, an arbitrary POVM decoder, average error tending to , and the liminf rate condition. It is defined operationally, not by regularization, so the identity includes the coding theorem.Real.binEntropy (nats); the maximizer is over . The final clause also asserts that the phase-product signals are states.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).
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.
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.Thompson's group consists of the increasing piecewise linear homeomorphisms of with finitely many pieces, dyadic rational breakpoints, and slopes that are integer powers of . It is finitely presented, has strong topological finiteness properties, and appears across group theory, dynamics and logic. Whether is amenable, i.e. whether its bounded functions admit a translation-invariant mean, is one of the best-known open questions about a single explicit group. It is a natural test case because the two classical routes to deciding amenability both fail: contains no nonabelian free subgroup (Brin–Squier 1985), so the free-subgroup obstruction is unavailable, yet is not elementary amenable (Cannon–Floyd–Parry 1996, Theorem 4.10). Geoghegan conjectured in 1979 that is nonamenable. The problem has attracted claimed resolutions in both directions, several later withdrawn or found to contain errors.
This mission asks for a formal proof of nonamenability as stated in an OpenAI preprint dated September 23, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
A homeomorphism of is a dyadic PL map if there are dyadic rationals and integers such that on each , . The group is the set of increasing dyadic PL homeomorphisms of , with multiplication , regarded as a discrete group. Let be the bounded real functions on . A left-invariant mean is a linear functional with , whenever , and for every . is amenable if such a mean exists.
Thompson's group is not amenable: there is no positive, normalized, left-invariant mean on .
The result itself. It settles Geoghegan's conjecture and the amenability problem for . Because has no free subgroups, becomes a finitely presented, torsion-free example of a nonamenable group without free subgroups. Through companion results the preprint derives that has uniformly bounded representations that are not unitarizable (Corollary 3.1, p. 7) and that Bernoulli percolation on every Cayley graph of has a nonuniqueness phase (Corollary 3.2, p. 8). The proof is short (Section 2) and uses an infinite-dimensional fixed-point phenomenon: the Benyamini–Sternfeld theorem that the unit ball of an infinite-dimensional Hilbert space admits a Lipschitz self-map moving every point by at least a fixed (Lemma 1.2, p. 2; Proc. AMS 1983).
Formalizing it. Given the length of the published argument, this is a realistic target for a complete formal proof of a result that had been open for over forty years. It needs the dyadic-partition model of , the Følner criterion (forward direction), and a Lipschitz map on a Hilbert ball with no approximate fixed points (Appendix A of the preprint constructs one on with ). The Følner direction from invariant means to Følner sets is reusable infrastructure for amenability in Mathlib.
Neither standard obstruction applies: there is no free subgroup to produce a paradoxical decomposition, and no structural closure property shows amenability. Følner sets, if they existed, would have to grow extremely fast (Moore's tower bounds), so explicit counting is ineffective. The preprint's argument converts approximate invariance of a finite set into an approximate fixed point of a Lipschitz map on a Hilbert ball, via recursively defined Hilbert-valued colours of dyadic partitions. The delicate points are exact covariance of normalized restrictions under the group action (equation (2.2), p. 4) and controlling the diagonal and nested pairs in the correlation expansion, which yields a uniform lower bound on the relative boundary of every finite set (Proposition 2.3, p. 5).
UnitInterval is Set.Icc (0:ℝ) 1; an element of F is a homeomorphism of it that is StrictMono and has a DyadicPLWitness: finitely many strictly increasing dyadic knots from to and integer exponents with the affine formula on each piece.F exists whose multiplication is composition ((h * g) x = h (g x)); since multiplication is fixed, this structure is unique.InvariantMean F is a real-linear functional on lp (fun _ : F => ℝ) ∞ that is positive, sends the constant to , and is invariant under leftPull h, ; the goal is ¬ Nonempty (InvariantMean F).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.
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.
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.
Random 3-SAT, a conjunction of random three-literal clauses on variables, is the classic test case for the typical behavior of satisfiability. Experiments placed the hardest instances near the density where half the formulas are satisfiable, and statistical physics predicts a sharp satisfiability threshold near . Once a limiting threshold is known to exist, a natural question is whether it is a computable real: is there an algorithm that, given , outputs a rational within of ? Existence alone does not imply this, since limits of computable sequences need not be computable (Specker 1949). This mission asks for such an algorithm.
The source of this mission is an OpenAI preprint dated September 27, 2026. Its contribution is computability of , beyond existence.
For , a proper random 3-clause chooses three distinct variables uniformly from and gives each an independent fair sign. Let be the conjunction of independent such clauses (sampled with replacement from the possibilities; the empty formula is satisfiable) and
A real is computable if a single algorithm, on input , halts with a rational satisfying .
There is such that for every fixed real
and one finite deterministic Turing machine, on input , halts with a rational with , using no oracle, advice, or noncomputable constant. Lean: OAI.FixedClauseThreshold.Computability.main, open on the platform.
The theorem makes the random 3-SAT threshold an effectively approximable constant: in principle its digits can be certified, although no efficiency bound is obtained. The method produces two families of finite certificates, rational lower bounds from a deletion estimate and rational upper bounds from finite hierarchical approximations of a soft pressure, and a fair search over them halts without any computable rate of finite-size convergence. The paper also gives a self-contained existence proof of (Theorem 4.4) for the same proper-clause model.
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.
Finite-size satisfiability probabilities are computable, but their convergence rate is unknown, so truncating at a finite certifies nothing. Lower certificates need an explicit bound on how far the finite-size centers can lie above the limit. Upper certificates are harder: one must show that above some finite, checkable object witnesses unsatisfiability in the limit. This requires a variational (Parisi-type) description of the limiting pressure of the soft constraint model, approximated by finitely many rational parameters with a proof that the approximation is complete at every rational density above the threshold.
ProperClause n k is Fin n → Option Bool with exactly defined entries; Formula n k m := Fin m → ProperClause n k; properSATProbability n 3 m is the exact counting ratio, equal to .MainStatement asserts with the two strict-side limits at , a sequence q : ℕ → ℚ with Computable (fun r => encode (q r)), a Nat.Partrec.Code c with c.eval r = some (encode (q r)), and for all .Infrastructure: Mathlib's Computable/Nat.Partrec.Code, finite counting for random formulas, Poisson clause processes, interpolation bounds, and Ruelle cascades for the upper certificates. Formalizations of Lemma 2.1 (finite-certificate search, purely computability-theoretic and reusable), Theorem 4.4 and Theorem 8.4 are welcome.
Add random clauses one at a time to a Boolean formula on variables until it first becomes unsatisfiable. The index of that first failure is the satisfiability hitting time of random -SAT. Its mean, divided by , converges to the satisfiability threshold; its variance measures the width of the transition window. Friedgut's sharp-threshold theorem shows the window is , but quantitative widths have remained far from the scale suggested by lower bounds. This mission asks for the order of the variance of for every fixed .
The source of this mission is an OpenAI preprint dated September 27, 2026.
Fix and . A proper -clause is an OR of literals on distinct variables; let be independent uniform choices among the signed proper clauses (signs fair, whole clauses may repeat). Put
and, for fixed , the capped hitting time . Since each assignment survives a clause with probability , is a.s. finite with all moments. Write
There are constants with
and for every fixed a constant with ; if then also for large . Hence for . Lean: OAI.RandomKSAT.variance_main, open on the platform.
The killing-probability exponent in the lifetime bound (Proposition 2.3) cannot be decreased, and the block-error term in the replacement lemma cannot be improved to uniformly. Lean: OAI.RandomKSAT.sharpness.
For the theorem determines the variance of the hitting time up to constants, so the transition window has width in the variance sense, matching Wilson's lower bound and improving Carenini's variance bound. For it leaves only a logarithmic gap, closed in a companion OpenAI preprint. Chebyshev's inequality then gives concentration of about at scale .
The results are proved in an OpenAI preprint; they have not been peer reviewed, and no machine-checked proof exists.
The Efron–Stein inequality reduces the upper bound to the expected squared delay caused by deleting one clause, which counts pairs of prefixes at which that clause is pivotal. Controlling this occupation time requires a uniform estimate relating how quickly a set of assignments is killed by shorter -clauses to its lifetime under -clauses, valid for every assignment set with no lower cutoff. Earlier arguments truncate the number of clauses incident to the deleted clause's variables at a logarithmic level, which costs a logarithm; keeping that number as a random parameter without destroying independence is the main obstacle. Appendix A shows the relevant exponents are sharp.
Clause n k is a dependent pair of a -element Finset (Fin n) and a sign vector on it; clauseLaw is uniform; streamLaw is the infinite product (Measure.infinitePi).firstFailure ω is the least with an unsatisfiable prefix, valued in ℕ∞; H = (firstFailure ω).toNat; T B ω = (min (firstFailure ω) ⌊Bn⌋).toNat. The infinite case has probability zero.variance is ProbabilityTheory.variance under streamLaw n k; ell, U are as displayed.blockKill u s S g is the probability that independent proper -clauses kill , and lifetime u k S is .Infrastructure: product measures on clause streams, Efron–Stein, conditioning on incidence patterns. Formalizations of Proposition 2.3 (lifetime from shorter-clause killing), Proposition 4.3 (conditional squared delay), Corollary 5.2 and Proposition 6.2 (linear variance lower bound) are welcome.
A random -SAT formula on Boolean variables is a conjunction of independent random clauses, each an OR of literals on distinct variables. As the clause density grows, the formula changes from almost surely satisfiable to almost surely unsatisfiable. Random -SAT is a central model in probabilistic combinatorics, the theory of algorithms and statistical physics: its threshold is where hard instances are expected to concentrate, and it is a proving ground for methods from spin-glass theory. The satisfiability conjecture, formulated explicitly by Chvátal and Reed, asserts that for each fixed the transition happens at a limiting density that does not drift with .
The source of this mission is an OpenAI preprint dated September 25, 2026, which gives an alternative proof of the existence of the limiting threshold.
Fix . For , a proper -clause chooses distinct variables among uniformly and gives each an independent fair sign, so each of the clauses is equally likely. Let be independent such clauses (sampled with replacement: two positions may hold the same clause) and
The ratio is the clause density.
For every fixed integer there is such that
No assertion is made at , and the value of is not identified. Lean: OAI.FixedClauseThreshold.main, open on the platform.
The theorem settles, for every fixed , the existence half of the threshold question: Friedgut's sharp transition happens at a location that converges. Previously this was known only for large (Ding–Sly–Sun) and for . Existence is a prerequisite for questions about the value of , its computability, and the fluctuations of the satisfiability hitting time, which companion OpenAI preprints address. The proof here proceeds through concentration of a capped last satisfiable index and a comparison between system sizes; it does not rely on Carenini's window.
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.
A sharp-threshold theorem gives a narrow window at each but no control of how the window's center moves with . Convergence needs a comparison between different system sizes, and interpolation methods from spin-glass theory deliver free-energy bounds, not hard satisfiability statements, and often only for even arity. The center must also be shown to concentrate polynomially, which requires bounding how many variables are forced along the clause process.
ProperClause n k is a function Fin n → Option Bool with exactly defined entries; some b at is the literal satisfied when .Formula n k m := Fin m → ProperClause n k (ordered, with replacement); properSATProbability n k m is the exact ratio of satisfiable formulas to all formulas, which equals under the uniform product law.HasLimitingThreshold k asserts with limits for and for at .Infrastructure: finite counting of formulas, Efron–Stein-type variance bounds, a deterministic concentration-to-convergence lemma (Theorem 5.1), and the Poisson/interpolation comparison with the transfer back to proper clauses. Formalizations of Proposition 2.2 (integrated forcing), Proposition 3.3 (polynomial concentration) and Theorem 5.1 are welcome.