Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Bose–Einstein condensation (BEC) means that a single one-particle state carries a macroscopic fraction of a many-boson system. It was predicted for the ideal gas by Bose and Einstein (1924–1925) and is observed in dilute atomic gases, but for interacting particles in the thermodynamic limit there was no rigorous proof, even in the ground state. The Penrose–Onsager criterion (Phys. Rev. 1956) identifies condensation with a macroscopic eigenvalue of the one-particle density matrix. Energy asymptotics of the dilute gas are now known to second order, but they do not determine single-orbital occupation, since the one-particle spectral gap closes as the volume grows. Lieb and Yngvason explicitly separated the condensation question from their energy theorem, and Solovej's 2025 survey lists fixed-density ground-state condensation as a major problem in the field (C. R. Physique 2025, Section 5).
This mission asks for a formal proof of ground-state condensation for the dilute three-dimensional hard-sphere Bose gas, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Let be the flat torus with torus distance . For particles and exclusion distance , the allowed configurations are
The hard-sphere Hamiltonian is the operator of the Dirichlet form on restricted to symmetric (bosonic) functions; wave functions vanish on forbidden configurations, and is the scattering length. A ground vector is a normalized bosonic minimizer of . For a normalized bosonic , the condensate fraction in the constant orbital is
and for a density operator it is defined by linearity. The gas parameter is with the density.
There are absolute constants such that, for all with and every sequence , with :
The constant does not depend on the gas parameter in this range.
The result itself. It is a proof of macroscopic condensation in an interacting continuum Bose gas with fixed density and fixed hard core, in the thermodynamic limit, uniformly over all ground states including degenerate ground spaces. Previous rigorous results let the gas parameter tend to zero with the volume, or concerned traps, scaling limits, or positive-temperature settings with different potentials. The theorem gives a positive fraction only; it does not reach the Lee–Huang–Yang depletion law.
Formalizing it. The statement involves Sobolev spaces with Dirichlet conditions on a configuration space of the torus, bosonic symmetry, density operators, and partial traces, none of which are packaged in Mathlib; the Lean development builds them concretely. The proof uses killed Brownian motion, percolation-type path constructions, and second-moment arguments. No machine-checked statement of BEC for an interacting system is known.
Energy estimates alone cannot detect occupation of the constant orbital, because the cost of moving particles out of it is of order per particle and vanishes in the limit. One must show directly that a typical ground state correlates distant parts of the box. The preprint compares a tagged particle's position in distant cells by moving trajectories along random lattice routes; multiplying local comparison costs along a route loses a factor at every step, so instead it averages over random routes and bounds the second moment of the averaged likelihood, where exact cancellation of normalizers leaves a cost depending only on mutual encounters of two routes (Introduction, pp. 4–5; Section 8). A separate phase argument passes from to complex (Lemma 2.3, p. 9).
Fin N → Fin 3 → AddCircle L; the allowed set uses the Euclidean torus distance with strict inequality a < dist.dirichletDomain is the closure, in , of jets of smooth compactly supported test functions with support in the allowed set; energy is the sum of squared norms of the partial derivatives. IsGroundVector means: in the domain, bosonic (a.e. permutation invariant), normalized, and of minimal energy among such vectors.occupation is exactly ; mixedOccupation T is the trace of compressed by the bounded map . GroundSupported T says every unit vector in is (the first component of) a ground vector.Lieb–Thirring inequalities bound the negative eigenvalues of a Schrödinger operator by an integral of the potential. Lieb and Thirring introduced them in 1975 to give a short proof of the stability of matter, and they remain basic tools in mathematical physics, spectral theory and the analysis of many-fermion systems. The sharp constants are known only in a few cases. In one dimension, the Lieb–Thirring conjecture predicts the sharp constant for every exponent : for it should be the constant of the best potential with a single bound state, given by an explicit profile.
The source of this mission, an OpenAI preprint dated September 23, 2026, proves the conjectured sharp constant for every .
For , let be the self-adjoint operator of the quadratic form
For its negative spectrum is discrete; write with multiplicity, possibly a priori. The optimal constant is
is the same supremum with only the lowest eigenvalue retained, and the semiclassical constant is
For and every ,
the constant equals , and with equality holds for . The Lean statement OAI.SharpLiebThirring.sharp_lieb_thirring is open on the platform.
The theorem settles the one-dimensional Lieb–Thirring conjecture on the whole interval , extending the case of Read and Schulz: allowing many bound states never beats a single optimally shaped well. Combined with the known endpoint results ( and ), it completes the sharp one-dimensional constants. It also gives the corresponding bound for signed potentials (Corollary 7.3), and through the Laptev–Weidl lifting method one-dimensional sharp constants feed into higher-dimensional estimates.
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. A formal proof would certify a proof whose key step is a finite-interval action inequality established by a continuation and degree argument for matrix fields.
Single-state bounds and numerical evidence say nothing about potentials with many bound states, and the conjecture requires a bound uniform over all orthonormal families of eigenfunctions. Methods that work at (where the inequality is dual to a kinetic-energy bound for orthonormal families) do not directly apply at other exponents, since the moment is not linear in the density matrix. The proof must keep track of the individual eigenvalue scales.
H1 packages with a weak derivative in , tested against smooth compactly supported functions.negativeMoment γ W is the supremum, in , over all finite orthonormal families of such eigenfunctions of ; this counts multiplicity and does not presuppose finiteness. oneStateMoment retains one eigenfunction.Admissible γ W is a.e. and ; potentialMass is the lower Lebesgue integral of ; the optimal constants are suprema over admissible with positive mass.A complete development needs Sobolev space and form methods, the variational characterization of negative eigenvalues, Gamma-function identities for , the explicit eigenvalue computation, and the paper's action inequality. Contributions formalizing Theorem 2.1 (action inequality) and the equality computation for the potential are welcome.
Given a group , adjoin one new generator and impose one relation , where is a word in and elements of . Can the result collapse to the trivial group when is nontrivial? The Kervaire conjecture says no. It arose from Kervaire's 1965 characterization of high-dimensional knot groups, which involves groups normally generated by a single element, and it is one of the best-known problems about equations over groups: when does an equation with coefficients in have a solution in some group containing ?
The source of this mission, an OpenAI preprint dated September 24, 2026, proves unimodular coefficient injectivity for every group by a route through spectral phase and a fixed-space theorem for unitary matrices.
Let be a group, , and the free product. Let be the homomorphism that kills and sends to ; is the exponent sum of in . A word is unimodular if . Write for the normal closure of in . The coefficient map is the composite
Its injectivity is equivalent to solvability of over : there is an overgroup and with .
The Lean statement OAI.Kervaire.coefficient_injective is open on the platform.
Theorem 1.1 immediately gives the Kervaire conjecture (Corollary 1.2): if then for every , since for the quotient maps onto . It proves the unimodular case of the stronger Kervaire–Laudenbach conjecture with no hypothesis on : no torsion-freeness, residual finiteness, hyperlinearity or countability. The paper's companion work extends the method to nonsingular systems of equations (Howie's conjecture).
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. The statement is short and entirely algebraic, which makes it an attractive formalization target; Mathlib already provides free products and normal closures.
The classical Gerstenhaber–Rothaus argument solves the equation in a unitary group and needs to embed in (an ultraproduct of) unitary groups, which is not known for arbitrary groups. Torsion in blocks the diagrammatic and topological arguments that work in the torsion-free case. A proof for every group therefore needs a representation available for all groups (the left regular representation, with its faithful finite trace) together with an argument that does not rely on finite-dimensional approximation of .
Monoid.Coprod A (Multiplicative ℤ); the exponent sum is Multiplicative.toAdd (Monoid.Coprod.snd w).Unimodular w is exponentSum w = 1 ∨ exponentSum w = -1.Subgroup.normalClosure {w}, and coefficientMap w is the quotient map composed with Monoid.Coprod.inl.A complete development needs the group von Neumann algebra of (or at least its trace), the spectral phase of unitaries and its subadditivity, a degree computation on a compact manifold of unitaries with fixed -planes, and corner-labelled planar diagrams with Euler-characteristic estimates. Contributions formalizing Corollary 1.2 from Theorem 1.1, Lemma 2.1 (subadditivity of spectral phase) and Lemma 3.1 (fixed-space lemma) are welcome.
Geometric group theory studies finitely generated groups through their word metrics, which are well defined up to quasi-isometry. A basic question is which algebraic properties are quasi-isometry invariants: if a group "looks like" a group from far away, must share 's algebraic structure? Gromov's polynomial-growth theorem (1981) answers this for virtually nilpotent groups. The next natural class is the virtually polycyclic groups — groups with a finite-index subgroup admitting a finite subnormal series with cyclic factors — which are exactly, up to finite index, the lattices in connected simply connected solvable Lie groups. Eskin, Fisher and Whyte conjectured that this class is quasi-isometrically rigid, and the question had been settled only for special families such as and certain abelian-by-abelian groups.
For finitely generated groups with word metrics, a -quasi-isometry satisfies and has -dense image. For finitely generated groups this is equivalent to a coarse equivalence: maps , sending pairs at bounded distance (differences in a fixed finite set) to pairs at bounded distance, with and at bounded distance from the identities. A uniform lattice in a locally compact group is a discrete subgroup with for a compact ; a lattice is a discrete subgroup whose coset space carries an -invariant probability measure.
For the height theorem: a connected simply connected Lie group is real-triangulable if the adjoint representation of its Lie algebra is simultaneously upper triangular in some real basis, with diagonal characters . Put and ; the exponential height map is the homomorphism whose differential is the quotient map. is unimodular if its left Haar measure is right invariant.
Let be connected, simply connected, real-triangulable and unimodular, with a proper left-invariant metric and a norm on . There is a finite subgroup such that for all , there is with: every self quasi-isometry of has some with
If a finitely generated group is quasi-isometric to a lattice in a connected simply connected solvable Lie group, then a finite-index subgroup of is a uniform lattice in some (possibly different) connected simply connected solvable Lie group.
Let be finitely generated and virtually polycyclic and finitely generated. If is quasi-isometric to , then
The second clause is the classical lattice realization of virtually polycyclic groups (Dekimpe's theorem, used in the source's proof of Corollary 1.2), recorded in the same formal statement. All three statements are published on the platform with status Open: no machine-checked proofs exist yet.
The result itself. Virtual polycyclicity becomes a quasi-isometry invariant among finitely generated groups, extending Gromov's theorem from nilpotent to solvable lattices and resolving the Eskin–Fisher–Whyte conjecture in its lattice form, where the ambient Lie group may change. The bounded-height theorem is a rigidity statement for quasi-isometries of an entire class of solvable Lie groups: up to bounded error and a finite group of linear symmetries, every quasi-isometry preserves height. This is the kind of control that previously required case-by-case coarse differentiation.
Formalizing it. The proof combines Lie theory, measured couplings, reduced cohomology, volume growth, Gromov's theorem and finiteness/duality results for elementary amenable groups — a long chain in which a machine check would add real confidence. Basic objects (coarse equivalences of groups, polycyclic series, uniform lattices, Lie groups with exponential maps) are reusable across geometric group theory.
Quasi-isometries carry no algebraic structure and can be wild at bounded scales, so the comparison group cannot be assumed solvable or even amenable a priori. Shalom's argument yields only a nontrivial homomorphism to , not full structure. The geometric core is height rigidity: one must show that a quasi-isometry cannot mix "up" and "down" directions of different exponential rates, uniformly over all quasi-isometries with given constants, and with a bounded (not merely sublinear) error, which is exactly what the later group-theoretic deduction needs.
GroupCoarseEquivalence, with bornologous maps and errors in finite sets — equivalent to quasi-isometry of word metrics.SimplyConnectedSolvableLieModel (finite-dimensional charted Lie group, Hausdorff, second countable, simply connected, solvable). Uniform lattices are discrete subgroups with a compact fundamental cover; finite-covolume lattices carry an invariant probability measure on the coset space.TriangularAdjoint basis, is any normed space linearly isomorphic to the canonical quotient, and is characterized through an exponential map. The metric is any compatible proper left-invariant metric with linear chain bounds — a quasi-isometric generalization of the source's fixed left-invariant Riemannian metric. The finite group is chosen before .A representation of a group by bounded invertible operators on a Hilbert space is uniformly bounded if , and unitarizable if after a change of inner product it becomes unitary, i.e. some bounded invertible makes every unitary. Unitary representations are the ones harmonic analysis knows how to decompose, so it matters which groups have only unitarizable uniformly bounded representations. Day and Dixmier showed in 1950 that every amenable group (one with an invariant mean) has this property, and Dixmier asked whether the converse holds. Dixmier's unitarizability problem has driven work in operator algebras, -invariants and measured group theory for seven decades.
The source of this mission, an OpenAI preprint dated September 23, 2026, answers Dixmier's question affirmatively for all discrete groups.
Let be a discrete group. is amenable if there is a linear functional on the bounded functions with , for , and , where .
A representation is a homomorphism into bounded operators on a complex Hilbert space (each is then invertible). It is similar to a unitary representation if there is a bounded invertible with unitary for every . is unitarizable if every uniformly bounded representation on every complex Hilbert space is similar to a unitary representation; the similarity may depend on the representation.
Every countable nonamenable has a representation on a separable Hilbert space with that is not similar to a unitary representation.
and for nonamenable and every there is with not similar to a unitary representation, on a separable space when is countable. The Lean statement OAI.Dixmier.current_main_theorem is open on the platform.
Theorem 1.1 characterizes amenability of discrete groups by a purely Hilbert-space property, without any quantitative bound on similarities, and shows that nonunitarizable representations can be chosen with uniform bound arbitrarily close to . Earlier results produced witnesses for groups with free subgroups, for residually finite groups with positive -Betti number, or for wreath-product extensions of ; the theorem gives a witness for every nonamenable itself. The paper also derives a consequence for group C-algebras using a companion similarity result.
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. The amenable direction (Day–Dixmier averaging) is classical and a natural first formalization step; the converse needs the paper's new operator construction.
A witness must be one representation for which no similarity exists, with no a priori control of the condition number of a putative unitarizer; quantitative criteria such as Pisier's do not apply. Nonamenable groups need not contain free subgroups and need not be residually finite, so the earlier free-group, random-forest and -Betti routes do not cover them. The paper builds bounded operator cocycles with no bounded implementer, which requires operators whose conjugation differences under translation are uniformly bounded while their distance from the translation commutant tends to infinity.
G with the discrete topology, using G →ᵇ ℂ for ; positivity is required on functions with nonnegative real values.G →* (H →L[ℂ] H) with [InnerProductSpace ℂ H] [CompleteSpace H]; SimilarToUnitary π asks for S : H ≃L[ℂ] H with for all .max u v, and the witness is built there; since the theorem holds for every v, this covers all Hilbert spaces.G, as in the paper.A complete development needs bounded operator cocycles and triangular representations, Hilbert direct sums, Hilbert–Schmidt estimates, Følner's criterion, induction of representations from subgroups, and invariant means. Contributions formalizing the Day–Dixmier direction, Proposition 2.2 (direct-sum obstruction) and Lemma 5.1 (induction from a subgroup) are welcome.
Higman's embedding theorem (1961) says that a finitely generated group embeds in a finitely presented group exactly when it is recursively presented, i.e. has a presentation with finitely many generators and a recursively enumerable set of relators. A consequence is that there is a single universal finitely presented group containing every finitely presented group. A natural higher-dimensional question asks whether finiteness can be pushed beyond presentations: finite presentability is the dimension-two case of the topological finiteness properties .
This preprint constructs a single group of type , i.e. with a classifying space having finitely many cells in every dimension, that contains every finitely presented group. This answers the form of the higher-dimensional Higman embedding question posed by Fournier-Facio and Zaremsky.
A classifying complex for a group is a connected CW complex with fundamental group isomorphic to and contractible universal cover; it may be infinite-dimensional. has type if some classifying complex has finite -skeleton, and type if some classifying complex has finitely many cells in every dimension. Type is equivalent to finite presentability. A group is finitely presented if it has a presentation with finitely many generators and relators.
In Lean (OAI.UniversalFInfinity), HasTypeFInfinity G asks for a Hausdorff connected space with a CW structure on Set.univ having finitely many -cells for every , a basepoint with , and a surjective covering map from a contractible space. Finite presentation is Mathlib's Group.IsFinitelyPresented.
There exists a group of type such that every finitely presented group admits an injective homomorphism into :
The result. Theorem 1.1 gives a universal group with the strongest standard topological finiteness property. Corollary 1.2 follows: the finitely generated subgroups of are exactly the finitely generated recursively presented groups. No word-problem hypothesis is imposed on the inputs, in contrast with the companion result on simple overgroups.
Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. A formalization requires finite-type CW complexes, classifying spaces and covering theory, Brown's criterion or a direct cell-count argument, Higman's universal finitely presented group, HNN extensions and an ascending-torus theorem (Theorem 5.1), none of which is fully in Mathlib.
Higman's universal group is only finitely presented; type requires finite control of relations among relations in every dimension, which is typically destroyed by the embeddings and amalgams used in Higman-type arguments. Fournier-Facio and Zaremsky show that the rope-trick construction fails , so a different route is needed. The preprint constructs a finitely presented envelope with two families of homomorphisms from the universal group and an ascending HNN-type mapping torus whose finiteness properties can be verified.
Type u; finitely presented groups are countable, so this loses nothing.Finite (cw.cell n) for every , , and a contractible covering space; no finite-dimensionality is required.Group.IsFinitelyPresented group, not a chosen list of presentations.The statement cannot be met trivially: a trivial or finite cannot contain all finitely presented groups, and the type requirement is substantive.
Needed infrastructure: CW complexes of finite type, spaces, HNN extensions, Higman's embedding theorem. Contributions toward Theorem 5.1 (ascending-torus theorem) or Proposition 6.2 are welcome.
A finitely generated group has decidable word problem if an algorithm decides, for every word in a fixed finite generating set and its inverses, whether it represents the identity. Embedding theorems translate this algorithmic property into algebra: Higman (1961) characterized subgroups of finitely presented groups, and Boone and Higman (1974) showed that decidable word problem is equivalent to embedding in a simple subgroup of a finitely presented group, asking whether the simple group can be finitely presented (the Boone–Higman conjecture).
This preprint proves a stronger statement in the direction of higher finiteness: every finitely generated group with decidable word problem embeds in a simple group of type , i.e. one with a classifying space having finitely many cells in each dimension. Since type implies finite presentation, this implies the Boone–Higman conjecture.
A classifying space is a connected CW complex with fundamental group and contractible universal cover. has type if some has finite -skeleton and type if some has finitely many cells in each dimension. Type is finite generation and type is finite presentation. A group is simple if it is nontrivial and has no normal subgroups besides and itself.
In Lean (OAI.SimpleFInftyOvergroups, definitions SimpleOvergroups), HasDecidableWordProblem G asks for a finite generating tuple with a ComputablePred identity predicate on words; HasTypeFInfty H asks for a Hausdorff connected space with a CW structure of finite type (Topology.CWComplex.FiniteType), a basepoint with , and a surjective covering map from a contractible space.
Every finitely generated group with decidable word problem admits an injective homomorphism into a nontrivial simple group of type .
The input need not be finitely presented and its word-problem algorithm may have arbitrary running time; the classifying space of may be infinite-dimensional.
The result. Theorem 1.1 answers the higher-finiteness strengthening of the Boone–Higman conjecture and implies the conjecture itself. With the classical converse (finitely presented simple groups have decidable word problem), it characterizes groups with decidable word problem as the finitely generated subgroups of simple groups of type .
Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. A formalization requires CW complexes of finite type, classifying spaces and covering theory (partially in Mathlib), Brown's homological finiteness criterion, Steinberg groups, and twisted Brin–Thompson groups with the Belk–Zaremsky finiteness theorem (Theorem 5.1 in the preprint, from the literature).
Finite presentation already fails to pass to subgroups; higher finiteness additionally requires controlling relations among relations in every dimension. Known families of simple groups contain large classes of groups but give no general construction from a word-problem algorithm. The proof needs an oligomorphic faithful action of a group of type with stabilizers of type , built from an algebraic envelope whose Steinberg-group kernel must be annihilated exactly (Theorem 4.6).
Type u; carries [Group.FG G].IsSimpleGroup H together with Nontrivial H encodes simplicity.ComputablePred on lists of (generator, sign) pairs for a specified generating tuple.The statement is not vacuous: the hypothesis holds for many groups (e.g. all finitely presented residually finite groups), and the conclusion requires a genuine embedding.
Needed infrastructure: finite-type CW complexes and spaces, Brown's criterion, group actions with finiteness properties, Steinberg groups over noncommutative algebras, and twisted Brin–Thompson groups. Contributions toward any of these are welcome.
The word problem for a group with a finite generating set asks whether a given word in the generators and their inverses represents the identity; it is decidable if one algorithm answers this for every word. Since Higman's embedding theorem (1961), a recurring theme in combinatorial group theory has been to characterize algorithmic properties of groups by embeddings into groups with good algebraic properties. Boone and Higman (1974) proved that a finitely generated group has decidable word problem if and only if it embeds in a simple subgroup of a finitely presented group, and asked whether the simple group can itself be taken finitely presented. This is the Boone–Higman conjecture.
This preprint states a proof of the conjecture: a finitely generated group has decidable word problem if and only if it embeds in a finitely presented simple group.
A group is finitely generated if some finite tuple generates it. A word is a finite list of letters ; has decidable word problem if for some finite generating tuple the set of words evaluating to is computable. A group is finitely presented if it has a presentation with finitely many generators and relations, and simple if it is nontrivial with no normal subgroups other than and itself. An embedding is an injective homomorphism.
In Lean (OAI.FiniteAlgebraicEnvelopes, definitions BooneHigman), words are List (Fin n × Bool), evalWord multiplies generators or their inverses, HasDecidableWordProblem G asserts a generating tuple whose identity predicate is ComputablePred, and EmbedsInFinitelyPresentedSimpleGroup G asserts a group in the same universe that is Group.IsFinitelyPresented and IsSimpleGroup, with an injective homomorphism from .
For every finitely generated group ,
The implication from right to left is classical (a finitely presented simple group has decidable word problem, and the property passes to finitely generated subgroups); the content is the forward implication.
The result. Theorem 1.1 gives a purely algebraic characterization of decidability of the word problem and settles a question open since 1974. Its intermediate result, Theorem 1.2, embeds every finitely generated group with decidable word problem in a finitely presented group with a faithful two-transitive action on a countably infinite set with finitely generated point stabilizers, which feeds Zaremsky's criterion for twisted Brin–Thompson groups.
Formalizing it. No machine-checked proof exists, and the source is an unrefereed preprint. Formalizing it requires computability of word problems, finite presentations (available in Mathlib as Group.IsFinitelyPresented), Steinberg groups over noncommutative rings, and twisted Brin–Thompson groups, which are not in Mathlib. The proof also uses Zaremsky's finite-presentation theorem (Theorem 2.3) from the literature, which a complete formalization must include.
Finite presentation does not pass to subgroups, so Boone and Higman's simple group and finitely presented group cannot simply be merged. Thompson's construction gives a finitely generated simple overgroup but provides no finite presentation. The new route needs a finitely presented group acting faithfully and two-transitively, built from a finitely presented algebra whose simplicity appears only after passing to a direct limit, and an exact calculation removing the kernel of the Steinberg group without assuming it is central.
GroupType : Type u with [Group GroupType] [Group.FG GroupType]; the target group lives in the same universe.ComputablePred on words over a specified finite generating tuple (Subgroup.closure (range generators) = ⊤); since the word problem's decidability is independent of the finite generating set, this matches the source.IsSimpleGroup includes nontriviality, matching the paper's convention.The statement is not trivially true: both directions are required for every finitely generated group, including infinitely presented ones.
Needed infrastructure: computable group presentations, Steinberg groups, mapping tori of endomorphisms, twisted Brin–Thompson groups and Zaremsky's criterion. Contributions toward the classical backward implication, or toward Theorem 1.2, are welcome.
Two numbers measure how "large" a discrete group is. The cohomological dimension is algebraic: the length of the shortest projective resolution of the trivial module over the group ring . The geometric dimension is topological: the least dimension of a CW complex with fundamental group and contractible universal cover (a classifying space or ). Cellular chains of a classifying space give a free resolution, so . Eilenberg and Ganea proved in 1957 that equality holds whenever , and Stallings and Swan settled dimension one. The remaining case — must a group of cohomological dimension two have a two-dimensional classifying space? — is the Eilenberg–Ganea conjecture, closely tied to Whitehead's asphericity conjecture in low-dimensional topology.
For a finite simplicial graph with vertex set , the right-angled Artin group is
and the height homomorphism sends every to . Its kernel is a Bestvina–Brady group.
The specific graph comes from the presentation complex of , which is integrally acyclic and has a nontrivial representation of its fundamental group into . Subdivide each of the two loops of into three edges, cone the boundary of each relator polygon to a new interior vertex (keeping one radial edge per boundary occurrence), and take the order complex of the resulting regular cell structure (7 vertices, 51 edges, 45 triangular sectors). This is a flag triangulation of ; is its 1-skeleton, i.e. the comparability graph of the cells. The group is .
A group is residually finite if every nontrivial element survives in some finite quotient.
For the group above,
In particular . The non-existence clause holds for classifying spaces with any number of cells. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. The theorem disproves the Eilenberg–Ganea conjecture with a finitely generated (indeed type , but not finitely presented) residually finite group, so the conjecture fails even for countable groups with strong finiteness properties. By Bestvina–Brady's dichotomy the Whitehead conjecture is not directly decided by this example, but the gap between the algebraic and geometric dimensions in dimension two is now exhibited concretely.
Formalizing it. The statement is concrete: an explicit finite graph, its Artin group and height kernel, a projective dimension, and existence/non-existence of CW models. The non-existence clause ranges over all CW complexes of arbitrary cardinality, which is exactly the kind of universally quantified topological claim where a machine check is valuable. Groundwork includes classifying spaces in Mathlib's CW-complex framework, projective dimension over group rings, and Bestvina–Brady Morse theory.
The kernel acts freely on an acyclic 2-complex, which gives , but an acyclic complex need not be contractible, and showing that one particular 2-dimensional model fails to be a says nothing about other models. The obstacle is to rule out every hypothetical two-dimensional classifying space, with arbitrarily many cells, and to do so for a group that is not finitely presented. Homological invariants cannot see the difference, since they agree with those of a genuine 2-dimensional model.
seedWord, rose vertices, circle edges and sectors; seedGraph is the comparability graph of the cell face relation. ArtinGroup is a PresentedGroup on commutators of adjacent vertices, height sends each generator to in Multiplicative ℤ, and SourceGroup is its kernel.cohomologicalDimension is the categorical projective dimension (in WithBot ℕ∞) of the trivial -module in ModuleCat.HasClassifyingSpace G n asks for a Hausdorff, path-connected CW complex with no cells above dimension , fundamental group isomorphic to , and a surjective covering map from a contractible space. The positive clause is stated in universe 0; the negative clause is universe-polymorphic, so no restriction on the cardinality of cells is imposed.A finitely generated group is (word-)hyperbolic if the geodesic triangles in its Cayley graph are uniformly thin, as in the hyperbolic plane. Such a group has a boundary at infinity , a compact space of asymptotic directions. The fundamental group of a closed hyperbolic 3-manifold is hyperbolic with boundary the 2-sphere. Cannon's conjecture asks for the converse: if a hyperbolic group has boundary homeomorphic to , does it act geometrically on hyperbolic three-space ? An affirmative answer characterizes, purely in terms of coarse geometry, which groups arise from closed hyperbolic 3-manifolds; it is one of the central problems of geometric group theory and is closely tied to the geometrization program for 3-manifolds.
The source of this mission, an OpenAI preprint dated September 23, 2026, follows the analytic route and proves the conjecture.
Let be a group with a finite symmetric generating set and Cayley graph with graph distance . is hyperbolic if there is such that every point on a side of a geodesic triangle lies within of the union of the other two sides. A geodesic ray based at is a sequence with ; two rays are equivalent if stays bounded. The boundary is the set of equivalence classes with the quotient of the topology of pointwise convergence.
is the upper half-space with distance , and is its full isometry group, including orientation-reversing isometries. A homomorphism gives a proper action if is finite for every compact , and a cocompact action if translates of one compact set cover .
The Lean statement OAI.CannonRelease.cannon is open on the platform.
The theorem identifies hyperbolic groups with 2-sphere boundary, up to finite kernels, with uniform lattices in . For torsion-free , the quotient is a closed hyperbolic 3-manifold, possibly nonorientable (Corollary 8.1), and the work of Kahn–Marković, Bergeron–Wise and Agol then gives virtual structure results (Corollary 8.2). It also settles the hypotheses of the reductions of Marković and of Groves et al. in full generality.
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. A formal proof would require formal infrastructure for hyperbolic groups and their boundaries, quasiconformal analysis and combinatorial modulus, very little of which is currently in Mathlib.
By the Cannon–Floyd–Parry and Bourdon–Kleiner criteria, the theorem reduces to a uniform upper bound on the combinatorial 2-modulus of curve families at all scales of the boundary. The bound is easy to state but there is no a priori reason why moduli of coverings of a topological sphere should stay bounded; Bonk–Kleiner needed the extra hypothesis that the conformal dimension is attained. A proof must extract analytic control (a nonconstant limit function with controlled oscillation) from a hypothetical sequence of coverings with unbounded modulus and contradict it using only hyperbolicity and the topology of the boundary.
CayleyData G is a finite symmetric generating set with connected SimpleGraph.mulCayley; ThinTriangles asks for one natural number working for all geodesic triangles given as walks of length equal to graph distance.ℕ → G with r 0 = 1 and dist (r i) (r j) = |i-j|; the boundary is the quotient by bounded synchronous distance. carries the discrete topology, rays the subspace product topology, and the boundary the quotient topology, which coincides with the visual topology for hyperbolic groups.EuclideanSpace ℝ (Fin 3); is the upper half-space with the explicit arcosh distance and subspace topology; isometries are self-homeomorphisms preserving that distance.A complete development needs Gromov hyperbolic groups and visual metrics, approximately self-similar spheres, combinatorial modulus and the Bonk–Kleiner/Bourdon–Kleiner uniformization criterion, and the Sullivan–Tukia straightening of uniformly quasiconformal groups. Contributions formalizing Proposition 2.6 (from a round boundary action to a geometric action on ) or Theorem 2.5 (the uniformization criterion) are welcome.
Pure type systems (PTSs) are a uniform framework covering the simply typed λ-calculus, System F, the calculus of constructions and the type theories behind proof assistants such as Coq and Lean. A system is specified by its sorts (like and ), axioms () and product rules (which dependent function types may be formed). Normalization is the key metatheoretic property: it underlies logical consistency and decidability of type checking. There are two versions. A term is weakly normalizing if some sequence of β-reductions reaches a normal form, and strongly normalizing if every reduction sequence is finite. Strong normalization is what implementations need (any evaluation strategy terminates) but it is much harder to prove. The Barendregt–Geuvers–Klop conjecture asserts that, for pure type systems, the system-wide weak property already implies the strong one.
A specification consists of a type of sorts, an axiom relation and a rule relation ; neither is assumed functional. Expressions are
up to renaming of bound variables. β-reduction is the compatible closure of , with steps allowed everywhere, including inside the annotation of a λ and both parts of a Π. Typing is generated by the seven standard PTS rules (axiom, variable, weakening, product, abstraction, application, conversion up to ). A context is valid if each declared type is typed by a sort in the preceding prefix, and is legal in if or for some .
The system is weakly (strongly) normalizing if every legal expression in every valid context is weakly (strongly) normalizing.
For every specification ,
Both quantifiers range over the whole system; the theorem does not claim that an individual weakly normalizing term is strongly normalizing, and it says nothing about η-reduction. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. For any PTS, a proof that every legal term has a normal form now yields termination of every β-reduction strategy, including reductions inside types and annotations that may continue after the computational body is normal. Earlier results needed nondependent products, cleanliness, negatability, a tiered sort hierarchy, or a translation requiring extra product rules; the general case — arbitrary sorts and nonfunctional rules — was not covered by any earlier result since Geuvers' 1993 formulation.
Formalizing it. The statement is entirely syntactic and finitary, so it is a natural target for a proof assistant, and the relevant objects (de Bruijn syntax, substitution, typing derivations) are standard formalization material. The proof in the source is long (over 70 pages) and combines reducibility candidates with a fixed-point construction over sort profiles; a machine check would substantially raise confidence. A formal PTS metatheory library (substitution lemmas, confluence, subject reduction) would be reusable for other type-theory formalizations.
The obvious route — reducibility candidates à la Tait–Girard — needs a model of types built by recursion on sorts, which fails for impredicative or nonfunctional specifications where a type can have several sorts and no hierarchy is available. Translation methods (CPS or irrelevance elimination) need specific product rules to preserve typing, which a general specification may lack. Weak normalization of one term cannot be used alone; the argument must exploit normal forms of other open expressions. Annotations add a further complication: erasing them can change the equational theory (Barthe–Coquand), so reduction inside annotations must be tracked rather than erased.
Expr S with var, sort, app, lam, pi), so α-equivalence is syntactic; substitution is parallel substitution with lifting.Beta is full compatible closure, including lam_domain, pi_domain and pi_body steps; conversion is Relation.EqvGen Beta.HasType has exactly the seven PTS rules; contexts are lists stored newest-first, each declaration typed in its prefix (ValidContext). Legal includes expressions occurring as types.Beta.S is arbitrary (any universe), and axioms and rules are arbitrary relations: no functionality, finiteness or hierarchy assumptions.A logic for unordered finite structures (graphs, databases, relational inputs given up to isomorphism) must give answers that do not depend on how the input elements are named. Many polynomial-time algorithms nevertheless make arbitrary intermediate choices, for example the pivot in Gaussian elimination, without changing their final answer. Choiceless polynomial time with counting (CPT), introduced by Blass, Gurevich and Shelah (1999), forbids such choices entirely: it computes with hereditarily finite sets over the input elements and can count, but can never pick one element from a set merely because the set is nonempty.
Witnessed symmetric choice (WSC), in the form of Lichter and Schweitzer (2022, arXiv version 3), adds a controlled form of choice: the logic may pick an element of a set provided it also constructs automorphisms of the input showing that all elements of that set are interchangeable, so the answer cannot depend on which one was picked. Lichter and Schweitzer asked whether CPT + WSC is strictly more expressive than CPT. This mission concerns a proof that it is.
The source of this mission is an OpenAI preprint dated September 24, 2026; its companion preprint (September 23, 2026) proves that CPT does not capture polynomial time.
Let be a finite set of atoms and the hereditarily finite sets over . CPT terms are built from variables, , , , , (the member of a singleton, else ), (the von Neumann ordinal ), comprehensions and iteration from ; formulas use input relations, equality and Boolean connectives. A sentence pairs a closed formula with a polynomial that bounds the number of iteration steps and the hereditary size of all intermediate objects on inputs with atoms; exceeding the bounds yields a default or a failure value .
A WSC operator iterates a step term in which, at each stage, a choice term proposes a nonempty set ; one element is chosen, and a witness term must produce automorphisms of the entire input that fix the parameters and all earlier stages and map any element of to any other. If the witnesses are valid along every possible choice sequence, the output formula's value on the terminal state is returned; otherwise the value is .
The true-model class of a sentence is the set of finite structures on which it returns true; false and are both outside it.
For the fixed vocabulary of eight binary relations there is a CPT + WSC sentence with exactly one WSC occurrence such that
The Lean statement OAI.WitnessedChoice.main (via BGS.MainStatement) is open on the platform.
Since every CPT sentence is a CPT + WSC sentence, Theorem 1.1 gives a strict inclusion of definable Boolean queries and answers the expressiveness question posed by Lichter and Schweitzer in the true-model sense. The separation holds against CPT with counting and sets of arbitrary finite rank, not a rank-restricted fragment. It leaves open whether CPT + WSC captures polynomial time and the effect of nesting WSC operators.
The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists.
Two different tasks must be done. The upper bound requires a legal WSC definition on all inputs, not only on the intended grid structures: witnesses must be genuine automorphisms of the whole input fixing the full history, which the sentence must check, with a fallback when the input is not of the intended shape. The lower bound must defeat every CPT sentence, including those that build nested sets of large rank; rank-sensitive support arguments (Dawar–Richerby–Rossman) do not suffice. The paper uses a nonabelian automorphism group whose central subgroup has rank-independent small supports, then a counting equivalence and a bounded-width description of complete CPT evaluations.
Term n / Formula n with de Bruijn-style Fin n variables, including iterate and the wsc formula; wscCount counts WSC occurrences.Option (none is ). resource p n = ⌊p(n)⌋ bounds iteration length and transitive-closure size.GoodWSC) quantifies over all choice prefixes; witnesses are permutationGraph g for permutations g that are input automorphisms, fix the free parameters and every earlier stage, and act transitively on the choice set.FiniteInput packs any finite carrier type with the eight-symbol relations (Ed, Cf, EB, VB, I, Z δ, δ : ZMod 3). Sentence.isCPT means wscCount = 0.A complete development needs hereditarily finite sets with permutation actions, support and counting-equivalence theory, and the grid structures; much of this is shared with the companion CPT noncapture mission. Contributions formalizing Proposition 4.4 (a total all-input definition), Proposition 5.3 (transitivity for every parameter tree), Theorem 5.5 (opposite grid answers), Proposition 6.3 (small-orbit support bound), Theorem 8.1 (transfer through small supports) and Theorem 9.3 (eventual equality for every CPT sentence) are welcome.
Descriptive complexity asks whether complexity classes can be characterized by logics, without reference to machines. Immerman and Vardi (1982) showed that on ordered finite structures, first-order logic with a least fixed-point operator expresses exactly the polynomial-time queries. On unordered structures, such as graphs given only up to isomorphism, an algorithm must not depend on an arbitrary ordering of the input, and whether some logic captures polynomial time there is a central open question (Chandra–Harel 1982, Gurevich 1988).
Choiceless polynomial time with counting (CPT), introduced by Blass, Gurevich and Shelah (1999), was for decades the strongest candidate: it computes with hereditarily finite sets built over the input elements, can count, and is invariant under automorphisms by construction. Blass, Gurevich and Shelah conjectured that CPT is still a proper fragment of polynomial time. This mission concerns a proof of that conjecture.
The source of this mission is an OpenAI preprint dated September 23, 2026.
Fix the field and the vocabulary of eight binary relation symbols . For a finite -structure put
With unknowns and (separate families), the system consists of
for every such that some and satisfy and . The query says this system is consistent over . No promise is imposed on the input.
A CPT program is a fixed finite set of rules that updates dynamic functions whose values are hereditarily finite sets over the atoms of , using pairing, union, comprehension, equality, membership, the input relations, and the cardinality operation (which returns a von Neumann ordinal). A program defines if for fixed polynomials , on every input of size it halts within steps, touches at most hereditarily finite objects, and accepts exactly when holds. No bound on set rank is imposed.
The Lean statement OAI.CPTSeparation.main is the conjunction of these three clauses. It is open on the platform.
The theorem confirms the Blass–Gurevich–Shelah noncapture conjecture for the full counting formalism: CPT does not capture polynomial time on unordered structures. It removes the leading candidate logic from Gurevich's question, which itself remains open. Because is expressible in fixed-point logic with a solvability or rank operator over (Corollary 3, p. 3), it also shows that neither of those logics is contained in CPT. The lower bound holds for programs of arbitrary set rank, unlike the bounded-rank lower bounds of Dawar–Richerby–Rossman.
The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists.
The polynomial-time upper bound is Gaussian elimination. The obstacle is the lower bound against every CPT program, including those that build sets of unbounded rank. Bounded-variable counting games handle fixed-point logic with counting but do not by themselves control CPT, which is strictly stronger (it decides CFI queries over ordered base graphs). Rank-dependent support arguments give lower bounds only for each fixed rank. The paper needs support bounds independent of rank, for which it uses a nonabelian automorphism group acting on grid structures, then a counting equivalence for all supported objects, and finally a transfer to complete computations via an interpretation characterization of CPT.
Input A gives a Boolean-valued binary relation for each Symbol (Ed, Cf, EB, VB, I, Z δ with δ : ZMod 3). Input.query is the existence of λ, μ satisfying the normalization and consistency equations exactly as above; an empty system is consistent.OrdinaryPolynomialTime asks for a function on ordered tables and a Turing.TM2ComputableInPolyTime machine with finite alphabets computing it from the cell-by-cell table encoding, agreeing with the query for every ordering of every structure.FullCPT defines terms and rules over hereditarily finite sets (Lists quotient), a state of finitely many nonempty locations, synchronous consistent updates, halt/accept flags, and the set of occurring objects (active elements plus roots of evaluated terms). EvaluationDefinable Q asks for one program and polynomials time, space that accept exactly the inputs satisfying Q, halting within time and with at most space occurring objects.A complete development needs: hereditarily finite sets and automorphism actions on them, support theory, counting equivalence games, the grid structures with their automorphism group, and a CPT-to-interpretation translation. Contributions formalizing Proposition 2 (polynomial-time decidability), Proposition 8 (small-orbit support bound), Proposition 13 (quantitative homogeneity) and Theorem 14 (transfer through small supports) are welcome.
Turing reducibility compares sets of natural numbers by their information content: if an oracle Turing machine with oracle computes the characteristic function of . Identifying mutually reducible sets gives the Turing degrees , partially ordered by . A central question of computability theory since the 1970s is how much of the underlying computational structure the abstract order remembers. The strongest possible answer is rigidity: the order has no nontrivial automorphisms, so every degree is determined by its position in the order.
After these results the remaining problem was rigidity at degrees outside the known fixed cone. The source of this mission, an OpenAI preprint dated September 24, 2026, proves full rigidity.
An oracle is a function (a set of natural numbers). means that the characteristic function of is partial recursive relative to . This is a preorder; its quotient by is the set of Turing degrees, partially ordered by . An automorphism of is a bijection with
No definability, Borel or continuity hypothesis is imposed on .
The Lean statement OAI.TuringRigidity.ManuscriptMain.rigidity is open on the platform.
Rigidity says that the order alone determines every Turing degree. By the theorem of Slaman and Woodin, it is equivalent to their biinterpretability conjecture: the degrees are biinterpretable without parameters with full second-order arithmetic (Corollary 5.1). Consequently every relation on degrees that is definable in second-order arithmetic and invariant under Turing equivalence is definable in the degree order, which settles a family of definability questions at once.
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. Its proof relies on the Slaman–Woodin representation theorem, whose cited source is an unpublished 2005 manuscript; a formalization would either need to formalize that input as well or isolate it as an explicit hypothesis, and would make the dependence fully transparent.
Earlier methods fix cones of degrees: coding arguments work above a sufficiently high base such as , where enough information can be coded and decoded. Below that base the coding machinery is not available, and an arbitrary automorphism carries no a priori regularity. The proof must turn the arithmetic (hence Borel) representation of an automorphism into recovery of every individual real, using a category argument that works for every irrational parameter, not only generic ones.
ℕ → Bool; reducibility is Mathlib's TuringReducible between the characteristic functions viewed as partial functions ℕ →. ℕ (values and ).Degree is Antisymmetrization Oracle Reduces with the induced partial order; automorphisms are order isomorphisms Degree ≃o Degree, i.e. bijections preserving and reflecting .A complete development needs relativized computability (oracle machines, joins, the jump), Borel and Baire-category arguments on and , and the Slaman–Woodin representation theorem (Theorem 3.1). Formalizing that theorem would itself be a substantial and reusable contribution. Contributions formalizing Proposition 4.1 (recovery of an irrational from four values of a Borel subadditive map with countable fibers) are welcome.
A class of structures is categorical in a cardinal if it has exactly one model of size up to isomorphism. Morley's theorem (1965) says that a complete first-order theory in a countable language categorical in one uncountable cardinal is categorical in all of them. Abstract elementary classes (AECs), introduced by Shelah in the 1970s, axiomatize classes of structures with a well-behaved notion of strong substructure (closure under isomorphism, coherence, unions of chains, a Löwenheim–Skolem number) without requiring first-order axiomatizability; they cover classes defined in infinitary logics and many classes of modules. Shelah's categoricity conjecture for AECs, in its eventual form, asks whether categoricity in one sufficiently large cardinal transfers to all sufficiently large cardinals. A sharper, prescribed-threshold form names the threshold explicitly: with (the Hanf number for existence of arbitrarily large models), categoricity in some should imply categoricity in every . Deciding which form holds is a central question in non-elementary model theory.
Work with relational structures in a finitary relational language (a set of relation symbols, each with a finite arity). An abstract elementary class is a class of -structures with a relation ("strong substructure") such that: is a partial order on refining substructure; and are closed under isomorphism; coherence holds (, , imply ); unions of -chains are in , are -extensions of each member, and are -below any common strong extension (Tarski–Vaught chain axioms); and there is a Löwenheim–Skolem number , the least such that every subset of a model lies in some with .
is categorical in if it has a model of size and any two models of size are isomorphic. The beth numbers are , and suprema at limits. CH is .
Assume CH. There is a countable finitary relational language and an AEC in such that
has two nonisomorphic models of cardinality , and, with ,
Hence is a categoricity cardinal from which downward transfer to fails, while eventual categoricity holds for this . The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. Combined with Gödel's relative consistency of CH, the theorem shows that, if ZFC is consistent, the prescribed-threshold form of Shelah's categoricity conjecture is not provable in ZFC (Corollary 6.1 of the source). The example has no amalgamation or joint embedding, which explains why transfer theorems that assume these properties are unaffected, and it is compatible with qualitative eventual categoricity. It also bears directly on a published claim of transfer at the prescribed bound for arbitrary AECs.
Formalizing it. Because the result contradicts a claimed theorem in the literature, an independent machine check is especially valuable. The formal statement verifies every AEC axiom explicitly, not just the two cardinal-arithmetic conclusions. Mathlib has cardinal and ordinal arithmetic, beth numbers and ZFC sets; the AEC framework built here would be reusable for further formal work in non-elementary model theory.
Most known non-transfer examples (Hart–Shelah) fail categoricity at small cardinals; here the failure must happen exactly at the Hanf-type bound while categoricity holds on a tail, with . One must build two nonisomorphic models at and simultaneously rule out any two nonisomorphic models above , without appealing to a general eventual-categoricity theorem. All AEC axioms — in particular coherence and smoothness of unions of arbitrary directed chains — must survive the exceptional sets used to separate models, which is where naive constructions break.
RelModel L with carrier a ZFSet (so cardinalities are cardinals of genuine sets in universe u) and relations indexed by arity; Type with countable.ClassData packages a predicate of objects and a strong-substructure relation; IsAEC lists the axioms above, including invariance under isomorphisms compatible with inclusion, coherence, and the union axioms for chains indexed by any nonzero ordinal.HasLSNumber ℵ₀ asserts both that is a Löwenheim–Skolem bound and that it is the least one.hanf κ = beth (succ (2^κ)).ord, endpoint = beth (ω_2), tailThreshold = beth (succ (2^{ℵ₁})).ord. The equality endpoint = hanf ℵ₀ is part of the goal (it follows from CH).Categorical μ includes existence of a model of size ; TwoModels asks for two nonisomorphic models of the given size.The Thorp shuffle cuts a deck in half, pairs cards in corresponding positions, and lets an independent fair coin order each pair before the pairs are interleaved. On cards, removing the deterministic rotation of coordinates turns physical shuffles into one binary coordinate sweep: in each coordinate direction, in order, every pair of positions differing in that coordinate is independently swapped with probability . After one sweep each card is uniform, but the joint permutation retains dependence because cards share switches.
By finite-group Fourier analysis (Diaconis–Shahshahani 1981), fast mixing of the whole deck follows from a power saving for the sweep in every irreducible representation of . The source obtains this saving by first controlling a perturbed sweep, in which each line permutation is mostly uniform, conditionally on prescribed trajectories of some cards, and then transferring the estimate analytically to the binary sweep.
Positions are binary strings , (Lean: Slot d := Fin d → Bool). For a coordinate , a layer flips bit of a position according to a fair coin attached to the edge ; the binary sweep applies the layers for in order, with all coins independent (Lean: binarySweep, binaryLaw d its law on ). For an irreducible unitary representation of of dimension , the sweep operator is
Write for the law of independent sweeps and .
For the conditional estimate, an ordered product grid is with each a power of two in ; a sweep permutes the lines parallel to coordinate , then coordinate , and so on, each line independently with law . A family of prescribed trajectories (disjoint at every layer) is conditioned on; the remaining random bijection of the free slots has average in each irreducible , with line cost .
There are a power of two , an integer and such that for every grid, every feasible family , every and every irreducible ,
with , , , and .
There are absolute constants and such that for all and every irreducible unitary representation of of dimension ,
the sign representation is annihilated, ; and there is an absolute integer such that
The goal is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. Since one binary sweep is exactly physical shuffles, the goal gives physical shuffles for mixing from every starting deck, and the support obstruction (Proposition 1.2: shuffles reach at most permutations) gives the matching lower bound ; thus , improving Morris 2013. The power saving in every irreducible representation is a stronger, reusable statement: it controls any number of further sweeps and any function of the permutation through Fourier analysis.
Formalizing it. The goal is stated for explicit finite objects (coins, sweeps, Fourier operators on ), with existential constants only. A formal proof would certify optimal-order mixing for the Thorp sweep. The conditional estimate (Theorem 3.1) is formalized separately and is the natural intermediate milestone.
The obvious induction—split the coordinates and multiply child bounds—breaks because revealing card paths changes the conditional law of the line permutations, and the induction must be stable when more paths are revealed. The source handles this with the line cost , which records the exact cost of prescribing positions without replacement. A second obstacle is that the conditional estimate is only available for mostly-uniform lines ( small), while the Thorp sweep is the binary case ; for a fixed grid the sweep operator is a matrix polynomial in whose behavior at is not controlled by real-segment bounds alone. Representations of very small "level" (first appearing on few tracked cards) need a separate sparse estimate.
binary_sweep_contraction_and_mixing): three conjuncts. BinaryContractionTarget: and every irreducible representation of Equiv.Perm (Slot d) on EuclideanSpace ℂ (Fin D) preserving norms, the operator norm of is at most (real power). Sign: for every , . UniformSweepMixingTarget: , total variation of the -fold convolution power translated by from uniform is at most . Physical shuffles are not modelled; the statement is about sweeps.conditional_main): grids are Grid with coordinates of (); trajectories are Holes with disjointness at every layer and coordinate-respecting steps; feasibility means some line choices realize them; the residual bijection is identified with the stabilizer of the input holes via a fixed reference completion; representations are UnitaryIrrep of that stabilizer; the Schatten moment is ; .all_grid_moment is a parameter-explicit form of the same induction under numerical largeness hypotheses and a small-perturbation hypothesis, kept as a plain item.The Thorp shuffle is a simple card-shuffling rule: cut a deck of cards into two equal halves, pair cards in corresponding positions, and let an independent fair coin decide the order within each pair when the pairs are interleaved. It is a standard test case for mixing-time methods and a building block in small-domain enciphering schemes. For every individual card is uniform after shuffles, but the joint order of all cards is much harder to control. Determining whether shuffles suffice to make the full permutation close to uniform was a long-standing question.
Index the positions by binary strings (in Lean, Card d := Fin d → Bool). One physical shuffle sends
with independent fair bits (Lean: step d ξ = rotate * pairSwitch ξ). After physical shuffles the rotations cancel, and the result is a coordinate sweep: one random matching switch in each coordinate direction. Write for the law on of physical shuffles (Lean: law d t, the fraction of coin sequences producing a given permutation).
For a partition let be the Specht module (the irreducible representation of indexed by ), of dimension , and let be the average of the sweep in . For an operator , and traces are unnormalized. The regular trace of the -th power is
in which the trivial representation contributes exactly . Total variation is .
There is an absolute real such that for every (so )
and for every integer with and every initial deck ,
The constant is not specified; only its existence and uniformity in are asserted. The goal is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. Since one sweep is physical shuffles, the second clause shows that Thorp shuffles bring the full permutation within of uniform from every starting deck. A counting argument on coin strings (Proposition 5.1 of the source) shows that at least physical shuffles are needed, so this order is optimal, improving the bound of Morris 2013. The regular-trace bound is stronger than an operator-norm bound for each irreducible: it controls all singular values with their multiplicities, which is what yields polynomially small total-variation distance.
Formalizing it. The statement is fully finite and explicit: an existential over one real constant followed by inequalities for each . A formal proof would certify an optimal-order mixing bound for a widely studied shuffle. Specht modules, Schatten-type traces via continuous functional calculus, and the shuffle law are all defined in the mission's definition file and can be reused for related shuffling problems.
Single-card and few-card statistics mix after one sweep, but the full permutation involves all bits of information, and the coin choices of a sweep interact across coordinates. The natural route—bounding the operator norm of separately in each irreducible representation—does not suffice, because the regular trace weights each representation by its dimension , and the number of partitions grows like . A uniform power must work simultaneously for representations of tiny dimension (very long first row), intermediate dimension, and dimension close to , and splitting the coordinates into row and column groups produces two symmetry decompositions that do not commute.
Fin d → Bool; permutations are Equiv.Perm (Card d); partitions of are Young diagrams of cardinality (Shapes (2^d)).Q d μ is the average over all coin sequences of length of the representation of run d d.absoluteTrace A P is the real part of the trace of CFC.rpow (CFC.sqrt (A⋆A)) P, i.e. ; regularTrace multiplies by finrank.sweepDistance d v σ is total variation of the law of physical shuffles, right-translated by , from the uniform weight . The integer is converted with Int.toNat; since and , and no truncation occurs.Many random permutations are analysed through what they do to a few labels at a time: the joint positions of chosen cards in a shuffle, or the images of a list of inputs under a block cipher built from a shuffle. Such partial information does not by itself control the whole permutation. The uniform law on the alternating group already has uniform images on every set of at most labels, yet it is at total-variation distance from uniform on . Converting partial-permutation estimates into full-permutation estimates therefore needs an additional argument, and this is the bottleneck in recent work on the Thorp shuffle, where fixed fractions of the deck were known to randomize quickly (Czumaj–Vöcking 2014; Czumaj 2015) long before the full deck was.
Let be a finite set of labels and , acting as maps from initial labels to final positions. For , let be the block subgroup of permutations that fix every label outside . Two permutations have the same images on exactly when they lie in the same left coset , so a bound on the law of those images is a bound on coset masses.
For a nonnegative weight on and a unitary representation of on a finite-dimensional complex inner-product space , the Fourier transform is , with . The Hilbert–Schmidt norm is unnormalized, . For the symmetric degree constant is
where ranges over the degrees of the irreducible complex representations of .
Partition into nonempty blocks and put . Let on have total mass at most one and satisfy
Then for every and every irreducible unitary of degree ,
No restriction is placed on the block sizes or on multiplicities in the restriction of to . The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. Theorem 1.1 is a quantitative transfer principle: a single law whose complementary partial images are never much heavier than uniform has a power saving in every irreducible representation of . With and it gives , which is enough for the principal application in the source (Corollary 3.6, p. 9): if the images of a uniformly chosen set of labels are close to uniform in average total variation and the sign mean tends to zero, then the product of just two independent copies of the permutation converges to uniform. This is the step used by the companion Thorp-shuffle preprints to turn fixed-list estimates into full-deck mixing in shuffles. The statement concerns arbitrary laws on and does not depend on any shuffle.
Formalizing it. The theorem is a finite inequality with explicit constants, so it is a natural target for machine checking. A proof would certify the partial-to-full transfer used by the Thorp mixing arguments, and would require reusable infrastructure: isotypic decompositions of restrictions to products of subgroups, Schur averaging, Hilbert–Schmidt and operator norms of group-algebra elements, and uniform bounds on symmetric-group Witten zeta sums. None of this is formalized yet.
The natural approach decomposes restricted to into tensor products of irreducibles of the blocks and bounds on each piece. This fails when a block type occurs with large multiplicity: a dimension count that pays for every copy gives no decay in . The bound must count each irreducible type of a block subgroup once, regardless of multiplicity, and must hold uniformly over all block sizes, which is why the constant is a supremum over every symmetric group. The Hilbert–Schmidt bound is harder than the operator bound, because it must control the whole Fourier matrix rather than its action on one vector.
Fintype with decidable equality; blocks are M : Fin b → Set X, nonempty, pairwise disjoint and covering. The block subgroup is blockSubgroup (M i), the permutations fixing each point outside M i.LeftCosetCap f H B: for every , , with the index H.index.complexFourier ρ f; hsNormSq is ; the operator norm is that of the associated continuous linear map; is Module.finrank ℂ V and the exponent is a real power.Equiv.Perm (Fin m), and is symmetricDegreeConstant u, an sSup over . The supremum is finite for every ; a solver must prove this boundedness, since sSup of an unbounded real set would be .At its critical weight, a self-avoiding path on the honeycomb lattice can make long excursions without paying an exponential cost. A basic quantitative question is how much of its total weight reaches the far side of a strip of height . Physics heuristics (Nienhuis's Coulomb gas and the conjectured scaling limit with boundary exponent ) predict that this crossing mass decays like . Rigorous results so far showed only that it tends to zero, with a polynomial upper bound with a tiny exponent.
The OpenAI preprint behind this mission, dated September 26, 2026 (source), claims the predicted power with bounded-factor constants: the crossing mass is comparable to , and the first horizontal-displacement moment of paths returning to the starting side is comparable to (Theorem 1.1, p. 2). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Use the honeycomb lattice dual to the equilateral triangular tiling of side one, with one edge direction horizontal; its vertices are the triangles up i j and down i j, where indexes the horizontal band. Let be the strip of bands. A path starts in the triangle up 0 0 (just above bottom port ), visits distinct triangles, moves between adjacent ones, and stays in bands . Its length is the number of visited triangles and its critical weight is with . An arch ends at up k 0 with (bottom port ); a bridge ends at a down triangle of the top band. Put and
Write if for all with fixed constants .
For every all sums above are finite, and with constants independent of ,
and is nonincreasing in .
The result itself. It establishes the predicted crossing power with uniform multiplicative constants, not just a logarithmic exponent, improving the qualitative decay of Beaton et al. and the polynomial upper bound of Krachun and Panagiotis. It is an input for the bridge-length and spatial-exponent results of companion preprints. The exponent of concerns an unnormalized displacement moment summed over all lengths; the fixed-length displacement conjecture and the scaling limit are different questions.
Formalizing it. The proof combines an exact boundary identity of Duminil-Copin–Smirnov type, finite-strip transfer matrices with integrable local relations, a Pfaffian that makes the stationary vector polynomial, and a comparison of the resulting positive integral with Bures–Laguerre ensembles. A formal proof would include the honeycomb boundary identity, the core of the connective-constant proof, which is itself a natural formalization target. No machine-checked honeycomb walk result of this kind is known.
The boundary identity (Lemma 4.2, p. 15) does not determine the power: it only gives between orders and . The preprint's route computes the arch moment first, as one coefficient of a ratio of Pfaffians (Proposition 4.1, p. 13), converts it into a positive -fold integral with Bures-type interaction (Section 5), and estimates that integral uniformly in by comparison with Laguerre laws (Section 6). The crossing power then follows from monotonicity and . A degree bound on the polynomial vacuum (Lemma 3.2, p. 10) is essential, because it turns interpolation into an identity argument.
ℤ × ℕ × Bool (column, band, up/down); adjacency joins an up triangle to the down triangles sharing an edge. Paths are Lists with Nodup, IsChain adjacent, head up 0 0, a prescribed last triangle, and all bands < N.rho ^ p.length on paths satisfying IsPath, and 0 otherwise; all masses are tsums over lists. The goal includes summability of each family, so the tsums are genuine sums.moment N = ∑' k : ℕ, (k+1) * K N (k+1), i.e. .Comparable f g asks for constants with for every ; powers are real rpow.Reusable contributions: the honeycomb boundary (parafermionic) identity in finite domains, and summability of critical walk weights in strips.
A random configuration on the vertices of a graph is a factor of IID if it can be produced by a measurable rule from independent uniform labels at the vertices, where the rule commutes with the graph's automorphisms. On trees this notion connects ergodic theory (which invariant processes are "Bernoulli-like"), local algorithms on sparse random graphs (factors of IID are limits of what local algorithms can produce), and statistical mechanics. The free Ising state on the -regular tree is the basic test case. It is easy to sample from a chosen root by broadcasting spins outward, but a factor rule may not use a root. Lyons asked for which inverse temperatures it is a factor of IID (Lyons 2017), and Nam, Sly and Zhang conjectured the answer after proving it for large below a non-explicit constant (Nam–Sly–Zhang 2022).
This mission asks for a formal proof of the exact threshold, including equality, as stated in an OpenAI preprint dated September 26, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Let be the infinite -regular tree with vertex set ; concretely, is the set of finite words over with no two equal consecutive letters, and is adjacent to . Put for . The free zero-field Ising law on is determined by its marginals on finite connected subtrees :
Equivalently, a fair spin at one vertex is broadcast along edges, each child agreeing with its parent with probability . A spin law is a factor of IID if it is the law of for i.i.d. uniform labels and a measurable such that, for each fixed automorphism , almost surely, where .
For every integer and every ,
The result itself. It answers the ferromagnetic case of Lyons's question and proves the Nam–Sly–Zhang conjecture for every . The threshold coincides with the reconstruction (extremality) threshold of the free state, and the result holds at equality, where non-reconstruction alone gives no factor rule (a weak limit of factors need not be a factor). The preprint also shows that, in this range, the factor can be chosen to commute with every automorphism on every input (Lemma 8.5, p. 46). The converse direction ( excludes a factor) is known from Sly's obstruction via the Backhausz–Szegedy–Virág bound and is reproved on p. 2.
Formalizing it. The preprint's construction uses Brownian observation processes, stochastic localization, innovation equations of nonlinear filtering, and conditional-copy coupling arguments. Mathlib has Brownian motion only in early form and no stochastic calculus for infinitely many coupled SDEs; a formal proof would build reusable stochastic-analysis infrastructure. The converse needs the BSV correlation bound for factors of IID. No machine-checked factor-of-IID result for a non-trivial Gibbs measure is known.
Rooted sampling is easy; the obstacle is to remove the root while keeping the output a measurable function of the labels. Finite-cluster constructions only work in the uniqueness range . The Nam–Sly–Zhang approach observes and expresses the posterior through innovations , which are independent Brownian motions; but being Brownian does not make a function of , and that is the central step (pp. 2–3). At criticality the field-response sums in the innovation equation are only borderline integrable near time zero, so infinite sums must be justified with an exact covariance-energy identity rather than with a contraction estimate (Section 1.2, p. 3).
TreeVertex d is the set of words in Fin d with distinct consecutive letters, treeAdj appends or removes one letter, and TreeAut d is the group of adjacency-preserving bijections.Measure.infinitePi of Lebesgue measure on ; spins take values in a two-element type with the discrete σ-algebra, and configurations carry the product σ-algebra.HasFreeIsingLaw θ μ prescribes on every cylinder over a finite connected Finset by the product formula above; these cylinders determine the law.IsFactorOfIID d θ asks for a measurable Phi with pushforward law HasFreeIsingLaw θ and, for each automorphism g, Phi (relabel g U) = relabel g (Phi U) for almost every U (null set may depend on g), matching (1.1).θ = Real.tanh β with and ; at both sides hold trivially (i.i.d. spins), which is consistent with the source. The stronger everywhere-equivariant version is not part of the goal.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.
A uniform spanning tree of a finite connected graph is a spanning tree chosen uniformly at random. On an infinite graph one takes limits along finite pieces: the free uniform spanning forest (FUSF) is the weak limit of uniform spanning trees of an increasing sequence of finite connected subgraphs, with no boundary identification. Uniform spanning forests connect random walks, electrical networks, determinantal processes and -Betti numbers of groups.
A random object on a graph is a factor of IID if it can be produced by one measurable rule from independent uniform labels on the vertices, in a way that commutes with all graph symmetries. Such representations are the measure-theoretic analogue of local algorithms, and they are central in ergodic theory of group actions. Whether the FUSF is a factor of IID was raised by Lyons at Oberwolfach in 2013, and Timár's 2025 paper describes the unrestricted question as open.
The source of this mission, an OpenAI preprint dated September 25, 2026, proves the unrestricted statement with one rule for all graphs.
Let be an infinite, connected, locally finite, simple, undirected graph. For a finite connected subgraph , let be the uniform law on spanning trees of . For finite connected subgraphs whose edges exhaust , the laws (edges outside absent) converge weakly; the limit on does not depend on the exhaustion (Proposition 2.2).
A rule takes a graph, real vertex labels and an edge. It is equivariant if for every isomorphism , and root independent if it uses no distinguished vertex.
A law on , finite, is strongly Rayleigh if whenever all ; on a countable set, every finite marginal must be strongly Rayleigh.
The Lean statement OAI.Problem336.fusf_is_factor_iid is open on the platform.
Theorem 1.1 answers the FUSF factor question without amenability, transience, unimodularity, degree bounds or moment assumptions, and with a single rule for all graphs; Corollary 1.2 gives the factor statement under every unimodular random graph law. Theorem 1.3 and Corollary 1.4 extend the method to all invariant strongly Rayleigh and determinantal processes on countable groups, addressing the regular-action case of the Lyons–Thom question. The paper asserts an ordinary Borel factor, not a finitary one.
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. Formalization would also provide uniform spanning trees, the free forest limit, strongly Rayleigh measures and determinantal laws as reusable Lean objects.
Previous constructions use structure that is absent in general: Wilson's algorithm works for the wired forest on transient graphs, and Timár's construction needs monotone limits along a hyperfinite exhaustion. A factor must produce one exact sample of the infinite-volume law while controlling all edges jointly, and equivariance forbids any choice of root or ordering. The paper's route observes the forest through independent Brownian noises and must show that the posterior drift has a uniformly Lipschitz response to the observations even when the fields are unbounded over the graph.
ℕ → ℕ → Bool; edges are pairs ; a connected graph on is automatically infinite. Equivariance is invariance under every permutation of applied to graph, labels and edge.RuleBorel is joint measurability of in the product σ-algebras.IsVertexIID requires the label coordinates to have independent Uniform finite-dimensional laws (with this forces a probability measure).HasFUSFLaw asks that every cylinder probability (edges in present, edges in absent) be the limit of the corresponding uniform-spanning-tree ratio along every exhaustion by finite connected subgraphs covering all edges.ProbabilityMeasure (Γ → Bool), left translation , i.i.d. labels in Set.Icc 0 1 via Measure.infinitePi, and Hermitian kernels with on finitely supported vectors.A complete development needs the matrix-tree theorem and Kirchhoff formulas, weak limits on , Brownian motion and a Borel Picard iteration for the decoder, and the Borcea–Brändén–Liggett theory. Contributions formalizing Proposition 2.2 (free exhaustion limit), Lemma 2.3 (finite-field forest response) and Proposition 4.2 (sampling from independent Brownian paths) are welcome.
Whether identical classical particles in , interacting only through a stable radial pair potential, can undergo a phase transition is a classical existence problem of rigorous statistical mechanics, highlighted in Simon's list of problems in mathematical physics (Simon 1984). A transition shows up as a singularity of the thermodynamic free energy. Earlier rigorous continuum transitions rely on extra structure — two species, many-body terms, hard cores, or interactions defined through a fixed partition into boxes — or on a mean-field limit in which the potential itself changes. A natural requirement for a satisfactory answer is a single fixed pair potential with a bounded core and an explicit integrable power-law tail.
Particles live in ; a radial pair potential is a function (in Lean, ℝ≥0 → ℝ) applied to pair distances. For the cube and ,
The potential is stable if for all configurations. The canonical free energy at density is
The packing constant is , where is the largest number of points in at mutual distance ; in Lean IsPackingDensity p asserts this limit. StrictTemperatureCorner f βc asserts finite left and right derivatives at with the right one strictly smaller, and non-differentiability.
At the single density : there are a bounded continuous stable with for and such that exists for all and
There are a bounded continuous , constants with
an open interval and one such that for every the free energy exists and is finite for every , and
This is Theorem 1.1 of the source. Both statements are published on the platform with status Open.
The result itself. The theorem gives a single-species, bounded, continuous radial pair potential with an explicit integrable power-law tail whose canonical free energy has a strict temperature corner at one critical inverse temperature for a whole interval of densities. The interaction is a genuine radial function of separations with all long-range terms kept; boxes appear only in the estimates. It does not treat Lennard–Jones-type potentials and does not identify the phases as conventional fluids. The companion preprint has a divergent core but only an tail; the fixed power margin here needs a quantitative range estimate not present there.
Formalizing it. The statement fixes the model completely (free boundary conditions on , Lebesgue measure without temperature normalization, , particles), so a formal proof would settle exactly which version of the problem is solved. The infrastructure (thermodynamic limits, convex duality for pressures, Kac comparisons) is reusable for the companion mission.
The Lebowitz–Penrose theory produces non-convex mean-field free energies only in the limit where the attraction range tends to infinity, and that limiting object is not the free energy of any fixed potential. A single potential must therefore contain infinitely many attractions at growing ranges, and the required singularity must survive all of them. Density coexistence at fixed temperature does not by itself give a temperature corner at a fixed density: two supporting slopes with equal density coordinate and different energy coordinates are needed. A pointwise power bound constrains how strong the successive attractions may be relative to their ranges, which is why a quantitative comparison with an explicit error is required.
EuclideanSpace ℝ (Fin 3); distances enter through nndist, so the potential is a function on ℝ≥0. Boundedness, continuity, stability with , and decay with are separate conjuncts.IsPackingDensity p (a limit), and is required; packingNumber is a sSup over a bounded set of naturals.IsCanonicalFreeEnergy φ ρ f asserts for every , so is determined on ; one-sided derivatives use HasDerivWithinAt on Iic βc and Ici βc.