Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A linear filling inequality captures a form of large-scale negative curvature. The source asks whether a finite aspherical complex with that property must admit a geometric model of local nonpositive curvature. The source is OpenAI's September 2026 manuscript.
A finite complex has its usual barycentric realization. Asphericity means higher homotopy groups vanish. A linear disk-filling inequality bounds triangular face moves needed to fill an edge loop by a constant times its length.
The defined proposition MainStatement holds, namely that there exist a finite abstract simplicial complex K on vertices Fin n, with its standard barycentric realization |K| (nonnegative coordinate vectors summing to 1 supported on a face), a basepoint x in |K|, and a real constant C ≥ 0 such that all of the following hold. |K| is connected and aspherical at x, meaning every homotopy group π_{m}(|K|,x) with m ≥ 2 is trivial. K satisfies a linear disk-filling inequality: every closed edge path p that bounds some disk, where a disk is a chain of elementary moves (collapsing a repeated vertex, removing a spur a,b,a, or replacing a,b,c by a,c across a nondegenerate triangular face, which costs one) reducing p to a single vertex, admits such a disk using at most C times (length of p minus 1) triangular faces. The fundamental group G = π₁(|K|,x) is word hyperbolic in the four-point sense: for some finite generating set S and some δ ≥ 0, every a,b,c,d in G satisfy d(a,c)+d(b,d) ≤ max(d(a,b)+d(c,d), d(a,d)+d(b,c)) + 2δ, where d is word distance. G admits no geometric CAT(0) action: there is no proper cocompact isometric action of G on any nonempty proper complete metric space X (in universe u) that is CAT(0), in the sense that segments exist with the squared-distance comparison inequality. Finally, for every finite complex L whose realization is homotopy equivalent to |K|, there is no metric on |L|, inducing its given topology, that is geodesic and locally CAT(−1), meaning each point has a ball that satisfies the hyperbolic-cosine midpoint inequality cosh d(z,m) ≤ (cosh d(z,x)+cosh d(z,y))/(2cosh(d(x,y)/2)) for segment midpoints m.
The goal is OAI.HyperbolicObstruction.main.
The goal also excludes a finite homotopy-equivalent complex with a compatible geodesic locally CAT(-1) metric. It joins a finite topological model, a group-theoretic obstruction, and a metric-model consequence. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
A large-scale hyperbolicity inequality does not directly construct a local curvature metric. Excluding all geometric actions requires more than finding a defect in the original complex’s chosen metric.
Word hyperbolicity uses the four-point word-distance condition. Excluded CAT(0) actions are on nonempty proper complete spaces. The final metric must induce the finite realization’s existing topology; changing that topology is not permitted.
The shared definitions are supplied by HyperbolicObstruction. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Standard generator subsets define natural subgroups in an Artin group. The source asks whether arbitrary conjugates of these subgroups remain in the same class after intersection. The source is OpenAI's September 2026 manuscript.
A standard parabolic subgroup is generated by a subset of the standard generators. A parabolic subgroup is any conjugate of one. There is no requirement that its Coxeter subgroup be finite.
The theorem, which is admitted in the source with a placeholder proof, states the following for a Coxeter matrix M on a finite, linearly ordered index set S, with Artin(M) the Artin group presented on generators S by the braid relations: the word of alternating generators s,t,s,... of length M(s,t) equals the alternating word beginning with t, for each pair s,t. For any two subsets X and Y of S and any two elements g and h of Artin(M), there exist a subset Z of S and an element k of Artin(M) such that the intersection of the two conjugate subgroups g P_X g⁻¹ and h P_Y h⁻¹ equals k P_Z k⁻¹. Here P_T is the standard parabolic subgroup generated by the images of the generators in T, and conjugation by g is the subgroup whose members x satisfy g⁻¹xg in P. There is no spherical-type or other restriction on M, so the intersection of two conjugates of standard parabolic subgroups is itself a conjugate of a standard parabolic subgroup.
The goal is OAI.HarmonicArtin.ParabolicIntersections.unconditional_parabolic_intersections. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The selected goal is closure under binary intersection. Attached results also give arbitrary intersections controlled by at most the rank many members, unique parabolic closure, and dynamics for irreducible non-clique groups. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Conjugation obscures the standard generating subsets, so intersecting and alone does not describe the subgroup intersection. The target must produce both a new subset and a new conjugating element.
The generating type is finite and linearly ordered. The Coxeter-matrix convention encodes an infinite label by zero. The dynamics milestone has additional irreducibility and non-clique assumptions; those are not imposed on the intersection theorem.
The shared definitions are supplied by ArtinParabolicIntersections. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Artin presentations often admit useful geometric models of nonpositive curvature. The source constructs a finite presentation designed to obstruct every geometric action on a proper CAT(0) space. The source is OpenAI's September 2026 manuscript.
A geometric action is an isometric group action that is proper and cocompact. CAT(0) is expressed by existence of geodesic segments and Euclidean comparison inequalities. The target uses one explicit Artin matrix on 116 generators.
The following explicit matrix on 116 generators is symmetric, has diagonal entries 1, and has every off-diagonal entry in {2, 3, ∞}, and that its Artin group admits no geometric action on any nonempty proper CAT(0) metric space. Index the generators by 0, …, 115. For each b = 0, 1, 2, form the ordered block (b, (b + 1) mod 3, 5 + 37b, …, 41 + 37b). Distinct generators have matrix entry 3 if they are consecutive in a block; otherwise they have entry 2 if they are nonconsecutive members of a block or one is 3 or 4 and the other is 0, 1, or 2; all remaining entries are ∞. The Artin group has these generators and, for each finite entry n, equates the two alternating words of length n starting with the corresponding generators. Here a CAT(0) space is a geodesic metric space satisfying Euclidean triangle comparison, and proper means that closed balls are compact. The excluded geometric action is an action by isometries such that, for every compact set K, only finitely many group elements g satisfy gK ∩ K ≠ ∅, and some compact set has translates covering the whole space. Thus, for every nonempty proper metric space and every action of this explicitly presented group, at least one of the CAT(0), isometry, compact-intersection finiteness, or compact-covering conditions fails.
The goal is OAI.ArtinCAT0.main.
The formal statement verifies the matrix’s structural properties and excludes actions of the resulting explicit group. It does not merely assert that some unspecified Artin group has an obstruction. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Ruling out one candidate complex is insufficient because the conclusion ranges over all nonempty proper metric spaces and actions. The algebraic relations must force a contradiction with geometric-action properties themselves.
The matrix is generated by three overlapping length-39 blocks plus sentinel relations. Properness is compact-intersection finiteness and cocompactness is coverage by translates of a compact set. The action target is universe-polymorphic.
The shared definitions are supplied by ArtinCAT0. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
A classifying-space problem asks whether a natural complex captures a group without additional higher homotopy. The source addresses the finite-rank Artin problem through the lifted spherical-cell complex. The source is OpenAI's September 2026 manuscript.
An Artin group is presented by alternating braid relations from a Coxeter matrix. A subset of generators is spherical when its associated Coxeter parabolic subgroup is finite. Lifted cells pair a group element with such a subset, with incidence determined by reduced coset words.
For every Coxeter matrix M indexed by a finite type S of standard generators, the topological space SalvettiCover(M) is contractible. The Artin group Artin(M) is the free group on S modulo the braid relators, one for each ordered pair (s,t): the alternating word s t s t ... of length M(s,t) times the inverse of the alternating word t s t s ... of the same length. A subset T of S is spherical when the standard parabolic subgroup of the Coxeter group generated by the simple reflections in T is finite. A lifted cell is a pair (a,T) of an Artin group element and a spherical subset. One lifted cell (a,T) is a face of (b,U) when T is contained in U and there is a word w in letters of U that is reduced in the Coxeter group (its Coxeter length equals the word length), is of minimal length in its coset with respect to the parabolic subgroup generated by T, and satisfies a = b times the image of w in the Artin group. The preorder on lifted cells is the reflexive transitive closure of this face relation, and SalvettiCover(M) is the geometric realization, as a topological space, of the nerve of that preorder viewed as a category.
The goal is OAI.HarmonicArtin.salvetti_cover_contractible.
The goal makes the full topological realization contractible, rather than only asserting vanishing of a selected homotopy group. It supplies a precise target for the covering-space component of the source. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Local spherical pieces need not automatically fit into a globally contractible realization. The face relation and its transitive closure must retain the interaction between Artin words and Coxeter length.
SalvettiCover is the geometric realization of the nerve of the lifted-cell preorder. The generator type is finite but need not be equipped with a chosen enumeration. The mission preserves this published model instead of substituting a different complex.
The shared definitions are supplied by HarmonicArtin. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Simplicity constrains normal subgroups, amenability provides almost invariant finite sets, and finite presentation gives a finite description by generators and relations. The source seeks an infinite group satisfying all three conditions together. The source is OpenAI's September 2026 manuscript.
A simple group is nontrivial and has no proper nontrivial normal subgroup. Følner amenability means that every finite collection of translations changes a suitable nonempty finite set by a small relative symmetric difference.
There exists a group G, with underlying type in the lowest universe, that is infinite, finitely presented, simple, and Følner-amenable. Here FolnerAmenable(G) is the defined proposition that for every finite subset K of G and every real ε>0 there is a nonempty finite subset D of G such that, for every g in K, the symmetric difference between the left translate gD={g·d : d∈D} and D has cardinality strictly less than ε times the cardinality of D. Simple means G is nontrivial and has no normal subgroups other than the trivial one and G itself, and finitely presented means G has a presentation with finitely many generators and finitely many relations.
The goal is OAI.SimpleAmenable.main.
The target supplies one group with simultaneous infinitude, simplicity, finite presentation, and the specified Følner property. Each condition is part of the conclusion. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Finite generation is weaker than finite presentation, and an amenability argument need not survive an arbitrary quotient or enlargement used to enforce simplicity. The construction must preserve all four properties.
Finite sets are Finsets and translations act on the left. The Følner witness is nonempty and the inequality is strict for every member of the given finite set. No uniform bound on the number of generators or relators is imposed.
The shared definitions are supplied by SimpleAmenable. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Residual finiteness means that finite quotients can distinguish every nonidentity group element. The source asks whether coarse negative curvature forces this separation property even without torsion. The source is OpenAI's September 2026 manuscript.
A torsion-free group has no nonidentity element whose positive power is the identity. A word-hyperbolic group admits a finite generating set whose Cayley graph has geodesic triangles of uniformly bounded thickness.
The theorem states, without a verified proof (it is admitted), that there exists a group G, in the lowest universe Type, that is torsion-free, word-hyperbolic, and not residually finite. Torsion-free means that for every g in G and every positive integer n, g^n = 1 implies g = 1, so no nonidentity element has finite order (this does not assert unique roots). Word-hyperbolic means that there is a finite subset S of G whose unit-edge Cayley graph (the simple graph with the multiplicative Cayley adjacency determined by S) is connected, which says that S generates G, and a natural number δ such that geodesic triangles are uniformly δ-thin. Precisely, for all vertices x, y, z and walks p from x to y, q from y to z and r from z to x, each of which is a geodesic (its length equals the graph distance between its endpoints), every vertex of each side lies within graph distance δ of some vertex on one of the other two sides. The statement also requires that G fail the Mathlib property Group.ResiduallyFinite.
The goal is OAI.Release075.main.
The goal puts a geometric condition and failure of finite-quotient separation into one existential statement. Torsion-freeness is retained explicitly. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Hyperbolicity concerns large-scale word geometry, whereas residual finiteness quantifies over every finite quotient. Checking a finite list of quotients cannot establish the required failure.
Hyperbolicity is encoded by vertexwise thin triangles in a connected unit-edge Cayley graph for some finite generating set. Torsion-freeness is the positive-power condition and does not mean a unique-roots property. Residual finiteness uses the Mathlib definition.
The shared definitions are supplied by TorsionFreeHyperbolic. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Periodic groups have only finite-order elements, but this local condition does not visibly bound the group’s size. The source asks whether an ordinary finite presentation forces such a group to be finite. The source is OpenAI's September 2026 manuscript.
A periodic group satisfies: for each element there is some positive power equal to the identity. A Steinberg group is generated by elementary root symbols subject to additive, commuting, and multiplicative commutator relations over a coefficient ring.
Two propositions hold together. For a natural number n and a ring R, a root is an ordered pair (i,j) of distinct indices in {0,…,n−1}, and the Steinberg group St(n,R) is the group generated by symbols x_{ij}(a), one for each root (i,j) and each a in R, subject to three families of relations: x_{ij}(a+b) = x_{ij}(a)x_{ij}(b); the commutator [x_{ij}(a), x_{kl}(b)] = x y x⁻¹ y⁻¹ is trivial whenever j≠k and i≠l; and for pairwise distinct i, j, k, the commutator [x_{ij}(a), x_{jk}(b)] equals x_{ik}(ab). A group is periodic if every element g has some positive integer m with gᵐ = 1. The first statement, MainStatement, asserts that there exist a ring R in the lowest universe, carrying an algebra structure over ZMod 2, such that St(12,R) is infinite, finitely presented, and periodic. The second statement, BurnsideStatement, asserts that there exists an infinite, finitely presented, periodic group G. The theorem asserts the conjunction of these two existence claims, with no bound on the orders of elements.
The goal is OAI.SourceBurnside.thm_main.
The formal goal includes both this ring-based construction and the general existence of an infinite finitely presented periodic group. It preserves the stronger concrete realization through a Steinberg group. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
A finite collection of torsion generators does not imply that every product has finite order. Conversely, infinitely many torsion relations do not supply an ordinary finite presentation. Both requirements must hold for the same infinite group.
The orders of elements may vary; no common exponent is asserted. Finite presentation is Mathlib’s group property. The goal does not include the manuscript’s separate nil-algebra, radical-algebra, or unitization conclusions.
The shared definitions are supplied by PeriodicGroup. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
The Partition Principle reverses the cardinal comparison provided by a surjection without requiring a section. The source studies whether this weaker form of comparison can hold while full Choice fails. The source is OpenAI's September 2026 manuscript.
The Partition Principle says that a surjection from onto implies an injection from into . Ordinal-indexed Choice provides choices for families indexed by internal ordinals. The formal consistency predicate rules out finite derivations of falsity in a specified first-order proof system.
A relative consistency result in pure first-order set theory with membership and equality: if ZF, meaning the full axioms of extensionality, empty set, pairing, union, power set, infinity and foundation together with every instance of Separation and Replacement for arbitrary formulas with arbitrary parameters, and without Choice, is consistent, then so is the theory obtained by adding three sentences to ZF. Consistency is syntactic: no finite classical natural-deduction derivation of falsity exists from the theory, allowing any finite supply of free variables. The added sentences are the Partition Principle PP, which says that whenever there is a set surjection from X onto Y then there is a set injection from Y into X, with functions coded internally as sets of Kuratowski pairs and the injection not required to be a section of the surjection; the ordinal-indexed Choice axiom ACwo, which says that for every internal von Neumann ordinal (transitive and internally well-ordered by membership) every family of nonempty sets indexed by it has a choice function; and the negation of full Axiom of Choice AC, which says that every set of nonempty sets has a choice function.
The goal is OAI.PartitionConsistency.main_consistency. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The chosen goal is the relative syntactic consistency claim. A separate attached model-construction target gives a transitive extension under its stronger ground-model assumptions. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
The function and ordinal notions must be expressed internally in the set-theoretic language. An ambient use of classical choice cannot substitute for satisfaction of the internal Choice sentence.
The source theory includes every Separation and Replacement instance with parameters. The auxiliary model target assumes a countable transitive ground and a standard inaccessible in that ground; it is not presented as an assumption-free construction over arbitrary countable transitive models.
The shared definitions are supplied by PartitionConsistency, PartitionPrinciple. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
A Diophantine representation translates membership in a computably enumerable set into solvability of one polynomial equation. The source asks whether the entire auxiliary witness can always be made unique. The source is OpenAI's September 2026 manuscript.
A single-fold representation uses an integer polynomial evaluated at natural-number inputs and witnesses. An input belongs to the represented set exactly when a witness makes the polynomial zero, and any two complete witnesses at the same input must coincide.
The proposition MainStatement holds, which asserts a single-fold Diophantine representation result with positive lengths. For every n ≥ 1 and every set S of n-tuples of natural numbers that is recursively enumerable (the predicate a ∈ S is REPred, i.e. semi-decidable), there exist m ≥ 1 and an integer polynomial P in the n input variables and m witness variables such that P represents S. Here evaluation takes natural-number inputs a and witnesses w, casts them to integers, and evaluates P over ℤ. Representation means that for every input a, first, a lies in S exactly when some witness w ∈ ℕ^m satisfies P(a,w)=0, and second, any two witnesses w and v with P(a,w)=0 and P(a,v)=0 are equal. So there is exactly one witness for members of S and none for nonmembers, and the uniqueness condition is imposed on every input a, with all witness coordinates included in w.
The goal is OAI.SingleFold.main.
The target strengthens mere existential representation by enforcing uniqueness across every auxiliary coordinate. It covers all recursively enumerable sets of positive-length natural tuples. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Encoding a computation with extra witnesses can introduce many choices that do not affect the represented input. Every such auxiliary choice must be controlled, rather than leaving hidden coordinates outside the uniqueness assertion.
The input length and witness length are positive naturals. REPred expresses recursive enumerability. Polynomial coefficients and evaluation are integral, while variables range over naturals cast into the integers. The goal is existential and does not require one fixed universal polynomial.
The shared definitions are supplied by SingleFold. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
An inequality involving only four rows can feed into a recursion for a much larger permutation shuffle. The source seeks an exponent strictly below two that survives a small perturbation of the uniform permutation law. The source is OpenAI's September 2026 manuscript.
A permanent expectation averages the product of four selected entries, one from each row and each column, over a probability law on the 24 permutations. Uniform marginals require every row to choose each column with probability .
The theorem is stated as admitted, not proved here. Sites are Fin 4, and a law is a real-valued mass function ν on the 24 permutations of the four sites. It states that there exist a real exponent p₀ with 4/3 < p₀ < 2 and a real ε > 0 such that the following holds for every law ν that is a probability law (all masses nonnegative and summing to 1), has total variation distance from the uniform law less than ε (total variation being half the sum over permutations π of |ν(π) − 1/24|), and has uniform marginals (for every pair of sites i and j, the total mass of permutations with π(i)=j equals 1/4). For every 4-by-4 array f of real numbers with all entries f(i,j) ≥ 0, the permanent expectation Σ_π ν(π) ∏_i f(i, π(i)) is at most the product over the four rows i of the normalized ℓ^{p₀} norm of row i, where the norm of a row g is ((Σ_j g(j)^{p₀})/4)^{1/p₀}, using the uniform counting normalization with division by 4.
The goal is OAI.FourRow.robust_permanent. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The goal is uniform over all nonnegative arrays and all probability laws within the chosen total-variation neighborhood that have exactly uniform marginals. The shared Thorp bundle is included as a separate supporting target. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Near-uniformity alone does not enforce the marginal identities. The exponent improvement must hold even for highly uneven nonnegative row entries.
The law has nonnegative real masses summing to one. Its distance from the uniform law is strictly less than the selected , and row norms use division by four. No explicit value for the existential exponent or radius is imposed.
The shared definitions are supplied by FourRowPermanent, ThorpRemaining. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Signed tensor components separate different sources of permutation symmetry. The source uses their diagram entropies to budget high moments of the Thorp sweep. The source is OpenAI's September 2026 manuscript.
A signed occurrence is an injective equivariant map from a tensor product of three Specht modules into the target module, with the second factor transposed. The weighted moment is the target dimension times the trace of a power of the sweep’s positive square.
There is a constant η₀>0 such that for every η with 0<η<η₀ there is a κ₀ with 0<κ₀<η/256 such that for every κ with 0<κ<κ₀ there is a positive integer power r, depending only on η and κ, with the following property for every d≥1. Let λ be a partition of 2^d (a Young diagram with 2^d cells), and let u+v+l=2^d with partitions α of u, β of v and γ of l, such that the signed occurrence condition holds: there is an injective complex-linear map from the tensor product of the Specht modules S^α ⊗ S^(β′) ⊗ S^γ, where β′ is the transpose of β, into S^λ that commutes with the action of S_u×S_v×S_l, embedded in S_(2^d) as block permutations on the consecutive blocks of sizes u, v and l. Here Specht modules are the cyclic submodules of the regular representation of the symmetric group generated by the polytabloid built from the row and column subgroups of a fixed tableau. Identify {0,…,2^d−1} with binary strings of length d, and for each coordinate i let the layer operator be the average of S^λ over the subgroup of permutations preserving every binary coordinate except the i-th. Let the sweep operator be the product of these d layer operators in reverse coordinate order, and let the sweep square be TT with T the sweep operator. Define the weighted moment as dim S^λ times the real part of tr((TT)^r). Then the logarithm of this moment, taken as −∞ when the moment is zero, is at most coefficient(η,d)·H(α,β) + remainderBudget(κ,d,l). Here coefficient(a,d)=a(1−1/(2√d)), the signed entropy H(α,β) is the sum, over all row lengths a of α and of β, of a·log((u+v)/a), and the remainder budget is 0 if l=0 and otherwise max(0, coefficient(κ,d)·l·log(2^d) − l·log(2^d/l)).
The goal is OAI.SignedSweeps.signed_occurrence_moment_bound. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The target makes the moment power depend only on two small budget parameters, uniformly over cube dimension and every signed occurrence. Supporting targets include the type-angle estimate and a shared mixing bundle. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Ignoring the signed occurrence hypothesis loses the representation-theoretic connection between the component diagrams and the target. The remainder diagram must be charged separately, including its empty case.
The quantifier order is , then each small , then , then each small , then one positive integer . Zero moments have logarithm minus infinity in EReal. Independent source groups stay separate references.
The shared definitions are supplied by SignedSweepMoment, SpinAngle, ThorpRemaining. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Compatibility of independently chosen row and column permutations controls how two families of local symmetries overlap. The source connects a weighted compatibility estimate to Thorp spectral bounds. The source is OpenAI's September 2026 manuscript.
A row system chooses a permutation in each row of an by array; a column system chooses a permutation in each column. They are compatible when their combined routing remains injective down each column. Nonnegative weights may bias each local permutation.
The proposition WeightedCompatibilityTheorem holds. Here, for natural numbers A and D, Rows assigns to each i in Fin A a permutation of Fin D, and Cols assigns to each j in Fin D a permutation of Fin A; a pair (r,c) is Compatible if for every column j the map i ↦ c(r_i(j))(i) is injective. The weightedCompatibility of real weight families w (indexed by i and a permutation of Fin D) and v (indexed by k and a permutation of Fin A) is (AD)! / ((D!)^A (A!)^D) times the uniform mean, over all pairs (r,c), of the indicator of compatibility times ∏_i w_i(r_i) ∏_k v_k(c_k). The marginalFactor for θ and a weight function u is the θ-th power of the uniform mean of u^(1/θ). The stated claim is that there exist reals L, C₀, m₀ > 0 such that for all natural numbers A and D, with n = AD, m = √n and θ = 1 − L/log m, whenever m ≥ m₀, θ > 0, and both A and D lie between m/2 and 2m, then for all nonnegative weight families w and v, weightedCompatibility(A,D,w,v) ≤ exp(C₀ n^(54/100)) · ∏_i marginalFactor(θ, w_i) · ∏_k marginalFactor(θ, v_k).
The goal is OAI.ThorpCompatibility.weightedCompatibility_main. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The formal goal is an entropy-type inequality for arbitrary nonnegative local weights in sufficiently large balanced rectangles. It supplies a concrete combinatorial estimate that can support spectral analysis. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
The compatibility indicator couples all row and column choices. A product of separate marginal expectations loses the injectivity constraint and cannot directly recover the stated exponent.
The rectangle satisfies , with both side lengths between and . The theorem existentially chooses positive and assumes positive . The marginal factor is the th power of the uniform mean of the weight to power .
The shared definitions are supplied by ThorpRemaining, ThorpWeightedCompatibility. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Row and column symmetries organize how permutation representations respond to a coordinate sweep. The source seeks dimension-dependent contraction strong enough to control the full deck. The source is OpenAI's September 2026 manuscript.
For a Young diagram , let be its Specht dimension and its averaged sweep operator. A Schatten norm measures all singular values, not only the largest one. The goal seeks one weight function on diagrams and a uniformly bounded family of norm exponents.
There exist a function W assigning a strictly positive real weight to every Young diagram, a real constant pStar ≥ 2, and exponents p(d) for each d ≥ 1 with 2 ≤ p(d) ≤ pStar, such that the following holds for every d ≥ 1 and every Young diagram μ with exactly 2^d cells. Let dim(μ) be the complex dimension of the Specht module of μ, spanned by the translates of the polytabloid in the permutation space on tabloids of μ, regarded as a Hilbert subspace. Let the Fourier sweep be the average, over all sequences ω of d coin configurations, of the unitary operator by which the product of d card-shuffling steps run(d,d)(ω) acts on this space; each step composes a cyclic rotation of the d-bit positions with a pair switch that flips the first bit according to a coin function of the remaining bits, and the 2^d card positions are identified with the cells of μ by a fixed bijection. Then dim(μ)^(3/4) ≤ W(μ) ≤ dim(μ); W(μ) times the p(d)-th power of the Schatten p(d)-norm of the Fourier sweep (the p(d)-th root of the sum of the p(d)-th powers of its singular values) is at most 1; and the operator norm of the Fourier sweep is at most dim(μ)^(-3/(4·pStar)). The proof is admitted in the source rather than established.
The goal is OAI.CubeShuffle.WeightedSweep.weighted_sweep_moments. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The target gives both a weighted singular-value estimate and an operator-norm consequence. These quantify contraction across representations of widely differing dimensions. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
An operator norm bound alone does not control the dimension-weighted sum of all modes. The weight and Schatten exponent must be chosen uniformly across every diagram of size .
The goal is weighted_sweep_moments, with , positive diagram weights, and one finite upper exponent . The finite-dimensional complex inner-product representations and the physical -step sweep are those of the supplied definitions.
The shared definitions are supplied by OccupiedOverlap, WeightedSweepMoments. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
The routing paths of different cards share switches. The source controls the resulting dependence through partial-permutation densities and representation contraction. The source is OpenAI's September 2026 manuscript.
Positions form a binary cube. A sweep operator averages the Specht-module action of all switch outcomes. The defect of a Young diagram is its number of cells outside the first row, and the level scale is .
The theorem states, as an admitted result, that nine separate formal statements about Thorp-shuffle routing hold simultaneously. Throughout, Card d is the set of d-bit strings (the 2^d cards), the sweep operator of a Young diagram mu (with the d bits relabelled to its cells by a bijection e) is the average over all butterfly switch settings of the Specht-module action of the butterfly permutation (or of its inverse, if the reverse flag is set), k = |mu| minus the first row length measures how far mu is from a single row, and the level scale of n and k is k(1+log(n/k)). (1) Adaptive: for some positive constants c, c', C, c0, for every d, mu, e and reverse flag, with h the level scale of 2^d and k, and D the dimension of the Specht module, the norm of the positive square F = S S* of the sweep operator S is at most exp(-c h), the trace of F^4 is at most exp(-c' log D + C h), and the norm of S is at most exp(-c0 (log D + h)). (2) Casimir: for some positive a and C, the palindrome row moment of order 1/64, raised to 64/65, is at most exp(C times level scale) for every injective k-tuple of cards; for every mu with k>0, the operator norm of the palindrome-shuffle operator K is at most exp(-a times level scale) and dim(Specht module) times the real trace of K^65 is at most exp(C times level scale); and for some positive integer l, from any starting permutations the total variation distance of the law of ld shuffle steps from uniform on all permutations of 2^d cards tends to 0 as d tends to infinity. (3) Dense truncation: for every density rho>0 and epsilon>0 there is c>0 such that, for r = rho 2^d, every injective r-tuple x, the proportion of palindrome-Benes coin outcomes whose density exponent exceeds r(H(rho)+entropy correction(rho)+epsilon) is at most exp(-c r), where H is a supremum over admissible cycle-length laws and allocations defined in the source. (4) Sparse contact: there are positive constants such that, for d at least 1 and 1 <= k < 2^d, the squared sweep-operator norm is at most min(1,(C d k/2^d)^(k/2)), the operator is zero when k=1, and the squared norm is also at most C^k (1+d)^(Ck) (k/2^d)^(k/2). (5) Harmonic: there exist positive constants (with 0<delta<1) and a positive integer p0 such that, for k>0, the norm W of K is at most exp(-c L), at most exp(CL) f^(-zeta) with f the dimension of the Specht module of the tail diagram (mu with its first row removed), and at most exp(-c1 L) D^(-c2); the sweep operator norm is at most exp(-cTail(L+log f)); and for each tuple length k with 1<=k<=2^d, the reflected tuple kernel has (1+delta)-moment bounded by exp(C times level scale) and its p0-th power trace bounded by exp(C times level scale). (6) Smoothing: there is an integer u>=1 and constant C such that the u-th power of every reflected sweep kernel on injective l-tuples has entries at most exp(Cl) divided by the falling factorial of 2^d, and the trace of the u-th power of the full-length kernel is at most exp(C 2^d). (7) Tail: for some p in (1,2] satisfying a density condition (L^p moment bounds of normalized kernel rows and columns by exp(C l)) and some C, the squared sweep-operator norm is at most exp(C k) times the dimension of the tail diagram's Specht module raised to -(p-1)/p. (8) High tail: for positive b, delta, C and some J0, the exponential moment 2^(b*cost) of the palindrome cost above height J-1 has base-2 logarithm at most C k 2^(-bJ) for J>=J0, the full palindrome cost has such moment at most C k (k/2^d)^delta, and a conditional version holds for the split coordinates when 2s<J. (9) Sparse saving: for some C and d0>0, whenever k<2^d and d^(3/4) <= log(2^d/k), the squared sweep norm is at most exp(Ck)(k/2^d)^(k/4), and for d>=d0 at most (k/2^d)^(k/4).
The goal is OAI.ThorpNine.main.
The central published goal is a conjunction of nine routing and operator estimates. It includes a mixing consequence but also retains the quantitative sparse, dense, and tail regimes needed by the formal package. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
The estimates cover different diagram shapes and occupancy scales. A bound effective for sparse defects can deteriorate in the dense regime, so one uniform estimate cannot simply be substituted for the entire bundle.
Each conjunct uses its own named MainStatement under the ThorpNine namespaces. The detailed readout below gives its quantifiers and constants. Both forward and reverse sweeps occur, and the package uses complex Specht-module Hilbert spaces.
The shared definitions are supplied by ThorpRouting. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Random coordinate frames allow comparison between different sequences of matching directions in a shuffle. The source uses partially observed card lists to obtain estimates for the full permutation law. The source is OpenAI's September 2026 manuscript.
The companion Conditional information under deterministic coordinate sweeps develops the conditional-information side of the same published eight-clause goal. Both manuscripts are represented by this one draft because they point to the identical formal statement, OAI.ThorpResults.remaining_main.
A Thorp shuffle acts on binary-labelled positions by independent pair switches followed by a cyclic coordinate rotation. A sweep consists of physical shuffles. Partial observations record an injective ordered list of card positions.
Eight asymptotic results about the Thorp shuffle of 2^d cards, whose positions are the d-bit strings, hold simultaneously. One Thorp step on d≥1 bits uses one fair coin for each (d−1)-bit suffix: the first bit of a position is flipped according to the coin of its remaining bits, and then the bits are cyclically rotated; the d=0 step is the identity. A shuffle of t steps composes t independent such steps, and 'distance' is total variation (half the L¹ distance) from the uniform law on permutations. (1) FrameMain: for every ε>0, for all large d and every starting permutation, the law after 32800·d steps is within total variation ε of uniform. (2) InformationMain has three parts. For large d, any k with 8k≤7·2^d, any start and any list of k distinct labelled positions, the law of the images of the labels after 256·d steps is within ε of uniform on injective k-lists. For large d and 16k≤15·2^d, the same list distance after 1024·d steps is at most (2^d)^(−3/2). Finally, distance(d, 2048·d) tends to 0, and for every d the distance from any start equals distance(d, 2048·d). (3) SpectrumMain: there is p>0 such that for all d≥1 the regularTrace at exponent 2p is at most 17/16 (a sum over Young-diagram shapes of size 2^d of dimension times the trace of |Q|^{2p}, where Q is the averaged Specht-module operator of d-step shuffles) and, for every integer M≥p and every σ, the sweep distance after M·d steps (total variation of the shifted law from uniform) is at most 1/8. (4) SignedMain: for all real η,κ with η>0 there is r≥1 such that, for all d≥1, every shape μ of size 2^d and all Young diagrams α,β,γ with |α|+|β|+|γ|=2^d, the logarithm of the weighted moment dim·Re tr((QQ)^r) is at most a(η,d)·signedEntropy(α,β)+remainderBudget(κ,d,|γ|), where a(η,d)=η(1−1/(2√d)), signedEntropy sums log((|α|+|β|)/rowlength) over cells of α and β, and the remainder is 0 if |γ|=0 and otherwise max(0, a(κ,d)·|γ|·log 2^d−|γ|·log(2^d/|γ|)). (5) DegreeSavingMain: there are an even r≥2 and η>0 such that for all d and shapes μ, dim·Re tr((QQ)^r) ≤ dim^(1−η). (6) FullDensityMain: there is v≥1 such that, for every ε>0 and large d, every shifted law after v·d steps has normalized squared L² density distance (2^d)!·Σ_g(law−1/(2^d)!)² below ε. (7) ForwardMixingMain: there is v≥1 such that for large d every shifted law after v·d steps has total variation below ε. (8) OptimalOrderMain: the mixing time, the least t with distance at most 1/4, is Θ(log 2^d).
The goal is OAI.ThorpResults.remaining_main.
The selected published goal packages eight results, including fixed-list estimates, spectral moments, signed moments, degree savings, full-density convergence, and optimal-order mixing. The detailed clauses below specify the complete bundle. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Changing coordinates must preserve the joint path law, including what has already been revealed. Marginal uniformity of individual cards does not control the full permutation.
The goal is the shared remaining_main bundle used by several companion manuscripts. It retains all eight formal clauses rather than claiming a new manuscript-specific statement. The displayed bounds are two of those clauses; the full conjunction remains the proof obligation.
The shared definitions are supplied by ThorpRemaining. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
The full permutation of a deck can remain far from uniform after each individual card is nearly uniform. The source analyzes Thorp mixing through representation estimates; the available goal isolates a reciprocal-dimension estimate and its Fourier consequence. The source is OpenAI's September 2026 manuscript.
A Specht module is a complex representation of a symmetric group associated with a partition. Sum the reciprocals of these dimensions over all partitions of , and let be the supremum of these sums for positive . A permutation distribution is compared with uniform through its averaged action on an irreducible representation.
A conjunction of two parts. First, for each n let reciprocalFirst(n) be the sum, over all partitions p of n, of 1/deg(p), where deg(p) is the complex dimension of the Specht module of shape p (the span of the permutation-group translates of the polytabloid built from the canonical tableau, inside the space of tabloids). Let C1 be the supremum of reciprocalFirst(n) over n ≥ 1. The theorem asserts that this set of values is bounded above, that reciprocalFirst(n) ≤ C1 for every n ≥ 1, and that exceptionalFirst(n) tends to 0 as n → ∞, where exceptionalFirst(n) is the same sum of 1/deg(p) restricted to partitions p whose defect n − max(first row length, first column length) is positive. Second, for every d ≥ 3, every bijection e between the set of positions {0,1}^d (functions Fin d → Bool) and Fin 8 × Fin(2^(d−3)), every finite-dimensional complex inner product space E, and every irreducible complex representation ρ of the symmetric group on the positions, acting on E by inner-product-preserving maps, the following holds. Let ν be a probability distribution on this symmetric group (nonnegative values summing to 1) such that, for each i in Fin 8 and each group element g, the total ν-mass of the coset g·B_i is at most 4·|Sym(2^(d−3))|/|Sym(positions)|, where B_i is the subgroup of permutations that act through e by an arbitrary permutation of the i-th block of 2^(d−3) points and fix all other points. Then the operator norm of Σ_g ν(g)ρ(g) is at most √(32·C1)·(dim E)^(−5/16).
The goal is OAI.Thorp.Current.first_reciprocal_main.
The goal also proves that the reciprocal sum over shapes of positive defect tends to zero. The Fourier bound applies to distributions satisfying the specified eight-block coset-mass condition. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
One-card mixing does not control high-dimensional permutation representations. The bound must account for small-dimensional exceptional shapes and quantify contraction in every admissible irreducible representation.
The Fourier clause has , positions on a -bit cube, a bijection into eight equal blocks, and unitary irreducible complex representations. Its coset-mass hypothesis is retained exactly. The target is a supporting representation estimate, not the paper’s final -shuffle total-variation theorem.
The shared definitions are supplied by ThorpFirstReciprocal. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
An external force rewards self-avoiding walks whose endpoints move in a chosen direction. The source studies critical honeycomb scaling; the available formal goal supplies existence of the forced free-energy limit. The source is OpenAI's September 2026 manuscript.
For an -step self-avoiding walk, the endpoint displacement is embedded in the complex plane. Its projection onto is the real part of times that displacement. The partition sum weights the walk by critical activity to the th power and an exponential force reward.
For every starting vertex o of the honeycomb lattice, every complex number e and every real number s, the sequence logPartition(o,e,s)(n) converges as n tends to infinity to freeEnergy(o,e,s). Here vertices are triangular-up or triangular-down sites labeled by integer column and row, each up vertex being adjacent to three down vertices and vice versa, with planar positions given in the complex plane. saws(o,n) is the set of self-avoiding walks of n steps from o, meaning vertex lists with no repetition. For such a walk γ, its displacement is the position of its endpoint minus the position of o, and its projection onto e is the real part of conj(e) times the displacement. The partition function is the sum over γ in saws(o,n) of ρ^n exp(s times that projection), with ρ = 1/√(2+√2). logPartition is log of this partition function divided by n, and freeEnergy is defined as the limit of logPartition at infinity, using Lean's limUnder convention. The statement therefore asserts that this limit exists and equals freeEnergy; it is a stated theorem whose proof is admitted in the source.
The goal is OAI.HoneycombForce.logPartition_tendsto.
The conclusion makes the defined free energy an actual convergent limit for every starting point, direction parameter, and real force. It establishes the thermodynamic quantity underlying later asymptotic questions. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Finite sums at each length do not guarantee convergence after normalization. Self-avoidance couples concatenated pieces, so ordinary independent-product arguments are unavailable without additional work.
The target allows any complex and real , without a unit-direction restriction. Length counts steps, and walk lists contain distinct vertices. The spatial exponent, thermal laws, and small-force exponent from the manuscript are not attached conclusions.
The shared definitions are supplied by HoneycombFreeEnergy. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Critical self-avoiding walks have weights balanced between exponential path growth and decay. The source studies bridge-length scaling; the available target establishes summability of the bridge sums used to define these quantities. The source is OpenAI's September 2026 manuscript.
A honeycomb bridge is a self-avoiding vertex list crossing a strip from a fixed initial port to any terminal port on the opposite layer. A path with vertices has critical weight , with .
For every integer h ≥ 1, six families of sums over self-avoiding bridge paths in a honeycomb strip are absolutely summable. Vertices of the honeycomb lattice are of two kinds, up(i,j) and down(i,j) with integer i and j, and the layer of a vertex is its second index j; an up vertex (i,j) is adjacent to the down vertices (i,j−1), (i,j) and (i−1,j), and adjacency is symmetric. A bridge path of height h is a list of distinct vertices, consecutive ones adjacent, starting at up(0,0), ending at some down(i,h−1), with every vertex in layers 0 through h−1. Its weight is λ^L, where L is the number of vertices and λ = 1/(2cos(π/8)) is the critical activity, and its first-length weight is L·λ^L. Let bridgeMass(h) be the total weight of all bridge paths. A path is confined if every vertex has horizontal coordinate (i + j/2 for up vertices, i + j/2 + 1/2 for down vertices) of absolute value at most h(log h)², and confinedMass(h) is the total weight of confined paths. The theorem asserts summability over all bridge paths of the weight, of the first-length weight, and of the first-length weight divided by bridgeMass(h), and summability over confined paths of the weight, of the first-length weight, and of the first-length weight divided by confinedMass(h). The proof is admitted in the source, not established here.
The goal is OAI.PolynomialVacuumBridge.Corridor.finite_bridge_sums.
The full formal statement gives six summability assertions, including normalized first-length weights and their corridor-confined counterparts. These are prerequisites for interpreting bridge masses and mean lengths. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Each strip has unbounded horizontal extent and admits paths of arbitrarily large length. Finite strip height therefore does not by itself make the path family finite.
The length convention counts vertices. Confinement means horizontal coordinate bounded by . The target proves summability, without asserting the manuscript’s asymptotic law. Normalized terms use the masses defined by tsum.
The shared definitions are supplied by HoneycombBridgeFiniteness. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
An Ising spin system probes a quadratic form only on cube vertices. The source asks whether random orthogonal eigenvectors allow its pressure to be determined by the limiting eigenvalue distribution at every positive temperature. The source is OpenAI's September 2026 manuscript.
The pressure is the normalized logarithm of the average Boltzmann weight under the uniform spin prior. Eigenvectors are Haar orthogonal, and the deterministic empirical eigenvalue laws converge weakly to a compactly supported probability law. The variational formula uses an edge-extended spectral transform.
For a spin system on N Ising spins σ ∈ {−1,1}^N, the rotated pressure for eigenvalues λ₁,…,λ_N, an orthogonal rotation U and a field c is (1/N) times the log of the average over all 2^N spin configurations of exp(H(σ)), where H(σ) = (1/2)∑ᵢ λᵢ (Uσ)ᵢ² + ∑ᵢ cᵢσᵢ. The theorem states that, for any probability space (Ω,P), random N×N orthogonal matrices U_N that are measurable and whose laws are right-invariant under multiplication (Haar-type), and any deterministic eigenvalue arrays (eig_N,i), the following holds under these assumptions: ν is a probability measure on ℝ whose support lies in [a,b] and contains both a and b; for every ε>0, eventually in N all eigenvalues lie in [a−ε,b+ε]; the empirical spectral laws (1/N)∑ᵢ δ_{eig_N,i} converge weakly to ν; and the inverse temperature β is strictly positive. Then, with eigenvalues β·eig_N,i, rotation U_N(ω)⁻¹ and zero external field, the expected rotated pressure ∫ pressure dP converges as N → ∞, and the pressure itself converges for P-almost every ω, in both cases to the real part of the variational functional of the measureR transform of the β-rescaled law of ν, evaluated at the edge β·b.
The goal is OAI.InvariantIsing.positive_temperature_pressure_unconditional. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The selected goal is the all-positive-temperature zero-field pressure theorem. The attached results also cover field laws, random spectra, Gaussian-pattern pressure and ground energy, and related norm limits under their stated assumptions. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Weak spectral convergence does not control rare extreme eigenvalues. The explicit no-outlier condition is essential to the selected statement’s comparison with the limiting spectral functional.
The spin prior is uniform probability, and temperature is implemented by multiplying eigenvalues by . The no-outlier condition holds eventually within every enlargement of the limiting support interval. Almost-sure convergence and expectation convergence are both conclusions; other attached variants keep their own uniform-integrability and field hypotheses.
The shared definitions are supplied by InvariantIsing. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Hausdorff dimension identifies a critical power of scale but need not give a positive measure at that power. The source proposes an iterated-logarithm correction for ordinary chordal SLE curves. The source is OpenAI's September 2026 manuscript.
A Hausdorff gauge is continuous, nondecreasing on nonnegative radii, zero at zero, and positive at positive radii. Its metric measure charges a covering set according to its diameter. Chordal SLE is represented by a capacity-two Loewner trace driven by scaled Brownian motion.
For every probability space (Ω, P) and every κ with 0<κ<8, if γ is an ordinary chordal SLE_κ family of curves on Ω, then almost surely the explicit Hausdorff gauge measure of every positive-time segment of the curve is positive. Here γ being an ordinary chordal SLE_κ means that each γ(ω,t) is measurable in ω and that there is a standard real Brownian motion B on (Ω,P) such that, for almost every ω, the curve t↦γ(ω,t)∈ℂ with driving function U(t)=√κ·B_t(ω) is a capacity-two trace: γ is continuous, starts at 0, stays in the closed upper half-plane, and there are conformal-type maps G_t from the unbounded component of the upper half-plane minus γ[0,t] to the upper half-plane and inverse maps F_t back, holomorphic, mutually inverse, with G_0 the identity, satisfying the Loewner equation ∂_t G_t(z)=2/(G_t(z)−U(t)) (one-sided at t=0), the normalization z(G_t(z)−z)→2t as z→∞, and F_t(U(t)+iy)→γ(t) as y→0⁺. The gauge h:ℝ→ℝ is any function that is continuous, nondecreasing on [0,∞), zero at 0 and positive for r>0, and that coincides, for all sufficiently small r>0, with r^{1+κ/8}·(log log(1/r))^{(1−κ/8)/2}. The gauge measure is the Hausdorff-type metric measure on ℂ built from r↦h(r) (with the ENNReal-valued radius cast through its real part). The conclusion is that, for almost every ω, simultaneously for all times 0<s<t, this measure of the image set γ(ω)([s,t]) is strictly positive.
The goal is OAI.SLEExactGauge.sourceLowerMain_proved.
The formal goal establishes simultaneous positivity for every nontrivial positive-time compact segment. It is the lower-positivity component of the manuscript’s exact-gauge claim. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
A dimension statement only determines a critical exponent; it does not decide the effect of a slowly varying correction. Positivity must hold for all segment times on one probability-one event.
The parameter satisfies . The goal does not assert finite measure, finite expected disk mass, or non-sigma-finiteness for a different gauge. The name sourceLowerMain_proved is a declaration name; its current theorem status is Open.
The shared definitions are supplied by SLELowerPositivity. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Broadcasting a label through noisy tree edges models how information decays with distance. The source studies when observations far from the root retain information about its three-state label. The source is OpenAI's September 2026 manuscript.
The symmetric channel preserves the input with probability and sends it to each other state with probability . Reconstruction advantage is the expected total variation between the posterior root law and the uniform prior.
For every natural number b ≥ 2 and every real λ that is admissible, meaning −1/2 ≤ λ ≤ 1, if b·λ² > 1 then the sequence of regular-tree advantages reconstructs. Here a three-state spin (an element of Fin 3) is passed through a symmetric channel that keeps the spin with probability (1+2λ)/3 and moves to each other spin with probability (1−λ)/3. The observation at depth 0 is the root spin, and the observation at depth n+1 is a multiset of depth-n observations, one for each of the offspring of the root, where the offspring count is the constant b (the regular case) and each child spin is obtained by passing the parent spin through the channel and then observed recursively. With a uniformly random root spin, the posterior of each spin given an observation is its conditional probability, defaulting to 1/3 when the observation has probability zero. The advantage of a family of laws indexed by the root spin is the sum over observations y of the marginal probability of y times half the sum over spins i of |posterior(y,i) − 1/3|. The regular advantage at depth n is this advantage for the regular b-ary observation law. Reconstructs means that this sequence in n converges to some limit L > 0. The statement is an admitted theorem, with its proof left as sorry.
The goal is OAI.ThreeState.regular_supercritical. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The selected goal is the regular-tree supercritical direction. Supporting published targets give Poisson reconstruction and equivalent supercritical formulations in a second definition group. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
The observation contains the full nested collection of descendants, and the posterior depends on correlated information inherited from their common ancestor. A single root-to-leaf correlation is insufficient to describe reconstruction.
Observations are nested multisets with a uniform three-state root. The attached targets establish reconstruction above the displayed threshold; non-reconstruction at or below equality and stochastic-block-model recovery are outside this draft’s formal scope.
The shared definitions are supplied by ThreeStateSupercritical, ThreeStateTreeClauses. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Cutoff means that a Markov chain’s transition from far from equilibrium to near equilibrium occurs in a negligible fraction of its mixing time. The source studies heat-bath dynamics for a disordered mean-field Ising model. The source is OpenAI's September 2026 manuscript.
The Sherrington–Kirkpatrick model has independent centered Gaussian pair couplings with variance and zero external field. One discrete update picks a site uniformly and resamples its spin from its conditional Gibbs law. Mixing time uses worst-case total variation distance.
For real parameters β with 0 ≤ β < 1/2, ε with 0 < ε < 1/2, and η > 0, two things hold for the Sherrington–Kirkpatrick model with n spins, where a disorder g is a real coupling for each pair i < j of sites and the Gibbs measure at zero external field has weight proportional to exp((1/2) Σᵢ Σⱼ σᵢ gᵢⱼ σⱼ) on spin configurations σ ∈ {±1}ⁿ (couplings symmetrized, diagonal zero). The dynamics is a heat-bath single-site chain: choose a site uniformly at random, then keep or flip its spin with probabilities proportional to the Gibbs masses of the two configurations (for n = 0 the transition matrix is the identity). The distance after k steps is the maximum over starting configurations of the total variation distance (half the ℓ¹ distance) between the k-step distribution and the Gibbs measure, and mixingTime(g, δ) is the least k whose distance is at most δ (the infimum of the set, so 0 if that set is empty). The disorder law makes the couplings independent centered Gaussians with variance β²/n. First, the probability under this law that the ratio mixingTime(g, ε) / mixingTime(g, 1 − ε) exceeds 1 + η tends to 0 as n → ∞. Second, for all sufficiently large n, every disorder g satisfies mixingTime(g, 1 − ε) > 0.
The goal is OAI.SKRatio.ratio_cutoff.
The available target gives ratio cutoff in probability over the disorder and eventual positivity of the denominator for every disorder. It isolates a precise mixing-time comparison. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Fast relaxation estimates alone do not prove that all fixed total-variation thresholds become asymptotically equivalent. The worst starting configuration and the random couplings both enter the comparison.
The attached range is , narrower than the full high-temperature range discussed in the manuscript. The target does not specify the cutoff location. Dynamics is discrete single-site updating; the exceptional transition is the identity.
The shared definitions are supplied by SKRatio. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
The spherical perceptron assigns random rewards to vectors of fixed length. The source asks for an exact pressure formula without a convexity or symmetry condition on the single-pattern potential. The source is OpenAI's September 2026 manuscript.
Configurations lie on the sphere of radius , equipped with uniform probability measure. There are independent Gaussian patterns. The variational value minimizes a Brownian stochastic-control functional plus an extended nonnegative entropy over monotone trials.
For a probability measure P on continuous paths ℝ≥0→ℝ under which the evaluation process is a real Brownian motion, and for parameters α>0, β>0 and a bounded continuous function φ:ℝ→ℝ, there is a real number p with three properties. First, the variational value equals p (as an extended real). That value is the infimum over all trials m of α times the control value of βφ at m, plus the entropy of m. A trial is a nondecreasing measurable function m:[0,1]→[0,1]. Its entropy is one half of the integral over t of 1/∫ₜ¹ m(s)ds minus 1/(1−t), taken in [0,∞]. The control value of f at m is the supremum, over progressively measurable controls v with finite cost E∫ m(t)v(t)²dt, of E f(B₁+∫₀¹ m(t)v(t)dt) minus half that cost. Second, the expected spherical-perceptron pressure E[pressure(N+1)] converges to p as N→∞. For dimension n, pressure is (1/n) log ∫ exp(β Σₐ φ(⟨gₐ,x⟩/√n)) dx, with x uniform on the sphere of radius √n in ℝⁿ. The gₐ are the rows of a pattern matrix with ⌊αn⌋ rows and n i.i.d. standard Gaussian entries per row. Third, the pressure concentrates: for every ε>0, the Gaussian probability that |pressure(N+1)−p|>ε tends to 0 as N→∞.
The goal is OAI.SphericalPerceptronFreeEnergy.main. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The selected main target proves finiteness of the variational value, convergence of expected pressure, and concentration around the same number. The linear-field formula is attached as a supporting result. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
An infimum involving a possibly infinite entropy must be connected with the actual finite-dimensional spherical integral. The potential is only bounded and continuous, so smoothness cannot be assumed.
Density and inverse temperature are strictly positive. Controls are progressively measurable for the stated Brownian filtration and have finite cost. Dimension is written as to stay positive. The Brownian and cascade-based linear-field definition groups are independent references.
The shared definitions are supplied by PerceptronFreeEnergy, SphericalField. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
The Ising perceptron weights binary configurations by their projections onto random patterns. The paper develops a variational description of its pressure; the available formal target checks that the proposed variational value is finite. The source is OpenAI's September 2026 manuscript.
An overlap path is an almost-everywhere class on with a monotone representative taking values in . The variational expression combines a Gaussian pattern functional with an Ising entropy, defined as a supremum over monotone nonnegative field steps.
For every real α ≥ 0 and every continuous function f : ℝ → ℝ that is bounded (there is K with |f(x)| ≤ K for all x), the variational value of the Ising perceptron model is a finite real number, i.e. variationalValue(α,f) equals the extended real (p : EReal) for some real p. Here variationalValue(α,f) is the infimum, over all admissible overlap paths q (almost-everywhere-defined functions on (0,1) that agree a.e. with a monotone function taking values in [0,1]), of α times the pattern functional of f at q plus the Ising entropy of q. The pattern functional is the limit as n→∞ of uniformPattern, a nested Gaussian transform over a uniform grid with n+1 cells built from cell averages of q and applied to f at 0, where each transform is either a Gaussian average or a log-exponential-moment average divided by d, depending on whether d is zero. The Ising entropy is the supremum, over field steps (a partition of [0,1] with nonnegative monotone step values), of the field recursion value plus half the integral of the step function against q. The statement asserts that this infimum is neither +∞ nor −∞.
The goal is OAI.IsingPerceptron.variationalValue_real_of_continuous.
The goal rules out both infinite extended-real values for continuous bounded potentials. This is a well-definedness component needed before a real-valued limit formula can be used. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
The entropy is a supremum over an unbounded family of fields and the outer expression is an infimum over paths. Boundedness of the input potential alone does not syntactically make this extended-real expression finite.
The target is variationalValue_real_of_continuous, with nonnegative density and continuous bounded potential. It does not assert convergence of finite-system pressure or the manuscript’s broader bounded-Borel result. Gaussian recursion and almost-everywhere path conventions are kept as published.
The shared definitions are supplied by IsingFiniteness. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
A diluted spin glass has finitely many interactions per spin on average. The source seeks the exact thermodynamic pressure using a hierarchy of random local-field laws. The source is OpenAI's September 2026 manuscript.
The pressure is the expected logarithm of the partition function divided by the number of Ising spins. A Poisson number of even-arity interactions and independent external fields define the model. The cavity functional uses nested probability laws and iterated logarithmic power means.
For every model of a diluted p-spin glass with Ising spins in {+1,-1} that satisfies the standing admissibility hypotheses, the free-energy density F_N converges, as N tends to infinity, to a variational value, so existence of the thermodynamic limit is part of the conclusion. A model consists of a density α ≥ 0, a probability law on interaction samples (θ, a, b, f), where θ is a real function on spin configurations in {±1}^p, a and b are reals and f assigns to each of the p slots a real function on spins, and a probability law for the external field on ℝ. Admissibility means: p is even and at least 2; α > 0; ‖θ‖ = max_s |θ(s)| and |h| are integrable under the disorder and field laws; almost surely a > 0 and, for every configuration s, exp θ(s) = a(1 + b ∏_l f_l(s_l)) with |b ∏_l f_l(s_l)| < 1; the functions f_1,…,f_p are independent and identically distributed, b is independent of the vector f, every power (−b)^n with n ≥ 1 is integrable, and E[(−b)^n] ≥ 0. No boundedness of interactions, fields or messages is added. F_N is (1/N) times the expectation of log Σ_σ exp(−H), where the number k of interactions is Poisson with mean αN, the k interactions are independent disorder samples, the N fields are independent field samples, and each interaction is placed on p index choices in {1,…,N} (repetitions allowed) averaged uniformly over all choices; here the log-weight of σ is Σ_j θ_j(σ at the chosen indices) + Σ_i h_i σ_i. The limit is the infimum over depths r ≥ 0 of φ_r, itself the infimum, over a nested law ζ in the r-fold hierarchy of probability measures (each level with the weak topology and its Borel σ-field) and exponents 0 < m_1 < … < m_r < 1, of the cavity functional B_r. B_r equals log 2 plus the Poisson(αp)-averaged expectation of the site term, a logarithm of an average over spin ε of exp(hε + Σ_j message_j(ε)), minus α(p−1) times the expectation of the log of the edge weight, with both terms evaluated through iterated log power-means in the exponents m_i.
The goal is OAI.DilutedSpinGlass.mezard_parisi.
The equality identifies the limit with the infimum over all finite hierarchy depths. Existence of the thermodynamic limit is part of the conclusion, not an assumption. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Upper bounds at each hierarchy depth do not yield equality with the infinite-size model. Unbounded disorder requires retaining integrability hypotheses through nested expectations.
The admissibility predicate requires positive density, even arity at least two, first moments, the specified interaction factorization, and positivity and integrability of the relevant powers. The statement adds no boundedness restriction on interactions, fields, or trial messages.
The shared definitions are supplied by DilutedSpin. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.