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?
Uniform discreteness places a lower bound on distances between points. The target tests whether that metric simplicity forces uniformly bounded finite-rank approximation in the associated Lipschitz-free space. The pinned manuscript supplies the research context.
The free space is the closed real span of point evaluations in the dual of Lipschitz functions vanishing at a base point. Approximation and bounded approximation retain their distinct operator-norm quantifiers.
The selected goal is OAI.DiscreteFree.source_endpoints. Its central assertion is
The theorem states that two propositions hold together, both about the Lipschitz-free space FreeSpace(o) of a pointed metric space (M,o), which is the closed linear span, inside the dual of the Banach space Lip0(o) of real Lipschitz functions vanishing at o (normed by the supremum of the slopes |f(x)-f(y)|/d(x,y)), of the point evaluations; delta(o,a) denotes the evaluation at a. The first, BlockStatement, says that for every natural number p ≥ 1 there exist a countable metric space M and a base point o with all distinct points at distance at least 1 and all distances at most 300p²+150p+5, together with a finite set A of M containing o, such that every bounded linear operator T on FreeSpace(o) of finite rank and norm at most p moves some delta(o,a) with a in A by at least 1/2, that is ‖T(delta(o,a))-delta(o,a)‖ ≥ 1/2. The second, MainStatement, says there exist a countable metric space M and a point o such that distinct points are at distance at least 1, M is unbounded, M is not a proper space, FreeSpace(o) has the approximation property (finite-rank bounded operators approximate the identity uniformly on every compact set to within any ε>0), and yet for every Λ ≥ 1 FreeSpace(o) fails the bounded approximation property with constant Λ, meaning the approximating finite-rank operators cannot all be chosen with norm at most Λ. The theorem is stated with sorry, so no proof is asserted here.
The selected conjunction includes quantitative block obstructions and an unbounded, nonproper, uniformly discrete example. The quantitative real-ℓ1 renorming target is retained as an additional reference. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Compact-set approximation must remain possible while every candidate uniform norm bound fails. The finite block obstruction must survive in one countable space.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
Additional published targets are included as separate references:
adc7f1241b42. Selected goal source.Markov type is a metric inequality for the displacement of reversible chains. The target connects this probabilistic control to the possibility of uniformly convex renorming. The pinned manuscript supplies the research context.
Chains are finite, stationary and reversible. A map sends their states into a complete real normed space, and the inequality compares n-step and one-step pth displacement moments.
The selected goal is OAI.MarkovSuperreflexivity.hasNontrivialMarkovType_iff_hasEquivalentUCNorm. Its central assertion is
The theorem states that for a real normed space X that is complete (a Banach space), X has nontrivial Markov type if and only if X admits an equivalent uniformly convex norm. Nontrivial Markov type means there exist p>1 and K>0 such that for every finite reversible Markov chain on m states {0,…,m−1}, with stationary probability vector π, nonnegative row-stochastic transition matrix P, and detailed balance π(s)P(s,t)=π(t)P(t,s), every map f from the states to X, and every n≥1, the expected value of ‖f(Z_n)−f(Z_0)‖^p along n-step paths, started from π, is at most K^p·n times the corresponding one-step expectation of ‖f(Z_1)−f(Z_0)‖^p. Having an equivalent uniformly convex norm means there is a seminorm q on X and constants a,b>0 with a‖x‖≤q(x)≤b‖x‖ for all x, such that for every ε in (0,2] there is δ>0 with q((x+y)/2)≤1−δ whenever q(x)≤1, q(y)≤1 and q(x−y)≥ε.
The exact target uses uniformly convex norms with two-sided equivalence constants. It is not phrased as a direct uniformly smooth norm construction. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The inequality is uniform over all finite chains and state maps, while the conclusion is one norm controlling all vectors of the Banach space.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.The separable quotient problem asks whether every infinite-dimensional Banach space admits a separable infinite-dimensional quotient. The selected statement isolates a negative result under the continuum hypothesis. The pinned manuscript supplies the research context.
A quotient is encoded as a surjective bounded linear map between Banach spaces over the same scalar field. The target considers both real and complex scalars.
The selected goal is OAI.SeparableQuotient.negative_main. Its central assertion is
The theorem states that, under the continuum hypothesis CH (the defined proposition that the cardinality of ℝ equals ℵ₁), the separable quotient assertion fails over both the real and the complex numbers, at any universe level u. Here SQ over a scalar field 𝕜 (ℝ or ℂ) asserts that every complete normed space X over 𝕜 in Type u that is not finite-dimensional has a separable quotient in the following sense: there exist a complete, separable, infinite-dimensional normed space Y over 𝕜, also in Type u, and a bounded 𝕜-linear map T from X to Y that is surjective. The conclusion is the conjunction of ¬SQ(ℝ) and ¬SQ(ℂ), so for each field there is an infinite-dimensional Banach space with no such bounded surjection onto an infinite-dimensional separable Banach space. The statement is admitted without proof in the source.
CH is an explicit assumption. The published goal does not state relative consistency, a positive model, or the complete independence assertion in the manuscript title. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The obstruction must rule out every bounded surjection onto every separable infinite-dimensional target space, rather than one proposed quotient.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.The homotopy hypothesis relates algebraic higher groupoids to spaces. Elementary expansions provide a concrete test of whether adjoining a higher cell preserves homotopy information. The pinned manuscript supplies the research context.
C is a globular coherator in the encoded convention, X is a cellular model, and Y is a pushout that attaches an (n+1)-disk along the source-face inclusion of an n-disk.
The selected goal is OAI.Grothendieck.elementary_expansion. Its central assertion is
The theorem states that, for a coherator C (a globular theory, meaning a category of shapes built from globes by iterated gluing, with morphisms preserving the globular pushouts, which has a cellular presentation as a countable-stage colimit of free extensions along admissible pairs of parallel cells and in which every admissible pair is filled by some morphism), the following holds for models of C, i.e. presheaves on C sending globular pushouts to pullbacks. Let X be a cellular model, meaning that it is built from an initial model by a well-ordered transfinite composition in which each successor step attaches cells freely along boundaries of cells of the previous stage. Let n be a natural number, let a be a map from the free model disk(n) on the n-globe to X, and let J_n : disk(n) → disk(n+1) be the map induced by the source-face inclusion of the n-globe into the (n+1)-globe. If Y, together with i : X → Y and b : disk(n+1) → Y, forms a pushout square of a and J_n, then i is a weak equivalence. Here weak equivalence means that i induces a bijection on sets of components (0-cells modulo being joined by a 1-cell) and, for every 0-cell x of X and every n, a bijection on homotopy groups, which are classes of n-loops based at the degenerate cells above x, identified when joined by an (n+1)-cell.
The selected goal is the elementary-expansion theorem. It does not itself assert the complete equivalence between the homotopy theory of spaces and all coherator models. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The conclusion requires preservation of components and every based homotopy group, for cellular models built through transfinite attachments.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.Tensorial absorption is a structural regularity property of a C*-algebra. A criterion in the central-sequence algebra would detect it through asymptotically commuting elements. The pinned manuscript supplies the research context.
For a nontrivial separable unital C*-algebra A and a free ultrafilter, the central algebra is the commutant of A's diagonal copy inside its norm ultrapower.
The selected goal is OAI.KirchbergRordam.character_criterion. Its central assertion is
The theorem states that, for a nontrivial separable C*-algebra A (in the base universe Type) and a free ultrafilter ω on the natural numbers, meaning an ultrafilter that refines the cofinite filter, the norm central-sequence algebra of A has no characters if and only if A is isomorphic to its minimal (spatial) C*-tensor product with the Jiang–Su algebra. The norm ultrapower of A is the quotient of the C*-algebra of bounded sequences in A by the ideal of sequences whose norms tend to zero along ω; the central algebra is the closed star-subalgebra of this ultrapower consisting of elements commuting with the diagonal copy of A, the images of constant sequences. The central algebra has no characters means that every star-homomorphism from it to ℂ (a linear, multiplicative, star-preserving map, not required to preserve the unit) is the zero map. The Jiang–Su algebra is the inductive limit C*-algebra of the standard prime-dimension-drop model system. The right-hand side asserts the existence of a star-algebra isomorphism over ℂ from A onto this tensor product. The proof is admitted in the source.
The target is the character criterion for one algebra and one free ultrafilter. The manuscript's infinite tensor-power consequence is not separately attached. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The two directions relate a scalar-valued representation obstruction to an isomorphism with a tensor product, using the precise inductive-limit Jiang–Su model.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.Quasitraces behave linearly on commutative subalgebras but need not initially be additive on all positive elements. A uniform defect on a fixed pair would separate them from traces. The pinned manuscript supplies the research context.
The algebra is separable and carries a normalized 2-quasitrace, meaning a quasitrace with the specified extension to two by two matrices. The witnesses are positive contractions.
The selected goal is OAI.Kaplansky.kaplansky_quasitrace_counterexample. Its central assertion is
The theorem (admitted in the source, not proved there) states that there exists a separable C*-algebra A, with its complex C*-algebra structure, for which the following hold. First, A carries a normalized 2-quasitrace. Here a 1-quasitrace is a function τ : A → ℂ such that τ(xx) is a nonnegative complex number for all x; τ(xx) = τ(xx*); τ(h + i k) = τ(h) + i τ(k) for self-adjoint h and k; and the restriction of τ to every norm-closed commutative (non-unital) star-subalgebra over ℂ is ℂ-linear. It is normalized if τ(1) = 1, and it is a 2-quasitrace if it extends to a 1-quasitrace σ on the 2×2 matrices over A (as a C*-matrix algebra) satisfying σ of the matrix with a in the upper-left corner and zeros elsewhere equal to τ(a) for all a. Second, there are positive contractions a and b in A, meaning each is of the form x*x and has norm at most 1, such that every normalized 2-quasitrace τ on A satisfies Re(τ(a+b) − τ(a) − τ(b)) ≥ 1/144. So no such τ is additive on this pair.
The selected goal is the quantitative quasitrace counterexample. The stable-finiteness and tensor-product consequences are retained as a separate published bundle. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The same positive contractions must exhibit the defect for every normalized 2-quasitrace, while at least one such quasitrace exists.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
Additional published targets are included as separate references:
adc7f1241b42. Selected goal source.Hilbert-space spectral localization does not automatically produce bounded elements of the underlying operator algebra. Bounded recovery asks when positive averaged detection survives that passage. The pinned manuscript supplies the research context.
A standard modular datum has a cyclic separating vector, spectral calculus and scalar centralizer. Unit vectors lie in shrinking bands around a fixed real spectral parameter.
The selected goal is OAI.BoundedRecovery.bounded_recovery. Its central assertion is
The theorem states that, for a standard modular datum S on a complex Hilbert space H (a von Neumann algebra M with a unit cyclic and separating vector ξ, a nondegenerate real spectral calculus D with unitary group D.unitary t, an antilinear isometric involution J, and a closed Tomita graph of a ↦ (aξ, a*ξ) over a ∈ M equal to the pairs (p, Jq) where p is mapped to q by the half-exponential graph of D) satisfying ScalarCentralizer (every a in M fixed by conjugation with D.unitary t for all real t is a complex multiple of the identity), the following holds. Let ω be an ultrafilter on ℕ that refines the at-infinity filter (ω ≤ atTop), let T be a bounded complex-linear operator on H, let s be real, and let δₙ > 0 tend to 0. Suppose hₙ are unit vectors, each with spectral support in the interval [s − δₙ, s + δₙ] (every bounded continuous function vanishing on that interval annihilates hₙ under the calculus), and suppose the limsup over n of the ω-limit of the symmetric time averages (1/2k)∫{−k}^{k} ‖T(D.unitary t hₙ)‖² dt is strictly positive. Then the recovery conclusion holds: there are a strictly increasing sequence nⱼ, operators vⱼ in M, and constants C and η > 0 such that for every j, ‖vⱼ‖ ≤ C, ‖T(vⱼ ξ)‖ ≥ η, and vⱼξ has spectral support in [s − 4δ{nⱼ}, s + 4δ_{nⱼ}]. The proof is admitted, not supplied.
The hypothesis is positivity of the specified ultrafilter time average and outer limsup. Bicentralizer triviality and further rigidity applications are not separate conclusions of this target. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The recovered vectors must come from uniformly bounded algebra elements while retaining detection and shrinking spectral support along a subsequence.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.A hierarchy of infinitely many overlap scales need not fill an interval. Full support asks whether an admissible zero-temperature SK minimizer leaves any gap below overlap one. The pinned manuscript supplies the research context.
An order parameter is a nonnegative, monotone, right-continuous integrable function on [0,1). The Parisi value is defined by a Brownian stochastic-control supremum. The Stieltjes measure μ lives on the subtype Time=[0,1); its support below is taken in that relative topology.
The selected goal is OAI.ZeroTemperatureSK.full_support. Its central assertion is
The theorem states that, for any probability space carrying a real Brownian motion B (a BrownianSystem W) and any order parameter γ on [0,1), if γ minimizes the Parisi functional over all order parameters, then a five-part full-support conclusion holds. An order parameter γ:[0,1)→ℝ is nonnegative, monotone, right-continuous and integrable (extended by zero outside [0,1)). For a time t and position x, the value is the supremum, over controls α progressive for the filtration generated by the Brownian increments after t and bounded by 1 in absolute value, of the expected payoff |x + B₁ − B_t + ∫_t^1 γ(s)α(s−t)ds| − ½∫_t^1 γ(s)α(s−t)²ds. The gradient and curvature are its first and second derivatives in x, and the Parisi functional is value at (0,0) minus ½∫_0^1 tγ(t)dt. Being a minimizer means the functional at γ is at most its value at every order parameter η. The conclusion says: (1) there is a measure μ on [0,1) with μ((−∞,t]) = γ(t) for every t in [0,1); (2) there is a diffusion X, a process progressive for the Brownian filtration that almost surely is continuous on [0,1], starts at 0, and satisfies X_t = B_t + ∫_0^t γ(s)·gradient(s,X_s)ds; (3) every such measure μ has full support, equal to all of [0,1); (4) γ is strictly increasing, γ(a)<γ(b) whenever a<b; and (5) for every such diffusion X and every t in [0,1), the expected square of the gradient at X_t equals t, and the expected square of the curvature at X_t equals 1.
The main target is the five-part full-support conclusion for every encoded minimizer and Brownian system. The separate value-consequences bundle is retained as an additional formal target. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The conclusion couples support, strict increase, diffusion existence and derivative identities. Minimization alone is not an assumption of those conclusions.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
Additional published targets are included as separate references:
OAI.SKValue.value_consequences (Open).adc7f1241b42. Selected goal source.Vertex operator algebras describe conformal theories algebraically, while conformal nets describe local operator algebras. Passing between them requires analytic control of fields. The pinned manuscript supplies the research context.
The selected algebra is simple, unitary, CFT-type and strongly rational. Its modes act on an inner product space, and smeared fields act on the Hilbert completion.
The selected goal is OAI.MinimalVertex.main. Its central assertion is
The theorem states that, for a CFT-type vertex operator algebra A on a complex inner product space V (a vertex algebra with vacuum, state-field map and Jacobi identity, together with a conformal vector, central charge, finite-dimensional graded pieces with degree-zero part spanned by the vacuum, conformal vector in degree 2 acting as the grading operator, and the Virasoro relations), equipped with a unitary structure U (an antilinear involution fixing the vacuum and conformal vector, compatible with all modes, together with a unit-norm vacuum and an invariance relation between a mode and the corresponding mode of the transformed adjoint-side vector), if A is simple (nonzero vacuum and no ideals other than 0 and the whole space) and strongly rational (self-contragredient, rational in the sense that every admissible weak module is completely reducible, and C2-cofinite), then three things hold. First, A has polynomial energy bounds: for every a in V there are C>0 and natural numbers p,k with ||a_(n) b|| ≤ C(1+|n|)^p ||(1+L_0)^k b|| for all integers n and all b in V. Second, the CKLW strong locality property holds: all vectors satisfy these bounds, and for every proper circle arc I the von Neumann algebra generated by closed smeared fields supported in I, built on the completion of V, lies in the commutant of the algebra attached to the complementary arc. Third, the assignment of these interval algebras to proper arcs admits the structure of an irreducible conformal net, meaning a separable Hilbert space with isotony, locality, a continuous Mobius representation extended to a continuous projective representation of smooth circle diffeomorphisms with covariance and locality of the action, a unit invariant vacuum that is unique up to scalar and cyclic, a positive self-adjoint Hamiltonian generating the rotation flow, and trivial commutant of all interval algebras apart from scalars.
The target proves polynomial energy bounds, the specified CKLW strong locality property, and existence of an irreducible conformal-net structure. Complete rationality, category equivalences and extension classification are not conclusions of this reference. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Formal algebraic identities must yield polynomial operator bounds and locality for closed smeared fields on the completion.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.The parity function tests whether a shallow quantum circuit can combine information from all input bits. Polynomially many ancillary qubits make the measured-output formulation substantially stronger than a restriction to clean final registers. The pinned manuscript supplies the research context.
Allowed gates are arbitrary one-qubit unitaries and Toffoli gates with finitely many controls. Gates within a layer have disjoint supports. Inputs occupy the first n qubits, with zero ancillas.
The selected goal is OAI.QAC.parity_lower_bound_polynomial_size. Its central assertion is
The theorem states that, for any positive integers d, k and C, there is a threshold n₀ such that for every n ≥ n₀ and every total qubit count N with n ≤ N ≤ C(n+1)^k, the following holds. Take any circuit given as a list of at most d physical layers on N qubits, where a layer is a list of gates with pairwise disjoint supports and each gate is either a one-qubit unitary on a single qubit or a Toffoli gate with an arbitrary finite set of control qubits and a target outside that set (flipping the target exactly when all controls are 1). The circuit's matrix is the product of the layer matrices, with the first layer acting first. For every choice of output qubit out among the N qubits, there exists an n-bit input x such that successProbability, the total Born probability over all final computational-basis strings y whose out-th bit equals the parity (sum mod 2) of x, is strictly less than 2/3. Here the input state is x placed on the first n qubits with all remaining qubits set to 0, and the remaining qubits are summed over with no requirement that they be clean. So fixed-depth circuits with polynomially many qubits cannot compute parity with worst-case success probability at least 2/3. The theorem is admitted in the source (proof is sorry).
The published goal fixes success threshold 2/3 and positive integer depth, polynomial exponent and coefficient. It does not state the manuscript's full range of positive advantages. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The bound covers arbitrary gates, all choices of output qubit and polynomially many total qubits. Discarded registers can retain unrestricted garbage.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.An exterior electron count defines a radius of a neutral atom without selecting individual electrons. Its scaling tests how well Thomas–Fermi theory describes the outer region of the full interacting atom. The pinned manuscript supplies the research context.
Choose any normalized ground state for each neutral atom with N+1 electrons. The radius is the infimum of radii outside which the expected electron mass is at most m.
The selected goal is OAI.NeutralAtom.generalized_outer_radii. Its central assertion is
The theorem states that, for every choice of wavefunctions Ψ_N for neutral atoms with N+1 electrons and nuclear charge Z=N+1 (each a spin-dependent complex function of N+1 positions in three-dimensional space, with spins taking two values), such that each Ψ_N is a normalized ground state, the outer radii of the atoms obey a Thomas–Fermi-type scaling law. A normalized ground state is an antisymmetric wavefunction with a weak gradient, square-integrable in each spin component together with its gradient, with finite Coulomb integrals against |Ψ|², total squared norm 1 summed over spins, and minimal energy among all such normalized functions. The energy is half the squared L² norm of the gradient plus the expectation of the Coulomb potential, which is −Z times the sum of inverse distances of electrons to the nucleus plus the sum of inverse inter-electron distances over pairs. The electron density is N+1 times the spin-summed integral of |Ψ|² over the other N positions, and the radius for m is the infimum of r≥0 such that the density mass outside the ball of radius r is at most m. For each m, upperRadius and lowerRadius are the limsup and liminf, in the extended reals, of these radii as N→∞ with N+1>m. With bTF=(81π²/2)^(1/3), the theorem states that both m^(1/3)·upperRadius(m) and m^(1/3)·lowerRadius(m) converge to bTF as m→∞ through the natural numbers.
The target uses extended-real upper and lower radii, followed by a natural-number limit in m. No spherical symmetry is assumed, and the atom remains neutral. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The assertion must hold for every choice of ground states. The inner large-charge limsup and liminf cannot be silently replaced with an assumed pointwise limit.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.Removing outer electrons changes an atom's energy on a smaller scale than its total binding energy. A total-energy asymptotic alone does not determine the difference. The pinned manuscript supplies the research context.
The quantum model uses antisymmetric spin-dependent wavefunctions, two spin states, weak gradients and the full nuclear and electron-electron Coulomb interactions. The comparison is with the Thomas–Fermi density functional.
The selected goal is OAI.CoulombAtom.generalized_ionization. Its central assertion is
The theorem states that the proposition MainStatement holds: there is a real constant a>0 such that three asymptotic statements about atomic ionization energies all hold with this same a. Here the quantum energy of N electrons around a nucleus of charge Z is the infimum, taken over admissible spin-dependent wavefunctions on (ℝ³)^N, of the energy (1/2) times the total squared L² norm of all gradient components, minus Z times the expectation of Σᵢ 1/|xᵢ|, plus the expectation of Σ_{i<j} 1/|xᵢ−xⱼ|, with energy defined as 0 when N=0. Admissibility means that each spin component and each prescribed gradient component is square integrable, the gradient components are the weak partial derivatives of the values, the values are antisymmetric under simultaneous permutation of spins and positions (by the sign of the permutation, almost everywhere), the total squared norm summed over spins is 1, and the nuclear and electron-electron Coulomb densities are integrable. The ionization energy of removing m electrons from a neutral atom of charge Z is ionization(m,Z)=E(Z, Z−m)−E(Z, Z), with natural-number subtraction. The Thomas-Fermi energy tfEnergy(Z,M) is the infimum over nonnegative integrable densities ρ on ℝ³ of total mass M, with ρ^{5/3}, ρ/|x| and ρ(x)ρ(y)/|x−y| integrable, of (3/10)(3π²)^{2/3}∫ρ^{5/3} − Z∫ρ/|x| + (1/2)∬ρ(x)ρ(y)/|x−y|, and tfIonization(m,Z)=tfEnergy(Z,Z−m)−tfEnergy(Z,Z) for real m and Z. The three conclusions are: for every real m>0, tfIonization(m,Z) tends to a·m^{7/3} as the real number Z tends to infinity; for all natural-number sequences m_j, Z_j with 1≤m_j<Z_j, m_j→∞ and Z_j/m_j→∞, the ratio ionization(m_j,Z_j)/m_j^{7/3} tends to a; and as m→∞ through the naturals, both limsup and liminf over Z of ionization(m,Z), each divided by m^{7/3}, tend to a.
The main proposition includes a positive common constant, the fixed-m Thomas–Fermi limit, the joint quantum limit, and normalized limsup and liminf limits. It concerns energies rather than outer-electron radii. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Errors negligible relative to the total atomic energy can still dominate ionization energies. The common leading constant must work in the joint regime and both iterated limits.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.Random site energies change the spectral behavior of a lattice Schrödinger operator. Identifying its almost-sure spectrum is one part of the planar Anderson problem. The pinned manuscript supplies the research context.
The lattice is the integer plane. A state is a square-summable complex function on its sites, and the potential at each site is independently uniform on the interval from −h to h, with h positive.
The selected goal is OAI.PlanarAnderson.anderson_spectrum_ae. Its central assertion is
The theorem states that for every real h>0, for almost every disorder configuration v under disorderLaw(h), there exists a bounded complex-linear operator H on the Hilbert space ℓ²(ℤ², ℂ) of square-summable complex functions on the planar lattice ℤ×ℤ such that H is an Anderson operator for v, H is self-adjoint, and the spectrum of H in ℂ equals the real interval [-4-h, 4+h] (embedded in ℂ as the points with imaginary part 0). Here a configuration is a real-valued function v on lattice sites, and disorderLaw(h) is the infinite product measure over sites of the uniform distribution (Lebesgue measure conditioned on the interval) on [-h,h], so the potential values are independent. H is an Anderson operator for v when, for every u in ℓ² and every site x=(a,b), (Hu)(a,b) = u(a+1,b)+u(a-1,b)+u(a,b+1)+u(a,b-1)+v(a,b)u(a,b), the sum of the four nearest-neighbour values plus the local potential times u at x. The statement is recorded as an admitted theorem.
The selected goal asserts existence, self-adjointness and the spectrum interval. Pure-point spectral type, a complete eigenbasis and dynamical localization are not conclusions of this published target. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The interval must be identified almost surely for an infinite random operator, including both exclusion of spectrum outside the interval and inclusion of its interior.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.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.
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.
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.
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.
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.