Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
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.
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.
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.
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.
A random environment can favor different directions at different sites. The source asks whether escape in one prescribed real direction can have an intermediate probability after averaging over the environment. The source is OpenAI's September 2026 manuscript.
A transition row assigns probabilities to the nearest-neighbor steps of the integer lattice. Rows at different sites are independent and have the same law. Strict ellipticity means every step probability is positive almost surely, without a common positive lower bound.
For every dimension d ≥ 3, a random walk in an i.i.d. random environment on the lattice ℤ^d obeys a directional zero-one law. Here a row at a site is a probability vector p on the 2d nearest-neighbour steps (coordinate direction i in Fin d, sign + or −), with each p(e) in [0,1] and the entries summing to 1. The environment assigns an independent row to every site, each drawn from a probability measure μ on rows, and the strict ellipticity hypothesis on μ says that μ-almost every row gives every one of the 2d steps strictly positive probability. Given the environment, the walker at site x moves to x plus the unit vector of step e with probability p_x(e); the annealed law of the path started at 0 averages over both the environment and the walk. For any nonzero real vector ℓ in ℝ^d, the escape event is that the path X satisfies Σᵢ Xₙ(i)·ℓᵢ → +∞ as n → ∞, that is, the walk tends to infinity in the direction ℓ. The conclusion is that the annealed probability of this event, starting from 0, is either exactly 0 or exactly 1.
The goal is OAI.DirectionalZeroOne.directional_zero_one.
The target gives a directional zero–one law under positivity alone. It makes no moment or uniform ellipticity 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.
Revisiting sites reuses the same random transition row, so path increments are not independent under the averaged law. Ordinary zero–one laws for independent increments do not directly apply.
Lean builds the annealed path measure through a Markov kernel on environment-position pairs. The starting site is the origin, the direction is any nonzero real vector, and escape means the scalar projection tends to positive infinity.
The shared definitions are supplied by DirectionalWalk. 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.
Conditioning on an explored Ising interface fixes many spins and can create alternating signs. The source develops comparison estimates that remain valid with arbitrary common pinned spins. The source is OpenAI's September 2026 manuscript.
A ferromagnetic Ising law weights sign configurations by the exponential of nonnegative pair couplings plus real external fields. Two probability mixtures prescribe source spins on , while the same spins are pinned on and a target event is prescribed on .
A comparison bound for a ferromagnetic Ising model on a finite graph with n vertices and m separately indexed edges (parallel edges allowed, no loops, nonnegative couplings K_e) and an arbitrary real external field h. A configuration σ has energy equal to the sum over edges of K_e σ_u σ_v plus the sum over vertices of h_v σ_v, with spins ±1, and weight exp(energy). Take pairwise disjoint vertex sets I, J, F, and kept vertices i ∈ I and j ∈ J that lie outside F. Fix spin configurations a and τ. For a configuration b, the conditional probability of σ_I = a given σ_J = b and σ_F = τ is the ratio of the total weight of configurations satisfying all three agreements to the total weight of those agreeing with b on J and τ on F. For any two probability mixtures mix and mix' on configurations (nonnegative weights summing to 1), the mixture probability is the mix-weighted average of these conditional probabilities over b; only the restriction of b to J matters. Let q be the terminal connection probability in the zero-field random-cluster (FK) model with q=2 on the graph with F deleted (not pinned): edges e are open with probability 1-exp(-2K_e), the vertices of I are identified together and those of J are identified together, and q is the probability that i and j lie in the same cluster. Then the ratio of the mixture probability under mix to that under mix' lies between exp(-4 artanh q) and exp(4 artanh q), for every such pair of mixtures, uniformly in h, a and τ. The theorem is stated with its proof admitted (sorry).
The goal is OAI.BufferedIsing.finite_graph_comparison.
The estimate controls likelihood ratios uniformly over mixtures, fields, and common signs. It is the finite-graph comparison component of the manuscript. 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.
Pinning a vertex changes neighboring fields; deleting it does something different. The comparison probability must come from the graph with the common pins deleted, with each terminal class contracted separately.
The graph is finite with indexed edges, allowing parallel edges and excluding loops before contraction. The sets are pairwise disjoint and each terminal class contains a supplied vertex. The zero-field random-cluster weight has cluster parameter two. The stopping-band approximation theorem is not an attached target.
The shared definitions are supplied by BufferedIsing. 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.
On an expanding infinite graph, the appearance of an infinite open cluster and the appearance of a unique one can occur at different densities. The source seeks a nonempty interval where infinitely many infinite clusters coexist. The source is OpenAI's September 2026 manuscript.
In bond percolation, edges are independently retained with probability . The critical threshold records appearance of infinite clusters; records uniqueness. The intermediate operator threshold records boundedness on of the two-point connection kernel.
For a bond graph G, given by a map from an edge type E to unordered pairs of vertices in an infinite vertex type V, that is connected, locally finite (each vertex lies in finitely many edges) and quasi-transitive (finitely many vertex representatives such that every vertex is the image of one under an automorphism of G acting on vertices and edges), and whose vertex isoperimetric constant hV(G), the infimum over nonempty finite vertex sets A of |outer vertex boundary of A|/|A|, is strictly positive, the MainConclusion holds for Bernoulli bond percolation on G. Writing pc for the infimum of parameters p at which an infinite cluster occurs with positive probability, pu for the infimum of p at which there is almost surely exactly one infinite cluster, ptwo for the supremum of p at which the two-point function τ_p(x,y)=P_p(x connected to y) is the matrix kernel of a bounded operator on ℓ²(V), and operatorNorm(p) for the infimum of operator norms of such operators, valued in [0,∞], the conclusion has four parts. First, the supremum of operatorNorm(p) over p<pc equals operatorNorm(pc). Second, operatorNorm(pc) is finite. Third, pc<ptwo≤pu. Fourth, there exist p₁<p₂<1 with pc<p₁ such that, for almost every i.i.d. uniform [0,1] edge labelling, for every p in [p₁,p₂] the configuration of edges with label at most p has infinitely many infinite clusters. The proof is omitted (sorry) in the source.
The goal is OAI.Percolation.BenjaminiSchramm.full_main. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The full goal also identifies the critical norm as the supremum from below and supplies simultaneous nonuniqueness over a fixed interval under the uniform-label coupling. Supporting statements cover critical laws and Cayley graphs. 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 separate almost-sure statement at each parameter does not establish one event valid for every parameter in an interval. Critical operator control must also survive the passage to the threshold itself.
The graph has infinitely many vertices, is connected and locally finite, has finitely many vertex orbits, and has positive vertex isoperimetric constant. Thresholds lie in the unit interval; operator norms may take extended nonnegative values. The independent Cayley definition group is retained separately.
The shared definitions are supplied by BenjaminiSchramm, CayleyPercolation. 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 edge travel times produce a deterministic large-scale shape. The source studies two distinct regularity questions: corners and flat boundary segments. The available exponential target addresses differentiability and the structure of supporting lines. The source is OpenAI's September 2026 manuscript.
In first-passage percolation, travel time is the infimum of path costs on the nearest-neighbor square lattice. A time-constant norm gives the asymptotic travel time in each direction. Its unit ball is the limit shape.
For any probability space (Ω, P) carrying an edge-weight family τ indexed by the edges of the nearest-neighbour lattice ℤ², where each vertex p has an east edge (p,false) and a north edge (p,true), such that the τ(e) are measurable, mutually independent, and each has the exponential distribution with rate 1 (the ExponentialEnvironment hypothesis), there exists a function μ on the plane ℝ² with the following properties. First, μ is a norm: nonnegative, zero only at the origin, subadditive, and satisfying μ(av)=|a|μ(v) for all real a. Second, μ is the time constant: for every v in ℝ², almost surely the first-passage time from (0,0) to the lattice point (⌊tv₀⌋,⌊tv₁⌋), defined as the infimum of path costs over nearest-neighbour step sequences (east, west, north, south) that sum the edge weights along the path, divided by t, converges to μ(v) as t→∞. Third, μ is Fréchet differentiable at every nonzero point. Fourth, at every point v with μ(v)=1 there is exactly one linear functional ℓ with ℓ(v)=1 and ℓ(w)≤μ(w) for all w. Fifth, the unit sphere of μ is a C¹ curve in the sense that near each point v with μ(v)=1 there is an open neighbourhood U and a C¹ function g on U whose zero set in U is exactly the set where μ=1, with g having a nonzero Fréchet derivative at each of those zeros. Sixth, for each boundary point v of the unit ball {μ≤1}, there is a unique line L that is the level set {z : g(z)=g(v)} of some nonzero continuous linear functional g that attains its maximum over the unit ball at v, so each boundary point has a unique supporting line. Seventh, every boundary point v of the unit ball has a C¹ curve chart: an open neighbourhood U of v and a C¹ map γ:ℝ→ℝ² with nowhere vanishing derivative, together with a function θ continuous on U, such that γ takes values in the boundary within U, θ(γ(t))=t for all t, and γ(θ(z))=z for each boundary point z in U.
The goal is OAI.PlanarFPP.manuscriptMain. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The chosen target supplies the norm and its limiting interpretation, unique normalized supporting functionals, unique supporting lines, and boundary charts. The Gamma-law differentiability statement is retained 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.
Pointwise convergence to a norm does not imply differentiability of that norm. Excluding corners requires additional information about nearby directions, and the chart conclusion requires regularity beyond mere continuity.
The main target uses independent rate-one exponential weights. It does not assert strict convexity, despite the broader manuscript title; strict convexity is not added implicitly. The Gamma target has arbitrary positive shape and rate. Each original definition group remains independent.
The shared definitions are supplied by GammaPassage, PlanarFirstPassage. 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 finite algebra has a lattice of congruences, ordered by inclusion. The source studies which finite lattices arise in this way, and the available goal captures its colored-graph characterization. The source is OpenAI's September 2026 manuscript.
A congruence is an equivalence relation preserved by every basic operation of an algebra. A graph witness assigns lattice-valued colors to pairs of finitely many vertices, with symmetry, diagonal, triangle, separation, and seed-connectivity conditions.
For any finite type Lat carrying a lattice structure with a least element ⊥, Lat is Representable if and only if it HasGraphWitness. Representable means that there is a positive size n and an algebra on Fin n (a finite list of operations, each of some finite arity, acting on the carrier) such that Lat is order-isomorphic to the poset of congruences of that algebra, where a congruence is an equivalence relation compatible with every operation: if corresponding arguments are related coordinatewise, the outputs are related; congruences are ordered by the inherited order on equivalence relations. HasGraphWitness means that there is a positive size n and a Lat-valued coloring color of ordered pairs from Fin n satisfying five conditions: color is symmetric; color(a,b)=⊥ exactly when a=b; color(a,b) ≤ color(a,m) ⊔ color(m,b) for all a, b, m; whenever lower ≰ upper in Lat, some pair has color ≤ lower but not ≤ upper; and for every nonempty finite set of seed pairs, any pair whose color is at most the join of the seed colors is connected to the seeds. Connected is the equivalence closure of the relation Marked, where a,b are Marked if some self-map p of the vertices satisfies color(p x,p y) ≤ color(x,y) for all x,y and sends some seed pair (s,t) to (a,b).
The goal is OAI.FiniteCongruence.graph_criterion.
The equivalence provides a finite combinatorial certificate for representation as an entire congruence lattice. It is the characterization component of the manuscript. 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.
Representing a lattice inside a congruence lattice is weaker than obtaining all congruences. The witness’s seed-connectivity condition must capture this fullness and work in both directions.
The lattice is finite and has a least element. The algebra carrier and graph witness carrier each have positive finite size. Operations have finite arities, and representation is an order isomorphism. The manuscript’s undecidability conclusions are not among the attached targets.
The shared definitions are supplied by FiniteCongruenceGraph. 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 odd-characteristic version of direct finiteness has different coefficient constraints from the binary case. The source fixes one odd prime and links a group-algebra counterexample to a cellular automaton. The source is OpenAI's September 2026 manuscript.
For a finitely supported coefficient function on a group, the cellular map sends a configuration to . The prime is the smallest prime factor of , where is a fixed central binomial coefficient.
The defined proposition MainClaim holds. Here sourceM is the central binomial coefficient C(1200,600), and sourcePrime is the smallest prime factor of (sourceM!)²+1. MainClaim asserts that this number p is prime and odd, and that there exist a finite field K of characteristic p with exactly p⁴ elements and a finitely generated group G containing a nontrivial element of finite order, together with two elements a and b of the group algebra K[G] such that ab = 1 but ba ≠ 1. Moreover, for the map cellular(b) sending x : G → K to g ↦ Σ_u b(u)·x(g·u), the sum running over the support of b, this map is injective but not surjective. The formal statement is admitted in the source rather than proved here.
The goal is OAI.OddKaplansky.main_theorem.
The conclusion combines a scalar one-sided inverse with failure of surjectivity of a finite-memory linear map. It specifies the characteristic and field size without claiming the construction works at every odd prime. 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 group must retain nontrivial torsion while supporting the required finite sums. Matrix-level relations and an arbitrary choice of characteristic do not meet this target.
The goal unfolds MainClaim. It proves primality and oddness of the fixed sourcePrime, then existentially supplies the finite field, finitely generated group, nontrivial finite-order element, and algebra elements. The cellular convention uses right-translated inputs .
The shared definitions are supplied by OddKaplansky. 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 determinant of a nonsingular integer matrix has absolute value at least one. The source examines the proposed counterpart for integer matrices over group rings, where the determinant is defined by an operator trace. The source is OpenAI's September 2026 manuscript.
The left regular operator associated to a group-ring matrix acts on by finite convolution. Its Fuglede–Kadison determinant in the invertible case is the exponential of half the real trace of the logarithm of its positive square.
The defined proposition MainStatement holds, i.e. there exist a group G that is finitely generated, an integer n ≥ 1, an n×n matrix A with entries in the integral group ring ℤ[G], and a bounded ℂ-linear operator T on the Hilbert space l²(G)^n (square-summable complex functions on Fin n × G) such that four conditions hold. First, the image of A in the rational group ring ℚ[G] (obtained by applying the integer-to-rational map to every coefficient) is an invertible matrix over ℚ[G]. Second, T is exactly the left-regular operator of A, meaning (Tξ)(i,h) = Σ_j Σ_g a_{ij}(g) ξ(j, g⁻¹h), where a_{ij}(g) ∈ ℤ is the coefficient of g in the entry A_{ij}. Third, T is invertible as a bounded operator on l²(G)^n. Fourth, its Fuglede–Kadison determinant fkDet(T) = exp(Re tr(log(T*T))/2) satisfies 0 < fkDet(T) < 1, where tr(S) = Σ_i ⟨e_i, S e_i⟩ is the unnormalized trace summing over the basis vectors e_i supported at the identity element of G in component i, and log is the continuous functional calculus logarithm.
The goal is OAI.GroupRingDeterminant.main.
The goal gives a square-matrix obstruction with both a rational group-ring inverse and a bounded operator inverse. This keeps the logarithm in the invertible setting. 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 trace logarithm is not an ordinary finite-dimensional determinant polynomial. The algebraic matrix and bounded regular operator must be shown to match exactly before the determinant estimate is meaningful.
The group is finitely generated and . Lean uses complex square-summable functions on Fin n × G, the unnormalized matrix trace, and continuous functional calculus for the logarithm. Invertibility is explicit on both the rational matrix and the operator.
The shared definitions are supplied by GroupRingDeterminant. 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.
Finite-dimensional linear algebra makes a one-sided inverse two-sided. The source asks whether finite support in a group algebra can replace finite dimension and presents a characteristic-two counterexample. The source is OpenAI's September 2026 manuscript.
The group algebra consists of finitely supported functions on a group with convolution multiplication. A ring is directly finite if always implies .
There exist a finite field K of characteristic 2 and a finitely presented group G such that G contains an element g of odd prime order ℓ (that is, orderOf g = ℓ with ℓ prime and odd), and the group algebra K[G] (the monoid algebra of G over K) contains elements a_out and b_out with a_out · b_out = 1 but b_out · a_out ≠ 1. Thus K[G] fails to be directly finite, giving a counterexample to direct finiteness. The statement is existential: it does not name a specific K, G, or prime ℓ, and the proof is admitted in the source.
The goal is OAI.KaplanskyCounterexample.finitelyPresented_counterexample. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The selected statement includes finite presentation and an element of odd prime order in the group. The weaker finitely generated formulation 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.
A matrix counterexample does not automatically provide scalar elements in a group algebra. The formal target requires genuine finitely supported scalar elements and verification of both products.
The field and group are existentially quantified, with the finite-field, characteristic, and finite-presentation structures carried explicitly. No claim that the field is exactly the two-element field is made. Odd-prime torsion is part of the conclusion.
The shared definitions are supplied by KaplanskyDirectFiniteness. 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.
Multiplicity measures the growth of infinitesimal neighborhoods in a local ring. The manuscript addresses Lech’s flat-local-map inequality; the available formal target isolates its complete-domain Frobenius-complex component. The source is OpenAI's September 2026 manuscript.
For a local domain of dimension , Hilbert–Samuel multiplicity is the limit of . A short complex has finite free terms in degrees through zero, finite-length homology, and nonzero zeroth homology. Its Frobenius scalar extensions define a normalized Euler-characteristic sequence.
The defined proposition DuttaDomainClaim holds, in universe u. That claim says: let D be a commutative Noetherian local domain (in universe u) that is complete in the adic topology of its maximal ideal, with prime characteristic p, and let F be a cochain complex of D-modules indexed by the integers that is a short complex. Short means every term F^i is free and finitely generated, F^i is zero whenever i < -dim D or i > 0, every homology module of F has finite length, and the homology of F in degree 0 is nonzero. Here dim is the Krull dimension (taken as 0 if it is the bottom value). Let F_n denote F after extending scalars along the n-fold iterate of the Frobenius map of D. The conclusion has three parts. First, every homology module of every F_n has finite length. Second, the sequence a_n = p^(-n dim D) * chi(F_n) converges as n tends to infinity, where chi(G) is the alternating sum, over i from 0 to dim D, of (-1)^i times the length of the homology of G in degree -i; this limit is the Dutta multiplicity of F. Third, the Hilbert-Samuel multiplicity of D, defined as the limit of (dim D)! times the length of D/m^N divided by N^(dim D) as N tends to infinity, is at most the Dutta multiplicity of F.
The goal is OAI.Lech.dutta_domain.
The goal formalizes the lower bound by Dutta multiplicity together with the convergence and finite-length statements needed to interpret it. This is a precise component of the paper’s multiplicity program. 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.
Lengths of homology after Frobenius extension must be controlled before normalized Euler characteristics can be used. A definition by a chosen limit does not by itself establish convergence.
The ring is a complete Noetherian local domain in prime characteristic. The goal is DuttaDomainClaim, not the unrestricted flat local homomorphism inequality. Dimensions and lengths use the natural-number conversions in the supplied definitions, and convergence is an explicit conclusion.
The shared definitions are supplied by DuttaDomain. 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 linear Fourier coefficients measure a Boolean function’s correlation with individual inputs. The source studies whether their sum can be controlled solely by the square root of the function’s real polynomial degree. The source is OpenAI's September 2026 manuscript.
A Boolean function here takes values in on a finite sign cube. Fourier coefficients use the uniform distribution. The Fourier degree is the largest support size of a nonzero coefficient; it is unrelated to degree over a field of characteristic two.
Two things about real Fourier analysis on Boolean cubes, where a Boolean input is read as a sign (false is +1, true is -1), averages are uniform, and degree is the ordinary real Fourier degree, meaning the largest size of a subset s with nonzero Fourier coefficient, the coefficient being the average of f(x) times the product of the signs of the coordinates in s. First, SignedViolations holds: for every real C>0 there is a positive integer n and a function f from {false,true}^n to the reals that takes only the values -1 and 1, is nonconstant, and satisfies C·√(deg f) < Σᵢ f̂({i}), the plain signed sum of its degree-one Fourier coefficients over single coordinates. Second, the set of ratios (Σᵢ |f̂({i})|)/√(deg f), taken over all positive n and all Boolean-valued f on n coordinates with positive Fourier degree, is not bounded above in the reals, so the supremum of these ratios is infinite.
The goal is OAI.SquareRootDegree.main.
Both signed violations and unbounded absolute ratios are retained. The result concerns failure of every constant multiple, which is stronger than exhibiting one violation of a proposed constant-one inequality. 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 ambient dimension is not itself a violation: the denominator depends on degree. The function must remain Boolean and nonconstant while its linear coefficient sum outgrows that denominator.
Inputs are Fin n → Bool, with false interpreted as and true as . The first clause requires positive dimension and a nonconstant function. The second restricts to positive Fourier degree and uses ¬ BddAbove, avoiding a real-valued infinity convention.
The shared definitions are supplied by SquareRootDegree. 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 Heilbronn triangle problem asks how large the smallest triangle in an -point set can be. A positive improvement in the exponent would contradict bounds at every scale arbitrarily close to . The source is OpenAI's September 2026 manuscript.
Points lie in the closed unit square in the real plane. Triangle area is half the absolute determinant of the two displacement vectors, and the lower-bound condition quantifies over all triples of distinct points.
The Heilbronn exponent δ is positive and that there exist a sequence of natural numbers n(j) tending to infinity and finite sets P(j) of points in the plane, such that for every j, n(j) ≥ 3, P(j) has exactly n(j) points, all lying in the closed unit square [0,1]×[0,1], and every triple of three distinct points of P(j) spans a triangle of area at least n(j)^(−2+δ). Triangle area is |(q₁−p₁)(r₂−p₂)−(q₂−p₂)(r₁−p₁)|/2. Here δ = 1/(100000·K) with K = T²+1, where T = C(M,3), M = C(4·41−1, 41) = C(163,41), so δ is an explicit but extremely small positive rational constant. Thus the statement asserts an infinite family of point sets whose smallest triangle area is at least a power n^(−2+δ).
The goal is OAI.Problem355.heilbronn_power_lower_bound. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The formal goal gives an unbounded sequence of configurations with a fixed explicit power improvement. An attached companion target rules out an eventual almost- upper bound at half that exponent. 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.
Avoiding collinear triples is insufficient: every nonzero triangle must also satisfy one uniform quantitative area bound. The exponent must stay positive independently of the size of the configuration.
The selected goal asserts a sequence tending to infinity, rather than the stronger all-sufficiently-large-sizes statement in the manuscript. The explicit exponent is heilbronnExponent, built from fixed binomial coefficients. Finite sets eliminate repeated points; real powers specify the area scale.
The shared definitions are supplied by HeilbronnTriangle. 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 triangle deletion constructs a partial triangle packing. Its terminal uncovered edges measure how efficiently this process covers pairs, and the source seeks the leading constant rather than only the growth exponent. The source is OpenAI's September 2026 manuscript.
Start from the complete graph on vertices. At each step choose a remaining triangle uniformly and remove its three edges. A triangle-free state stays fixed. The terminal leave is the edge count at the end.
For the random triangle-removal process, three limits hold as n tends to infinity. The process starts from the complete graph on n vertices, with graphs represented as sets of 2-element subsets of Fin n. At each step, if the current graph G contains triangles (3-subsets all of whose pairs are edges of G), one triangle is chosen uniformly at random and its three edges are deleted; if there is no triangle, the graph stays unchanged. Running this for C(n,2) steps gives the terminal law on graphs, and expectation and probability are taken with respect to it. Writing normalizedLeave(G) = |E(G)| / n^(3/2) and sharpConstant c = 1/(2√2), the theorem asserts: first, the expected value of (normalizedLeave(G) − c)² tends to 0; second, for every ε > 0, the probability that |normalizedLeave(G) − c| > ε tends to 0; and third, the expected number of edges of the terminal graph divided by n^(3/2) tends to c.
The goal is OAI.SharpTerminalLeave.sharp_terminal_leave.
The three conclusions record mean-square concentration, concentration in probability, and the limiting normalized expectation. The exact leading constant is part of the 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.
Early evolution estimates need to remain informative near termination, where triangles become scarce. A high-probability estimate alone need not control the second moment required here.
Graphs are finite sets of pairs from Fin n, with transitions given by probability mass functions. Running for the initial edge count guarantees that the absorbing terminal law is reached. Expectations are finite sums and all limits are along natural tending to infinity.
The shared definitions are supplied by TriangleRemoval. 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.
Finite matroid packing and covering principles connect disjoint spanning sets with independent covers. The source seeks a concrete obstruction to extending the unrestricted principle to infinite ground sets. The source is OpenAI's September 2026 manuscript.
A matroid records independent subsets and their closure. A packing/covering partition divides the common ground set into a part with disjoint spanning sets in restrictions and a part covered by independent sets in contractions. Self-duality means equality with the dual on the same labelled ground set.
The ground type E = ℤ × D, where D is the type of pairs consisting of a natural number m and a Boolean function on Boolean m-tuples, is countable and infinite, and that there exist two matroids M₀ and M₁ on E, each with ground set all of E, each equal to its own dual, such that no independent set of M₀ and independent set of M₁ have union all of E. Yet the pair fails HasPackingCovering. That predicate asks for a partition of the common ground set into P and C, two disjoint subsets S₀ and S₁ of P that are spanning in the restrictions M₀|P and M₁|P respectively, and subsets I₀ and I₁ of C that are independent in the contractions of M₀ and M₁ onto C (the dual of the restriction of the dual to C), with I₀ ∪ I₁ = C. So the theorem asserts a countably infinite pair of self-dual matroids with no such packing-covering decomposition.
The goal is OAI.InfiniteMatroidCounterexample.main. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The goal simultaneously supplies a countable infinite example, failure of a full independent cover, and failure of every mixed partition. Additional attached statements treat partitional matroids, intersection, and the separate packing and covering assertions. 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.
Failure of a full independent cover does not by itself exclude a mixed partition. The matroids must satisfy the infinite independence axioms, including maximal extension, throughout the construction.
The ground type is the fixed product of integers with finite Boolean-function data. Mathlib matroids have ground set equal to the entire type in the goal. The two source definition groups have overlapping declarations and remain separate reference groups, with no aggregate import.
The shared definitions are supplied by InfiniteMatroid, InfiniteMatroidCorollaries. 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.
Excluding a fixed clique should force independent sets larger than those guaranteed by average degree alone. The source asks for the full logarithmic improvement uniformly across graph sizes. The source is OpenAI's September 2026 manuscript.
An independent set contains no adjacent pair. Write for the number of vertices, for average degree, and for the largest independent-set size. A graph is clique-free of order when it contains no pairwise adjacent vertices.
For every natural number r ≥ 4, there is a real constant c > 0 such that the following holds for every finite simple graph G on a vertex type V (a Fintype). Here the average degree d(G) is defined as 2|E(G)|/|V|, twice the number of edges divided by the number of vertices (as a real number). If G contains no clique of size r (it is r-clique-free) and d(G) ≥ 2, then the independence number α(G), the maximum size of an independent set, satisfies α(G) ≥ c · |V| · log(d(G)) / d(G), where log is the natural logarithm of real numbers. The constant c may depend on r but not on G.
The goal is OAI.CliqueFreeLog.logarithmic_independence_bound.
The bound improves the general inverse-degree scale by a factor of natural logarithmic size. The constant may depend on the forbidden clique but must work for every input graph. 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 condition forbids ordinary cliques rather than imposing bounded complexity on every neighborhood. Estimates using maximum degree alone do not establish the stated average-degree bound.
The representation is Mathlib SimpleGraph on a finite type. Real.log is the natural logarithm and the hypothesis keeps its argument and the denominator positive. The empty graph is excluded by that hypothesis.
The shared definitions are supplied by CliqueFreeLog. 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 spanning subgraph in which every vertex has degree two may split into several cycles. Barnette’s question asks when planarity, bipartiteness, and connectivity force those vertices onto one cycle. The source is OpenAI's September 2026 manuscript.
A cubic graph has degree three at every vertex. A bipartite graph has two vertex classes with every edge crossing between them. A Hamiltonian cycle visits all vertices exactly once before returning to its starting point. Planarity is represented by a drawing using injective continuous edge arcs in the real plane.
Every finite simple graph with decidable vertex equality and adjacency has a Hamiltonian cycle if each vertex has degree three, the vertices can be partitioned into two classes with every edge joining different classes, the graph is planar, and it is three-vertex-connected. Here planarity means that vertices can be placed at distinct points of the real plane and edges drawn as injective continuous arcs whose interiors contain no vertices and whose interiors are disjoint for distinct undirected edges; reversing an edge reverses its arc. Three-vertex-connectivity means that the graph has at least four vertices and remains connected after deletion of any set of at most two vertices. The conclusion is the existence of one closed cycle visiting every vertex exactly once before returning to its starting vertex.
The goal is OAI.Barnette.main.
A proof would turn the source’s Hamiltonicity claim into a result available for arbitrary finite graphs satisfying these exact hypotheses. It would also provide a reusable bridge between geometric embeddings and combinatorial walks. 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.
Degree constraints do not guarantee that a spanning cycle cover is connected. The target requires a single cycle and must handle unrestricted face sizes, so verifying local degree conditions is insufficient.
The published goal unfolds MainStatement. Three-vertex-connectivity requires at least four vertices and connectedness after deletion of any set of at most two vertices. The Hamiltonian object is a closed graph walk satisfying the cycle and vertex-coverage conditions. Stronger edge-avoidance conclusions from the paper are not attached as targets.
The shared definitions are supplied by BarnetteHamiltonian. 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.