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.
Quantum Max-Cut asks for a quantum state that maximizes the energy of a graph's antiferromagnetic interactions. Entanglement can improve the achievable energy, making the problem a natural setting for studying approximation algorithms.
This campaign aims to formalize the strongest possible approximation guarantees in Lean. Each ratio corresponds to the same theorem:
There exists a uniform polynomial-time algorithm that, for every graph with nonnegative rational edge weights, prepares a quantum state whose expected Quantum Max-Cut energy is at least times the optimum.
The optimum ranges over all quantum states, including entangled states. Higher approximation ratios are better.
The verified starting bound is . The first open target is , the historical general-graph guarantee of Gharibian and Parekh (2019). The bound is a later target. A mathematical guarantee enters the campaign's verified record once its Lean proof is complete.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
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.
The Thorp shuffle cuts a deck in half, pairs cards in corresponding positions, and lets an independent fair coin order each pair before the pairs are interleaved. On cards, removing the deterministic rotation of coordinates turns physical shuffles into one binary coordinate sweep: in each coordinate direction, in order, every pair of positions differing in that coordinate is independently swapped with probability . After one sweep each card is uniform, but the joint permutation retains dependence because cards share switches.
By finite-group Fourier analysis (Diaconis–Shahshahani 1981), fast mixing of the whole deck follows from a power saving for the sweep in every irreducible representation of . The source obtains this saving by first controlling a perturbed sweep, in which each line permutation is mostly uniform, conditionally on prescribed trajectories of some cards, and then transferring the estimate analytically to the binary sweep.
Positions are binary strings , (Lean: Slot d := Fin d → Bool). For a coordinate , a layer flips bit of a position according to a fair coin attached to the edge ; the binary sweep applies the layers for in order, with all coins independent (Lean: binarySweep, binaryLaw d its law on ). For an irreducible unitary representation of of dimension , the sweep operator is
Write for the law of independent sweeps and .
For the conditional estimate, an ordered product grid is with each a power of two in ; a sweep permutes the lines parallel to coordinate , then coordinate , and so on, each line independently with law . A family of prescribed trajectories (disjoint at every layer) is conditioned on; the remaining random bijection of the free slots has average in each irreducible , with line cost .
There are a power of two , an integer and such that for every grid, every feasible family , every and every irreducible ,
with , , , and .
There are absolute constants and such that for all and every irreducible unitary representation of of dimension ,
the sign representation is annihilated, ; and there is an absolute integer such that
The goal is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. Since one binary sweep is exactly physical shuffles, the goal gives physical shuffles for mixing from every starting deck, and the support obstruction (Proposition 1.2: shuffles reach at most permutations) gives the matching lower bound ; thus , improving Morris 2013. The power saving in every irreducible representation is a stronger, reusable statement: it controls any number of further sweeps and any function of the permutation through Fourier analysis.
Formalizing it. The goal is stated for explicit finite objects (coins, sweeps, Fourier operators on ), with existential constants only. A formal proof would certify optimal-order mixing for the Thorp sweep. The conditional estimate (Theorem 3.1) is formalized separately and is the natural intermediate milestone.
The obvious induction—split the coordinates and multiply child bounds—breaks because revealing card paths changes the conditional law of the line permutations, and the induction must be stable when more paths are revealed. The source handles this with the line cost , which records the exact cost of prescribing positions without replacement. A second obstacle is that the conditional estimate is only available for mostly-uniform lines ( small), while the Thorp sweep is the binary case ; for a fixed grid the sweep operator is a matrix polynomial in whose behavior at is not controlled by real-segment bounds alone. Representations of very small "level" (first appearing on few tracked cards) need a separate sparse estimate.
binary_sweep_contraction_and_mixing): three conjuncts. BinaryContractionTarget: and every irreducible representation of Equiv.Perm (Slot d) on EuclideanSpace ℂ (Fin D) preserving norms, the operator norm of is at most (real power). Sign: for every , . UniformSweepMixingTarget: , total variation of the -fold convolution power translated by from uniform is at most . Physical shuffles are not modelled; the statement is about sweeps.conditional_main): grids are Grid with coordinates of (); trajectories are Holes with disjointness at every layer and coordinate-respecting steps; feasibility means some line choices realize them; the residual bijection is identified with the stabilizer of the input holes via a fixed reference completion; representations are UnitaryIrrep of that stabilizer; the Schatten moment is ; .all_grid_moment is a parameter-explicit form of the same induction under numerical largeness hypotheses and a small-perturbation hypothesis, kept as a plain item.The Thorp shuffle is a simple card-shuffling rule: cut a deck of cards into two equal halves, pair cards in corresponding positions, and let an independent fair coin decide the order within each pair when the pairs are interleaved. It is a standard test case for mixing-time methods and a building block in small-domain enciphering schemes. For every individual card is uniform after shuffles, but the joint order of all cards is much harder to control. Determining whether shuffles suffice to make the full permutation close to uniform was a long-standing question.
Index the positions by binary strings (in Lean, Card d := Fin d → Bool). One physical shuffle sends
with independent fair bits (Lean: step d ξ = rotate * pairSwitch ξ). After physical shuffles the rotations cancel, and the result is a coordinate sweep: one random matching switch in each coordinate direction. Write for the law on of physical shuffles (Lean: law d t, the fraction of coin sequences producing a given permutation).
For a partition let be the Specht module (the irreducible representation of indexed by ), of dimension , and let be the average of the sweep in . For an operator , and traces are unnormalized. The regular trace of the -th power is
in which the trivial representation contributes exactly . Total variation is .
There is an absolute real such that for every (so )
and for every integer with and every initial deck ,
The constant is not specified; only its existence and uniformity in are asserted. The goal is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. Since one sweep is physical shuffles, the second clause shows that Thorp shuffles bring the full permutation within of uniform from every starting deck. A counting argument on coin strings (Proposition 5.1 of the source) shows that at least physical shuffles are needed, so this order is optimal, improving the bound of Morris 2013. The regular-trace bound is stronger than an operator-norm bound for each irreducible: it controls all singular values with their multiplicities, which is what yields polynomially small total-variation distance.
Formalizing it. The statement is fully finite and explicit: an existential over one real constant followed by inequalities for each . A formal proof would certify an optimal-order mixing bound for a widely studied shuffle. Specht modules, Schatten-type traces via continuous functional calculus, and the shuffle law are all defined in the mission's definition file and can be reused for related shuffling problems.
Single-card and few-card statistics mix after one sweep, but the full permutation involves all bits of information, and the coin choices of a sweep interact across coordinates. The natural route—bounding the operator norm of separately in each irreducible representation—does not suffice, because the regular trace weights each representation by its dimension , and the number of partitions grows like . A uniform power must work simultaneously for representations of tiny dimension (very long first row), intermediate dimension, and dimension close to , and splitting the coordinates into row and column groups produces two symmetry decompositions that do not commute.
Fin d → Bool; permutations are Equiv.Perm (Card d); partitions of are Young diagrams of cardinality (Shapes (2^d)).Q d μ is the average over all coin sequences of length of the representation of run d d.absoluteTrace A P is the real part of the trace of CFC.rpow (CFC.sqrt (A⋆A)) P, i.e. ; regularTrace multiplies by finrank.sweepDistance d v σ is total variation of the law of physical shuffles, right-translated by , from the uniform weight . The integer is converted with Int.toNat; since and , and no truncation occurs.Many random permutations are analysed through what they do to a few labels at a time: the joint positions of chosen cards in a shuffle, or the images of a list of inputs under a block cipher built from a shuffle. Such partial information does not by itself control the whole permutation. The uniform law on the alternating group already has uniform images on every set of at most labels, yet it is at total-variation distance from uniform on . Converting partial-permutation estimates into full-permutation estimates therefore needs an additional argument, and this is the bottleneck in recent work on the Thorp shuffle, where fixed fractions of the deck were known to randomize quickly (Czumaj–Vöcking 2014; Czumaj 2015) long before the full deck was.
Let be a finite set of labels and , acting as maps from initial labels to final positions. For , let be the block subgroup of permutations that fix every label outside . Two permutations have the same images on exactly when they lie in the same left coset , so a bound on the law of those images is a bound on coset masses.
For a nonnegative weight on and a unitary representation of on a finite-dimensional complex inner-product space , the Fourier transform is , with . The Hilbert–Schmidt norm is unnormalized, . For the symmetric degree constant is
where ranges over the degrees of the irreducible complex representations of .
Partition into nonempty blocks and put . Let on have total mass at most one and satisfy
Then for every and every irreducible unitary of degree ,
No restriction is placed on the block sizes or on multiplicities in the restriction of to . The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. Theorem 1.1 is a quantitative transfer principle: a single law whose complementary partial images are never much heavier than uniform has a power saving in every irreducible representation of . With and it gives , which is enough for the principal application in the source (Corollary 3.6, p. 9): if the images of a uniformly chosen set of labels are close to uniform in average total variation and the sign mean tends to zero, then the product of just two independent copies of the permutation converges to uniform. This is the step used by the companion Thorp-shuffle preprints to turn fixed-list estimates into full-deck mixing in shuffles. The statement concerns arbitrary laws on and does not depend on any shuffle.
Formalizing it. The theorem is a finite inequality with explicit constants, so it is a natural target for machine checking. A proof would certify the partial-to-full transfer used by the Thorp mixing arguments, and would require reusable infrastructure: isotypic decompositions of restrictions to products of subgroups, Schur averaging, Hilbert–Schmidt and operator norms of group-algebra elements, and uniform bounds on symmetric-group Witten zeta sums. None of this is formalized yet.
The natural approach decomposes restricted to into tensor products of irreducibles of the blocks and bounds on each piece. This fails when a block type occurs with large multiplicity: a dimension count that pays for every copy gives no decay in . The bound must count each irreducible type of a block subgroup once, regardless of multiplicity, and must hold uniformly over all block sizes, which is why the constant is a supremum over every symmetric group. The Hilbert–Schmidt bound is harder than the operator bound, because it must control the whole Fourier matrix rather than its action on one vector.
Fintype with decidable equality; blocks are M : Fin b → Set X, nonempty, pairwise disjoint and covering. The block subgroup is blockSubgroup (M i), the permutations fixing each point outside M i.LeftCosetCap f H B: for every , , with the index H.index.complexFourier ρ f; hsNormSq is ; the operator norm is that of the associated continuous linear map; is Module.finrank ℂ V and the exponent is a real power.Equiv.Perm (Fin m), and is symmetricDegreeConstant u, an sSup over . The supremum is finite for every ; a solver must prove this boundedness, since sSup of an unbounded real set would be .At its critical weight, a self-avoiding path on the honeycomb lattice can make long excursions without paying an exponential cost. A basic quantitative question is how much of its total weight reaches the far side of a strip of height . Physics heuristics (Nienhuis's Coulomb gas and the conjectured scaling limit with boundary exponent ) predict that this crossing mass decays like . Rigorous results so far showed only that it tends to zero, with a polynomial upper bound with a tiny exponent.
The OpenAI preprint behind this mission, dated September 26, 2026 (source), claims the predicted power with bounded-factor constants: the crossing mass is comparable to , and the first horizontal-displacement moment of paths returning to the starting side is comparable to (Theorem 1.1, p. 2). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Use the honeycomb lattice dual to the equilateral triangular tiling of side one, with one edge direction horizontal; its vertices are the triangles up i j and down i j, where indexes the horizontal band. Let be the strip of bands. A path starts in the triangle up 0 0 (just above bottom port ), visits distinct triangles, moves between adjacent ones, and stays in bands . Its length is the number of visited triangles and its critical weight is with . An arch ends at up k 0 with (bottom port ); a bridge ends at a down triangle of the top band. Put and
Write if for all with fixed constants .
For every all sums above are finite, and with constants independent of ,
and is nonincreasing in .
The result itself. It establishes the predicted crossing power with uniform multiplicative constants, not just a logarithmic exponent, improving the qualitative decay of Beaton et al. and the polynomial upper bound of Krachun and Panagiotis. It is an input for the bridge-length and spatial-exponent results of companion preprints. The exponent of concerns an unnormalized displacement moment summed over all lengths; the fixed-length displacement conjecture and the scaling limit are different questions.
Formalizing it. The proof combines an exact boundary identity of Duminil-Copin–Smirnov type, finite-strip transfer matrices with integrable local relations, a Pfaffian that makes the stationary vector polynomial, and a comparison of the resulting positive integral with Bures–Laguerre ensembles. A formal proof would include the honeycomb boundary identity, the core of the connective-constant proof, which is itself a natural formalization target. No machine-checked honeycomb walk result of this kind is known.
The boundary identity (Lemma 4.2, p. 15) does not determine the power: it only gives between orders and . The preprint's route computes the arch moment first, as one coefficient of a ratio of Pfaffians (Proposition 4.1, p. 13), converts it into a positive -fold integral with Bures-type interaction (Section 5), and estimates that integral uniformly in by comparison with Laguerre laws (Section 6). The crossing power then follows from monotonicity and . A degree bound on the polynomial vacuum (Lemma 3.2, p. 10) is essential, because it turns interpolation into an identity argument.
ℤ × ℕ × Bool (column, band, up/down); adjacency joins an up triangle to the down triangles sharing an edge. Paths are Lists with Nodup, IsChain adjacent, head up 0 0, a prescribed last triangle, and all bands < N.rho ^ p.length on paths satisfying IsPath, and 0 otherwise; all masses are tsums over lists. The goal includes summability of each family, so the tsums are genuine sums.moment N = ∑' k : ℕ, (k+1) * K N (k+1), i.e. .Comparable f g asks for constants with for every ; powers are real rpow.Reusable contributions: the honeycomb boundary (parafermionic) identity in finite domains, and summability of critical walk weights in strips.
Random 3-SAT, a conjunction of random three-literal clauses on variables, is the classic test case for the typical behavior of satisfiability. Experiments placed the hardest instances near the density where half the formulas are satisfiable, and statistical physics predicts a sharp satisfiability threshold near . Once a limiting threshold is known to exist, a natural question is whether it is a computable real: is there an algorithm that, given , outputs a rational within of ? Existence alone does not imply this, since limits of computable sequences need not be computable (Specker 1949). This mission asks for such an algorithm.
The source of this mission is an OpenAI preprint dated September 27, 2026. Its contribution is computability of , beyond existence.
For , a proper random 3-clause chooses three distinct variables uniformly from and gives each an independent fair sign. Let be the conjunction of independent such clauses (sampled with replacement from the possibilities; the empty formula is satisfiable) and
A real is computable if a single algorithm, on input , halts with a rational satisfying .
There is such that for every fixed real
and one finite deterministic Turing machine, on input , halts with a rational with , using no oracle, advice, or noncomputable constant. Lean: OAI.FixedClauseThreshold.Computability.main, open on the platform.
The theorem makes the random 3-SAT threshold an effectively approximable constant: in principle its digits can be certified, although no efficiency bound is obtained. The method produces two families of finite certificates, rational lower bounds from a deletion estimate and rational upper bounds from finite hierarchical approximations of a soft pressure, and a fair search over them halts without any computable rate of finite-size convergence. The paper also gives a self-contained existence proof of (Theorem 4.4) for the same proper-clause model.
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.
Finite-size satisfiability probabilities are computable, but their convergence rate is unknown, so truncating at a finite certifies nothing. Lower certificates need an explicit bound on how far the finite-size centers can lie above the limit. Upper certificates are harder: one must show that above some finite, checkable object witnesses unsatisfiability in the limit. This requires a variational (Parisi-type) description of the limiting pressure of the soft constraint model, approximated by finitely many rational parameters with a proof that the approximation is complete at every rational density above the threshold.
ProperClause n k is Fin n → Option Bool with exactly defined entries; Formula n k m := Fin m → ProperClause n k; properSATProbability n 3 m is the exact counting ratio, equal to .MainStatement asserts with the two strict-side limits at , a sequence q : ℕ → ℚ with Computable (fun r => encode (q r)), a Nat.Partrec.Code c with c.eval r = some (encode (q r)), and for all .Infrastructure: Mathlib's Computable/Nat.Partrec.Code, finite counting for random formulas, Poisson clause processes, interpolation bounds, and Ruelle cascades for the upper certificates. Formalizations of Lemma 2.1 (finite-certificate search, purely computability-theoretic and reusable), Theorem 4.4 and Theorem 8.4 are welcome.
Add random clauses one at a time to a Boolean formula on variables until it first becomes unsatisfiable. The index of that first failure is the satisfiability hitting time of random -SAT. Its mean, divided by , converges to the satisfiability threshold; its variance measures the width of the transition window. Friedgut's sharp-threshold theorem shows the window is , but quantitative widths have remained far from the scale suggested by lower bounds. This mission asks for the order of the variance of for every fixed .
The source of this mission is an OpenAI preprint dated September 27, 2026.
Fix and . A proper -clause is an OR of literals on distinct variables; let be independent uniform choices among the signed proper clauses (signs fair, whole clauses may repeat). Put
and, for fixed , the capped hitting time . Since each assignment survives a clause with probability , is a.s. finite with all moments. Write
There are constants with
and for every fixed a constant with ; if then also for large . Hence for . Lean: OAI.RandomKSAT.variance_main, open on the platform.
The killing-probability exponent in the lifetime bound (Proposition 2.3) cannot be decreased, and the block-error term in the replacement lemma cannot be improved to uniformly. Lean: OAI.RandomKSAT.sharpness.
For the theorem determines the variance of the hitting time up to constants, so the transition window has width in the variance sense, matching Wilson's lower bound and improving Carenini's variance bound. For it leaves only a logarithmic gap, closed in a companion OpenAI preprint. Chebyshev's inequality then gives concentration of about at scale .
The results are proved in an OpenAI preprint; they have not been peer reviewed, and no machine-checked proof exists.
The Efron–Stein inequality reduces the upper bound to the expected squared delay caused by deleting one clause, which counts pairs of prefixes at which that clause is pivotal. Controlling this occupation time requires a uniform estimate relating how quickly a set of assignments is killed by shorter -clauses to its lifetime under -clauses, valid for every assignment set with no lower cutoff. Earlier arguments truncate the number of clauses incident to the deleted clause's variables at a logarithmic level, which costs a logarithm; keeping that number as a random parameter without destroying independence is the main obstacle. Appendix A shows the relevant exponents are sharp.
Clause n k is a dependent pair of a -element Finset (Fin n) and a sign vector on it; clauseLaw is uniform; streamLaw is the infinite product (Measure.infinitePi).firstFailure ω is the least with an unsatisfiable prefix, valued in ℕ∞; H = (firstFailure ω).toNat; T B ω = (min (firstFailure ω) ⌊Bn⌋).toNat. The infinite case has probability zero.variance is ProbabilityTheory.variance under streamLaw n k; ell, U are as displayed.blockKill u s S g is the probability that independent proper -clauses kill , and lifetime u k S is .Infrastructure: product measures on clause streams, Efron–Stein, conditioning on incidence patterns. Formalizations of Proposition 2.3 (lifetime from shorter-clause killing), Proposition 4.3 (conditional squared delay), Corollary 5.2 and Proposition 6.2 (linear variance lower bound) are welcome.
A random -SAT formula on Boolean variables is a conjunction of independent random clauses, each an OR of literals on distinct variables. As the clause density grows, the formula changes from almost surely satisfiable to almost surely unsatisfiable. Random -SAT is a central model in probabilistic combinatorics, the theory of algorithms and statistical physics: its threshold is where hard instances are expected to concentrate, and it is a proving ground for methods from spin-glass theory. The satisfiability conjecture, formulated explicitly by Chvátal and Reed, asserts that for each fixed the transition happens at a limiting density that does not drift with .
The source of this mission is an OpenAI preprint dated September 25, 2026, which gives an alternative proof of the existence of the limiting threshold.
Fix . For , a proper -clause chooses distinct variables among uniformly and gives each an independent fair sign, so each of the clauses is equally likely. Let be independent such clauses (sampled with replacement: two positions may hold the same clause) and
The ratio is the clause density.
For every fixed integer there is such that
No assertion is made at , and the value of is not identified. Lean: OAI.FixedClauseThreshold.main, open on the platform.
The theorem settles, for every fixed , the existence half of the threshold question: Friedgut's sharp transition happens at a location that converges. Previously this was known only for large (Ding–Sly–Sun) and for . Existence is a prerequisite for questions about the value of , its computability, and the fluctuations of the satisfiability hitting time, which companion OpenAI preprints address. The proof here proceeds through concentration of a capped last satisfiable index and a comparison between system sizes; it does not rely on Carenini's window.
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.
A sharp-threshold theorem gives a narrow window at each but no control of how the window's center moves with . Convergence needs a comparison between different system sizes, and interpolation methods from spin-glass theory deliver free-energy bounds, not hard satisfiability statements, and often only for even arity. The center must also be shown to concentrate polynomially, which requires bounding how many variables are forced along the clause process.
ProperClause n k is a function Fin n → Option Bool with exactly defined entries; some b at is the literal satisfied when .Formula n k m := Fin m → ProperClause n k (ordered, with replacement); properSATProbability n k m is the exact ratio of satisfiable formulas to all formulas, which equals under the uniform product law.HasLimitingThreshold k asserts with limits for and for at .Infrastructure: finite counting of formulas, Efron–Stein-type variance bounds, a deterministic concentration-to-convergence lemma (Theorem 5.1), and the Poisson/interpolation comparison with the transfer back to proper clauses. Formalizations of Proposition 2.2 (integrated forcing), Proposition 3.3 (polynomial concentration) and Theorem 5.1 are welcome.
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.Whether a single species of classical particles in , interacting only through a stable radial pair potential, can undergo a phase transition is one of the long-standing existence questions of rigorous statistical mechanics; it appears in Simon's list of problems in mathematical physics (Simon 1984). A phase transition is detected as a loss of regularity of the thermodynamic free energy. Lattice models and continuum models with extra structure (several species, many-body terms, hard cores, box-restricted interactions) were handled long ago; ordinary pair potentials finite at every positive separation remained the difficult case.
A radial pair potential is on with . It is admissible if is Borel measurable, is finite and locally bounded on , and
With and free boundary conditions, the canonical partition function is
and the canonical free-energy density at density is
In Lean, radialPotential φ takes values in EReal (value ⊤ at the origin), energy is the pair sum, partition φ β L N is the integral above, and HasCanonicalFreeEnergy φ f says for all .
There exist an admissible with as , a free-energy function realizing the canonical limit for every , a nonempty open interval and one such that for every the one-sided -derivatives exist and
This is Theorem 1.1 of the source (MainStatement). The goal is published on the platform with status Open.
The result itself. The theorem exhibits a genuine one-species pair potential, finite at every positive separation and with all cross-cube interactions retained, whose canonical free energy is not in temperature at a fixed density, with one critical temperature for an entire interval of densities. It does not concern the Lennard–Jones potential, does not identify the coexisting states as liquid/vapor/solid, and does not give a power-law tail ; formulations of the historical problem that require such a margin are not resolved by it. A companion preprint (A radial continuum phase transition with algebraic decay) gives a bounded potential with tail .
Formalizing it. The statement is fully explicit about the model, normalization, and boundary conditions, so a formal proof would remove any ambiguity about which version of the problem is solved. It requires thermodynamic limits for superstable continuum systems, convex-analytic facts about pressures, and a Kac/Lebowitz–Penrose comparison with uniform estimates, none of which is currently in Mathlib.
Density coexistence for a grand-canonical system does not by itself produce a temperature corner at a fixed density; one needs two supporting slopes of the pressure with the same density coordinate and different energy coordinates. Classical tools for transitions (Peierls arguments, reflection positivity, Kac limits) either need lattice structure, many-body terms, or a limit in which the potential itself changes. Here a single fixed potential must be built through infinitely many attractions at growing ranges, and the convex supporting-slope information must survive every approximation step while preserving stability and integrable tails.
EuclideanSpace ℝ (Fin 3); the potential is EReal-valued with ⊤ at the origin, and the Boltzmann weight is when the energy is ⊤. Stability is stated in EReal, which also rules out ⊥.Nat.floor; the limit is over real .HasDerivWithinAt on Iic βc and Ici βc, so both are finite real numbers; is pinned by HasCanonicalFreeEnergy for every , so it cannot be chosen freely near .In the low-temperature phase of the Sherrington–Kirkpatrick (SK) spin glass, the Gibbs measure is believed to split into many nearly separated pieces, and local dynamics such as heat-bath (Glauber) updates should take a very long time to move between them. Worst-case slow mixing (some bad starting state) is a weak statement: it says nothing about what happens when the chain is started from a typical equilibrium sample, which is how such chains are used in practice. This mission asks for a much stronger obstruction: for most equilibrium configurations held fixed as starting points, the dynamics is still far from equilibrium after a stretched-exponential time.
The source of this mission is an OpenAI preprint dated September 24, 2026. It covers the entire range , at zero field, for typical rather than worst-case starts.
For and independent standard Gaussians , put
In continuous-time heat-bath dynamics each site has a rate-one clock; when site rings, its spin becomes with probability , where . Let be its kernel and the discrete kernel that resamples one uniformly chosen site. For a fixed start ,
Let . For every fixed ,
The order matters: is drawn from and then held fixed as the starting state. Lean: OAI.SK.main, open on the platform; it writes the joint probability as the disorder average of the Gibbs mass of slow starts.
The theorem shows that throughout the low-temperature phase, a Gibbs-sampled start carries information that local updates cannot erase in time ; in particular (Corollary 1.2) every polynomial time scale is too short from a typical start. This separates the zero-field low-temperature SK model from the high-temperature and large-field regimes, where polynomial mixing holds. The exponent is not claimed to be optimal; numerical studies suggest .
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.
Integrating the transition kernel over the starting state recovers at every time, so averaging arguments are useless; the obstruction must be established start by start, for a set of starts of Gibbs mass tending to one. Free-energy barrier criteria in the style of Ben Arous–Jagannath do not apply to the pure quadratic SK covariance. The proof needs quantitative Parisi-type comparisons for constrained replica overlaps, and a mechanism ("locking") that forces small overlaps with a third replica to stay put when two replicas overlap substantially.
hamiltonian J x = (∑_{i<j} J_{ij} x_i x_j)/√n; disorderLaw n is the product of standard Gaussians over pairs .heatBath β J x y is the one-step kernel: average over sites of the conditional resampling probability, nonzero only when agrees with off (so holding is included).discreteKernel iterates it; continuousKernel β J t = ∑_k e^{-nt}(nt)^k/k! · K^k, the uniformized rate- chain, equivalent to rate-one clocks per site.continuousBadMass β n and discreteBadMass β n are of the Gibbs mass of starts with distance at time timeScale n = exp(n^κ) (resp. its floor).Infrastructure: finite Markov chains, Gaussian interpolation (Guerra–Talagrand bounds for constrained overlaps), Parisi functional regularity, and Gaussian concentration. The paper's Theorem 2.4 (quantitative free-energy comparison), Proposition 4.4 (absolute-overlap locking) and Proposition 6.1 (stretched-exponential coverage) are natural intermediate targets.
The Sherrington–Kirkpatrick (SK) model is the mean-field spin glass, and is its equilibrium critical point. Physicists expect critical slowing down: at a phase transition, local dynamics needs time growing polynomially in the system size to relax. For the SK model this was studied through linearized mean-field theory, dynamical equations for correlation and response, and simulations of equilibrium autocorrelations on an time scale. Rigorous results on Glauber dynamics had concentrated on high temperature, where mixing is fast. This mission asks for a rigorous total-variation obstruction at : most equilibrium configurations, used as starting states, are still far from equilibrium after time.
The source of this mission is an OpenAI preprint dated September 24, 2026.
At and zero field, let be independent for and
A heat-bath update at site resamples from its conditional law given the other spins. In continuous time every site has an independent rate-one clock (generator ); in discrete time each step updates a uniformly chosen site (kernel ). For a fixed start , and are the total-variation distances to .
For every deterministic with and every deterministic integer ,
Lean: OAI.CriticalSK.realized_equilibrium_initial_states, open on the platform.
With , and : for every , with probability tending to one,
For every fixed ,
with a separate Lean target for the lower bounds alone.
The theorem shows that at criticality the slow direction is visible from typical equilibrium starts, not only from adversarial ones, and pins the time scale to the spectral edge of the coupling matrix. Theorem 1.2 identifies the covariance scale , contrasting with bounded covariance at every . A companion OpenAI preprint uses Theorems 1.1 and 1.2 as inputs for matching upper bounds .
The results are proved in an OpenAI preprint; they have not been peer reviewed, and no machine-checked proof exists.
Averaging over the starting state gives back the stationary law, so the obstruction must be proved start by start. The slow observable is the projection on the top eigenvector of the coupling matrix; the difficulty is the static estimate that this projection is rarely small on the scale under the Ising Gibbs law. This requires edge-of-spectrum random matrix estimates, a precise comparison between the Ising law and a tilted spherical law, and control of the conditioning on the sphere.
hamiltonian W x = ∑_{i<j} W_{ij} x_i x_j; disorderLaw n is the product of gaussianReal 0 (1/n) over pairs .siteKernel W i is the heat-bath kernel on configurations agreeing off ; discreteKernel = n^{-1}∑_i siteKernel; continuousKernel W t = exp(t ∑_i (siteKernel W i - 1)).continuousGoodMass/discreteGoodMass are the Gibbs masses of starts with distance ; convergence in probability is written as for all .covarianceNorm is the Euclidean operator norm; linearRayleigh is a real sSup over nonzero (the quotient is bounded and the set nonempty).sInf over times at which all starts are within .Infrastructure: finite continuous-time Markov chains (matrix exponentials), GOE edge estimates, tridiagonal models, spherical integrals. The intermediate results Proposition 3.1, Theorem 5.3 and Proposition 5.4 are natural further milestones.
The Sherrington–Kirkpatrick (SK) model (1975) is the basic mean-field spin glass: Ising spins interact through independent Gaussian couplings of variance , so each spin is weakly coupled to every other one with random signs. The model is the testing ground for questions about disordered systems, about sampling from Gibbs measures, and about the performance of Markov chain Monte Carlo. A central question is whether Glauber (heat-bath) dynamics, which resamples one spin at a time from its conditional law, relaxes at a rate independent of the system size. Equivalently: does the Gibbs measure satisfy a dimension-free Poincaré inequality with respect to the heat-bath Dirichlet form?
The equilibrium high-temperature phase is , where the free energy equals its annealed value (Aizenman, Lebowitz and Ruelle 1987). Dynamical results had reached only part of this range.
The source of this mission is an OpenAI preprint dated September 24, 2026, which treats every fixed .
Fix . Let be a symmetric matrix with zero diagonal and independent entries for . The zero-field Gibbs law on is
Let be the conditional expectation under given all spins except ; it averages over and its -th flip with Gibbs weights. The unscaled Dirichlet form is
The discrete heat-bath chain picks a uniform site and resamples it, with transition operator ; its spectral gap is over nonconstant .
There is a finite constant such that
and consequently the discrete heat-bath chain has spectral gap at least with probability tending to one. Lean: OAI.SKGap.sk_main, open on the platform.
The theorem gives a size-independent relaxation time for continuous-time heat-bath dynamics (rate-one clocks) throughout the high-temperature phase, for every observable simultaneously on one disorder event. It extends the dynamical picture from to the full equilibrium range , where only linear-observable (covariance) control was previously known. A Poincaré inequality is the input for mixing bounds and for companion results on cutoff and critical slowing down.
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.
Dobrushin-type influence bounds fail because the sum of absolute couplings at a site grows like ; any argument must exploit cancellations from the random signs. Covariance bounds control only linear observables, while the Poincaré inequality must hold for all -dimensional families of test functions at once. The natural route through stochastic localization runs into rare observation events: an event of exponentially small probability can still carry most of the variance of a particular test function, and invertibility of the field equation must hold at every sufficiently accurate solution along the observation path.
Fin n → Bool, with spinValue mapping to ; couplings are indexed by pairs (Edge n) and symmetrized with zero diagonal by coupling.hamiltonian g 0 x = ½ ∑_{i,k} x_i J_{ik} x_k; mass, expectation, variance are exact finite sums over .conditionalExpectation g h i f x is the two-point Gibbs average over and its -th flip; dirichlet is the unscaled form .disorderLaw β n = Measure.pi (fun _ => gaussianReal 0 (β^2/n)) over the edges (variance ).discreteGap g is the infimum of over with positive variance.MainStatement β asserts a single for which both the Poincaré event and the gap event have probability tending to .Formalization needs Gaussian product measures, finite Gibbs measures and heat-bath operators, and the analysis behind the proof: matrix concentration, TAP/AMP-type field recursions and stochastic localization. Formal versions of the paper's intermediate results (for example Proposition 8.3, the terminal observation gap) are welcome.
The classical model (for , the classical Heisenberg model) places a unit vector at each site of the square lattice and favours alignment of neighbouring spins. It is the basic lattice model of a system with continuous symmetry. In two dimensions the Mermin–Wagner theorem rules out spontaneous magnetization at every positive temperature, but it does not say how fast spins decorrelate. For (the plane rotator) correlations decay only polynomially at low temperature — the Berezinskii–Kosterlitz–Thouless phase. For , Polyakov's 1975 renormalization-group argument predicts mass generation: exponential decay of correlations at every positive temperature, the lattice analogue of asymptotic freedom in four-dimensional non-Abelian gauge theory. A rigorous proof at low temperature has long been a central question of rigorous statistical mechanics.
Let be a finite subgraph of the nearest-neighbour square lattice , and let be edge strengths with . Put a spin at each vertex. The free-boundary Gibbs measure is
where is the uniform probability measure on the unit sphere and is the normalizing integral. There are no boundary spins and no external field. The two-point function is , and is Euclidean distance.
For every integer and every there are and such that, for every finite nearest-neighbour subgraph of , every and all ,
The constants depend only on and and may deteriorate as . The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. Uniformity over all finite subgraphs and strengths gives the same bound for free-boundary limits on boxes (Corollary 1.2 of the source) and for their subsequential infinite-volume limits, hence finite susceptibility. It confirms rigorously, for the spin two-point function, the mass-generation prediction for at arbitrarily low temperature, the regime left open by high-temperature and large- results, and contrasts sharply with the case. The source does not claim a transfer-matrix gap for all local observables, correlation-length asymptotics, or uniqueness of Gibbs states.
Formalizing it. The statement is a uniform estimate on explicit finite-dimensional integrals; a formal proof would certify a result the physics literature has expected since 1975. Groundwork includes Gibbs measures on products of spheres, rotation (Ward) identities, and random-cluster/sign-cluster representations, reusable for other lattice spin models.
Mermin–Wagner and McBryan–Spencer type arguments only show that order is destroyed and give polynomial bounds; they allow a zero decay rate and cannot distinguish from . Any proof must use the non-Abelian nature of the symmetry group, since the conclusion fails for . Exponential decay at high temperature (small ) follows from expansions, but at large spins are strongly aligned over long distances and no small parameter is available. Reducing to three components by conditioning produces random, dependent couplings, so the three-component estimate must hold uniformly over all strength arrays.
ℤ × ℤ; a LatticeGraph is a finite vertex set with a finite set of positively oriented nearest-neighbour edges (each undirected edge represented once). Strengths are functions G.edges → ℝ with , so deleting edges and weakening couplings are covered.Metric.sphere 0 1 of EuclideanSpace ℝ (Fin n); the single-site law is the normalized sphere measure (toSphere of Lebesgue measure); the configuration law is the product measure.correlation is the ratio of integrals ; the partition function is strictly positive, so the division is genuine.Random planar maps are graphs embedded in the sphere, chosen at random; they are the discrete models of two-dimensional quantum gravity. Decorating a map with a Fortuin–Kasteleyn (FK) random-cluster configuration with parameter couples the geometry of the map to a statistical-mechanics model (percolation, Ising, Potts), and the coupling changes the large-scale shape of the map. For the maps are expected to converge to Liouville quantum gravity surfaces; for the cluster weight is so strong that the map is predicted to become tree-like at large scales. This mission concerns that tree-like regime.
The source of this mission, an OpenAI preprint dated September 24, 2026, proves the finite-volume CRT prediction for every .
A rooted planar map is a connected graph embedded in the oriented sphere, up to orientation-preserving homeomorphism, with a distinguished dart (oriented edge); loops and multiple edges are allowed. For an edge subset , is the number of connected components of , isolated vertices included. For and , sample with according to
Let be graph distance on using all edges and .
For a standard normalized Brownian excursion on , ; the quotient by with the pushforward of Lebesgue measure is the Brownian CRT .
The Gromov–Hausdorff–Prokhorov (GHP) distance between compact metric probability spaces is the infimum, over isometric embeddings into a common space, of the maximum of the Hausdorff distance of the images and the Lévy–Prokhorov distance of the pushed-forward measures.
in distribution for the GHP topology, as through all positive integers. The Lean statement OAI.FKCRT.finite_fk_maps_converge_to_brownian_crt is open on the platform.
The theorem establishes the tree side of the geometric phase transition of FK planar maps at in the natural finite-volume setting: the law is conditioned on the total size, the metric uses every edge, and the measure is the degree measure. Feng's infinite-volume result does not imply it, and a limit of an unconditioned encoding walk gives neither conditioning nor metric control. Together with companion results for , it completes the picture surface versus tree.
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. A formal proof would also build reusable infrastructure: combinatorial maps as rotation systems, the GHP topology, and the Brownian CRT, none of which is in Mathlib.
The FK weight of a nonseparable block depends on its shape, not only on its size, so the block-weighted map results with uniform blocks do not apply, and exponential moments of block sizes are not available. The proof must show that the block tree is a critical Galton–Watson tree with finite offspring variance, and that graph distance along every ancestral path is asymptotically a constant times the depth, uniformly over all paths, using only a second moment.
Fin (2*(n+1)) (edge involution without fixed points, vertex rotation), connected, with (genus zero), modulo isomorphisms fixing dart 0. The Lean index corresponds to edges, and the scale is .Finsets of edge orbits; clusterCount counts components including isolated vertices; loops are omitted from adjacency only.MetricMeasureData packages a carrier, a distance and a measure; Valid means a compact metric probability space with Borel σ-algebra. ghpEDist is the infimum over pseudometrics on the disjoint union extending both distances.F continuous for ghpEDist at valid objects.A complete development needs Sheffield's inventory bijection or an equivalent finite word identity, Tutte's block decomposition, conditioned Galton–Watson tree limits with finite variance (Aldous; Broutin–Marckert), and GHP comparison lemmas. Contributions formalizing Proposition 2.2 (finite word identity), Proposition 4.3 (exact finite representation), Theorem 5.5 (uniform marked path sums) and Lemma 6.3 (metric and mass comparison) are welcome.
Plethysm — decomposing into irreducible -representations — is one of the oldest open problems in the representation theory of the general linear group, and it is central to geometric complexity theory, where the coordinate rings of Chow varieties of products of linear forms control lower-bound arguments. Foulkes' conjecture (1950) predicts that for there is a -equivariant injection . A natural candidate is supplied by a specific map, the canonical Foulkes–Howe map ; its surjectivity yields such an embedding by complete reducibility. Its image is the degree- part of the coordinate ring of the Chow variety of decomposable -forms, so surjectivity for large is a statement about that variety's normalization. The question is from which degree on the map is surjective, uniformly in .
Let be a finite-dimensional complex vector space and its symmetric algebra. is the span of products of vectors. For (, ), the canonical Foulkes–Howe map is the linear map determined by
where the outer products on the left and right are taken in and respectively. Equivalently: identify with symmetric tensors via averaging, multiply such tensors in , and project back. That this formula is well defined on is part of the content.
For every finite-dimensional complex and integers , , there is a unique linear map
satisfying the displayed formula on monomials, and is surjective.
The bound is not claimed to be sharp; the content is a stabilization degree polynomial in and independent of . The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. Surjectivity gives, by complete reducibility, a -equivariant embedding for (Corollary 4 of the source), e.g. the sixth-power comparison for . It answers positively the request for a polynomial bound in Landsberg's Problem 7.19, and it says that the coordinate ring of the Chow variety of decomposable -forms agrees with its normalization in every degree . Since the canonical map is known to fail to be injective at and , an explicit range of surjectivity is the right kind of statement for this specific map.
Formalizing it. The statement is purely algebraic and uniform in , , . A formal proof would need multilinear algebra over symmetric algebras (symmetric powers of symmetric powers), which is reusable for plethysm and invariant-theory projects.
Surjectivity is equivalent to the vanishing of every symmetric -linear form on whose diagonal vanishes on products of vectors. The naive induction on fails because the factors in different slots share a common product and cannot be varied independently; the dimension of also grows the space of such forms without bound, so arguments using a fixed basis or dimension count do not give a uniform bound. Brion's effective bound depends on , and regularity bounds for the normalization do not locate the top degree of the quotient that controls stabilization.
SymPow n V of Mathlib's SymmetricAlgebra ℂ V spanned by products of vectors, and is SymPow b (SymPow a V).IsFoulkesMap a b V μ states the monomial formula above, with the normalizing factor and the sum over -tuples of permutations of Fin a.The Hattori–Stallings trace refines the rank of a finitely generated projective module over a group ring into one complex number per conjugacy class of . These numbers enter group-ring Euler characteristics, where they retain information that an ordinary numerical Euler characteristic forgets. Bass's trace conjecture (complex group-ring form) predicts that the trace of every projective module vanishes at every conjugacy class of an element of infinite order. For torsion-free groups this forces the trace to be an integer rank, and that in turn implies the Kaplansky idempotent conjecture: a group ring of a torsion-free group over a field of characteristic zero has no idempotents other than and . Both questions date from the 1960s–1970s and were previously known only for restricted classes of groups (linear, elementary amenable, amenable, hyperbolic, or groups satisfying the Farrell–Jones conjecture).
This mission asks for a formal proof of the complex Bass trace conjecture for all discrete groups, with the torsion-free consequences as a milestone, 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 a group and its complex group ring. is the Grothendieck group of finitely generated projective right -modules. An idempotent matrix represents the module ; its Hattori–Stallings trace is the class of in , extended additively to . Identifying this quotient with finitely supported functions on conjugacy classes (sum the coefficients over each class), is the coefficient of at the class .
For the corollary: is torsion-free if its only element of finite order is . The canonical trace is , the augmentation is , , and applies entrywise. is the coefficient at , and is the augmentation rank.
Let be torsion-free. (i) For every and idempotent , ; hence and . (ii) For every commutative unital domain of characteristic zero, every with is or .
For every group , every and every of infinite order,
equivalently, is supported on conjugacy classes of finite-order elements.
The result itself. Theorem 1.1 holds for arbitrary groups, with no amenability, finiteness, assembly-map or homological-dimension hypothesis. Combined with Linnell's restriction it gives the integral Bass conjecture (Corollary 9.1, p. 29) and, via Berrick–Chatterji–Mislin, statements about homotopy idempotents on manifolds (Corollary 9.2, p. 29). Corollary 1.2 settles Kaplansky's idempotent conjecture in characteristic zero, including over commutative domains rather than only fields. The analytic Kadison–Kaplansky statement in and the positive-characteristic idempotent problem are not addressed.
Formalizing it. The statements need only group rings (MonoidAlgebra), matrices, projective modules and conjugacy classes, all in Mathlib, so both are precise algebraic targets. The proof combines finite path sums in the group with a Pfaffian cocycle (Sections 7–8) and a geometric vanishing theorem for sparse simplicial cycles built from separating filtrations, simplicial volume estimates and free actions on Cantor-type spaces (Sections 2–6). None of this exists in Mathlib; the sparse-chain vanishing theorem (Theorem 2.1, p. 6) is of independent interest. No machine-checked proof of either conjecture, even for special group classes, is known.
Previous proofs pass through analytic completions or assembly maps and therefore need hypotheses on the group (amenability, hyperbolicity, Farrell–Jones), or through cyclic homology and need finite homological dimension of the reduced centralizers. The preprint turns an idempotent and an infinite-order element into simplicial cycles of every even dimension with connected supports in one graph of bounded degree, and a cocycle evaluating to (Propositions 7.3 and 8.3, pp. 24–27). The difficulty is to show that invariant cocycles vanish on such sparse cycles in high dimension for an arbitrary acting group , with no bound on its homological dimension (Theorem 2.1, p. 6): naive filling arguments need either amenability or finite dimensionality.
Module (MonoidAlgebra ℂ G)ᵐᵒᵖ structure, by isomorphism and direct-sum relations (ModuleK0); the Hattori–Stallings trace factors through a presentation of each module by an idempotent matrix. Its values are ConjClasses G →₀ ℂ.BassTrace.K0.Group), matrixTrace (sum of identity coefficients of diagonal entries) and augmentedMatrix; part (ii) quantifies over every commutative domain R with CharZero R.TorsionFree G is the usual condition (every finite-order element is ).Let be a finite-dimensional algebra over a field. A finite-dimensional module is self-orthogonal if for every . Tachikawa's second conjecture asserts that over a self-injective algebra every self-orthogonal module is projective. It belongs to the cluster of homological conjectures around quasi-Frobenius algebras and dominant dimension recorded in Tachikawa's 1973 monograph, alongside the Nakayama, generalized Nakayama and Auslander–Reiten conjectures. Since automatically when is self-injective, it is exactly the self-injective case of the Auslander–Reiten conjecture. Enomoto and Marczinzik showed that Tachikawa's second conjecture for two-fold trivial extensions implies the Auslander–Reiten conjecture, so the two were expected to stand or fall together.
This mission formalizes the main theorem of an OpenAI preprint dated September 23, 2026 (source), which claims a counterexample over a symmetric algebra. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open (stated, not yet proved).
Let be the rational function field in three algebraically independent variables. Write . A finite-dimensional -algebra is symmetric if as -bimodules, where ; equivalently there is a -linear isomorphism with . Symmetric algebras are self-injective. For a finite-dimensional left -module , is computed in the category of left -modules.
There exist a finite-dimensional associative unital symmetric -algebra and a finite-dimensional unital left -module such that is not projective and
In particular Tachikawa's second conjecture is false, and since is self-injective the same pair is a symmetric counterexample to the Auslander–Reiten conjecture.
The result itself. The theorem disproves Tachikawa's second conjecture in the strongest natural class (symmetric algebras). Through an associated endomorphism algebra, the preprint further claims counterexamples to the classical, generalized and strong Nakayama conjectures, the Auslander–Gorenstein conjecture and the Wakamatsu tilting conjecture, persisting under every field extension (Corollary 1.2, p. 4), together with consequences for finitistic dimensions (Corollary 1.3, p. 5). Those corollaries are not part of this mission's goal. A companion preprint gives an explicit eight-simple triangular counterexample to the Auslander–Reiten conjecture.
Formalizing it. The statement uses only notions already in Mathlib (finite-dimensional algebras, projective modules, Abelian.Ext in ModuleCat), so it is a clean target. The proof needs trivial extensions , totally acyclic complexes, stable categories of symmetric algebras, Koszul computations of -algebras, and Hochschild bar complexes; these are reusable throughout representation theory.
Known non-examples come close but fail: Schulz's quantum exterior modules have vanishing higher self-extensions but nonzero ; Böhmler and Marczinzik have a commutative self-injective example with only . Vanishing in every positive degree requires controlling an infinite resolution. In the preprint, the passage to a symmetric algebra also requires vanishing of the negative part of a complete self-extension complex (condition (1.1), p. 2), which is what the transfer through the trivial extension , (Proposition 3.2, p. 12) consumes. Producing it needs two twists acting by distinct scalars on every nonzero homogeneous self-map space, and genuine bimodule lifts of stable maps (Proposition 6.1, p. 21).
FractionRing (MvPolynomial (Fin 3) (ZMod 2)), i.e. with independent variables.SymmetricOver k A asks for a -linear equivalence e : A ≃ₗ[k] Module.Dual k A with e (a*b) c = e b (c*a) and e (a*b) c = e a (b*c), i.e. a bimodule isomorphism .Counterexample asserts existence of A : Type with Ring and Algebra k structures, Module.Finite k A, symmetric; and M with compatible Module A, Module k (IsScalarTower), Module.Finite k M, ¬ Module.Projective A M, and Subsingleton (Abelian.Ext (ModuleCat.of A M) (ModuleCat.of A M) n) for all n > 0.In the representation theory of finite-dimensional algebras, vanishing of groups is the standard way of detecting projectivity homologically. The Auslander–Reiten conjecture (1975) asserts that a finitely generated module over an Artin algebra is projective as soon as
It arose from Auslander and Reiten's work on the generalized Nakayama conjecture and sits in a web of homological conjectures (Nakayama, Tachikawa, Gorenstein-projective, Auslander–Gorenstein) that were long expected to hold. A module is Gorenstein-projective if it is a cokernel in a doubly infinite exact complex of finitely generated projectives that stays exact under ; the Gorenstein-projective conjecture is the restriction of the Auslander–Reiten conjecture to such modules.
This mission formalizes the main theorem of an OpenAI preprint dated September 23, 2026 (source), which claims an explicit counterexample to both conjectures. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open (stated, not yet proved).
Let be the field of rational functions in three algebraically independent variables over . A finite-dimensional -algebra is an Artin algebra. For a left -module , is computed in the abelian category of left -modules. denotes the Jacobson radical. is Gorenstein-projective when for an exact complex of finitely generated projective modules such that every map into a projective that vanishes on the image of factors through . For a field extension , write and .
There exist a finite-dimensional -algebra and a finite-dimensional nonprojective left -module such that
is Gorenstein-projective, as -algebras, and . All of these conclusions hold again for and for every field extension .
The result itself. The theorem refutes the Auslander–Reiten conjecture for Artin algebras and the Gorenstein-projective conjecture; by extending scalars to an algebraic closure it also refutes them over an algebraically closed field of characteristic two. Since is then a nonprojective generator with no positive self-extensions, the generator formulation fails too. The structural data ( simple modules, split, ) place the example just outside the radical-cube-zero class where the conjecture is now known. The commutative case is not resolved.
Formalizing it. A formal proof would require Ext in module categories (available in Mathlib via Abelian.Ext), complete resolutions, triangular matrix algebras, trivial extensions and Hochschild cocycles, and base change of Ext under field extension. The counterexample is concrete, so much of the verification reduces to finite linear algebra over plus an infinite periodic-type resolution with uniform kernel formulas.
All positive results exploit some finiteness or rigidity (complete intersections, Cohen–Macaulay domains, radical cube zero, Auslander's condition), and the natural candidates for counterexamples (Schulz's quantum exterior algebra modules) have self-extensions that only vanish eventually, with . Vanishing in every positive degree, simultaneously against and , is the hard requirement. The preprint (Section 1.2, pp. 3–4) converts a suitable stable map over a symmetric algebra into a module over a triangular algebra (Proposition 3.1, p. 6), uses powers of for a resolution with uniform kernels, and kills every positive self-extension with two independent twists , using that has infinite multiplicative order.
FractionRing (MvPolynomial (Fin 3) (ZMod 2)), and the goal also asserts that the three generators are algebraically independent over .System (types in Type, with Ring, Algebra K, Module, and IsScalarTower K Λ Z instances). Conclusions asserts finite dimensionality over , ¬ Module.Projective Λ Z, the totally acyclic witness, Subsingleton of Abelian.Ext in ModuleCat for all against and against , a -algebra isomorphism , and .E with Algebra K E in an arbitrary universe; the module structure on must satisfy , which pins it to the standard one.Every module over a ring has a projective resolution, and its length, the projective dimension, measures how far the module is from being projective. Over a finite-dimensional algebra, some modules have infinite projective dimension; the finitistic dimension conjectures ask whether, among the modules whose projective dimension is finite, these finite values are bounded. The questions were publicized by Bass in 1960 and became central problems in the representation theory of finite-dimensional algebras, tied to many other homological conjectures (Nakayama, Gorenstein symmetry, Auslander–Reiten), each of which would follow from finiteness of the finitistic dimension.
The source of this mission is an OpenAI preprint dated September 23, 2026, which constructs a counterexample to the little finitistic-dimension conjecture over . A companion OpenAI preprint independently gives a characteristic-two example.
Let be a finite-dimensional unital algebra over . For a left -module , is the minimal length of a projective resolution. The little finitistic dimension is
and the big finitistic dimension is the same supremum over all left modules. Over a finite-dimensional algebra, finitely generated and finite-dimensional modules coincide. The little finitistic-dimension conjecture asserts for every such .
Injective left modules generate if the smallest triangulated subcategory of the unbounded derived category of left modules that contains them and is closed under arbitrary coproducts is the whole category.
The Lean statement OAI.LittleFinitistic.Main.exists_counterexample is open on the platform.
injective left -modules do not generate, and injective right -modules do.
Theorem 1.1 refutes the little finitistic-dimension conjecture: a single finite-dimensional algebra has finitely generated modules with terminating projective resolutions of unbounded length. Since , it also refutes the big version for Artin algebras, and by Rickard's theorem gives an algebra for which injectives do not generate the derived category. Corollary 1.2 shows that finiteness can fail on one side and hold on the other in the most extreme way, in contrast with Cummings' equivalence of universal finiteness and left–right symmetry.
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. Because many homological conjectures were known to follow from the finitistic-dimension conjecture, an independent check of a counterexample is of direct interest.
Positive results cover large classes (monomial, radical cube zero, representation dimension at most three), so a counterexample must escape all of them. The finitistic dimension of one fixed algebra must be unbounded, which requires encoding an unbounded family of terminating processes into fixed finite data. The paper realizes a "selection process" from an infinite finitely presented group algebra by a single bounded bimodule complex over a finite-dimensional algebra; making this realization uniform in the input module, and turning it into ordinary projective resolutions over a trivial extension, are the main obstacles.
A : Type with [Ring A] [Algebra ℂ A] and FiniteDimensional ℂ A; modules are objects of ModuleCat.{0} A, finiteness is Module.Finite A N.projectiveDimension is Mathlib's CategoryTheory.projectiveDimension, valued in WithBot ℕ∞, equal to ⊤ for infinite dimension; littleFinitisticDimension and bigFinitisticDimension are suprema over modules of finite projective dimension.Aᵐᵒᵖ.InjectivesGenerate uses HasDerivedCategory.standard and quantifies over isomorphism-closed triangulated properties closed under coproducts indexed by Type u and containing all injectives in degree 0.A complete development needs derived tensor products of bimodule complexes, trivial extension algebras and their bar resolutions, finite presentations of group algebras and their finite-dimensional representations, and (for the milestone) Rickard's theorem and Cummings' triangular algebra. Contributions formalizing Proposition 2.1 (selection), Theorem 4.1 (tensor realization) and Proposition 6.1 (bar splitting) are welcome.
For a field and a group , the group algebra consists of finite formal sums with , multiplied by extending the group law bilinearly. If has finite order , then , so has zero divisors. Kaplansky's zero-divisor conjecture asserts that this is the only source: if is torsion-free, has no nonzero zero divisors. Together with the unit and idempotent conjectures it is one of the central problems connecting ring theory, group theory and topology, and positive answers are known for large classes of groups (elementary amenable groups, groups with the unique-product property, torsion-free 3-manifold groups).
A group is torsion-free if with implies . It is finitely presented if it has a presentation with finitely many generators and relations. A classifying space (or ) for is a path-connected space with whose universal cover is contractible; it is finite two-dimensional if it is a finite CW complex with cells only in dimensions . A group with a finite-dimensional classifying space is automatically torsion-free, but the formal goal asks for both properties explicitly.
The coefficient field is , and is Mathlib's MonoidAlgebra (ZMod 2) G.
There exist a group and such that
This is the full Theorem 1.1 of the source, including its "Moreover" clause. The source proves existence probabilistically; it does not exhibit a concrete presentation. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. If correct, the theorem disproves Kaplansky's zero-divisor conjecture over , a problem open since the 1940s, and shows that torsion-freeness — even together with finite presentability and a 2-dimensional classifying space — does not force to be a domain. It implies that fails the unique-product property, and it bears on the implications among the Kaplansky conjectures (zero divisors, units, idempotents) and on approaches through the Atiyah conjecture and division-ring embeddings.
Formalizing it. The claim refutes a long-standing conjecture by an intricate probabilistic and topological construction, which is a strong case for machine verification. A full formal proof needs the probabilistic existence argument, planar separation, and asphericity of a 2-complex — none of which is a routine Mathlib application. Partial contributions (e.g. the characteristic-2 cancellation argument once asphericity and root separation are assumed, or the torsion-freeness of groups with finite-dimensional ) are welcome. A related machine-checked result exists only for the weaker non-unique-product property of Gardam's lattice (Mian–Siddique 2026).
Writing down whose product cancels in characteristic two is the easy part; the source does this by a parity argument on a graph of simultaneous steps. The hard part is two safeguards in the quotient group: both factors must remain nonzero (no vertex label other than the root can collapse to the identity), and the group must be torsion-free, which the source obtains by proving the 2-complex is aspherical. Standard tools — small-cancellation or CAT(0) criteria — are not applied; instead the source must exclude spherical arrangements of arbitrarily many paths of arbitrary length, which a union bound over sizes cannot handle.
TorsionFree G is the plain group-theoretic notion (, implies ); finite presentability is Group.IsFinitelyPresented.HasFiniteTwoDimensionalClassifyingSpace G asks for a Hausdorff, path-connected space with a finite CW structure on all of , no cells above dimension , at least one -cell, a group isomorphism , and a surjective covering map from a contractible space onto (so is aspherical). Requiring a -cell excludes only the case of free groups, whose group algebras are domains.Type and is existentially quantified together with its group structure; the zero divisors are elements of MonoidAlgebra (ZMod 2) G.