OAI Math

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

Uniform discreteness places a lower bound on distances between points. The target tests whether that metric simplicity forces uniformly bounded finite-rank approximation in the associated Lipschitz-free space. The pinned manuscript supplies the research context.

Setting

The free space is the closed real span of point evaluations in the dual of Lipschitz functions vanishing at a base point. Approximation and bounded approximation retain their distinct operator-norm quantifiers.

Formalization target

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

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

The theorem states that two propositions hold together, both about the Lipschitz-free space FreeSpace(o) of a pointed metric space (M,o), which is the closed linear span, inside the dual of the Banach space Lip0(o) of real Lipschitz functions vanishing at o (normed by the supremum of the slopes |f(x)-f(y)|/d(x,y)), of the point evaluations; delta(o,a) denotes the evaluation at a. The first, BlockStatement, says that for every natural number p ≥ 1 there exist a countable metric space M and a base point o with all distinct points at distance at least 1 and all distances at most 300p²+150p+5, together with a finite set A of M containing o, such that every bounded linear operator T on FreeSpace(o) of finite rank and norm at most p moves some delta(o,a) with a in A by at least 1/2, that is ‖T(delta(o,a))-delta(o,a)‖ ≥ 1/2. The second, MainStatement, says there exist a countable metric space M and a point o such that distinct points are at distance at least 1, M is unbounded, M is not a proper space, FreeSpace(o) has the approximation property (finite-rank bounded operators approximate the identity uniformly on every compact set to within any ε>0), and yet for every Λ ≥ 1 FreeSpace(o) fails the bounded approximation property with constant Λ, meaning the approximating finite-rank operators cannot all be chosen with norm at most Λ. The theorem is stated with sorry, so no proof is asserted here.

Significance and status

The selected conjunction includes quantitative block obstructions and an unbounded, nonproper, uniformly discrete example. The quantitative real-ℓ1 renorming target is retained as an additional reference. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

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

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

Additional published targets are included as separate references:

• OAI.DiscreteFree.real_l1_quantitative_renorming (Open).

Selected references

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

Motivation

A positive averaged midpoint modulus need not supply a positive one-sided asymptotic modulus. Tree-potential norms give explicit spaces in which to separate those notions. The pinned manuscript supplies the research context.

Setting

Coordinates are finite lists of natural numbers. Tests have bounded prefix potentials, one of the specified quadratic budgets and a budget-dependent support condition; the normed space is completed.

Formalization target

The selected goal is OAI.BoundedTreePotentials.TreeCalculus.main_counterexample. Its central assertion is

$$\overline\delta_X(t)\geq\sqrt{1+t^2/4}-1\qquad(0<t<1).$$

The theorem states that, for every choice of a Boolean flag r (whether the root node, the empty list, is included as a coordinate) and every quadratic kind k among sibling, antichain and global, the following hold for the Banach space X = TestCompletion(treeTestFamily r k). Here nodes are finite lists of natural numbers, the potential of a coefficient function f at a node s is the sum of f over all prefixes of s, and a coefficient function f is a tree test if f vanishes at the root when r is false, every potential satisfies |potential f s| ≤ 1, a quadratic budget holds, and a support condition holds. The budget says that the sum of f(s)² over every admissible finite set B of nodes is at most 1, where admissible means: all of B are children of one common parent (sibling), pairwise prefix-incomparable (antichain), or any finite set (global). The support condition is vacuous for sibling, finite support for antichain, and square-summability for global. The tree test family is the set of such functions on the coordinates, and each finitely supported vector x is given the norm sup over tests f of |Σ x_i f_i|; X is the completion of this normed space. First, X is complete, separable, and not finite-dimensional over ℝ. Second, for every 0 < t < 1, the averaged modulus of X, defined as the infimum over unit vectors x of the supremum over closed finite-codimension subspaces F of the infimum over y in F with ‖y‖ ≥ 1 of (‖x+ty‖+‖x−ty‖)/2 − 1, is at least √(1+t²/4) − 1. Third, for every real normed space Y that is linearly homeomorphic to X, Y does not satisfy IsAUCReal, meaning it is false that the one-sided modulus (defined like the averaged one but with ‖y‖ = 1 and the quantity ‖x+ty‖ − 1) is positive for every t > 0.

Significance and status

The formal statement quantifies over both root flags and all three encoded quadratic kinds. Its claims are completeness, separability, infinite dimension, the stated modulus bound and no linearly equivalent AUC space. 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 lower estimate must coexist with an obstruction to every equivalent AUC norm, not just failure for the original tree norm.

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, Midpoint convexity from bounded tree potentials and path costs, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

Independent positive multipliers on a branching tree generate concrete subspaces of real L1. Their asymptotic geometry can distinguish midpoint estimates from AUC renormability. The pinned manuscript supplies the research context.

Setting

A nonconstant positive multiplier has probability law μ, mean one and finite second moment. Path products are multiplied along nonempty prefixes, and their L1 classes generate a closed real span.

Formalization target

The selected goal is OAI.IndependentProducts.main_general. Its central assertion is

$$\dim\operatorname{productSpan}(\mu)=\infty,\qquad\neg\exists\text{ equivalent AUC norm}.$$

The theorem states that, for any Borel measure μ on ℝ satisfying the multiplier hypotheses, the closed real L¹ span of the path products is infinite-dimensional, and no equivalent norm on it is AUC. The hypotheses say that μ is a probability measure, almost every value is positive, μ is not almost surely equal to any constant, its mean is 1, and the identity function has a finite second moment (is in L²). Vertices are finite lists of positive integers, a sample assigns a real number to each nonroot vertex, and the product measure is the infinite product of independent copies of μ, one per nonroot vertex. The path product of a vertex v multiplies the sample values at the nonempty prefixes of v, and is 1 for the root. productSpan(μ) is the topological closure, in L¹ of the product measure, of the real linear span of the classes equal almost everywhere to some path product. The theorem concludes first that productSpan(μ) is not finite-dimensional over ℝ. Second, for every seminorm N on productSpan(μ) that is an equivalent norm, meaning there are constants 0<a≤b with a‖x‖≤N(x)≤b‖x‖ for all x, N fails the AUC property, which requires that, for every t>0, the one-sided asymptotic modulus of N at t is strictly positive. That modulus is the infimum over N-unit vectors x of the supremum over closed finite-codimension subspaces F of the infimum of N(x+ty)−1 over y in F with N(y)=1. The statement is given as an admitted theorem without proof.

Significance and status

The selected general target asserts infinite dimension and absence of AUC renormings. Specific exponential and Gaussian-square midpoint estimates are separate published targets, retained as additional references. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

The obstruction must work for every admissible multiplier distribution and every equivalent norm, rather than only a particular exponential example.

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.IndependentProducts.main_exponential (Open).
• OAI.IndependentProducts.main_gaussian_12 (Open).
• OAI.IndependentProducts.main_gaussian_24 (Open).

Selected references

• OpenAI, Independent products in real L1: asymptotic midpoint convexity without AUC renormings, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

Recursive potentials can define tree norms with controlled midpoint behavior. The central question is whether that control forces an asymptotically uniformly convex renorming. The pinned manuscript supplies the research context.

Setting

The encoded constructions include root-sum and zero-root completions, finite tree heads, aggregation spaces and variable-exponent coordinate models. Two least nonnegative potential fields determine the norms.

Formalization target

The selected goal is OAI.ComparatorModel.RecursivePotentials.main. Its central assertion is

$$\overline\delta(t)\geq t^3/128\qquad(0<t<1).$$

The theorem states (its proof is admitted with sorry) that the defined proposition MainClaim holds. MainClaim asserts that there exist constructions, over index types in universe 0, of the finite rooted tree head structure, the tree-vector spaces, the zero-root tree-vector spaces, the aggregation-vector spaces, and their l^p-coordinate models, such that eleven statements about completions of finite-support vectors on rooted trees hold simultaneously. These comprise: (1) completion statements saying that the root-sum tree space for the sequence tree and for the joined tree, and the zero-root space for the joined tree, are complete, infinite-dimensional, with continuous coordinates extending the vector coordinates, continuous potential fields P and Q extending the finite-tree ones, norm equal to P+Q at the root (or both P and Q at the root in the zero-root case, where the root coordinate vanishes), and with norm-nonincreasing idempotent coordinate projections onto initial subtrees having finite-dimensional range, closed finite-codimensional tails and approximation of tail elements by vectors vanishing on the head, and that XZero and XJoined are reflexive; (2) a main statement giving the lower bound t^3/128 on the averaged modulus of XSigma and XJoined for 0<t<1, a cubic-type uniform convexity inequality (‖x+z‖+‖x-z‖)/2 ≥ ‖x‖+‖z‖^3/(8(2‖x‖+‖z‖)^2) for x supported on a head and z vanishing there, and that no equivalent norm on XSigma, XZero or XJoined has the AUC property (positive modulus at every positive t); (3) positivity of the averaged modulus of XSigma at every positive radius t; (4) a separation statement for XJoined: for each ε>0 there is η in (0,1), equal to min(1/2, logarithmicGamma(2, ε/16)) when ε≤2, such that if ‖x±z_n‖≤1 for all n and the z_n are pairwise at distance at least ε, then ‖x‖≤1-η; (5) properties of the variable-exponent l^2-sum of height-h tree spaces with exponents 1+1/h, namely completeness, reflexivity, separable dual, a root-sum functional ν (nonnegative, definite, subadditive, absolutely homogeneous) bounded above and below by explicit multiples of the l^p norm, dense finitely supported vectors, and finite-rank projections; (6) a recursive characterization of the l^p-model potentials by least pairs, with ν equal to the root P plus Q; (7) for every equivalent norm A on the variable space, the modulus at lower/upper vanishes; (8) the absence of any equivalent AUC norm there; (9) a sixth-power stability inequality and (10) a cubic stability inequality for admissible heads, with explicit constants; and (11) a weak-tail estimate: if x and a weakly null sequence y_j with ‖y_j‖≥ε, 0<ε≤1, satisfy ‖x±y_j‖≤1, then ‖x‖≤θ(ε)<1.

Significance and status

The published MainClaim is an eleven-part package, not only the displayed midpoint inequality. Its additional completion, separation, stability, weak-tail and no-AUC assertions remain part of the goal. 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 bundled target must coordinate completion, continuous coordinate maps, finite-head approximations, reflexivity and uniform estimates across several related spaces.

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, Midpoint convexity from two recursive potentials, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

Fixed-point bounds compare Hamiltonian dynamics with critical points of smooth functions. Degenerate fixed points are central to the unrestricted formulation tested here. The pinned manuscript supplies the research context.

Setting

The space is the complex projective quadric threefold, represented through its unit quadric and quotient tangent directions. Hamiltonian maps are endpoints of the specified smooth isotopies.

Formalization target

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

$$\#\mathrm{Fix}(\varphi)=3<4\leq\mathrm{Crit}(Q^3).$$

The theorem states that the complex projective quadric Q = {[z] ∈ ℂP⁴ : ∑ⱼ₌₀⁴ zⱼ² = 0} admits a Hamiltonian bijection φ with exactly three fixed points, whereas every smooth real-valued function on Q has at least four critical points, including functions with degenerate critical points; equivalently, 3 < 4 ≤ the infimum of their critical-set cardinalities, with infinite cardinalities recorded as ∞. Here Hamiltonian means that φ is the endpoint of an isotopy starting at the identity whose forward maps, inverse maps, and Hamiltonian have globally smooth extensions on ℝ × ℂ⁵. For times in [0,1], the maps preserve the unit quadric, are inverse there, and commute with multiplication by unit complex scalars; the Hamiltonian is invariant under these scalars. They satisfy ω(∂ₜFₜ(z),v) = dHₜ(Fₜ(z))[v] for every horizontal v at Fₜ(z), where ω(u,v) = 2 Im ∑ⱼ conjugate(uⱼ)vⱼ and horizontality at z means both ∑ⱼ conjugate(zⱼ)vⱼ = 0 and ∑ⱼ zⱼvⱼ = 0. Smooth functions on Q are those with smooth local extensions after pullback to the unit quadric, and criticality means that every such extension has zero derivative in all horizontal directions. Moreover, φ has a degenerate fixed point: some unit representative z and nonzero horizontal vector v admit a smooth local lift G of φ with G(z) = z and DG(z)v − v = a iz for some real a. Thus the induced derivative on the quotient tangent has a genuine nonzero eigenvector with eigenvalue 1.

Significance and status

The goal includes the lower bound on all smooth critical sets and at least one degenerate fixed point. A rational cup-length computation is not a separate conclusion 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

Counting fixed points is insufficient: the construction must satisfy the Hamiltonian lift conditions and give a genuine nonzero quotient-tangent eigenvector at a degenerate point.

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, Three fixed points on the symplectic quadric threefold, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

Negative curvature suggests strong analytic control, but bounded holomorphic coordinates impose a different global condition. The target constructs a complex threefold separating them. The pinned manuscript supplies the research context.

Setting

The construction uses the encoded Hartogs domain and a complete Kähler metric with sectional curvature between two negative constants. Holomorphic coordinate obstructions are stated in the published main proposition.

Formalization target

The selected goal is OAI.PinchedHartogs.main_theorem. Its central assertion is

$$-C\leq K_g\leq-c<0.$$

The theorem states that there exist a subset M of ℂ³ (realized as ℂ² × ℂ) and a matrix-valued function g assigning a 3×3 complex matrix to each point, together with real numbers A and B, such that M is open, nonempty and contractible, and g is a Kähler metric on M, meaning g is C^∞ on M, Hermitian at each point (g_ij = conj(g_ji)), positive definite (the Hermitian form of g at u has positive real part for every nonzero u), and satisfies the closedness condition ∂g_kj/∂z_i = ∂g_ij/∂z_k, with ∂ the Wirtinger derivative (1/2)(∂_x − i∂_y). Moreover the metric is geodesically complete on M: for every point p in M and every vector v there is a C^∞ curve γ: ℝ → M with γ(0)=p, γ'(0)=v that satisfies the geodesic equation γ''k + Σ Γ^k{ac} γ'_a γ'_c = 0 for all t, where the Christoffel symbols are built from the inverse of g and the ∂ derivatives of g. The metric is also negatively pinched: 0 < A ≤ B and, for every point of M and every real-linearly independent pair u, v, the sectional curvature, computed from the explicit curvature tensor formula in the source, lies between −B and −A. In addition, M has no bounded coordinates: there is no map F from ℂ³ to ℂ³, holomorphic on a neighbourhood of every point of M and bounded in every component on M, whose complex Jacobian determinant is nonzero at every point of M. Finally, M is not biholomorphic to a bounded domain, that is, there is no bounded open set N with holomorphic maps F on M and G on N, each analytic near the respective set, mapping M into N and N into M, which are mutually inverse.

Significance and status

The selected main theorem requires a nonempty open contractible domain, a geodesically complete Kähler metric with two-sided negative real-sectional pinching, no bounded holomorphic map to complex three-space with everywhere-nonsingular differential, and no biholomorphism to a bounded domain. The controlled potential and metric-transfer statements are attached as supporting milestones. 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

Metric completeness and two-sided negative curvature must coexist with a global obstruction to bounded holomorphic coordinates.

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.PinchedHartogs.controlled_potential (Open).
• OAI.PinchedHartogs.metric_transfer (Open).

Selected references

• OpenAI, A negatively pinched Kähler threefold without bounded holomorphic coordinates, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

Homogeneous minimizers model possible free-boundary singularities. A nonflat example in seven dimensions supplies one side of the claimed critical-dimension threshold. The pinned manuscript supplies the research context.

Setting

The one-phase Bernoulli energy on a ball is the integral of squared weak gradient plus the indicator of positivity. Competitors are nonnegative Sobolev functions with the prescribed H1-zero-boundary difference.

Formalization target

The selected goal is OAI.Bernoulli.nonflat_in_seven. Its central assertion is

$$\exists u:\mathbb R^7\to\mathbb R,\quad u(rx)=ru(x)\ (r>0,\ \text{a.e. }x),\quad u\text{ minimizes }E,\quad u\text{ is not flat}.$$

The theorem states that there exists a function u: ℝ⁷ → ℝ that is nonnegative almost everywhere, belongs locally to H¹, and is a global minimizer of the one-phase Bernoulli energy E_B(u) = ∫B (|∇u|² + 1{u>0}) dx. Here ∇u is a distributional gradient, and global minimality means that, for every open ball B of positive radius and every nonnegative almost-everywhere Sobolev competitor v ∈ H¹(B) with v − u ∈ H¹₀(B), one has E_B(u) ≤ E_B(v). Membership in H¹₀(B) requires approximation by smooth functions compactly supported in B, with both the functions and their gradients converging in L². The function is nonzero in the sense that it is not equal to zero almost everywhere, and it is homogeneous of degree one: for each real r > 0, u(rx) = r u(x) for almost every x. Nevertheless, it is not flat: there is no unit vector e ∈ ℝ⁷ for which u(x) = max(⟨x,e⟩, 0) almost everywhere. All almost-everywhere statements and integrals use Lebesgue measure.

Significance and status

The selected goal is existence of a nonzero nonflat one-homogeneous global minimizer in dimension seven. Flatness in dimensions at most six and singular-set dimension bounds are not attached conclusions. 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 stationary cone is insufficient: the example must minimize against all admissible ball competitors and fail every half-space profile.

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 critical dimension for one-phase Bernoulli minimizers, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

An optimal coupling can exist even when no deterministic transport maps attain its cost. The target separates attainment from equality of infima for a three-marginal repulsive cost. The pinned manuscript supplies the research context.

Setting

All three marginals are the same smooth compactly supported probability density in real three-space, with smooth compactly supported square root. Coincident points have infinite Coulomb cost.

Formalization target

The selected goal is OAI.Problem356.coulomb_counterexample_and_equal_infima. Its central assertion is

$$\inf_{T_2,T_3}\int c(x,T_2x,T_3x)\,d\mu=\min_{\pi\in\Pi(\mu,\mu,\mu)}\int c\,d\pi.$$

The theorem states, without a proof being verified here, that there exists a function ρ on three-dimensional Euclidean space ℝ³ satisfying a full Coulomb conclusion. This means ρ is a nonnegative C^∞ function with compact support, whose square root is also C^∞ with compact support, and with integral 1 over ℝ³; its density measure μ (Lebesgue measure weighted by ρ) is a probability measure. Consider three-marginal couplings of μ, namely probability measures on triples (x,y,z) of points of ℝ³ all of whose three coordinate marginals equal μ, with cost 1/|x−y| + 1/|x−z| + 1/|y−z| valued in [0,∞] (the inverse of distance zero is ∞). The Kantorovich value of μ is the infimum of the expected cost over all such couplings, and the theorem asserts it is finite and attained by some coupling. Further, no pair of measurable maps T₂,T₃ each preserving μ (pushing μ forward to itself) is a Monge optimizer: for every such pair, the expected cost of the triple (x,T₂x,T₃x) under μ is strictly larger than the Kantorovich value. Nevertheless, the Monge value, the infimum of this graph cost over all such pairs of μ-preserving maps, equals the Kantorovich value, and for every ε>0 there are μ-preserving maps T₂,T₃ with finite graph cost at most the Kantorovich value plus ε.

Significance and status

The goal includes a finite attained Kantorovich value, no Monge minimizer, equal infima and arbitrarily accurate finite-cost maps. Other dimensions and Riesz exponents are not part of this selected 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

Every measure-preserving pair of maps must be strictly suboptimal, while a sequence of such pairs still approaches the coupling minimum.

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 the Monge ansatz for the three-marginal Coulomb cost, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

Incompressible transport can implement prescribed geometric operations on coding sheets. The selected statement concerns one such finite transport construction with effective smooth forcing. The pinned manuscript supplies the research context.

Setting

Source and target rectangles have rational data and specified positive diagonal ratios. In the formula, D_i(y)=q_i+diag(r_i)(y−p_i), with source and target centers p_i and q_i. Space is represented periodically with period ten, and the viscosity is a positive computable real.

Formalization target

The selected goal is OAI.Solenoidal.sheet_theorem. Its central assertion is

$$X(1,\mathrm{sheet}(y))=\mathrm{sheet}(D_i y)\pmod{(10\mathbb Z)^3}.$$

The theorem states that, for any natural number N, any sheet datum D of size N, and any computable real viscosity ν>0, there exist a forcing field f and a velocity field u (each a time-dependent vector field on ℝ³) and a flow map X such that the following hold. Here D consists of N source rectangles and N target rectangles with rational corners, all inside the square [2,3]², with the sources pairwise separated by a positive distance and likewise the targets, together with positive rational ratios in each of two coordinates such that the diagonal affine map from source i to target i, which sends the source center to the target center and scales offsets by the ratios, maps the source rectangle exactly onto the target rectangle. Both f and u are periodic in space with period 10 in every coordinate and are C^∞ in space and time jointly. The forcing f is effective, meaning that all its mixed space-time partial derivatives can be approximated to any rational accuracy by a single fixed partial recursive procedure from computable names of the evaluation point. Moreover f has zero mean over the fundamental cell [0,10)³ at every time, is divergence free, and is 1-periodic in time. The field u is a classical solution on t≥0 of the forced Navier–Stokes equations ∂ₜu + (u·∇)u = −∇p + ν Δu + f with zero pressure, zero initial data, incompressibility and spatial periodicity, so u is a solution driven by f without pressure. Any classical solution v with pressure p for the same f and ν and with zero initial velocity coincides with u, and has p identically zero, for all t≥0. The flow map X satisfies X(0,a)=a and solves the particle-path equation dX/dt=u(t,X) for t≥0, and for each i and each point y of the i-th source rectangle, the time-1 flow image of the sheet point (y₀,y₁,2) agrees modulo the torus ℝ³/(10ℤ)³ with the sheet point at the diagonal-map image of y. Further, u vanishes in a neighborhood of every integer time, the advection term (u·∇)u vanishes everywhere, and both f and u have all their mixed space-time derivatives uniformly bounded by rational bounds computable from the derivative multi-index by a fixed partial recursive procedure. Finally, if N=0 then f and u are identically zero.

Significance and status

The target is the sheet theorem, including its encoded uniqueness statement and zero-advection conditions. Machine-halting detection is not a conclusion of this published goal. 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 simultaneously enforce smoothness, incompressibility, temporal periodicity, effective bounds and exact transport on every point of each sheet rectangle.

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, Geometric Programs for Solenoidal Forcing, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

A force whose derivatives decay rapidly can still encode a computation in a particle trajectory. The selected construction makes the observer condition and effectiveness requirements precise. The pinned manuscript supplies the research context.

Setting

For each finite deterministic machine and valid input, compilers produce smooth force and velocity fields on nonnegative time and real three-space, with common compact spatial support.

Formalization target

The selected goal is OAI.AlternatingNS.alternating. Its central assertion is

$$\exists t\geq0:\ X_1(t)>0\quad\Longleftrightarrow\quad M\text{ halts on }w.$$

The theorem states that for every positive real viscosity ν computable by rational approximations with error at most 2⁻ⁿ, there exist computable compilers for a force f and velocity U, and one compact set K⊂ℝ³, with the following property for every well-formed finite deterministic Turing machine M and valid finite input w. The compiled programs describe smooth fields f,U on [0,∞)×ℝ³, both spatially supported in K for all nonnegative times, such that every mixed space-time derivative D satisfies sup_{t≥0,x}(1+t+‖x‖)ᴶ‖Df(t,x)‖<∞ and the analogous bound for U, for every nonnegative integer J. Each program supplies rational approximations to all mixed derivatives at rational space-time points with requested error 2⁻ᵏ, effective moduli of continuity on bounded regions, and integer bounds for all these weighted derivative norms. The velocity starts from zero, is divergence-free, and solves the classical forced Navier–Stokes equation ∂ₜU+(U·∇)U=νΔU+f with identically zero pressure; specifically f=∂ₜU+(U·∇)U−νΔU. On every interval [0,T], U is continuous in H² and continuously differentiable in L², and U and its spatial derivative are uniformly bounded in space and time. Moreover, any classical solution (v,p) with the same force and zero initial velocity equals (U,0) pointwise for all nonnegative times, provided on every [0,T] it has v continuous in H², continuously differentiable in L², and uniformly bounded, and p continuous in H¹. Here these Sobolev continuity conditions mean continuous L² representatives of every spatial derivative through the indicated order; time derivatives at zero are taken within [0,∞). Every initial point a has a unique trajectory X(a,t) for t≥0 satisfying X(a,0)=a and ∂ₜX(a,t)=U(t,X(a,t)). Finally, the trajectory starting at (−1,0,0) has strictly positive first coordinate at some nonnegative time if and only if M halts on w, where encountering a missing instruction also counts as halting.

Significance and status

The goal is the alternating-coordinate construction at every positive computable viscosity. It includes Sobolev time regularity, effective bounds, zero initial velocity and the exact observer condition, rather than all three manuscript constructions. 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 encoding must preserve all weighted derivative bounds and uniqueness in the stated comparison class while recording arbitrarily long computations.

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, Computation under Rapidly Vanishing Navier–Stokes Forcing, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

Volume-preserving box transport supplies geometric operations for a finite computation. The selected goal assembles these into a force and a fixed particle observer. The pinned manuscript supplies the research context.

Setting

A finite machine and input determine effective velocity and force coefficients. The force depends affinely on positive viscosity, and after time one the velocity is periodic and depends only on the machine.

Formalization target

The selected goal is OAI.BalancedTransport.balanced_three_stack_realization. Its central assertion is

$$\exists t\geq0:\ X(t,(4,0,0))\in(-1,2)^3\quad\Longleftrightarrow\quad M\text{ halts on }w.$$

The theorem states that there exist velocity fields U(M,w), force coefficients f₀(M,w) and f₁(M,w), material flows X(M,w), and a globally 1-periodic velocity field R(M) for each finite deterministic tape machine M, with the following properties for every finite input word w. On nonnegative time and ℝ³, U, f₀ and f₁ are smooth and vanish outside a common spatial compact set independent of time; every mixed space-time derivative of U is uniformly bounded. Moreover, f₀ = ∂ₜU + (U·∇)U and f₁ = −ΔU. All three families are uniformly effective from the encoded machine and input: algorithms approximate every mixed derivative component at rational space-time points within 2⁻ⁿ, provide global integer bounds on these derivatives, and provide integer support radii. The velocity is 1-periodic after time 1 and satisfies U(M,w)(t,x) = R(M)(t,x) for every t ≥ 1, so its later field depends only on M. The flow satisfies X(0,a) = a and ∂ₜX(t,a) = U(t,X(t,a)); its trajectory starting at (4,0,0) enters (−1,2)³ at some nonnegative time exactly when M halts on w, meaning that a configuration with no next transition is reached after finitely many machine steps. For every viscosity ν > 0, the force f = f₀ + νf₁ is smooth, has uniformly bounded mixed derivatives, and is 1-periodic after time 1; U with pressure zero solves the incompressible Navier–Stokes equation ∂ₜU + (U·∇)U = νΔU + f with U(0,·) = 0. This velocity is unique among smooth zero-data solutions in the comparison class, and every such solution has spatially constant pressure. The comparison class requires the velocity and all spatial derivatives through order two to be continuous in time as L² functions, the velocity to be continuously differentiable in time in L², velocity and first spatial derivatives to be bounded on each finite time slab, and pressure, after subtracting a time-dependent scalar, together with its first spatial derivatives to be continuous in time in L²; (U,0) belongs to this class. Finally, derivative approximations and global derivative bounds for f are computable when ν is computable, and computable relative to any rational name of ν whose nth approximation has error at most 2⁻ⁿ.

Significance and status

The balanced three-stack realization is the main goal; balanced box routing is a separate supporting reference. The exact conclusion permits spatially constant pressure in competing solutions and explicitly states its comparison class. 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

Uniform effectiveness, compact support, periodic behavior and uniqueness must all coexist with exact halting detection.

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.BoxTransport.Routing.balanced_box_routing (Open).

Selected references

• OpenAI, Incompressible Box Transport and Finite Computation, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Matrix multiplication and arithmetic cost

Multiplying matrices is a basic operation whose asymptotic cost is measured by the number of scalar arithmetic operations needed as the matrix dimensions increase. The familiar entry-by-entry algorithm has cubic cost. The question addressed here is how small an exponent can describe exact multiplication of square matrices when algorithms may use more elaborate finite computations. OpenAI's October 2, 2026 paper establishes the bound $9/4$ for matrices over the complex numbers. Its Theorem 1.1 concerns asymptotic arithmetic complexity, with arbitrarily small positive slack in the exponent.

Finite programs and admissible exponents

An arithmetic program is a finite sequence of register computations. A step can load a field constant, read an input entry, or add, subtract, or multiply two values from preceding registers. Constant loads and input reads have zero cost. Each addition, subtraction, and multiplication has cost one. There is no division operation in this program model. Outputs are selected registers, and a program is correct only when these outputs equal the matrix product for every pair of input matrices.

For a field $F$, a real number $\tau$ is an admissible exponent if, for every real $\varepsilon>0$, there exists a real constant $C>0$ such that every integer size $n\geq1$ admits a correct program with cost at most $C n^{\tau+\varepsilon}$. The constant must work uniformly for all sizes and all input entries. The chosen program may depend on $n$ and $\varepsilon$. The definition does not charge for a separate procedure that constructs these programs. The arithmetic matrix multiplication exponent $\omega_F$ is the real infimum of the set of admissible exponents.

Formalization target

The goal is exactly the complex-field exponent conclusion of OpenAI's Theorem 1.1:

$$\omega_{\mathbb C}\leq\frac94.$$

In the Lean source, the quantity on the left is OAI.MatrixMultiplication.Arithmetic.omega ℂ. The bound on the right is the exact real rational (9 : ℝ) / 4, equal to $2.25$. The inequality is non-strict. The theorem does not assert a strict inequality below $9/4$, and it is not quantified over arbitrary fields.

The paper also states the corresponding algorithmic conclusion with every positive exponent slack. The goal here retains the exact infimum formulation used by its released comparator challenge. In particular, the bound should not be read as asserting that one fixed family has cost $C n^{9/4}$ without any slack, or that an algorithm is efficient at a specified finite matrix size.

What the formal result provides

The result places $9/4$ above the asymptotic arithmetic exponent in a model with explicitly defined programs, outputs, correctness, and operation counts. It gives a statement that other formal developments can use without leaving those conventions implicit. The dependence on the complex field is part of that statement, so results using another field or another computational model require their own justified connection.

This is a port and verification of an existing proof, not a claim that the source theorem remains unproved. The released Lean development contains the proof entry point. Keeping the original definitions and conclusion allows compatibility changes to be reviewed independently of the mathematical claim.

Why the supporting development matters

An asymptotic exponent bound requires one uniform cost constant for every positive matrix size, while correctness quantifies over all pairs of matrices at each size. A computation for selected dimensions or selected inputs cannot satisfy those requirements. Arguments about tensors must also support the stated arithmetic program cost, including the operations needed for the relevant linear combinations. The infimum formulation makes its defining set and the interpretation of its bounds part of the supporting mathematics, rather than assumptions to insert into the target theorem.

Formalization scope and conventions

The environment is Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Matrices are functions on finite index sets. Program evaluation and output selection give exact field values. The main theorem fixes the field to $\mathbb C$, excludes size zero from admissibility, and uses real powers for its cost estimates. Constants may be arbitrary complex numbers; no bit-cost interpretation is asserted.

The definition item preserves the original source block, including its rectangular matrix multiplication definitions and complex dual exponent. Those additional definitions support the shared source development but are not additional mission goals. A complete proof must establish the displayed bound without an admitted lemma, a new axiom, or an assumption equivalent to that bound. Reusable components include the arithmetic program model, finite tensor constructions, asymptotic bounds, and the bridge from tensor rank to arithmetic operations.

Selected references

• OpenAI, An Upper Bound of 9/4 for the Matrix Multiplication Exponent, preprint, October 2, 2026. Paper, Theorem 1.1.
• OpenAI, MatrixMultiplication comparator challenge and Lean development, 2026, source revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Exact challenge statement.