Functional Analysis

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

Rademacher cotype measures how vector norms compare with random signed sums. The target relates cotype of a space and its dual to boundedness of the Rademacher projection. The pinned manuscript supplies the research context.

Setting

X is a nonzero real Banach space with the ordinary approximation property: finite-rank operators approximate the identity on each compact set, with no uniform operator-norm bound required.

Formalization target

The selected goal is OAI.Cotype.mainTarget_proved. Its central assertion is

$$K\text{-convex}(X)\quad\Longleftrightarrow\quad\mathrm{finite\ cotype}(X)\land\mathrm{finite\ cotype}(X^*).$$

The theorem states that, for every real Banach space X (a complete real normed space) that is nontrivial, the defined proposition MainTarget(X) holds. MainTarget(X) says: if X has the approximation property, then X is K-convex if and only if both X and its dual space of continuous linear functionals X →L[ℝ] ℝ have finite cotype. Here the approximation property means that for every compact set M ⊆ X and every δ > 0 there is a continuous linear operator S : X → X with finite-dimensional range such that ‖Sx − x‖ < δ for all x in M. On the discrete cube {±1}ⁿ (with sign false = +1 and true = −1), the L² norm of f : cube → X is the square root of the average of ‖f(ε)‖² over all ε. The moment of f at coordinate i is the average of ε_i f(ε), and the Rademacher projection of f is the function ε ↦ Σᵢ ε_i times the moment at i. X is K-convex if there is a constant K ≥ 0 such that, for every n and every f on the n-cube, the L² norm of the Rademacher projection of f is at most K times the L² norm of f. X has cotype q, for real q ≥ 2, if there is C ≥ 0 such that, for every n and all vectors x₁, …, xₙ in X, (Σ ‖xᵢ‖^q)^(1/q) ≤ C times the L² norm of ε ↦ Σ ε_i xᵢ. Finite cotype means cotype q for some such q.

Significance and status

The approximation property is a hypothesis inside MainTarget. The statement does not assert the equivalence without it; the cube normalization is the encoded average L² norm. 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 cotype exponents may differ, and ordinary approximation cannot be strengthened silently to bounded approximation.

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 cotype–cotype conjecture under the approximation property, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

A Banach norm supplies both linear and metric structure. A bi-Lipschitz equivalence controls distances, but the target asks for spaces whose linear structures cannot be identified. The pinned manuscript supplies the research context.

Setting

The two spaces are real, complete and separable. The obstruction uses the space of null sequences with values in the real Hilbert space ℓ².

Formalization target

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

$$\frac4{21}\|s-t\|\leq\|\Psi(s)-\Psi(t)\|\leq\frac{76}{25}\|s-t\|.$$

The theorem states that the defined proposition MainClaim holds (it is admitted in the source, not proved here). MainClaim asserts that there exist two separable real Banach spaces X and Y, each given as a type with a norm, a real normed-space structure, completeness and separability, together with a bijection Ψ from X onto Y, such that Ψ is a bi-Lipschitz equivalence with explicit constants: for all s and t in X, (4/21)‖s−t‖ ≤ ‖Ψ(s)−Ψ(t)‖ ≤ (76/25)‖s−t‖. Moreover, there is no continuous linear equivalence (linear homeomorphism) between X and Y, so the two spaces are Lipschitz equivalent but not linearly isomorphic. In addition, there is a linear isometric embedding of C0L2 into X, where C0L2 is the space of continuous functions from the natural numbers to the real Hilbert space ℓ² that vanish at infinity. Finally, Y does not contain a linear copy of C0L2, meaning there is no bounded linear map T from C0L2 to Y and constant a>0 with a‖x‖ ≤ ‖T x‖ for every x in C0L2.

Significance and status

The goal includes the explicit distortion bounds, lack of continuous linear equivalence, an isometric copy of c0(ℓ²) in X, and absence of a bounded-below linear copy in Y. 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 global metric bijection must coexist with a linear embedding obstruction, so the counterexample cannot follow merely from nonlinearity of a particular map.

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, Lipschitz Equivalent Separable Banach Spaces Need Not Be Linearly Isomorphic, 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

Hochschild cohomology measures whether a cocycle equation admits a primitive. In an operator algebra the boundedness requirement is part of the mathematical problem. The pinned manuscript supplies the research context.

Setting

Cochains are continuous complex multilinear maps into the von Neumann algebra itself, with its natural left and right multiplication actions.

Formalization target

The selected goal is OAI.BoundedHochschild.KadisonRingrose.main_result. Its central assertion is

$$df=0\quad\Longrightarrow\quad\exists g:\ dg=f,\qquad\deg(f)=n+2.$$

The theorem states that, for a complex von Neumann algebra M (a C*-algebra with a partial order making it star-ordered, equipped with the W*-algebra structure), and any natural number n, every bounded Hochschild cocycle of degree n+2 with values in M is a coboundary. Here a cochain of degree m is a continuous complex m-linear map from M^m to M. The Hochschild differential of a cochain f of degree m, evaluated at (v_0,...,v_m), is v_0 f(v_1,...,v_m) plus the sum over j from 0 to m-1 of (-1)^(j+1) f(v_0,...,v_j v_{j+1},...,v_m), where the j-th and (j+1)-th inputs are multiplied into one, plus (-1)^(m+1) f(v_0,...,v_{m-1}) v_m. The hypothesis is that f has degree n+2 and its differential vanishes at every (n+3)-tuple of elements of M. The conclusion is that there exists a continuous multilinear cochain g of degree n+1 whose differential equals f at every (n+2)-tuple of elements of M.

Significance and status

The goal covers every natural n, hence degrees at least two. It does not include a separately referenced degree-one inner-derivation theorem. 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

An algebraic primitive is insufficient: the lower-degree cochain must remain continuous and bounded in the encoded operator-norm sense.

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, Vanishing of higher bounded Hochschild cohomology, 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

Group von Neumann algebras encode a free group's regular representation as an operator algebra. Whether the rank remains visible in that algebra is the motivating isomorphism problem. The pinned manuscript supplies the research context.

Setting

The parameter runs over extended nonnegative reals greater than one. Integer ranks use group factors, infinity uses countably many generators, and other parameters use the encoded stabilized corner model.

Formalization target

The selected goal is OAI.FreeGroupFactorMain.Interpolation.allInterpolatedIsomorphic. Its central assertion is

$$L(\mathbb F_r)\cong L(\mathbb F_s)\qquad(1<r,s\leq\infty).$$

The theorem states that for any two extended nonnegative real parameters r and s, both strictly greater than 1 (so either may be infinite), the interpolated factors attached to r and s are isomorphic as C*-algebras with trace and topology, meaning the type of normal tracial equivalences between them is nonempty. The interpolated factor at a parameter is chosen by cases: for r = ∞ it is the group von Neumann algebra of the free group on countably many generators; for r equal to a natural number n it is the group von Neumann algebra of the free group on n generators; otherwise it is the corner pAp of the stabilization of the rank-two free group algebra, cut down by a selected star projection p whose stabilized projection trace is the real number 1/√(r−1), with the trace being the stabilized trace rescaled by the inverse of that value. Each carries its canonical trace or this rescaled trace and an ultraweak-type topology. A NormalTracialEquiv between two such models consists of a ℂ-linear star-algebra isomorphism that preserves the traces and is continuous in both directions for the given topologies.

Significance and status

The goal is a nonempty type of normal tracial equivalences between the precise interpolated models. Statements about fundamental groups are not separate attached targets. 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 required equivalence must preserve the algebra, involution and trace, and be continuous in both directions for the specified topologies.

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 isomorphism of the free group factors, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

Covering numbers measure the size of a set at a given scale: $N(A,B)$ is the least number of translates of $B$ needed to cover $A$. Their logarithms, the metric entropy, appear across approximation theory, operator theory (entropy numbers of compact operators), probability (Dudley's bound) and learning theory. A basic question in asymptotic geometric analysis is how metric entropy behaves under duality: if $K$ is hard to cover by $L$, is the polar body $L^\circ$ equally hard to cover by $K^\circ$? The duality conjecture for metric entropy, originating in Pietsch's 1972 work on operator ideals, predicts that the two quantities agree up to universal constants, independently of the dimension.

Timeline

• 1972. Pietsch formulates the duality problem for entropy numbers of operators.
• 1987. König and Milman compare the $n$-th roots of the two covering numbers, which on the logarithmic scale allows an additive error proportional to $n$ (doi:10.1007/BFb0078138).
• 1989. Bourgain, Pajor, Szarek and Tomczak-Jaegermann prove entropy-number comparisons under geometric and regularity assumptions, with rank-dependent losses (doi:10.1007/BFb0090048).
• 2004. Artstein, Milman and Szarek prove the conjecture when one body is a Euclidean ball (hence an ellipsoid) (doi:10.4007/annals.2004.159.1313); Artstein, Milman, Szarek and Tomczak-Jaegermann prove universal duality for convexified packing and state the dimension-free conjecture as Conjecture 1 (doi:10.1007/s00039-004-0486-3).
• 2007. E. Milman obtains a comparison for arbitrary symmetric bodies with logarithmic losses in scale and entropy (doi:10.1007/s00020-006-1479-4).
• 2022. Hu, Peale and Reingold relate dual covering numbers to sample complexity in learning theory (PMLR v167).

The source of this mission is an OpenAI preprint dated September 24, 2026, which disproves the dimension-free conjecture.

Setting

Work in $\mathbb R^n$ with the standard pairing $\langle x,y\rangle=\sum_i x_iy_i$. A convex body is a compact convex set with nonempty interior; it is origin-symmetric if $K=-K$. Its polar is

$$K^\circ=\{y\in\mathbb R^n:\ \langle x,y\rangle\le1\ \text{for all }x\in K\}.$$

For bounded $A$ and a body $B$, the covering number $N(A,B)$ is the least $M$ such that $A\subseteq\bigcup_{j=1}^M(c_j+B)$ for some $c_1,\dots,c_M\in\mathbb R^n$ (centres need not lie in $A$). Logarithms are natural. Let $L=[-1,1]^n$ be the cube; its polar $L^\circ$ is the cross-polytope.

The duality conjecture asks for absolute constants $a,b\ge1$ such that, for every $n$ and all origin-symmetric convex bodies $K,L\subset\mathbb R^n$,

$$\frac1b\log N(L^\circ,aK^\circ)\ \le\ \log N(K,L)\ \le\ b\log N(L^\circ,a^{-1}K^\circ).$$

Formalization targets

Goal: Theorem 1.1

For every $a,b\ge1$ there are $n\ge1$ and an origin-symmetric convex body $K\subset\mathbb R^n$ such that, with $L=[-1,1]^n$,

$$\log N(K,L)\ >\ b\,\log N\bigl(L^\circ,\ a^{-1}K^\circ\bigr).$$

The Lean statement OAI.MetricEntropyDuality.exists_entropy_duality_counterexample_with_covers is open on the platform.

Significance

The theorem shows that the upper inequality of the conjecture fails for every proposed pair of constants, so the two-sided conjecture has a negative answer, even when one body is a cube. It also separates ordinary covering entropy from convexified-packing entropy, for which Artstein–Milman–Szarek–Tomczak-Jaegermann proved universal duality (Corollary 5.1 of the source). Dimension-dependent results (König–Milman, E. Milman) remain compatible with the counterexample, which shows that some dependence on dimension or structure is unavoidable.

The result is stated in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. The counterexample is explicit and finite-dimensional, which makes a full formalization realistic.

Difficulty

The known positive cases (Euclidean balls, ellipsoids, bounded K-convexity) suggest the conjecture is true, and the obvious candidate bodies, products and cubes, satisfy it. A counterexample needs a body whose primal entropy against the cube is large while the polar side is small; the paper reduces this to a finite matrix with entries in $[0,1]$ whose rows are pairwise $1$-separated in the sup norm while the absolutely convex hull of its columns admits a small uniform approximation list. Producing such matrices requires partition structures over finite fields with uniform control over all row coordinates, and the entropy gap must beat every fixed $b$ after the scale change $a^{-1}$.

Formalization scope

• Space: RealSpace (Fin n) = Fin n → ℝ with pairing the standard dot product; cube is $[-1,1]^n$; polar K uses $\le1$.
• Covers A B centers means every $x\in A$ has some centre $c_j$ with $x-c_j\in B$; coveringNumber is the sInf of the admissible $M$. The statement includes Coverable side conditions, which only certify that both infima are over nonempty sets.
• IsSymmetricConvexBody = compact, convex, $x\in K\iff -x\in K$, nonempty interior.
• The scale enters as a⁻¹ • polar K; logs are Real.log of natural numbers cast to reals.

A complete development needs support functions and polarity, elementary covering-number bounds, finite-field polynomial zero bounds (Schwartz–Zippel), and the matrix-to-body conversion. The covering-number and polarity layer is reusable for other convex-geometry missions. Contributions formalizing Lemma 2.1 (matrix-to-body conversion), Proposition 3.2 (uniform compression) and Proposition 4.3 (partitions with separated rows) are welcome.

Selected references

• OpenAI, Counterexamples to the duality conjecture for metric entropy, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Counterexamples-to-the-duality-conjecture-for-metric-entropy-September-24-2026/main.pdf
• S. Artstein, V. Milman, S. J. Szarek, Duality of metric entropy, Ann. of Math., 2004. https://doi.org/10.4007/annals.2004.159.1313
• S. Artstein, V. Milman, S. Szarek, N. Tomczak-Jaegermann, On convexified packing and entropy duality, Geom. Funct. Anal., 2004. https://doi.org/10.1007/s00039-004-0486-3
• H. König, V. D. Milman, On the covering numbers of convex bodies, GAFA Seminar, 1987. https://doi.org/10.1007/BFb0078138
• J. Bourgain, A. Pajor, S. J. Szarek, N. Tomczak-Jaegermann, On the duality problem for entropy numbers of operators, GAFA Seminar, 1989. https://doi.org/10.1007/BFb0090048
• E. Milman, A remark on two duality relations, Integral Equations Operator Theory, 2007. https://doi.org/10.1007/s00020-006-1479-4
• J. T. Schwartz, Fast probabilistic algorithms for verification of polynomial identities, J. ACM, 1980. https://doi.org/10.1145/322217.322225

Motivation: isometries of unit spheres

The Mazur–Ulam theorem (1932) says that every surjective isometry between real normed spaces is affine. The whole space is not always available, though: often only distances between unit vectors are known. Tingley's problem (1987) asks whether the metric of the unit sphere alone already determines the linear structure, that is, whether every surjective isometry between the unit spheres of two real Banach spaces extends to a real-linear isometry of the spaces (Tingley 1987). The question has been studied for almost four decades, mostly class by class: for sequence spaces, $L^p$ spaces, operator algebras and two-dimensional spaces. Nearly all known positive results depend on the structure of the particular spaces involved.

Timeline

• 1932 — Mazur and Ulam: surjective isometries between real normed spaces are affine.
• 1972 — Mankiewicz extends isometries between convex sets with nonempty interior. A unit sphere has empty interior, so this does not apply.
• 1987 — Tingley poses the problem and shows that surjective isometries between spheres of finite-dimensional spaces preserve antipodal points (Tingley 1987).
• 1994 — Wang treats spheres of $C_0(\Omega)$-type spaces (Wang 1994).
• 2003 — Ding handles $\ell^p(\Gamma)$-type spaces, $p>1$, $p\ne 2$ (Ding 2003).
• 2011 — Cheng and Dong formulate the Mazur–Ulam property (sphere isometries from a given space into an arbitrary target extend linearly) (Cheng–Dong 2011).
• 2012 — Tan proves the Mazur–Ulam property for real $L^p(\mu)$, $1<p<\infty$, $p\neq 2$ (Tan 2012).
• 2014 — Tanaka: sphere isometries preserve maximal convex subsets of the sphere (Tanaka 2014).
• 2018 — Fernández-Polo and Peralta (von Neumann algebras, JMAA 2018); Mori (preduals, JMAA 2018).
• 2020 — Mori and Ozawa: Mazur–Ulam property for unital $C^*$-algebras and real von Neumann algebras (Studia Math. 2020).
• 2022 — Banakh: every two-dimensional real Banach space has the Mazur–Ulam property (Banakh 2022).
• 2025–2026 — Further class results: Schreier spaces (Fakhoury 2025); Haagerup noncommutative $L_p$ and Schatten classes (Huang–Zhu, arXiv:2608.30131; arXiv:2607.11244).
• 2026 — An OpenAI preprint, A positive solution to Tingley's problem (OpenAI Math Release, September 23, 2026), claims the general affirmative answer for all real Banach spaces. It has not been peer reviewed, and the claim has not been formally verified.

Setting

Let $X$ and $Y$ be real Banach spaces, both nonzero. The unit sphere is $S_X=\{x\in X:\|x\|=1\}$ with the metric inherited from $X$. A map $f:S_X\to S_Y$ is an isometry if $\|f(x)-f(y)\|=\|x-y\|$ for all $x,y\in S_X$, and it is surjective if every point of $S_Y$ is attained.

Any linear extension of $f$ is forced to be the radial extension

$$T(0)=0,\qquad T(x)=\|x\|\,f\!\left(\frac{x}{\|x\|}\right)\quad(x\neq 0).$$

In Lean, UnitSphere X is the subtype $\{x : X \mid \|x\|=1\}$ and normalize x hx is $x/\|x\|$ as an element of it.

Formalization targets

Goal: Tingley's problem (Theorem 1.1)

For nonzero real Banach spaces $X,Y$ and every surjective isometry $f:S_X\to S_Y$ there is a surjective real-linear isometry $T:X\to Y$ such that

$$T|_{S_X}=f,\qquad T(0)=0,\qquad T(x)=\|x\|\,f\!\left(\tfrac{x}{\|x\|}\right)\ (x\neq0),$$

and $T$ is the only real-linear map $X\to Y$ that agrees with $f$ on $S_X$. This is the full statement of Theorem 1.1 of the source. The goal is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. An affirmative answer turns a forty-year class-by-class programme into a single theorem: the metric of the unit sphere of any real Banach space determines the space up to linear isometry. Every space then has the Mazur–Ulam property in the sense of Cheng and Dong, with no separability, reflexivity, smoothness or strict convexity assumptions. For complex Banach spaces viewed as real spaces the conclusion is real-linearity only; complex-linearity is not claimed.

Formalizing it. The claimed proof combines classical tools (supporting functionals, Banach-space ultrapowers, Darbo's fixed-point theorem with the Kuratowski measure of noncompactness, the Mazur–Ulam theorem) with new geometric estimates on aligned chords. A machine-checked proof would certify a result whose proof has not yet been refereed. The Mazur–Ulam theorem itself is already in Mathlib (IsometryEquiv.toRealLinearIsometryEquiv); ultrapowers of Banach spaces and Darbo's theorem are not.

Difficulty

The radial map $T$ preserves norms and preserves distances between points of the same radius. What has to be shown is that it preserves distances between points on different spheres, $\|f(x)-qf(y)\|=\|x-qy\|$ for $0<q<1$, using only distances measured on a single sphere. Once this holds, $T$ is a surjective isometry fixing $0$ and Mazur–Ulam gives linearity. The obvious attempt (extend the isometry to a neighbourhood, or use convex-set extension theorems such as Mankiewicz's) fails because the sphere has empty interior. Structural arguments (smoothness, facial structure, explicit duals) cover only special classes of spaces. In general, the maximal defect $\sup|\|f(x)-qf(y)\|-\|x-qy\||$ need not be attained, and no compactness is available in infinite dimensions.

Formalization scope

• $X$ and $Y$ are arbitrary types with NormedAddCommGroup, NormedSpace ℝ and CompleteSpace, and Nontrivial (the source's "nonzero"). Universe levels are independent, and no separability or dimension hypothesis is imposed.
• The sphere is UnitSphere X := {x // ‖x‖ = 1} with the subtype metric; Isometry f and Function.Surjective f are the hypotheses.
• The conclusion is an existential over X ≃ₗᵢ[ℝ] Y (a bijective real-linear isometry) with the five clauses: agreement on the sphere, $T0=0$, the radial formula, surjectivity, and uniqueness among all X →ₗ[ℝ] Y that agree with $f$ on the sphere. No hypothesis assumes any distance between different radii, so the statement is not trivialized.
• Infrastructure a full development needs: Hahn–Banach supporting functionals, Banach-space ultrapowers (or another attainment device), the Kuratowski measure of noncompactness and Darbo's fixed-point theorem, together with Mathlib's Mazur–Ulam theorem. Ultrapowers and Darbo's theorem would be reusable well beyond this mission.

Selected references

• D. Tingley, Isometries of the unit sphere, Geom. Dedicata 22 (1987), 371–378. https://doi.org/10.1007/BF00147942
• S. Mazur and S. Ulam, Sur les transformations isométriques d'espaces vectoriels normés, C. R. Acad. Sci. Paris 194 (1932), 946–948.
• P. Mankiewicz, On extension of isometries in normed linear spaces, Bull. Acad. Polon. Sci. Sér. Sci. Math. Astronom. Phys. 20 (1972).
• R. S. Wang, Isometries between the unit spheres of $C_0(\Omega)$ type spaces, Acta Math. Sci. 14 (1994), 82–89. https://doi.org/10.1016/S0252-9602(18)30093-6
• G. G. Ding, The isometric extension problem in the unit spheres of $\ell^p(\Gamma)$ $(p>1)$ type spaces, Sci. China Ser. A 46 (2003), 333–338. https://doi.org/10.1360/03ys9035
• L. Cheng and Y. Dong, On a generalized Mazur–Ulam question, J. Math. Anal. Appl. 377 (2011), 464–470. https://doi.org/10.1016/j.jmaa.2010.11.025
• D.-N. Tan, Extension of isometries on the unit sphere of $L^p$ spaces, Acta Math. Sin. (Engl. Ser.) 28 (2012), 1197–1208. https://doi.org/10.1007/s10114-011-0302-6
• R. Tanaka, A further property of spherical isometries, Bull. Aust. Math. Soc. 90 (2014), 304–310. https://doi.org/10.1017/S0004972714000185
• F. J. Fernández-Polo and A. M. Peralta, On the extension of isometries between the unit spheres of von Neumann algebras, J. Math. Anal. Appl. 466 (2018), 127–143. https://doi.org/10.1016/j.jmaa.2018.05.062
• M. Mori, Tingley's problem through the facial structure of operator algebras, J. Math. Anal. Appl. 466 (2018), 1281–1298. https://doi.org/10.1016/j.jmaa.2018.06.050
• M. Mori and N. Ozawa, Mankiewicz's theorem and the Mazur–Ulam property for $C^*$-algebras, Studia Math. 250 (2020), 265–281. https://doi.org/10.4064/sm180727-14-11
• T. Banakh, Every 2-dimensional Banach space has the Mazur–Ulam property, Linear Algebra Appl. 632 (2022), 268–280. https://doi.org/10.1016/j.laa.2021.09.020
• G. Darbo, Punti uniti in trasformazioni a codominio non compatto, Rend. Sem. Mat. Univ. Padova 24 (1955), 84–92.
• OpenAI, A positive solution to Tingley's problem, OpenAI Math Release preprint, September 23, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-positive-solution-to-Tingleys-problem-September-23-2026/paper.pdf

Motivation

A von Neumann algebra is a unital algebra of bounded operators on a Hilbert space that is closed under adjoints and in the weak operator topology. For a set $S$ of operators, $W^*(S)$ denotes the smallest von Neumann algebra containing $S$. The generator problem, going back to Kadison's 1967 list of problems, asks whether every von Neumann algebra with separable predual is singly generated, $M=W^*(x)$ for a single bounded operator $x$; equivalently, whether two self-adjoint operators always suffice. It is one of the oldest structural questions about von Neumann algebras, and by classical reductions everything comes down to type II$_1$ factors.

Timeline

• 1962–1969. Pearcy proves single generation for type I algebras (doi:10.2307/2034069); Suzuki and Saitô for hyperfinite algebras (1963, doi:10.2748/tmj/1178243811); Wogen for properly infinite algebras (1969, doi:10.1090/S0002-9904-1969-12157-9); Douglas and Pearcy develop matrix-generation techniques (1969, doi:10.1307/mmj/1029000161).
• 1972. Behncke treats tensor products of two II$_1$ factors (doi:10.2748/tmj/1178241478).
• 1974. Willig's direct-integral theorem reduces the general problem to II$_1$ factors (doi:10.2748/tmj/1178241231).
• 1981. Popa constructs irreducible hyperfinite subfactors (doi:10.1007/BF01389015).
• 1985–2002. Popa treats factors with Cartan subalgebras (doi:10.7146/math.scand.a-12110); Ge and Popa treat property $\Gamma$ factors (1998, doi:10.1215/S0012-7094-98-09405-4); Ge and Shen treat certain property (T) factors (2002, doi:10.1073/pnas.022593699).
• 2008–2009. Dykema, Sinclair, Smith and White study generator invariants and their amplification formula (arXiv:0706.1953); Shen's generator invariant unifies the positive classes (arXiv:math/0511327).
• 2012. Sherman shows that finite generation of every countably generated II$_1$ factor would suffice (arXiv:0908.4565).
• 2021. Popa studies tight decompositions and stable single generation (arXiv:1910.14653).
• 2025. Gao, Kunnawalkam Elayavalli, Patchell and Tan prove single generation under an internal sequential-commutation hypothesis (arXiv:2404.12380).

The source of this mission is an OpenAI preprint dated September 23, 2026, which claims single generation for every II$_1$ factor with separable predual.

Setting

Let $H$ be a complex Hilbert space and $M\subseteq B(H)$ a unital $*$-subalgebra closed in the weak operator topology. $M$ is a factor if its centre is $\mathbb C1$; it is finite if every isometry $v\in M$ ($v^*v=1$) is unitary; it is diffuse if every nonzero projection has a proper nonzero subprojection. A nonzero finite diffuse factor is a type II$_1$ factor; it carries a unique faithful normal tracial state $\tau$, with $\|x\|_2=\tau(x^*x)^{1/2}$. $M$ has separable predual if $M$ is isometrically the dual of a separable Banach space; this does not require $H$ or $M$ to be norm-separable.

An inclusion of factors $P\subseteq M$ is irreducible if $P'\cap M=\mathbb C1$. $\mathcal U(M)$ denotes the unitary group.

Formalization targets

Milestone: Theorem 1.1 (relative generation)

For an irreducible inclusion $P\subset M$ of II$_1$ factors with $M$ of separable predual,

$$\{u\in\mathcal U(M):\ W^*(P,u)=M\}\ \text{ is a dense }G_\delta\text{ in }(\mathcal U(M),\|\cdot\|_2).$$

Goal: Theorem 1.2 (single generation)

$$M\ \text{a II}_1\text{ factor with separable predual}\ \Longrightarrow\ \exists\,x\in M:\quad W^*(x)=M.$$

The Lean statement OAI.Generator.single_generation_of_II1_separable_predual is open on the platform.

Significance

Combined with Willig's reduction and the known type I and properly infinite cases, Theorem 1.2 gives single generation of every von Neumann algebra with separable predual, an affirmative answer to the generator problem. The paper also deduces that the generator invariants $G$ and $G_{\mathrm{sa}}$ of Dykema–Sinclair–Smith–White vanish for every such factor, and that Voiculescu's free entropy dimensions $\delta,\delta_0$ are not invariants of the generated algebra (Corollary 6.1), since $L(\mathbb F_n)$ has both a free semicircular $n$-tuple and a self-adjoint pair as generators. Theorem 1.1 is of independent interest: it shows that relative generators are generic, not merely existent.

These results are stated in an OpenAI preprint; they have not been peer reviewed, and no machine-checked proofs exist.

Difficulty

Earlier positive results all relied on extra structure (Cartan subalgebras, property $\Gamma$, tensor decompositions, sequential commutation) to build a generator. Without such structure one must show that a unitary $u$ generates $M$ over $P$, which requires detecting every vector of $L^2(M)$ through words in $P$ and $u$. Perturbing $u$ along a long word changes it many times, and operator-norm bounds on the accumulated perturbation grow with the word length; a length-uniform estimate is needed. The Baire-category step also needs the projection onto $L^2(W^*(P,u))$ to vary semicontinuously in $u$.

Formalization scope

• Algebras are concrete StarSubalgebra ℂ (H →L[ℂ] H); WOTClosed uses Mathlib's weak operator topology, and wstar s is the infimum of WOT-closed star-subalgebras containing $s$ (unital by construction).
• IsII1Factor = nonzero Hilbert space, WOT-closed, trivial centre, finite (isometries are unitary), diffuse. No trace is assumed.
• HasSeparablePredual asks for a separable Banach space $X$ in the same universe with a conjugate-linear isometric equivalence between its dual and the algebra; this is equivalent to the usual condition.
• For Theorem 1.1, the trace is part of the conclusion (IsNormalizedTrace: normalized, positive, faithful, tracial, ultraweakly continuous), the topology on unitary large is generated by trace 2-distance balls, and the locus is $\{u: \mathrm{wstar}(P\cup\{u\})=M\}$.

A complete development needs the standard theory of II$_1$ factors (trace, $L^2(M)$, conditional expectations, ultrapowers), Popa's free independence in ultraproducts and irreducible hyperfinite subfactors, Haagerup's inequality for free groups, and the Baire category theorem on the unitary group. This infrastructure is reusable across operator-algebra missions. Contributions formalizing Proposition 3.2 (perturbation bounds) and Popa's irreducible hyperfinite embedding (Theorem 5.1) are welcome.

Selected references

• OpenAI, Relative generation and the generator problem for finite factors, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Relative-generation-and-the-generator-problem-for-finite-factors-September-23-2026/paper.pdf
• P. Willig, Generators and direct integral decompositions of $W^*$-algebras, Tohoku Math. J., 1974. https://doi.org/10.2748/tmj/1178241231
• D. Sherman, On cardinal invariants and generators for von Neumann algebras, Canad. J. Math., 2012. https://arxiv.org/abs/0908.4565
• K. Dykema, A. Sinclair, R. Smith, S. White, Generators of II$_1$ factors, Oper. Matrices, 2008. https://arxiv.org/abs/0706.1953
• L. Ge, S. Popa, On some decomposition properties for factors of type II$_1$, Duke Math. J., 1998. https://doi.org/10.1215/S0012-7094-98-09405-4
• J. Shen, Type II$_1$ factors with a single generator, J. Operator Theory, 2009. https://arxiv.org/abs/math/0511327
• S. Popa, Independence properties in subalgebras of ultraproduct II$_1$ factors, J. Funct. Anal., 2014. https://arxiv.org/abs/1308.3982
• U. Haagerup, An example of a non nuclear $C^*$-algebra, which has the metric approximation property, Invent. Math., 1979. https://doi.org/10.1007/BF01410082
• D. Gao, S. Kunnawalkam Elayavalli, G. Patchell, H. Tan, Internal sequential commutation and single generation, IMRN, 2025. https://arxiv.org/abs/2404.12380

Motivation

The invariant subspace problem asks whether every bounded operator on a separable infinite-dimensional complex Hilbert space has a nontrivial closed invariant subspace. Inside a finite von Neumann algebra there is a sharper, algebra-relative version: given $T$ in a type $\mathrm{II}_1$ factor $M$, is there a projection $p\in M$ with $0<\tau(p)<1$ and $(1-p)Tp=0$, i.e. a nontrivial $T$-invariant subspace whose projection lies in $M$? The Brown measure, built from the Fuglede–Kadison determinant, gives such projections whenever it is not a point mass (Haagerup–Schultz). The open territory is therefore operators whose Brown measure is a point mass, in particular quasinilpotent ones.

Zhu, Fang and Shi (2017) studied the weighted irrational rotations $T_f=Uf(V)$ in the hyperfinite $\mathrm{II}_1$ factor and asked whether $T_f$ must have a nontrivial invariant projection when $f$ is nonzero almost everywhere, $|f|$ is nonconstant and the determinant of $f(V)$ is zero. This mission formalizes a negative answer for every prescribed irrational angle.

Timeline

• 1952. Fuglede and Kadison introduce the determinant on finite factors (doi:10.2307/1969645).
• 1986. Brown defines the spectral distribution (Brown measure) of an operator in a $\mathrm{II}_1$ factor.
• 2004. Dykema and Haagerup construct nontrivial hyperinvariant subspaces for the quasinilpotent DT-operator, whose Brown measure is a point mass (doi:10.1016/S0022-1236(03)00167-8).
• 2008. Tucci constructs quasinilpotent generators of the hyperfinite factor that do have nontrivial invariant projections (doi:10.1016/j.jfa.2008.03.012).
• 2009. Haagerup and Schultz attach a hyperinvariant projection to each Borel set, with trace equal to its Brown mass (doi:10.1007/s10240-009-0018-7). Dykema and Schultz identify the Brown measure of weighted rotations as uniform measure on a circle of radius the determinant (arXiv:math/0512197).
• 2017. Zhu, Fang and Shi give a direct proof of that Brown-measure formula, exhibit continuous weights with one zero and determinant zero, and pose the question above (doi:10.7146/math.scand.a-25625).

The source of this mission is an OpenAI preprint dated September 27, 2026.

Setting

Fix an irrational $\theta\in(0,1)$. Let $R_\theta$ be the von Neumann algebra generated by unitaries $U,V$ with $VU=e^{2\pi i\theta}UV$ and trace $\tau(U^mV^n)=0$ for $(m,n)\ne(0,0)$, $\tau(1)=1$; it is the hyperfinite $\mathrm{II}_1$ factor. Concretely, on $\mathcal H=L^2(\mathbb R/\mathbb Z;\ell^2(\mathbb Z))$, $U$ shifts the $\ell^2(\mathbb Z)$ coordinate and $V$ multiplies the $k$-th coordinate at $x$ by $e^{2\pi i(x+k\theta)}$. For a continuous $f:\mathbb T\to[0,1]$ set $T_f=Uf(V)$. A projection $p\in R_\theta$ is invariant for $T_f$ if $(1-p)T_fp=0$; it is nontrivial if $p\ne0,1$. The Fuglede–Kadison determinant of $f(V)$ is $\exp\int_{\mathbb T}\log f\,dm$, with $m$ the normalized Haar measure.

Formalization targets

Goal: Theorem 1.1 (with Corollary 6.2)

For every irrational $\theta\in(0,1)$ there is a continuous $f:\mathbb T\to[0,1]$ with

$$f^{-1}(0)=\{1\},\qquad \int_{\mathbb T}\log f\,dm=-\infty,$$

such that every projection $p\in R_\theta$ with $(1-p)\,Uf(V)\,p=0$ equals $0$ or $1$; moreover $T_f\ne0$, $\|T_f^n\|^{1/n}\to0$, and $\Delta(T_f)=0$.

Milestones

• Theorem 1.1 at some angle. The same conclusion for one irrational angle, in the abstract tracial model on $\ell^2(\mathbb Z^2)$.
• Theorem A.1 (product realization). A second model on $\mathbb T^{\mathbb N}$: angles $\theta_i$ with $\sum\theta_i<\infty$, rationally independent with $1$, and $f(x)=\exp(-\sum c_i\lfloor x_i+\theta_i\rfloor)$, giving a nonzero quasinilpotent $T=U\pi(f)$ in a $\mathrm{II}_1$ factor with only trivial invariant projections and the stated polar structure.
• Abstract consequence. Some $\mathrm{II}_1$ factor with separable predual contains a nonzero quasinilpotent operator with no nontrivial invariant projection.

The goal OAI.Invariant233.Results.prescribed_irrational_counterexample is open on the platform.

Significance

Theorem 1.1 answers the Zhu–Fang–Shi question negatively, with the angle fixed in advance and no Diophantine condition. Combined with Dykema's observation that hyperinvariant subspaces of $T\in M$ have projections in $M$, it yields (Corollary 1.4) a nonzero quasinilpotent operator on every separable infinite-dimensional Hilbert space with no nontrivial hyperinvariant subspace, so its commutant is a proper, strongly closed, transitive unital algebra. It also shows that, at determinant zero, the Haagerup–Schultz method cannot be supplemented by any invariant projection in the factor for these operators. The conclusion concerns projections in $R_\theta$; ordinary invariant subspaces of the Hilbert-space representation are not excluded.

The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists.

Difficulty

Brown-measure methods give nothing here: at determinant zero the Brown measure is $\delta_0$, so Haagerup–Schultz projections are trivial, and point-mass Brown measure does not by itself exclude invariant projections (Dykema–Haagerup, Tucci). One must show directly that a hypothetical invariant projection, viewed as a measurable field of projections, contradicts weighted orthogonality identities along rotation orbits. The weight's logarithmic drops must be rare enough to keep a finite window under control yet strong enough to suppress the infinite tail, and this must work at an arbitrary prescribed angle, which forces large divisible frequencies. Passing from a measurable weight to a continuous one with a single zero requires an intertwining multiplier that may be unbounded.

Formalization scope

• The circle is AddCircle (1:ℝ) with Haar probability; the zero of $f$ is at $0\in\mathbb R/\mathbb Z$, which corresponds to $1\in\mathbb T$.
• The Hilbert space is Lp (lp (fun _ : ℤ => ℂ) 2) 2 circleMeasure; Rotation.U is the fibrewise shift and Rotation.V θ multiplies by $e^{2\pi i(x+k\theta)}$; Rotation.algebra θ is the double commutant of $\{U,V\}$.
• HasOnlyTrivialInvariantProjections M T quantifies over self-adjoint idempotents $p\in M$ with $(1-p)Tp=0$; no commutation with $T$ is required.
• NormQuasinilpotent T is $\|T^n\|^{1/n}\to0$; the determinant is the vector-state Fuglede–Kadison determinant $\inf_{\varepsilon>0}\exp\frac12\tau\log(T^*T+\varepsilon)$, avoiding $\log0$.

A complete development needs crossed-product (group-measure-space) von Neumann algebras, measurable fields of projections, the Fuglede–Kadison determinant, and uniform averaging under irrational rotation. Contributions formalizing Theorem 5.2 (the measurable-weight obstruction), Lemma 5.1 (conditional convolution obstruction), Corollary 6.2 (quasinilpotence) and Lemma A.4 (the product algebra is a $\mathrm{II}_1$ factor) are welcome.

Selected references

• OpenAI, Invariant-projection counterexamples for every irrational rotation, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Invariant-projection-counterexamples-for-every-irrational-rotation-September-27-2026/paper.pdf
• Z. Zhu, J. Fang, R. Shi, On a class of operators in the hyperfinite II$_1$ factor, Math. Scand., 2017. https://doi.org/10.7146/math.scand.a-25625
• B. Fuglede, R. V. Kadison, Determinant theory in finite factors, Ann. of Math., 1952. https://doi.org/10.2307/1969645
• U. Haagerup, H. Schultz, Invariant subspaces for operators in a general II$_1$-factor, Publ. Math. IHÉS, 2009. https://doi.org/10.1007/s10240-009-0018-7
• K. Dykema, H. Schultz, Brown measure and iterates of the Aluthge transform for some operators arising from measurable actions, Trans. Amer. Math. Soc., 2009. https://doi.org/10.1090/S0002-9947-09-04762-X
• K. Dykema, U. Haagerup, Invariant subspaces of the quasinilpotent DT-operator, J. Funct. Anal., 2004. https://doi.org/10.1016/S0022-1236(03)00167-8
• G. H. Tucci, Some quasinilpotent generators of the hyperfinite II$_1$ factor, J. Funct. Anal., 2008. https://doi.org/10.1016/j.jfa.2008.03.012
• K. Dykema, Hyperinvariant subspaces for some B-circular operators, Math. Ann., 2005. https://doi.org/10.1007/s00208-005-0669-8

Motivation

The classification programme for simple nuclear $C^*$-algebras identifies a class of algebras that are determined by K-theory and traces. Membership in that class is governed by regularity properties: finite nuclear dimension, absorption of the Jiang–Su algebra $\mathcal Z$, and strict comparison. Uniform property $\Gamma$, introduced by Castillejos, Evington, Tikuisis, White and Winter, is a central divisibility condition: it asks for projections in a central sequence algebra that cut every trace exactly in half, uniformly across the whole trace space, while preserving trace values against fixed coefficients. Together with strict comparison it is equivalent to $\mathcal Z$-stability for simple separable unital nuclear algebras (Castillejos–Evington–Tikuisis–White). Schafhauser, Tikuisis and White asked (Problem XXI of their problem list) whether real rank zero of the uniform tracial ultrapower of the tracial completion already forces uniform property $\Gamma$.

Timeline

• 1943, 1969, 1970. Murray and von Neumann introduce property $\Gamma$ for II$_1$ factors (doi:10.2307/1969107); Dixmier gives its central-projection formulation (doi:10.1007/BF01404306); McDuff studies central sequences and absorption of the hyperfinite factor (doi:10.1112/plms/s3-21.3.443).
• 1976. Connes classifies injective factors (doi:10.2307/1971057).
• 1991. Brown and Pedersen introduce real rank zero (doi:10.1016/0022-1236(91)90056-B).
• 1999. Jiang and Su construct the algebra $\mathcal Z$ (doi:10.1353/ajm.1999.0012).
• 2010–2012. Winter and Zacharias define nuclear dimension and the Toms–Winter conjecture is formulated (doi:10.1016/j.aim.2009.12.005); Winter proves finite nuclear dimension implies $\mathcal Z$-stability (doi:10.1007/s00222-011-0334-7); Matui and Sato prove strict comparison implies $\mathcal Z$-stability with finitely many extremal traces (doi:10.1007/s11511-012-0084-4).
• 2013. Ozawa introduces uniform tracial completions (J. Math. Sci. Univ. Tokyo).
• 2021–2022. Castillejos, Evington, Tikuisis, White and Winter introduce uniform property $\Gamma$ and prove $\mathcal Z$-stability implies finite nuclear dimension (doi:10.1007/s00222-020-01013-1); CETW develop it systematically (doi:10.1093/imrn/rnaa282).
• 2023. Carrión et al. develop tracially complete $C^*$-algebras (arXiv:2310.20594).
• 2025–2026. Schafhauser, Tikuisis and White list Problem XXI (arXiv:2506.10902); Vaccaro, Kessinger–Toms and Fu obtain related implications (arXiv:2604.24682, arXiv:2607.23817, arXiv:2605.21655); Toms constructs a simple separable unital AH algebra without uniform property $\Gamma$ (arXiv:2606.12188).

The source of this mission is an OpenAI preprint dated September 23, 2026, which answers Problem XXI affirmatively (and, by separate arguments, also treats the unital Toms–Winter conjecture).

Setting

Let $A$ be a unital $C^*$-algebra with nonempty set $T(A)$ of tracial states. The uniform 2-seminorm is

$$\|a\|_{2,T(A)}=\sup_{\tau\in T(A)}\tau(a^*a)^{1/2}.$$

The uniform tracial completion $B=\overline A^{T(A)}$ consists of bounded sequences in $A$ that are Cauchy for $\|\cdot\|_{2,T(A)}$, modulo those tending to zero; each $\tau\in T(A)$ extends to a designated trace $\bar\tau$ on $B$. For a free ultrafilter $\omega$ on $\mathbb N$, the uniform tracial ultrapower $B^\omega$ is the algebra of bounded sequences in $B$ modulo those whose uniform 2-norm tends to zero along $\omega$. Its limit traces are

$$\lambda([(b_j)])=\lim_{j\to\omega}\bar\tau_j(b_j),\qquad \tau_j\in T(A),$$

and $\Lambda_\omega$ denotes the set of these. $B$ embeds in $B^\omega$ as constant sequences.

A unital $C^*$-algebra has real rank zero if every self-adjoint element is a norm limit of self-adjoint elements with finite spectrum. $A$ is stably finite if every isometry in every matrix algebra over $A$ is unitary, and nuclear if its algebraic tensor product with any $C^*$-algebra carries a unique $C^*$-norm.

Formalization targets

Goal: Theorem 1.1

Let $A$ be unital, separable, simple, infinite-dimensional, nuclear and stably finite with $T(A)\neq\varnothing$, and let $\omega$ be a free ultrafilter. If $B^\omega$ has real rank zero, then there is a projection $p\in B^\omega\cap B'$ with

$$\lambda(px)=\tfrac12\,\lambda(x)\qquad(x\in B,\ \lambda\in\Lambda_\omega).$$

This is the halving formulation of uniform property $\Gamma$ used in Problem XXI. The Lean statement OAI.ComparatorModel.CurrentMain.main is open on the platform.

Significance

The theorem shows that real rank zero at the level of the tracial ultrapower is enough to produce uniform property $\Gamma$, with no restriction on the trace space; the paper also deduces that every trace on $B$ is a designated extension (Corollary 1.2). Since uniform property $\Gamma$ plus strict comparison gives $\mathcal Z$-stability, this links projection structure in tracial ultrapowers to the Toms–Winter regularity theory. The equivalence between the halving formulation and the usual all-$m$ formulation is due to Carrión et al.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.

Difficulty

Real rank zero supplies many projections in $B^\omega$, but nothing makes them central, and halving must hold simultaneously for every limit trace and every coefficient $x\in B$. Divisibility results derived from real rank zero (Vaccaro) give tracially large order-zero maps without centrality; uniform property $\Gamma$ needs commutation with all of $B$ and exact coefficient identities. Equality of the scalar traces $\lambda(p)$ alone is not enough. Nuclearity by itself does not suffice either, as Toms' AH example shows, so the real rank zero hypothesis must be used in an essential way.

Formalization scope

• TracialState A is a positive linear functional with $\tau(1)=1$ and $\tau(ab)=\tau(ba)$; the order on $A$ is the $C^*$ order (StarOrderedRing).
• The uniform tracial completion is the quotient of the star-subalgebra of uniformly 2-Cauchy elements of $\ell^\infty(\mathbb N,A)$ by uniformly 2-null sequences; the ultrapower is the quotient of $\ell^\infty(\mathbb N,B)$ by sequences 2-null along U, computed with the designated traces $\bar\tau$.
• TopologicallySimple, StablyFinite (via CStarMatrix), IsNuclear (subsingleton of $C^*$-norms on algebraic tensor products, in a fixed universe) and RealRankZero (finite-spectrum self-adjoint approximation) are defined directly.
• UniformPropertyGammaAt A U asserts a star projection $p$ commuting with the image of $B$ and halving familyLimitTrace … s for every sequence of traces s : ℕ → TracialState A.
• MainClaim existentially packages five auxiliary Prop classes (quotient $C^*$-norm, closure properties of null and Cauchy sequences, existence of ultralimits, and vanishing of limit traces on null sequences). They are true general facts that a proof must establish; they are not assumptions.

A complete development needs ultrapowers and tracial completions of $C^*$-algebras, nuclearity and completely positive approximation, and real rank zero; all of this is reusable for the other regularity missions of this family. Contributions formalizing Theorem 1.3 (finite-set central splitting) and Corollary 1.2 are welcome.

Selected references

• OpenAI, Tracial projection methods and uniform property $\Gamma$, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Tracial-projection-methods-and-uniform-property-Gamma-September-23-2026/paper.pdf
• J. Castillejos, S. Evington, A. Tikuisis, S. White, Uniform property $\Gamma$, Int. Math. Res. Not., 2022. https://doi.org/10.1093/imrn/rnaa282
• J. Castillejos, S. Evington, A. Tikuisis, S. White, W. Winter, Nuclear dimension of simple $C^*$-algebras, Invent. Math., 2021. https://doi.org/10.1007/s00222-020-01013-1
• C. Schafhauser, A. Tikuisis, S. White, Nuclear $C^*$-algebras: 99 problems, 2026. https://arxiv.org/abs/2506.10902
• J. R. Carrión et al., Tracially Complete $C^*$-Algebras, 2023. https://arxiv.org/abs/2310.20594
• L. G. Brown, G. K. Pedersen, $C^*$-algebras of real rank zero, J. Funct. Anal., 1991. https://doi.org/10.1016/0022-1236(91)90056-B
• W. Winter, J. Zacharias, The nuclear dimension of $C^*$-algebras, Adv. Math., 2010. https://doi.org/10.1016/j.aim.2009.12.005
• H. Matui, Y. Sato, Strict comparison and $\mathcal Z$-absorption of nuclear $C^*$-algebras, Acta Math., 2012. https://doi.org/10.1007/s11511-012-0084-4
• A. Vaccaro, Stable rank one, tracial local homogeneity and uniform property $\Gamma$, 2026. https://arxiv.org/abs/2604.24682

Motivation

How rigid is a von Neumann algebra inside $B(H)$? If two algebras $M,N\subseteq B(H)$ have unit balls that are uniformly close, must they be the same algebra up to a small change of coordinates? Kadison and Kastler introduced the distance between the unit balls in 1972 (Amer. J. Math. 1972) and asked whether sufficiently close algebras are spatially isomorphic, implemented by a unitary close to the identity. The positive answer for a class of algebras is called (strong) Kadison–Kastler stability. The problem connects perturbation theory, Hochschild cohomology, and Kadison's similarity problem, and it was settled previously only for injective (amenable) algebras, type I algebras, and specific nonamenable examples.

This mission asks for a formal proof of the uniform strong Kadison–Kastler stability theorem stated in an OpenAI preprint dated September 23, 2026 (source): a single tolerance works for all von Neumann algebras on all Hilbert spaces. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1972 — Kadison and Kastler introduce the metric and prove stability results for type I algebras (Amer. J. Math. 1972).
• 1974–1975 — Phillips proves spatial isomorphism for close type I algebras (Pacific J. Math. 1974); Christensen obtains a conjugating unitary near the identity (J. LMS 1975).
• 1977 — Christensen (Invent. Math. 1977), Johnson (Proc. LMS 1977) and Raeburn–Taylor (JFA 1977) settle the injective case.
• 1980 — Christensen's theory of near inclusions (Acta Math. 1980).
• 1982 — Johnson's examples show that for C*-algebras the implementing unitary cannot always be chosen near the identity in a uniform way (Canad. Math. Bull. 1982).
• 1983 — Haagerup's cyclic similarity estimate (Ann. of Math. 1983).
• 2010–2012 — Christensen, Sinclair, Smith, White and Winter prove spatial isomorphism for close separable nuclear C*-algebras (PNAS 2010; Acta Math. 2012).
• 2012–2014 — Cameron, Christensen, Sinclair, Smith, White and Wiggins construct the first nonamenable Kadison–Kastler stable factors, $(L^\infty(X)\rtimes SL_n(\mathbb Z))\bar\otimes R$ for $n\ge3$ (PNAS 2012; Duke 2014).
• September 2026 — The OpenAI preprint claims uniform stability for all von Neumann algebras (Theorem 1.1, p. 2).

Setting

Let $H$ be a complex Hilbert space and $B(H)$ the bounded operators with the operator norm. A von Neumann algebra $M\subseteq B(H)$ is a unital $*$-subalgebra equal to its double commutant (in particular it contains the identity $I_H$). Write $M_1=\{x\in M:\|x\|\le1\}$ for its unit ball. The Kadison–Kastler distance is the Hausdorff distance of unit balls,

$$d(M,N)=\max\Bigl(\sup_{x\in M_1}\inf_{y\in N_1}\|x-y\|,\ \sup_{y\in N_1}\inf_{x\in M_1}\|x-y\|\Bigr).$$

A unitary $u\in B(H)$ conjugates $M$ to $N$ if $uMu^*=N$.

Formalization targets

Goal: Theorem 1.1 (p. 2)

For every $\varepsilon>0$ there is $\delta>0$ such that for every complex Hilbert space $H$ and all von Neumann algebras $M,N\subseteq B(H)$ with $d(M,N)<\delta$, there is a unitary $u\in B(H)$ with

$$uMu^*=N\qquad\text{and}\qquad\|u-I_H\|<\varepsilon .$$

The tolerance $\delta$ depends only on $\varepsilon$: not on the algebras, their type, their representations, or the size of $H$.

Significance

The result itself. It answers the Kadison–Kastler perturbation question in its strongest uniform form for von Neumann algebras, including all nonamenable and type III cases and non-separable Hilbert spaces. Consequences include that every algebraic or analytic invariant preserved by unitary conjugacy (type, factoriality, property $\Gamma$, Cartan subalgebras) is locally constant in the Kadison–Kastler metric. The analogous C*-algebra statement fails in its uniform-unitary form by Johnson's examples, so the theorem is specific to von Neumann algebras.

Formalizing it. The statement uses only Mathlib's VonNeumannAlgebra, unitary operators and Hausdorff distance, so it is fully expressible today. The proof, however, draws on free probability, tracial ultraproducts, Tomita–Takesaki theory, crossed products, Poisson boundaries and measurable cocycles, most of which are absent from Mathlib. Formalizing even the amenable (injective) case would be a substantial reusable contribution.

Difficulty

Closeness of unit balls supplies nearby elements but no linear or multiplicative correspondence between the algebras, and it gives no control at matrix levels, where perturbation arguments naturally live. For nonamenable algebras the classical route through vanishing Hochschild cohomology is unavailable. The preprint proceeds by cases. For finite factors it proves a uniform bound on all matrix amplifications of commutator maps (Theorem 3.1, p. 11) and corrects nearby unitaries to a measurable cocycle over an amenable boundary action (Section 4). Infinite factors require comparing modular groups through Tomita graphs (Proposition 6.5, p. 41) and aligning the modular action (Proposition 7.1, p. 45) before passing to crossed products (Theorem 8.4, p. 59). General algebras then require aligning centers and passing from separable to arbitrary Hilbert spaces (Section 9) without losing uniformity.

Formalization scope

• $H$ ranges over complex Hilbert spaces (NormedAddCommGroup, InnerProductSpace ℂ, CompleteSpace) in a fixed universe u; $\delta$ is chosen before $H$, so the uniformity over Hilbert spaces is part of the statement.
• VonNeumannAlgebra H is Mathlib's notion; these algebras contain the identity, so "unital with identity $I_H$" is built in.
• kkDistance M N is Metric.hausdorffDist of the closed unit balls. Both balls contain $0$ and are bounded, so the Hausdorff distance is finite and the definition is exactly (1.1).
• NearConjugacy M N ε asks for a unitary $v$ with $v\,M\,v^*=N$ as sets and $\|v-1\|<\varepsilon$.
• There is no trivializing reading: the hypotheses are satisfied by $M=N$, and the conclusion is nontrivial for $M\neq N$.

Selected references

• OpenAI, Universal strong Kadison–Kastler stability, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Universal-strong-Kadison-Kastler-stability-September-23-2026/paper.pdf
• R. V. Kadison, D. Kastler, Perturbations of von Neumann algebras. I. Stability of type, Amer. J. Math. 94 (1972). https://doi.org/10.2307/2373592
• E. Christensen, Perturbations of type I von Neumann algebras, J. London Math. Soc. (1975). https://doi.org/10.1112/jlms/s2-9.3.395
• E. Christensen, Perturbation of operator algebras, Invent. Math. 43 (1977). https://doi.org/10.1007/BF01390201
• B. E. Johnson, Perturbations of Banach algebras, Proc. London Math. Soc. (1977). https://doi.org/10.1112/plms/s3-34.3.439
• I. Raeburn, J. L. Taylor, Hochschild cohomology and perturbations of Banach algebras, J. Funct. Anal. (1977). https://doi.org/10.1016/0022-1236(77)90072-6
• E. Christensen, Near inclusions of C-algebras*, Acta Math. 144 (1980). https://doi.org/10.1007/BF02392125
• B. E. Johnson, A counterexample in the perturbation theory of C-algebras*, Canad. Math. Bull. 25 (1982). https://doi.org/10.4153/CMB-1982-043-4
• U. Haagerup, Solution of the similarity problem for cyclic representations of C-algebras*, Ann. of Math. 118 (1983). https://doi.org/10.2307/2007028
• E. Christensen, A. M. Sinclair, R. R. Smith, S. A. White, W. Winter, Perturbations of nuclear C-algebras*, Acta Math. 208 (2012). https://doi.org/10.1007/s11511-012-0075-5
• J. Cameron, E. Christensen, A. M. Sinclair, R. R. Smith, S. A. White, A. D. Wiggins, Kadison–Kastler stable factors, Duke Math. J. 163 (2014). https://doi.org/10.1215/00127094-2819736

Motivation

Bose–Einstein condensation (BEC) means that a single one-particle state carries a macroscopic fraction of a many-boson system. It was predicted for the ideal gas by Bose and Einstein (1924–1925) and is observed in dilute atomic gases, but for interacting particles in the thermodynamic limit there was no rigorous proof, even in the ground state. The Penrose–Onsager criterion (Phys. Rev. 1956) identifies condensation with a macroscopic eigenvalue of the one-particle density matrix. Energy asymptotics of the dilute gas are now known to second order, but they do not determine single-orbital occupation, since the one-particle spectral gap closes as the volume grows. Lieb and Yngvason explicitly separated the condensation question from their energy theorem, and Solovej's 2025 survey lists fixed-density ground-state condensation as a major problem in the field (C. R. Physique 2025, Section 5).

This mission asks for a formal proof of ground-state condensation for the dilute three-dimensional hard-sphere Bose gas, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1924–1925 — Bose and Einstein predict condensation in the ideal Bose gas (Z. Phys. 1924).
• 1947 — Bogoliubov's theory assumes a macroscopically occupied zero mode.
• 1956 — Penrose and Onsager's density-matrix criterion for condensation.
• 1957 — Dyson's bounds on the hard-sphere ground-state energy (Phys. Rev. 1957); Lee, Huang and Yang predict depletion of order $\sqrt{\rho a^3}$ (Phys. Rev. 1957).
• 1998 — Lieb and Yngvason prove the leading dilute energy asymptotics $4\pi\rho a$ (PRL 1998).
• 2002 — Lieb and Seiringer prove BEC for trapped gases in the Gross–Pitaevskii limit (PRL 2002).
• 2020 — Deuchert and Seiringer: homogeneous Gross–Pitaevskii limit at positive temperature (ARMA 2020).
• 2021–2026 — Fournais's length scales for BEC (EMS 2021); Fournais–Solovej's Lee–Huang–Yang lower bound including hard cores (Invent. Math. 2023); Basti et al.'s matching upper bound for hard spheres (arXiv:2603.13084); results of Chong–Liang–Nam (JFA 2026) and Junge (arXiv:2603.20776) in joint dilute and large-volume limits.
• September 2026 — The OpenAI preprint claims condensation at fixed density and fixed exclusion distance (Theorem 1.1, p. 3).

Setting

Let $\Lambda_L=(\mathbb R/L\mathbb Z)^3$ be the flat torus with torus distance $d_L$. For $N$ particles and exclusion distance $a>0$, the allowed configurations are

$$\Omega_{N,L,a}=\{X\in\Lambda_L^N:\ d_L(x_i,x_j)>a\ \text{for } i<j\}.$$

The hard-sphere Hamiltonian is the operator of the Dirichlet form $q[f]=\sum_{i=1}^N\int|\nabla_if|^2$ on $H^1_0(\Omega_{N,L,a})$ restricted to symmetric (bosonic) functions; wave functions vanish on forbidden configurations, and $a$ is the scattering length. A ground vector is a normalized bosonic minimizer of $q$. For a normalized bosonic $\Psi$, the condensate fraction in the constant orbital $\varphi_0=L^{-3/2}$ is

$$B(\Psi)=\frac{\langle\varphi_0,\Gamma^{(1)}_\Psi\varphi_0\rangle}{N}=\frac1{L^3}\int_{\Lambda_L^{N-1}}\Bigl|\int_{\Lambda_L}\Psi(x,Y)\,dx\Bigr|^2dY\in[0,1],$$

and for a density operator it is defined by linearity. The gas parameter is $\rho a^3$ with $\rho$ the density.

Formalization targets

Goal: Theorem 1.1 and Corollary 1.2 (p. 3)

There are absolute constants $\varepsilon_0,c_0>0$ such that, for all $a,\rho>0$ with $\rho a^3<\varepsilon_0$ and every sequence $N_k\to\infty$, $L_k\to\infty$ with $N_k/L_k^3\to\rho$:

1. for every choice of (possibly complex) bosonic ground vectors $\Psi_k$, $\ \liminf_k B(\Psi_k)\ge c_0$;
2. for every sequence of density operators $T_k$ supported on the bosonic ground spaces, the same bound holds for the occupation of $T_k$ (in particular for the normalized ground-space projections).

The constant $c_0$ does not depend on the gas parameter in this range.

Significance

The result itself. It is a proof of macroscopic condensation in an interacting continuum Bose gas with fixed density and fixed hard core, in the thermodynamic limit, uniformly over all ground states including degenerate ground spaces. Previous rigorous results let the gas parameter tend to zero with the volume, or concerned traps, scaling limits, or positive-temperature settings with different potentials. The theorem gives a positive fraction only; it does not reach the Lee–Huang–Yang depletion law.

Formalizing it. The statement involves Sobolev spaces with Dirichlet conditions on a configuration space of the torus, bosonic symmetry, density operators, and partial traces, none of which are packaged in Mathlib; the Lean development builds them concretely. The proof uses killed Brownian motion, percolation-type path constructions, and second-moment arguments. No machine-checked statement of BEC for an interacting system is known.

Difficulty

Energy estimates alone cannot detect occupation of the constant orbital, because the cost of moving particles out of it is of order $L^{-2}$ per particle and vanishes in the limit. One must show directly that a typical ground state correlates distant parts of the box. The preprint compares a tagged particle's position in distant cells by moving trajectories along random lattice routes; multiplying local comparison costs along a route loses a factor at every step, so instead it averages over random routes and bounds the second moment of the averaged likelihood, where exact cancellation of normalizers leaves a cost depending only on mutual encounters of two routes (Introduction, pp. 4–5; Section 8). A separate phase argument passes from $|\Psi|$ to complex $\Psi$ (Lemma 2.3, p. 9).

Formalization scope

• Configurations are Fin N → Fin 3 → AddCircle L; the allowed set uses the Euclidean torus distance with strict inequality a < dist.
• The form domain dirichletDomain is the closure, in $L^2\times(L^2)^{3N}$, of jets of smooth compactly supported test functions with support in the allowed set; energy is the sum of squared $L^2$ norms of the partial derivatives. IsGroundVector means: in the domain, bosonic (a.e. permutation invariant), normalized, and of minimal energy among such vectors.
• occupation is exactly $B(\Psi)$; mixedOccupation T is the trace of $T$ compressed by the bounded map $\Psi\mapsto L^{-3/2}\int\Psi(x,\cdot)\,dx$. GroundSupported T says every unit vector in $(\ker T)^\perp$ is (the first component of) a ground vector.
• Density operators are positive bounded operators with trace one, computed in a fixed Hilbert basis.
• Hypotheses on the sequences are only those of the source; the ground-vector hypothesis is required for every index $k$, which loses nothing since $\liminf$ depends only on tails.

Selected references

• OpenAI, Ground-state condensation in the dilute hard-sphere gas, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Ground-state-condensation-in-the-dilute-hard-sphere-gas-September-24-2026/paper.pdf
• O. Penrose, L. Onsager, Bose–Einstein condensation and liquid helium, Phys. Rev. 104 (1956). https://doi.org/10.1103/PhysRev.104.576
• F. J. Dyson, Ground-state energy of a hard-sphere gas, Phys. Rev. 106 (1957). https://doi.org/10.1103/PhysRev.106.20
• T. D. Lee, K. Huang, C. N. Yang, Eigenvalues and eigenfunctions of a Bose system of hard spheres and its low-temperature properties, Phys. Rev. 106 (1957). https://doi.org/10.1103/PhysRev.106.1135
• E. H. Lieb, J. Yngvason, Ground state energy of the low density Bose gas, Phys. Rev. Lett. 80 (1998). https://doi.org/10.1103/PhysRevLett.80.2504
• E. H. Lieb, R. Seiringer, Proof of Bose–Einstein condensation for dilute trapped gases, Phys. Rev. Lett. 88 (2002). https://doi.org/10.1103/PhysRevLett.88.170409
• S. Fournais, J. P. Solovej, The energy of dilute Bose gases II: the general case, Invent. Math. (2023). https://doi.org/10.1007/s00222-022-01175-0
• A. Deuchert, R. Seiringer, Gross–Pitaevskii limit of a homogeneous Bose gas at positive temperature, Arch. Ration. Mech. Anal. (2020). https://doi.org/10.1007/s00205-020-01489-4
• J. P. Solovej, Mathematical physics of dilute Bose gases, C. R. Physique (2025). https://doi.org/10.5802/crphys.247
• G. Basti, M. Brooks, S. Cenatiempo, A. Olgiati, B. Schlein, The Lee–Huang–Yang energy for a dilute gas of hard spheres: an upper bound, arXiv:2603.13084 (2026). https://arxiv.org/abs/2603.13084v2

Motivation: Banach's simple Lebesgue-spectrum problem

A measure-preserving transformation $T$ of a probability space acts on square-integrable functions by the Koopman operator $U_Tg=g\circ T$, a unitary operator. Its spectral type (discrete, singular continuous, absolutely continuous) and its multiplicity are basic invariants of ergodic theory. The Lebesgue spectrum is the spectral type of the shift on $\ell^2(\mathbb Z)$, the type of Bernoulli shifts and other strongly chaotic systems, where it occurs with infinite multiplicity. Banach's problem asks whether Lebesgue spectrum can occur with multiplicity one: is there a transformation whose Koopman operator on the orthogonal complement of the constants is unitarily equivalent to multiplication by $w$ on $L^2(S^1)$? Equivalently, is there a single function whose bilateral orbit under $U_T$ is an orthonormal basis of the mean-zero space? The problem combines spectral theory with the construction of explicit dynamics, and a smooth example would show this spectral behavior is compatible with the regularity of differentiable dynamics.

Timeline

• 1949 — Rokhlin asks for ergodic automorphisms with simple, or at least finite-multiplicity, Lebesgue spectrum (Uspekhi Mat. Nauk 1949, §4, no. 7).
• 1960 — Ulam records a real-line form of the question attributed to Banach (A Collection of Mathematical Problems, Interscience, 1960, §6, p. 76).
• 1970 — Anosov and Katok introduce approximation-by-conjugation constructions of smooth ergodic diffeomorphisms (Trudy MMO 1970).
• 1978 — Helson and Parry construct cocycles over aperiodic transformations with associated Lebesgue spectrum (Ark. Mat. 1978).
• 1984 — Mathew and Nadkarni construct a transformation with a Lebesgue component of multiplicity two (Bull. LMS 1984).
• 1999 — Guenais connects Morse cocycles with flat polynomials and constructs a group action with simple spectrum of mixed type (ETDS 1999).
• 2001 — Fayad constructs $C^\infty$ volume-preserving torus diffeomorphisms with simple (not Lebesgue) spectrum (J. LMS 2001).
• 2020–2023 — Prikhod'ko constructs a finite-measure flow with simple Lebesgue spectrum (Sb. Math. 2020); Fayad–Forni–Kanigowski (JAMS 2021) and Abdedou–Fayad–Kessi (DCDS 2023) obtain smooth flows with countable Lebesgue multiplicity; el Abdalaoui presents an infinite-measure conservative example (arXiv:1508.06439). None of these gives a probability-preserving map with simple Lebesgue spectrum on the whole mean-zero space.
• 2026 — The OpenAI preprint A smooth three-torus diffeomorphism with simple Lebesgue spectrum (OpenAI Math Release, September 23, 2026) claims a $C^\infty$ volume-preserving diffeomorphism of $\mathbb T^3$ with this property. It has not been peer reviewed and its theorem is not formally verified.

Setting

Let $\mathbb T=\mathbb R/\mathbb Z$ and let $\mu$ be normalized Lebesgue (Haar) measure on $\mathbb T^3$. A bijection $T:\mathbb T^3\to\mathbb T^3$ is a $C^\infty$ diffeomorphism if $T$ and $T^{-1}$ lift locally to $C^\infty$ maps of $\mathbb R^3$. It is volume preserving if $\mu(T^{-1}A)=\mu(A)$ for every measurable $A$. Let $L^2_0(\mathbb T^3,\mu)$ be the closed subspace of complex square-integrable functions with integral zero, and $U_Tg=g\circ T$. Let $m$ be Haar measure on the circle and $w(z)=e^{2\pi i z}$ the first Fourier character.

In Lean (namespace OAI.ThreeTorus), the torus is Fin 3 → UnitAddCircle with the product Haar measure, smoothness is local smooth lifting on Fin 3 → ℝ, $L^2_0$ is the subspace meanZero of Lp ℂ 2 μ, and MainConclusion packages the theorem below.

Formalization targets

Goal: smooth simple Lebesgue spectrum (Theorem 1.1)

There exist a $C^\infty$ volume-preserving diffeomorphism $T$ of $\mathbb T^3$ and a real-valued $f\in L^2_0(\mathbb T^3,\mu)$ such that

$$\{\,f\circ T^n : n\in\mathbb Z\,\}\ \text{is an orthonormal basis of } L^2_0(\mathbb T^3,\mu);$$

moreover $T$ is ergodic, and there is a unitary $W:L^2_0(\mathbb T^3,\mu)\to L^2(S^1,m)$ with

$$W(g\circ T)=w\cdot W(g)\qquad\text{for all } g\in L^2_0 .$$

The goal is published on the platform with status Open.

Significance

The result itself. The theorem answers the probability-preserving form of Banach's problem, with the strongest kind of example: the invariant measure is the standard smooth volume on a compact manifold, the map is $C^\infty$, and the conclusion covers the whole mean-zero space, both spectral type and multiplicity. Earlier work produced Lebesgue components, Lebesgue spectrum of higher multiplicity, simple spectrum of other types, flows, or infinite-measure examples; time-$t$ maps of simple-Lebesgue flows have infinite multiplicity, so they do not answer the question. The source also derives from it mixing (of all orders, using a separate companion multiple-mixing theorem), zero Kolmogorov–Sinai entropy (via Rokhlin's finite-multiplicity entropy theorem) and vanishing Lyapunov exponents (Corollary 6.1, p. 28).

Formalizing it. The statement exercises Mathlib's $L^p$ spaces, Haar measure on the additive circle, ergodicity and Fourier characters together. A formal proof would certify a long quantitative construction (successive smooth passages, stationary-phase estimates, Fourier signals) whose convergence must be checked simultaneously in the $C^\infty$ topology and in spectral norms.

Difficulty

Smooth constructions by successive conjugation (Anosov–Katok type) naturally produce maps with singular or discrete spectral behavior, because each approximating map is close to a rotation or an integrable twist with pure point or very structured spectrum. Lebesgue spectral type requires the spectral measure of every function to be absolutely continuous with the right density, and simplicity requires a single orbit to span the whole space. Making both hold in the limit, while keeping the limit map $C^\infty$, requires controlling spectral densities at every scale and approximating every target function by translates of one fixed vector — the step where generic perturbation arguments give no control.

Formalization scope

• The torus is Fin 3 → UnitAddCircle with Measure.pi of AddCircle.haarAddCircle; $T$ is an Equiv.Perm with Smooth T and Smooth T.symm (local $C^\infty$ lifts), and MeasurePreserving T μ μ.
• $L^2_0$ is the complex subspace of Lp ℂ 2 μ with zero integral; $f$ is real-valued almost everywhere. The orbit $v_n=f\circ T^n$ is required to be orthonormal with dense span, i.e. a Hilbert basis indexed by $\mathbb Z$.
• The spectral model is stated with an explicit linear isometric equivalence W : H₀ ≃ₗᵢ[ℂ] CircleH intertwining composition with $T$ and multiplication by fourier 1. Ergodicity is Mathlib's Ergodic T μ.
• Mixing, zero entropy and Lyapunov exponents (Section 6) are not part of the goal.
• Needed infrastructure: stationary-phase estimates, spectral measures of Koopman operators, smooth volume-preserving changes of coordinates on the torus. Spectral-theory infrastructure for Koopman operators is reusable throughout ergodic theory.

Selected references

• V. A. Rokhlin, Selected topics from the metric theory of dynamical systems, Uspekhi Mat. Nauk 4 (1949). https://www.mathnet.ru/eng/rm8607
• S. M. Ulam, A Collection of Mathematical Problems, Interscience Tracts in Pure and Applied Mathematics 8, 1960.
• D. V. Anosov and A. B. Katok, New examples in smooth ergodic theory. Ergodic diffeomorphisms, Trudy Moskov. Mat. Obshch. 23 (1970). https://www.mathnet.ru/eng/mmo237
• H. Helson and W. Parry, Cocycles and spectra, Ark. Mat. 16 (1978). https://doi.org/10.1007/BF02385994
• J. Mathew and M. G. Nadkarni, A measure preserving transformation whose spectrum has Lebesgue component of multiplicity two, Bull. London Math. Soc. 16 (1984). https://doi.org/10.1112/blms/16.4.402
• M. Guenais, Morse cocycles and simple Lebesgue spectrum, Ergodic Theory Dynam. Systems 19 (1999). https://doi.org/10.1017/S0143385799126579
• B. R. Fayad, Partially mixing and locally rank one smooth transformations and flows on the torus $\mathbb T^d$, $d\ge3$, J. London Math. Soc. 64 (2001). https://doi.org/10.1112/S0024610701002447
• A. A. Prikhod'ko, On ergodic flows with simple Lebesgue spectrum, Sb. Math. 211 (2020). https://doi.org/10.1070/SM8147
• B. Fayad, G. Forni and A. Kanigowski, Lebesgue spectrum of countable multiplicity for conservative flows on the torus, J. Amer. Math. Soc. 34 (2021). https://doi.org/10.1090/jams/970
• OpenAI, A smooth three-torus diffeomorphism with simple Lebesgue spectrum, OpenAI Math Release preprint, September 23, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-smooth-three-torus-diffeomorphism-with-simple-Lebesgue-spectrum-September-23-2026/paper.pdf

Motivation

Edit distance $\mathrm{ED}(x,y)$ is the least number of single-symbol insertions, deletions and substitutions transforming a string $x$ into $y$. It is the basic similarity measure for strings, but it is expensive to compute and awkward to index. A standard way around this is to embed strings into $\ell_1$ so that $\ell_1$ distances approximate edit distances; the quality of such a map is its distortion. Low-distortion embeddings give fast approximate nearest-neighbour search and sketching for edit distance, so the best possible distortion has been studied for two decades.

This preprint determines the exponential scale of the optimal distortion: for strings of length at most $d$, it is $\exp(\Theta(\sqrt{\log d\,\log\log d}))$, uniformly over finite alphabets.

Background

• 1966. Levenshtein studies codes correcting insertions, deletions and substitutions.
• 1974. Wagner and Fischer describe edit scripts through increasing traces (alignments).
• 1995. Linial, London and Rabinovich develop the geometry of finite metric embeddings into $\ell_1$.
• 2003. Andoni, Deza, Gupta, Indyk and Raskhodnikova give binary subsets with $\ell_1$ distortion approaching $3/2$.
• 2006. Khot and Naor prove an $\Omega(\sqrt{\log d/\log\log d})$ lower bound via cuts and Fourier analysis of noisy shifts.
• 2007. Ostrovsky and Rabani prove the upper bound $\exp(O(\sqrt{\log d\log\log d}))$ for binary strings of length $d$.
• 2009. Krauthgamer and Rabani prove an $\Omega(\log d)$ lower bound for binary strings of length $d$.
• 2026. The OpenAI preprint Edit Distance in $\ell_1$: Matching Bounds up to Constants in the Exponent (dated September 27, 2026) proves a matching lower bound $\exp(\Omega(\sqrt{\log d\log\log d}))$. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

For a finite alphabet $\Sigma$ and $d \ge 1$, let $\Sigma^{\le d}$ be the set of strings of length at most $d$, including the empty string. Edit scripts may pass through strings of any length. Let $\ell_1$ be the space of absolutely summable real sequences. Define

$$E_\Sigma(d) = \inf_{f:\Sigma^{\le d}\hookrightarrow \ell_1}\Big(\max_{x\ne y}\frac{\|f(x)-f(y)\|_1}{\mathrm{ED}(x,y)}\Big)\Big(\max_{x\ne y}\frac{\mathrm{ED}(x,y)}{\|f(x)-f(y)\|_1}\Big),$$

the infimum over injective maps with no restriction on dimension or computability.

In Lean (OAI.EditDistortion), edit x y is the least length of a Script true n x y of unit insertions, deletions and substitutions on List Alpha; L1 = lp (fun _ : ℕ => ℝ) 1; distortion ρ f is the product of the two maximal ratios for an embedding f : X ↪ L1; leastDistortion is the infimum over embeddings; E Alpha d applies this to {x : List Alpha // x.length ≤ d}; exponentScale c d = exp(c·sqrt(log d · log log d)).

Formalization targets

Goal: Theorem 1.1

There are absolute $c, C > 0$ and $d_0$ such that for every $d \ge d_0$ and every finite alphabet with $|\Sigma| \ge 2$,

$$\exp\big(c\sqrt{\log d\,\log\log d}\big) \le E_\Sigma(d) \le \exp\big(C\sqrt{\log d\,\log\log d}\big).$$

The lower bound is witnessed by a finite set of binary strings of one common length at most $d$, and the same two bounds hold for $\sup_{2 \le |\Sigma| < \infty} E_\Sigma(d)$.

Significance

The result. Theorem 1.1 shows that the Ostrovsky–Rabani embedding is optimal up to the constant in the exponent, closing the gap between $\Omega(\log d)$ (Krauthgamer–Rabani) and $\exp(O(\sqrt{\log d\log\log d}))$. It rules out any $\ell_1$ embedding of edit distance with distortion $\exp(o(\sqrt{\log d\log\log d}))$, which limits $\ell_1$-based approaches to approximate edit-distance search.

Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. The upper bound relies on Ostrovsky and Rabani's fixed-length theorem (Theorem 5.1 in the preprint, taken from the literature) plus reductions proved in the preprint, so a full formalization also requires formalizing the Ostrovsky–Rabani embedding. The lower bound (Sections 2–4) is the new contribution.

Difficulty

Any lower bound must control every alignment of two strings, including matchings that cross the boundaries of the blocks used to build them, because an insertion or deletion shifts an entire suffix. Earlier Fourier-analytic arguments (Khot–Naor) and recursive constructions (Krauthgamer–Rabani) lose too much to reach the $\sqrt{\log d\log\log d}$ exponent; reaching it requires a construction whose combinatorial separation and an $\ell_1$ displacement inequality match at that scale.

Formalization scope

• Strings are List Alpha with Fintype Alpha, 2 ≤ card Alpha; the domain includes the empty string and all lengths up to $d$.
• Edit distance includes substitutions; edit is an sInf over script lengths, which is attained since scripts always exist.
• distortion uses sSup over finitely many ratios (the domain is finite), so no default values arise; leastDistortion is sInf over all injective maps into $\ell_1(\mathbb{N})$.
• BinaryWitness c d asks for a finite nonempty set of Boolean lists of common length $n \le d$ whose least distortion is at least exponentScale c d; a singleton has least distortion $0$, so the witness must be nontrivial.

The statement cannot be met trivially: both bounds are required with constants uniform in the alphabet.

Needed infrastructure: cut decompositions of finite $\ell_1$ metrics, Fourier analysis on finite abelian groups, prime-number estimates (Rosser–Schoenfeld), and the Ostrovsky–Rabani construction. Contributions toward the displacement inequality (Proposition 2.2) or the recursive construction (Proposition 3.1) are welcome.

Selected references

• OpenAI, Edit Distance in $\ell_1$: Matching Bounds up to Constants in the Exponent, OpenAI Math Release preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Edit-Distance-in-l1-Matching-Bounds-up-to-Constants-in-the-Exponent-September-27-2026/paper.pdf
• R. Ostrovsky, Y. Rabani, Low distortion embeddings for edit distance, J. ACM 54(5), Article 23, 2007. https://doi.org/10.1145/1284320.1284322
• R. Krauthgamer, Y. Rabani, Improved lower bounds for embeddings into $L_1$, SIAM J. Comput. 38(6), 2009.
• S. Khot, A. Naor, Nonembeddability theorems via Fourier analysis, Math. Ann. 334(4), 2006. https://doi.org/10.1007/s00208-005-0745-0
• A. Andoni, M. Deza, A. Gupta, P. Indyk, S. Raskhodnikova, Lower bounds for embedding edit distance into normed spaces, SODA 2003.
• N. Linial, E. London, Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2), 1995. https://doi.org/10.1007/BF01200757
• V. I. Levenshtein, Binary codes capable of correcting deletions, insertions, and reversals, Soviet Physics Doklady 10(8), 1966.
• R. A. Wagner, M. J. Fischer, The string-to-string correction problem, J. ACM 21(1), 1974. https://doi.org/10.1145/321796.321811

Motivation

The volume product of a convex body measures how large a body and its polar can simultaneously be. For a body without a distinguished centre, the polar is taken about the point that makes it smallest, the Santaló point, so the product is invariant under all invertible affine maps. The Blaschke–Santaló inequality identifies ellipsoids as the maximizers. Mahler's conjecture for general convex bodies asks for the minimizers and predicts simplices, with minimum value $(n+1)^{n+1}/(n!)^2$. The question arose from Mahler's work on polarity and the geometry of numbers, and it is the sharp form of the Bourgain–Milman reverse Santaló inequality.

This mission asks for a formal proof of the general Mahler conjecture with its equality case, as stated in an OpenAI preprint dated September 22, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Timeline

• 1938–1939 — Mahler proves the planar inequality among polygons with triangles as equality cases (Ein Minimalproblem für konvexe Polygone, Mathematica (Zutphen) B, 1938) and formulates the higher-dimensional problem (Časopis 1939).
• 1949 — Santaló's affine invariant and the centre now named after him (Portugaliae Math., 1949).
• 1987 — Bourgain and Milman prove an inverse Santaló inequality with an exponential constant (Invent. Math. 1987).
• 1991 — Meyer completes the planar case for arbitrary convex bodies: triangles are exactly the minimizers (Monatsh. Math. 1991).
• 2006 — Meyer and Reisner use shadow systems to prove the sharp inequality for polytopes with at most $n+3$ vertices (Mathematika 2006).
• 2008–2012 — Kuperberg's explicit lower bounds via Gauss linking integrals (GAFA 2008); Nazarov's complex-analytic proof of Bourgain–Milman (GAFA seminar 2012).
• 2011 — Kim and Reisner prove strict local minimality at every simplex (Mathematika 2011).
• 2018 — Klartag's cone/Laplace-transform formulation of Mahler volumes (Adv. Math. 2018).
• 2024 — Mastrantonis and Rubinstein extend Nazarov's method to nonsymmetric bodies (arXiv:2206.06188).
• 2026 — Chen, Li, Xi and Xu prove the three-dimensional general case with tetrahedra as minimizers (arXiv:2605.09334).
• September 2026 — The OpenAI preprint claims the general conjecture in every dimension (Theorem 1.1, p. 1).

Setting

A convex body $K\subset\mathbb R^n$ is a compact convex set with nonempty interior; $|\cdot|$ is Lebesgue measure and $\langle\cdot,\cdot\rangle$ the Euclidean inner product. For an interior point $z$, the polar of $K$ about $z$ is

$$(K-z)^\circ=\{y\in\mathbb R^n:\ \langle y,x-z\rangle\le1\ \text{for all }x\in K\},$$

and the volume product is

$$P(K)=\inf_{z\in\operatorname{int}K}|K|\,|(K-z)^\circ|.$$

The infimum is attained at the unique Santaló point $s(K)$. A simplex is the convex hull of $n+1$ affinely independent points.

Formalization targets

Goal: the general Mahler conjecture (Theorem 1.1, p. 1)

For every $n\ge1$ and every convex body $K\subset\mathbb R^n$,

$$P(K)\ \ge\ \frac{(n+1)^{n+1}}{(n!)^2},$$

with equality if and only if $K$ is a simplex.

Significance

The result itself. It is the exact form of a problem open since the 1930s and previously settled only in dimensions $2$ and $3$ and for polytopes with few vertices. Because the infimum over centres is taken, it gives the same lower bound for $|K||(K-z)^\circ|$ at every interior point $z$. Via the known geometric-to-functional implication, the preprint derives the sharp functional Mahler inequality for log-concave functions and an entropy–transport inequality (Corollary 1.2, p. 4; Corollary 8.1, p. 41). The symmetric conjecture, with the larger constant $4^n/n!$, is a different statement treated in a companion preprint.

Formalizing it. The proof combines convex cones and their Laplace transforms, Gaussian Sobolev calculus, Moreau's decomposition, matrix divided differences, and certified one-variable inequalities. A formal proof would provide checked versions of these tools and of the Santaló point's existence and uniqueness. No machine-checked proof of the conjecture in any dimension $n\ge2$ is known.

Difficulty

Symmetrization does not apply, the volume product is not convex along natural deformations except in restricted families (shadow systems), and local minimality at simplices says nothing about distant bodies. In the preprint's route the main obstacle (Introduction, pp. 2–3) is that the Jacobian matrices $P_z=D\Pi_C(Z+\xi_z)$ of the Gaussian-averaged cone projections neither commute nor increase in $z$: bounding them separately loses both the sharp constant and the equality case. Controlling them jointly requires comparing the whole family with spectral thresholds of a linear Gaussian matrix (Sections 5–7), and equality must then force the cone to split into half-lines.

Formalization scope

• Bodies are subsets of EuclideanSpace ℝ (Fin n) with IsCompact, Convex ℝ and nonempty interior, and $n\ge1$.
• polarAt K z is the polar about $z$; volumeProduct K is the sInf over interior K of (volume K).toReal * (volume (polarAt K z)).toReal. For an interior $z$ the polar is bounded, so toReal reads the true volume; the index set is nonempty because the interior is.
• The goal is a conjunction: the inequality, and volumeProduct K = (n+1)^(n+1)/(n!)^2 iff K = convexHull ℝ (range v) for some affinely independent v : Fin (n+1) → _.
• The Santaló point is not named in Lean; using the infimum over interior points is equivalent to evaluating at $s(K)$ because the infimum is attained there (Section 2 of the preprint).

Welcome contributions: polar bodies and their volumes in Mathlib, the Santaló point, Laplace transforms of convex cones, and Gaussian integration by parts.

Selected references

• OpenAI, The Mahler Conjecture for General Convex Bodies, OpenAI Math Release preprint, September 22, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Mahler-Conjecture-for-General-Convex-Bodies-September-22-2026/paper.pdf
• OpenAI, The symmetric Mahler conjecture and its equality cases, OpenAI Math Release preprint, September 22, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-symmetric-Mahler-conjecture-and-its-equality-cases-September-22-2026/paper.pdf
• K. Mahler, Ein Übertragungsprinzip für konvexe Körper, Časopis Pěst. Mat. Fys. 68 (1939). https://doi.org/10.21136/CPMF.1939.109441
• M. Meyer, Convex bodies with minimal volume product in $\mathbb R^2$, Monatsh. Math. (1991). https://doi.org/10.1007/BF01351770
• J. Bourgain, V. Milman, New volume ratio properties for convex symmetric bodies in $\mathbb R^n$, Invent. Math. (1987). https://doi.org/10.1007/BF01388911
• G. Kuperberg, From the Mahler conjecture to Gauss linking integrals, GAFA (2008). https://doi.org/10.1007/s00039-008-0669-4
• M. Meyer, S. Reisner, Shadow systems and volumes of polar convex bodies, Mathematika (2006). https://doi.org/10.1112/S0025579300000061
• J. Kim, S. Reisner, Local minimality of the volume-product at the simplex, Mathematika (2011). https://doi.org/10.1112/S0025579310001555
• B. Klartag, Isotropic constants and Mahler volumes, Adv. Math. (2018). https://doi.org/10.1016/j.aim.2018.03.009
• V. Mastrantonis, Y. A. Rubinstein, The Nazarov proof of the non-symmetric Bourgain–Milman inequality, Indiana Univ. Math. J. (2024). https://arxiv.org/abs/2206.06188
• S. Chen, Y. Li, D. Xi, Z. Xu, The Mahler Conjecture in Three Dimensions, preprint (2026). https://arxiv.org/abs/2605.09334v3