OAI Math

Motivation

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.

Setting

A Thorp shuffle acts on $2^d$ binary-labelled positions by independent pair switches followed by a cyclic coordinate rotation. A sweep consists of $d$ physical shuffles. Partial observations record an injective ordered list of card positions.

Formalization targets

$$\sup_\sigma\|q_d^{*32800d}\sigma-U\|_{\mathrm{TV}}\to0,\qquad t_{\mathrm{mix}}(d)=\Theta(\log 2^d).$$

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.

Significance

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.

Difficulty

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.

Formalization scope

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.

Selected references

• OpenAI, Random coordinate frames and partial permutation laws, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.
• OpenAI, Conditional information under deterministic coordinate sweeps, preprint, September 2026. Companion manuscript.

Motivation

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.

Setting

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 $k(1+\log(n/k))$.

Formalization targets

$$\text{adaptive bounds}\ \wedge\ \text{Casimir bounds}\ \wedge\ \text{dense truncation}\ \wedge\ \text{sparse contact}\ \wedge\ \text{harmonic bounds}\ \wedge\ \text{smoothing}\ \wedge\ \text{tail bounds}\ \wedge\ \text{high-tail bounds}\ \wedge\ \text{sparse saving}.$$

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.

Significance

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.

Difficulty

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.

Formalization scope

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.

Selected references

• OpenAI, Routing densities and representation contraction for Thorp sweeps, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

Signed tensor components separate different sources of permutation symmetry. The source uses their diagram entropies to budget high moments of the Thorp sweep. The source is OpenAI's September 2026 manuscript.

Setting

A signed occurrence is an injective equivariant map from a tensor product of three Specht modules into the target module, with the second factor transposed. The weighted moment is the target dimension times the trace of a power of the sweep’s positive square.

Formalization targets

$$\log\!\left(\dim S^\lambda\,\operatorname{Re}\operatorname{tr}(Q^*Q)^r\right)\le a(\eta,d)H(\alpha,\beta)+R(\kappa,d,\ell).$$

There is a constant η₀>0 such that for every η with 0<η<η₀ there is a κ₀ with 0<κ₀<η/256 such that for every κ with 0<κ<κ₀ there is a positive integer power r, depending only on η and κ, with the following property for every d≥1. Let λ be a partition of 2^d (a Young diagram with 2^d cells), and let u+v+l=2^d with partitions α of u, β of v and γ of l, such that the signed occurrence condition holds: there is an injective complex-linear map from the tensor product of the Specht modules S^α ⊗ S^(β′) ⊗ S^γ, where β′ is the transpose of β, into S^λ that commutes with the action of S_u×S_v×S_l, embedded in S_(2^d) as block permutations on the consecutive blocks of sizes u, v and l. Here Specht modules are the cyclic submodules of the regular representation of the symmetric group generated by the polytabloid built from the row and column subgroups of a fixed tableau. Identify {0,…,2^d−1} with binary strings of length d, and for each coordinate i let the layer operator be the average of S^λ over the subgroup of permutations preserving every binary coordinate except the i-th. Let the sweep operator be the product of these d layer operators in reverse coordinate order, and let the sweep square be TT with T the sweep operator. Define the weighted moment as dim S^λ times the real part of tr((TT)^r). Then the logarithm of this moment, taken as −∞ when the moment is zero, is at most coefficient(η,d)·H(α,β) + remainderBudget(κ,d,l). Here coefficient(a,d)=a(1−1/(2√d)), the signed entropy H(α,β) is the sum, over all row lengths a of α and of β, of a·log((u+v)/a), and the remainder budget is 0 if l=0 and otherwise max(0, coefficient(κ,d)·l·log(2^d) − l·log(2^d/l)).

The goal is OAI.SignedSweeps.signed_occurrence_moment_bound. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.

• one sided type angle.
• remaining main.

Significance

The target makes the moment power depend only on two small budget parameters, uniformly over cube dimension and every signed occurrence. Supporting targets include the type-angle estimate and a shared mixing bundle. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Ignoring the signed occurrence hypothesis loses the representation-theoretic connection between the component diagrams and the target. The remainder diagram must be charged separately, including its empty case.

Formalization scope

The quantifier order is $\eta_0$, then each small $\eta$, then $\kappa_0<\eta/256$, then each small $\kappa$, then one positive integer $r$. Zero moments have logarithm minus infinity in EReal. Independent source groups stay separate references.

The shared definitions are supplied by SignedSweepMoment, SpinAngle, ThorpRemaining. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, Signed tensor densities and diagram budgets for the Thorp shuffle, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

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.

Setting

The Partition Principle says that a surjection from $X$ onto $Y$ implies an injection from $Y$ into $X$. 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.

Formalization targets

$$\operatorname{Con}(\mathrm{ZF})\quad\Longrightarrow\quad\operatorname{Con}(\mathrm{ZF}+\mathrm{PP}+\mathrm{AC}_{\mathrm{wo}}+\neg\mathrm{AC}).$$

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.

• exists model partitionPrinciple without choice.

Significance

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.

Difficulty

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.

Formalization scope

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.

Selected references

• OpenAI, The Partition Principle does not imply Choice, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

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.

Setting

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.

Formalization targets

$$\exists R\text{ over }\mathbb F_2:\ \operatorname{St}_{12}(R)\text{ is infinite, finitely presented, and periodic}.$$

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.

Significance

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.

Difficulty

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.

Formalization scope

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.

Selected references

• OpenAI, An infinite finitely presented periodic group, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

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.

Setting

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.

Formalization targets

$$\exists G:\quad |G|=\infty,\quad G\text{ finitely presented and simple},\quad\forall K,\varepsilon>0\ \exists D:\ |gD\triangle D|<\varepsilon|D|\ (g\in K).$$

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.

Significance

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.

Difficulty

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.

Formalization scope

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.

Selected references

• OpenAI, An infinite finitely presented simple amenable group, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

A classifying-space problem asks whether a natural complex captures a group without additional higher homotopy. The source addresses the finite-rank Artin problem through the lifted spherical-cell complex. The source is OpenAI's September 2026 manuscript.

Setting

An Artin group is presented by alternating braid relations from a Coxeter matrix. A subset of generators is spherical when its associated Coxeter parabolic subgroup is finite. Lifted cells pair a group element with such a subset, with incidence determined by reduced coset words.

Formalization targets

$$\operatorname{ContractibleSpace}(\operatorname{SalvettiCover}(M))\qquad\text{for every Coxeter matrix }M\text{ on finite }S.$$

For every Coxeter matrix M indexed by a finite type S of standard generators, the topological space SalvettiCover(M) is contractible. The Artin group Artin(M) is the free group on S modulo the braid relators, one for each ordered pair (s,t): the alternating word s t s t ... of length M(s,t) times the inverse of the alternating word t s t s ... of the same length. A subset T of S is spherical when the standard parabolic subgroup of the Coxeter group generated by the simple reflections in T is finite. A lifted cell is a pair (a,T) of an Artin group element and a spherical subset. One lifted cell (a,T) is a face of (b,U) when T is contained in U and there is a word w in letters of U that is reduced in the Coxeter group (its Coxeter length equals the word length), is of minimal length in its coset with respect to the parabolic subgroup generated by T, and satisfies a = b times the image of w in the Artin group. The preorder on lifted cells is the reflexive transitive closure of this face relation, and SalvettiCover(M) is the geometric realization, as a topological space, of the nerve of that preorder viewed as a category.

The goal is OAI.HarmonicArtin.salvetti_cover_contractible.

Significance

The goal makes the full topological realization contractible, rather than only asserting vanishing of a selected homotopy group. It supplies a precise target for the covering-space component of the source. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Local spherical pieces need not automatically fit into a globally contractible realization. The face relation and its transitive closure must retain the interaction between Artin words and Coxeter length.

Formalization scope

SalvettiCover is the geometric realization of the nerve of the lifted-cell preorder. The generator type is finite but need not be equipped with a chosen enumeration. The mission preserves this published model instead of substituting a different complex.

The shared definitions are supplied by HarmonicArtin. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, Harmonic heights and the Artin K(pi,1) conjecture, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

Standard generator subsets define natural subgroups in an Artin group. The source asks whether arbitrary conjugates of these subgroups remain in the same class after intersection. The source is OpenAI's September 2026 manuscript.

Setting

A standard parabolic subgroup is generated by a subset of the standard generators. A parabolic subgroup is any conjugate of one. There is no requirement that its Coxeter subgroup be finite.

Formalization targets

$$gA_Xg^{-1}\cap hA_Yh^{-1}=kA_Zk^{-1}\quad\text{for some }Z\subseteq S,\ k\in A_M.$$

The theorem, which is admitted in the source with a placeholder proof, states the following for a Coxeter matrix M on a finite, linearly ordered index set S, with Artin(M) the Artin group presented on generators S by the braid relations: the word of alternating generators s,t,s,... of length M(s,t) equals the alternating word beginning with t, for each pair s,t. For any two subsets X and Y of S and any two elements g and h of Artin(M), there exist a subset Z of S and an element k of Artin(M) such that the intersection of the two conjugate subgroups g P_X g⁻¹ and h P_Y h⁻¹ equals k P_Z k⁻¹. Here P_T is the standard parabolic subgroup generated by the images of the generators in T, and conjugation by g is the subgroup whose members x satisfy g⁻¹xg in P. There is no spherical-type or other restriction on M, so the intersection of two conjugates of standard parabolic subgroups is itself a conjugate of a standard parabolic subgroup.

The goal is OAI.HarmonicArtin.ParabolicIntersections.unconditional_parabolic_intersections. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.

• unconditional arbitrary intersections.
• unconditional nonclique dynamics.
• unconditional parabolic closure.

Significance

The selected goal is closure under binary intersection. Attached results also give arbitrary intersections controlled by at most the rank many members, unique parabolic closure, and dynamics for irreducible non-clique groups. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Conjugation obscures the standard generating subsets, so intersecting $X$ and $Y$ alone does not describe the subgroup intersection. The target must produce both a new subset and a new conjugating element.

Formalization scope

The generating type is finite and linearly ordered. The Coxeter-matrix convention encodes an infinite label by zero. The dynamics milestone has additional irreducibility and non-clique assumptions; those are not imposed on the intersection theorem.

The shared definitions are supplied by ArtinParabolicIntersections. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, Parabolic intersections in Artin groups, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

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.

Setting

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.

Formalization targets

$$\exists K:\quad K\text{ finite, connected, aspherical, with linear disk filling},\quad\pi_1K\text{ hyperbolic with no geometric CAT(0) action}.$$

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.

Significance

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.

Difficulty

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.

Formalization scope

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.

Selected references

• OpenAI, A hyperbolic group with no geometric CAT(0) action, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

Replacing a hyperboloidal end by an asymptotically flat end can connect Bondi mass with ADM mass. The source seeks a replacement that preserves interior geometry, the energy condition, and almost all enclosing area. The source is OpenAI's September 2026 manuscript.

Setting

A CKS exterior datum describes a three-dimensional hyperboloidal end and its mass aspect. Its Bondi charge is energy-momentum $(E,P)$, assumed strictly future timelike. An enclosing cut is a surface in the supplied geometric class; its area is computed from the metric.

Formalization targets

$$g_R\ge(1-\varepsilon(R))g,\quad\varepsilon(R)\to0,\quad m_{\mathrm{ADM}}(g_R)=\sqrt{E^2-|P|^2}+\eta_R,\quad0\le\eta_R\le2R^{-1/2}.$$

For a connected, Hausdorff, second countable smooth 3-manifold N with boundary and a smooth Riemannian metric g with a smooth symmetric tensor field K, such that N is orientable, the boundary is compact and nonempty, g is complete, and (g,K) satisfies the pointwise local-chart physical dominant energy condition PhysicalDEC, the following holds. Suppose d is a CKS exterior-end datum for (g,K): a coordinate end outside radius d.chart.radius in which g and K are represented by smooth perturbations, together with a smooth mass aspect function on the sphere and the tensor patches realizing it. If the Bondi charge (energy, momentum) of d's mass aspect, (E,P), is timelike, meaning |P|<E, then there exist another such datum d', a radius R₀ with d'.chart.radius<R₀ and 12≤R₀, and a function ε with ε(R)→0 as R→∞, such that d' has Bondi charge (√(E²−|P|²),0), and the minimal enclosing area of g is finite. Moreover, for every R≥R₀ one has 0≤ε(R)<1 and there are a complete smooth metric gR, a smooth symmetric tensor field kR, spatial tensor fields G and k on Euclidean 3-space, and a number η with these properties. The pair (gR,kR) agrees with (g,K) at every point outside the chart domain or with chart coordinate norm at most R, and satisfies PhysicalDEC and integrable constraints. Also gR≥(1−ε(R))g as quadratic forms. On the end, gR and kR equal the end metrics built from G and k in d'.chart. Each Cartesian component of G minus the identity satisfies the order-1 Symbol condition from CKSADM, and k vanishes where ‖x‖>2R². As r→∞ the spatial ADM energy of G tends to √(E²−|P|²)+η and the ADM momentum of (G,k) tends to 0, with 0≤η≤2R^(−1/2). Finally, gR has finite minimal enclosing area, (1−ε(R)) times the minimum enclosing area of g is at most that of gR, and for every outer domain D the cut areas of g and gR are finite and satisfy (1−ε(R))·cutArea(g,D)≤cutArea(gR,D).

The goal is OAI.CKSSourceExterior.area_controlled_end_replacement. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.

• schwarzschild equality examples.

Significance

The selected goal constructs end replacements with zero limiting ADM momentum and quantitative area comparison, including minimum enclosing area. The Schwarzschild equality examples are attached as a separate 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.

Difficulty

Changing the end can create a cheaper enclosing surface or violate the dominant energy condition. Agreement on each retained interior region does not alone prevent either problem.

Formalization scope

The manifold is a connected Hausdorff second-countable smooth three-manifold with compact nonempty boundary, and the original complete data satisfy the physical dominant energy condition. The main target is end replacement; it does not itself state the final Bondi–Penrose inequality. The equality-example target keeps its stronger boundary and no-additional-horizon hypotheses.

The shared definitions are supplied by CKSBondiPenrose, CKSBondiPenrose_002. 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.

Selected references

• OpenAI, Area-controlled end replacement and the Bondi Penrose inequality in the CKS class, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

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.

Setting

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.

Formalization target

The selected goal is OAI.CoulombAtom.generalized_ionization. Its central assertion is

$$I(m,Z)/m^{7/3}\longrightarrow a,\qquad m\to\infty,\ Z/m\to\infty.$$

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.

Significance and status

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.

Difficulty

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.

Formalization scope

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.

Selected references

• OpenAI, Generalized ionization energies for full Coulomb atoms, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

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.

Setting

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.

Formalization target

The selected goal is OAI.NeutralAtom.generalized_outer_radii. Its central assertion is

$$m^{1/3}R_m^{\rm upper},\ m^{1/3}R_m^{\rm lower}\longrightarrow (81\pi^2/2)^{1/3}.$$

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.

Significance and status

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.

Difficulty

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.

Formalization scope

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.

Selected references

• OpenAI, Generalized outer-electron radii of neutral Coulomb atoms, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

Character sums express phase constraints on complex Hadamard matrices. In dimension six these constraints also bear on how many mutually unbiased bases can coexist. The pinned manuscript supplies the research context.

Setting

A complex Hadamard matrix has unit-modulus entries and conjugate-transpose product 6I. Equivalence permits row and column permutations and unit phases. Tao's cubic matrix supplies the exceptional class.

Formalization target

The selected goal is OAI.MUB6.fourier_and_family_bound. Its central assertion is

$$g_H(\pi(1,1,1,-1,-1,-1))=0,\qquad n_{\rm MUB}\leq5.$$

The theorem states a conjunction of two claims about 6x6 complex matrices and mutually unbiased bases in C^6. First, for every complex Hadamard matrix H of order 6 (all entries of modulus 1 and HH = 6I, where H is the conjugate transpose) that is not equivalent to the specific matrix tao, every permutation π of the six coordinates gives g(H, alpha∘π) = 0. Here the character of a column x at an integer exponent vector a is the product over i of x_i^{a_i}, g(H,a) is (1/6) times the sum over the six columns k of H of the character of column k at a, and alpha is the exponent vector (1,1,1,-1,-1,-1), so alpha∘π is alpha with its entries permuted. Equivalence of H and K means K_{ij} = u_i H_{r(i),c(j)} v_j for some row and column permutations r, c and unit-modulus complex phase vectors u and v. The matrix tao has entries ω^{e_{ij}}, where ω = exp(2πi/3) and e is a fixed 6x6 exponent matrix with zero first row and column and a five-cycle pattern of exponents 0, 1, 2 in the remaining 5x5 block. Second, for every natural number n, if there exist n orthonormal bases of C^6 that are pairwise mutually unbiased, meaning |<b_i, b'_j>|^2 = 1/6 for all vectors of two distinct bases, then n ≤ 5. This is stated as an admitted theorem, not a verified proof.

Significance and status

The goal is the conjunction of Fourier vanishing outside the specified equivalence class and the bound on attainable families. The cube-fiber statement is an additional published supporting target with its own hypotheses. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

Orthogonality immediately kills certain degree-two characters, but the target concerns a balanced degree-six character and a separate global bound on families of bases.

Formalization scope

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.HadamardSix.rowRatio_cubeFiber_sum_zero (Open).

Selected references

• OpenAI, Exact Fourier certificates for complex Hadamard matrices of order six, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.