All missions

Motivation

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.

Setting

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.

Formalization target

The selected goal is OAI.DiscreteFree.source_endpoints. Its central assertion is

$$\mathrm{AP}(\mathcal F(M))\quad\land\quad\forall\Lambda\geq1,\ \neg\mathrm{BAP}_\Lambda(\mathcal F(M)).$$

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.

Significance and status

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.

Difficulty

Compact-set approximation must remain possible while every candidate uniform norm bound fails. The finite block obstruction must survive in one countable space.

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.DiscreteFree.real_l1_quantitative_renorming (Open).

Selected references

• OpenAI, A uniformly discrete counterexample to bounded approximation in Lipschitz-free spaces, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

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.

Setting

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.

Formalization target

The selected goal is OAI.MarkovSuperreflexivity.hasNontrivialMarkovType_iff_hasEquivalentUCNorm. Its central assertion is

$$\mathrm{Markov\ type}>1\quad\Longleftrightarrow\quad\mathrm{equivalent\ uniformly\ convex\ norm}.$$

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)≥ε.

Significance and status

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.

Difficulty

The inequality is uniform over all finite chains and state maps, while the conclusion is one norm controlling all vectors of the Banach space.

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, Nontrivial Markov Type Forces Superreflexivity, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

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.

Setting

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.

Formalization target

The selected goal is OAI.SeparableQuotient.negative_main. Its central assertion is

$$\mathrm{CH}\quad\Longrightarrow\quad\neg\mathrm{SQ}(\mathbb R)\land\neg\mathrm{SQ}(\mathbb C).$$

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.

Significance and status

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.

Difficulty

The obstruction must rule out every bounded surjection onto every separable infinite-dimensional target space, rather than one proposed quotient.

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, Relative independence of the separable quotient problem, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

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.

Setting

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.

Formalization target

The selected goal is OAI.Grothendieck.elementary_expansion. Its central assertion is

$$X\longrightarrow X\amalg_{D_n}D_{n+1}\quad\text{is a weak equivalence}.$$

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.

Significance and status

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.

Difficulty

The conclusion requires preservation of components and every based homotopy group, for cellular models built through transfinite attachments.

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, The Grothendieck homotopy hypothesis via elementary expansions, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

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.

Setting

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.

Formalization target

The selected goal is OAI.KirchbergRordam.character_criterion. Its central assertion is

$$\mathrm{Char}(F_\omega(A))=\varnothing\quad\Longleftrightarrow\quad A\cong A\otimes_{\min}\mathcal Z.$$

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.

Significance and status

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.

Difficulty

The two directions relate a scalar-valued representation obstruction to an isomorphism with a tensor product, using the precise inductive-limit Jiang–Su model.

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, The Kirchberg–Rørdam character criterion, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

Uniqueness of irreducible representations is a strong condition on a C*-algebra. The target asks for a counterexample to the expected compact-operator characterization without added set-theoretic hypotheses. The pinned manuscript supplies the research context.

Setting

Representations are nonzero star homomorphisms on complete complex inner product spaces. Irreducibility is expressed by closed invariant subspaces, and equivalence by an intertwining linear isometry.

Formalization target

The selected goal is OAI.NaimarkZFC.main. Its central assertion is

$$\exists A:\quad\mathrm{simple}(A)\land\mathrm{unique\ irreducible\ representation}(A)\land A\not\cong\mathcal K(H).$$

The theorem states that, for every universe level choice, there exists a type A carrying a C*-algebra structure (over ℂ) with the following five properties. First, A is simple in the sense that it is nontrivial and its only closed two-sided ideals are {0} and A itself. Second, A is not finite-dimensional as a complex vector space. Third, there is a continuous linear functional τ : A → ℂ that is a faithful tracial state: τ has norm 1, τ(aa) is a nonnegative real number for every a, τ(ab) = τ(ba) for all a and b, and τ(aa) > 0 whenever a ≠ 0. Fourth, A has a unique irreducible representation up to unitary equivalence: whenever π and ρ are nonzero star-homomorphisms (non-unital algebra homomorphisms preserving star) from A into the bounded operators on complete complex inner product spaces H and K, taken in the stated universe levels, and each has no closed invariant subspace other than 0 and the whole space, there is a linear isometric isomorphism U : H → K with U(π(a)x) = ρ(a)(Ux) for all a and x. Fifth, for every complete complex inner product space H in the stated universe, A is not isomorphic to the algebra of compact operators on H, meaning there is no injective star-homomorphism φ : A → B(H) whose range is exactly the set of compact operators on H.

Significance and status

The target explicitly requires simplicity, infinite dimension, a faithful tracial state and failure of all compact-operator isomorphisms in the stated universes. No additional set-theoretic hypothesis appears in its binders. 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 construction must combine infinite dimension, a faithful trace and uniqueness across the specified representation universes.

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, A counterexample to Naimark's problem in ZFC, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

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.

Setting

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.

Formalization target

The selected goal is OAI.Kaplansky.kaplansky_quasitrace_counterexample. Its central assertion is

$$\operatorname{Re}(\tau(a+b)-\tau(a)-\tau(b))\geq1/144.$$

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.

Significance and status

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.

Difficulty

The same positive contractions must exhibit the defect for every normalized 2-quasitrace, while at least one such quasitrace exists.

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.KaplanskyConsequences.stable_finiteness_bundle (Open).

Selected references

• OpenAI, A counterexample to Kaplansky's quasitrace conjecture and failure of tensor-product stable finiteness, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

Norm ultrapowers permit approximations along a free ultrafilter. An explicit algebra excluded from every nuclear target ultrapower tests the limits of this embedding mechanism. The pinned manuscript supplies the research context.

Setting

The group is the stated dyadic semidirect product. Its full group C*-algebra is specified by a universal property, and the ultrapower is bounded sequences modulo norm-null sequences along the ultrafilter.

Formalization target

The selected goal is OAI.NuclearUltrapower.main_no_embedding. Its central assertion is

$$A\not\hookrightarrow B^\omega\quad\text{for every nonzero unital nuclear }B.$$

The theorem states that, working in universe level 0, there exist a nonzero unital complex C*-algebra A and a group homomorphism ι from G into the unitary group of A such that the following hold. Here G is the semidirect product of the additive group of 3-vectors over the dyadic rationals Z[1/2] by SL₃(ℤ) × ℤ, where a matrix acts linearly on the vectors and the integer n acts by multiplication by 2ⁿ. First, (A, ι) is the full group C*-algebra of G: the span of ι(G) is dense in A, and every homomorphism of G into the unitaries of a nonzero unital C*-algebra D extends uniquely to a unital -homomorphism A → D. Second, A is separable as a topological space. Third, for every nonzero unital C-algebra B that is nuclear in the tensor-norm sense (minimal and maximal C*-tensor norms agree on B ⊗ C for every C*-algebra C) and every free ultrafilter ω on ℕ (one containing no finite set), there is no injective unital -homomorphism from A into the norm ultrapower of B, namely bounded B-valued sequences modulo those tending to 0 along ω. Fourth, there exist a nonzero unital C-algebra O and two elements s₀, s₁ of O satisfying the Cuntz relations (each sᵢsᵢ = 1 and s₀s₀ + s₁s₁* = 1), with O universal for these relations, such that for every free ultrafilter ω there is likewise no injective unital *-homomorphism from A into the norm ultrapower of O. The theorem is admitted in the source, not proved.

Significance and status

The goal includes separability, the full group universal property, nonembedding and the Cuntz-algebra corollary in the stated base universe. 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

A single source algebra must obstruct all nuclear targets and free ultrafilters. Universal full-group and Cuntz-algebra constructions are part of the target.

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, An explicit obstruction to nuclear norm-ultrapower embeddings, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

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.

Setting

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.

Formalization target

The selected goal is OAI.BoundedRecovery.bounded_recovery. Its central assertion is

$$\|v_j\|\leq C,\quad\|T(v_j\xi)\|\geq\eta>0,\quad\operatorname{supp}_D(v_j\xi)\subset[s-4\delta_{n_j},s+4\delta_{n_j}].$$

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.

Significance and status

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.

Difficulty

The recovered vectors must come from uniformly bounded algebra elements while retaining detection and shrinking spectral support along a subsequence.

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, Bounded recovery for modular spectral averages, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

A bounded algebra representation need not visibly preserve adjoints. The similarity problem asks whether one bounded change of Hilbert-space coordinates restores that structure. The pinned manuscript supplies the research context.

Setting

Representations are continuous unital complex algebra homomorphisms into bounded operators on a complete complex inner product space. The conjugating operator must have a bounded inverse.

Formalization target

The selected goal is OAI.KadisonSimilarity.similarityTheorem. Its central assertion is

$$S\pi(a^*)S^{-1}=(S\pi(a)S^{-1})^*.$$

The theorem states that, for every C*-algebra A in universe u and every complex inner product space K in universe v that is complete (a Hilbert space), every bounded unital representation of A on K is similar to a star representation. Here a bounded unital representation is a continuous ℂ-algebra homomorphism π from A into the algebra of bounded linear operators on K; being an algebra homomorphism of unital algebras, it preserves the identity. Similarity to a star representation means that there is an invertible bounded operator S on K, with bounded inverse, such that for every a in A, S π(a*) S⁻¹ equals the adjoint of S π(a) S⁻¹. Equivalently, the conjugated map a ↦ S π(a) S⁻¹ commutes with the involution. This is the Kadison similarity statement as a defined proposition SimilarityTheorem, and the source declares it as a theorem whose proof is admitted rather than supplied.

Significance and status

Similarity is the selected goal. The two commutator formulations and explicit hyperreflexivity estimate remain distinct references with their own constants and universes. 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

One operator S must work simultaneously for every algebra element. Uniform matrix-amplification estimates cannot acquire a dimension-dependent constant.

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.KadisonSimilarity.universalCommutatorTheorem (Open).
• OAI.KadisonSimilarity.universalHyperreflexivity (Open).
• OAI.Kadison.uniform_commutator (Open).

Selected references

• OpenAI, Kadison's similarity theorem through uniform derivation estimates, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

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.

Setting

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.

Formalization target

The selected goal is OAI.ZeroTemperatureSK.full_support. Its central assertion is

$$\operatorname{supp}\mu=[0,1),\qquad \mathbb E[u_x(t,X_t)^2]=t,\quad\mathbb E[u_{xx}(t,X_t)^2]=1.$$

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.

Significance and status

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.

Difficulty

The conclusion couples support, strict increase, diffusion existence and derivative identities. Minimization alone is not an assumption of those conclusions.

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.SKValue.value_consequences (Open).

Selected references

• OpenAI, Full support of the zero-temperature Sherrington-Kirkpatrick order parameter, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

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.

Setting

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.

Formalization target

The selected goal is OAI.MinimalVertex.main. Its central assertion is

$$\mathrm{energy\ bounds}\ \land\ \mathrm{strong\ locality}\ \land\ \mathrm{irreducible\ conformal\ net}.$$

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.

Significance and status

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.

Difficulty

Formal algebraic identities must yield polynomial operator bounds and locality for closed smeared fields on the completion.

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, Strongly rational unitary vertex operator algebras and conformal nets, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

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.

Setting

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.

Formalization target

The selected goal is OAI.QAC.parity_lower_bound_polynomial_size. Its central assertion is

$$\exists x\in\{0,1\}^n:\quad P(\mathrm{output}=\mathrm{parity}(x))<2/3.$$

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).

Significance and status

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.

Difficulty

The bound covers arbitrary gates, all choices of output qubit and polynomially many total qubits. Discarded registers can retain unrestricted garbage.

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, Regular trajectories, pruning and quantum parity, 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

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

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.

Setting

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.

Formalization target

The selected goal is OAI.PlanarAnderson.anderson_spectrum_ae. Its central assertion is

$$\sigma(H_v)=[-4-h,4+h].$$

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.

Significance and status

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.

Difficulty

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.

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, Pure-Point Spectrum for the Two-Dimensional Anderson Model at Every Positive Disorder, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal 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

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.

Setting

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.

Formalization targets

$$M=M^{\mathsf T},\quad M_{ss}=1,\quad M_{st}\in\{2,3,\infty\}\ (s\ne t),\qquad A_M\text{ has no geometric action on a nonempty proper CAT(0) space}.$$

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.

Significance

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.

Difficulty

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.

Formalization scope

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.

Selected references

• OpenAI, An Artin group with no geometric CAT(0) action, 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

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

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

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.

Setting

For a Young diagram $\mu$, let $D$ be its Specht dimension and $Q$ 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.

Formalization targets

$$D^{3/4}\le W(\mu)\le D,\quad W(\mu)\|Q\|_{p(d)}^{p(d)}\le1,\quad\|Q\|\le D^{-3/(4p_*)},\quad2\le p(d)\le p_*.$$

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.

• occupied overlap.
• occupied overlap endpoint.

Significance

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.

Difficulty

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 $2^d$.

Formalization scope

The goal is weighted_sweep_moments, with $d\ge1$, positive diagram weights, and one finite upper exponent $p_*$. The finite-dimensional complex inner-product representations and the physical $d$-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.

Selected references

• OpenAI, Row–column symmetry and contraction of coordinate sweeps, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

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.