Three fixed points on the symplectic quadric threefoldOpen Problem
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.
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.
The cotype–cotype conjecture under the approximation propertyOpen Problem
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.
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.
Lipschitz Equivalent Separable Banach Spaces Need Not Be Linearly IsomorphicOpen Problem
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 ℓ².
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.
A torsion-free hyperbolic group that is not residually finiteOpen Problem
Motivation
Residual finiteness means that finite quotients can distinguish every nonidentity group element. The source asks whether coarse negative curvature forces this separation property even without torsion. The source is OpenAI's September 2026 manuscript.
Setting
A torsion-free group has no nonidentity element whose positive power is the identity. A word-hyperbolic group admits a finite generating set whose Cayley graph has geodesic triangles of uniformly bounded thickness.
Formalization targets
∃G:G torsion-free and word-hyperbolic,¬ResiduallyFinite(G).
The theorem states, without a verified proof (it is admitted), that there exists a group G, in the lowest universe Type, that is torsion-free, word-hyperbolic, and not residually finite. Torsion-free means that for every g in G and every positive integer n, g^n = 1 implies g = 1, so no nonidentity element has finite order (this does not assert unique roots). Word-hyperbolic means that there is a finite subset S of G whose unit-edge Cayley graph (the simple graph with the multiplicative Cayley adjacency determined by S) is connected, which says that S generates G, and a natural number δ such that geodesic triangles are uniformly δ-thin. Precisely, for all vertices x, y, z and walks p from x to y, q from y to z and r from z to x, each of which is a geodesic (its length equals the graph distance between its endpoints), every vertex of each side lies within graph distance δ of some vertex on one of the other two sides. The statement also requires that G fail the Mathlib property Group.ResiduallyFinite.
The goal puts a geometric condition and failure of finite-quotient separation into one existential statement. Torsion-freeness is retained explicitly. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Difficulty
Hyperbolicity concerns large-scale word geometry, whereas residual finiteness quantifies over every finite quotient. Checking a finite list of quotients cannot establish the required failure.
Formalization scope
Hyperbolicity is encoded by vertexwise thin triangles in a connected unit-edge Cayley graph for some finite generating set. Torsion-freeness is the positive-power condition and does not mean a unique-roots property. Residual finiteness uses the Mathlib definition.
The shared definitions are supplied by TorsionFreeHyperbolic. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Selected references
OpenAI, A torsion-free hyperbolic group that is not residually finite, preprint, September 2026. Manuscript.
Single-fold Diophantine representationsOpen Problem
Motivation
A Diophantine representation translates membership in a computably enumerable set into solvability of one polynomial equation. The source asks whether the entire auxiliary witness can always be made unique. The source is OpenAI's September 2026 manuscript.
Setting
A single-fold representation uses an integer polynomial evaluated at natural-number inputs and witnesses. An input belongs to the represented set exactly when a witness makes the polynomial zero, and any two complete witnesses at the same input must coincide.
Formalization targets
a∈S⟺∃w∈Nm:P(a,w)=0,P(a,w)=P(a,v)=0⟹w=v.
The proposition MainStatement holds, which asserts a single-fold Diophantine representation result with positive lengths. For every n ≥ 1 and every set S of n-tuples of natural numbers that is recursively enumerable (the predicate a ∈ S is REPred, i.e. semi-decidable), there exist m ≥ 1 and an integer polynomial P in the n input variables and m witness variables such that P represents S. Here evaluation takes natural-number inputs a and witnesses w, casts them to integers, and evaluates P over ℤ. Representation means that for every input a, first, a lies in S exactly when some witness w ∈ ℕ^m satisfies P(a,w)=0, and second, any two witnesses w and v with P(a,w)=0 and P(a,v)=0 are equal. So there is exactly one witness for members of S and none for nonmembers, and the uniqueness condition is imposed on every input a, with all witness coordinates included in w.
The target strengthens mere existential representation by enforcing uniqueness across every auxiliary coordinate. It covers all recursively enumerable sets of positive-length natural tuples. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Difficulty
Encoding a computation with extra witnesses can introduce many choices that do not affect the represented input. Every such auxiliary choice must be controlled, rather than leaving hidden coordinates outside the uniqueness assertion.
Formalization scope
The input length and witness length are positive naturals. REPred expresses recursive enumerability. Polynomial coefficients and evaluation are integral, while variables range over naturals cast into the integers. The goal is existential and does not require one fixed universal polynomial.
The shared definitions are supplied by SingleFold. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Selected references
OpenAI, Single-fold Diophantine representations, preprint, September 2026. Manuscript.
Signed tensor densities and diagram budgets for the Thorp shuffleOpen Problem
Motivation
Signed tensor components separate different sources of permutation symmetry. The source uses their diagram entropies to budget high moments of the Thorp sweep. The source is OpenAI's September 2026 manuscript.
Setting
A signed occurrence is an injective equivariant map from a tensor product of three Specht modules into the target module, with the second factor transposed. The weighted moment is the target dimension times the trace of a power of the sweep’s positive square.
Formalization targets
log(dimSλRetr(Q∗Q)r)≤a(η,d)H(α,β)+R(κ,d,ℓ).
There is a constant η₀>0 such that for every η with 0<η<η₀ there is a κ₀ with 0<κ₀<η/256 such that for every κ with 0<κ<κ₀ there is a positive integer power r, depending only on η and κ, with the following property for every d≥1. Let λ be a partition of 2^d (a Young diagram with 2^d cells), and let u+v+l=2^d with partitions α of u, β of v and γ of l, such that the signed occurrence condition holds: there is an injective complex-linear map from the tensor product of the Specht modules S^α ⊗ S^(β′) ⊗ S^γ, where β′ is the transpose of β, into S^λ that commutes with the action of S_u×S_v×S_l, embedded in S_(2^d) as block permutations on the consecutive blocks of sizes u, v and l. Here Specht modules are the cyclic submodules of the regular representation of the symmetric group generated by the polytabloid built from the row and column subgroups of a fixed tableau. Identify {0,…,2^d−1} with binary strings of length d, and for each coordinate i let the layer operator be the average of S^λ over the subgroup of permutations preserving every binary coordinate except the i-th. Let the sweep operator be the product of these d layer operators in reverse coordinate order, and let the sweep square be TT with T the sweep operator. Define the weighted moment as dim S^λ times the real part of tr((TT)^r). Then the logarithm of this moment, taken as −∞ when the moment is zero, is at most coefficient(η,d)·H(α,β) + remainderBudget(κ,d,l). Here coefficient(a,d)=a(1−1/(2√d)), the signed entropy H(α,β) is the sum, over all row lengths a of α and of β, of a·log((u+v)/a), and the remainder budget is 0 if l=0 and otherwise max(0, coefficient(κ,d)·l·log(2^d) − l·log(2^d/l)).
The target makes the moment power depend only on two small budget parameters, uniformly over cube dimension and every signed occurrence. Supporting targets include the type-angle estimate and a shared mixing bundle. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Difficulty
Ignoring the signed occurrence hypothesis loses the representation-theoretic connection between the component diagrams and the target. The remainder diagram must be charged separately, including its empty case.
Formalization scope
The quantifier order is η0, then each small η, then κ0<η/256, then each small κ, then one positive integer r. Zero moments have logarithm minus infinity in EReal. Independent source groups stay separate references.
The shared definitions are supplied by SignedSweepMoment, SpinAngle, ThorpRemaining. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Selected references
OpenAI, Signed tensor densities and diagram budgets for the Thorp shuffle, preprint, September 2026. Manuscript.
Compatibility entropy and the spectrum of a Thorp sweepOpen Problem
Motivation
Compatibility of independently chosen row and column permutations controls how two families of local symmetries overlap. The source connects a weighted compatibility estimate to Thorp spectral bounds. The source is OpenAI's September 2026 manuscript.
Setting
A row system chooses a permutation in each row of an A by D array; a column system chooses a permutation in each column. They are compatible when their combined routing remains injective down each column. Nonnegative weights may bias each local permutation.
The proposition WeightedCompatibilityTheorem holds. Here, for natural numbers A and D, Rows assigns to each i in Fin A a permutation of Fin D, and Cols assigns to each j in Fin D a permutation of Fin A; a pair (r,c) is Compatible if for every column j the map i ↦ c(r_i(j))(i) is injective. The weightedCompatibility of real weight families w (indexed by i and a permutation of Fin D) and v (indexed by k and a permutation of Fin A) is (AD)! / ((D!)^A (A!)^D) times the uniform mean, over all pairs (r,c), of the indicator of compatibility times ∏_i w_i(r_i) ∏_k v_k(c_k). The marginalFactor for θ and a weight function u is the θ-th power of the uniform mean of u^(1/θ). The stated claim is that there exist reals L, C₀, m₀ > 0 such that for all natural numbers A and D, with n = AD, m = √n and θ = 1 − L/log m, whenever m ≥ m₀, θ > 0, and both A and D lie between m/2 and 2m, then for all nonnegative weight families w and v, weightedCompatibility(A,D,w,v) ≤ exp(C₀ n^(54/100)) · ∏_i marginalFactor(θ, w_i) · ∏_k marginalFactor(θ, v_k).
The formal goal is an entropy-type inequality for arbitrary nonnegative local weights in sufficiently large balanced rectangles. It supplies a concrete combinatorial estimate that can support spectral analysis. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Difficulty
The compatibility indicator couples all row and column choices. A product of separate marginal expectations loses the injectivity constraint and cannot directly recover the stated exponent.
Formalization scope
The rectangle satisfies n=AD, with both side lengths between n/2 and 2n. The theorem existentially chooses positive L,C0,m0 and assumes positive θ. The marginal factor is the θth power of the uniform mean of the weight to power 1/θ.
The shared definitions are supplied by ThorpRemaining, ThorpWeightedCompatibility. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Selected references
OpenAI, Compatibility entropy and the spectrum of a Thorp sweep, preprint, September 2026. Manuscript.
Polynomial vacuum representations and bridge mass for honeycomb walksOpen Problem
Motivation
Critical self-avoiding walks have weights balanced between exponential path growth and decay. The source studies bridge-length scaling; the available target establishes summability of the bridge sums used to define these quantities. The source is OpenAI's September 2026 manuscript.
Setting
A honeycomb bridge is a self-avoiding vertex list crossing a strip from a fixed initial port to any terminal port on the opposite layer. A path with L vertices has critical weight λL, with λ=(2cos(π/8))−1.
Formalization targets
γ∑w(γ)<∞,γ∑L(γ)w(γ)<∞(h≥1),
For every integer h ≥ 1, six families of sums over self-avoiding bridge paths in a honeycomb strip are absolutely summable. Vertices of the honeycomb lattice are of two kinds, up(i,j) and down(i,j) with integer i and j, and the layer of a vertex is its second index j; an up vertex (i,j) is adjacent to the down vertices (i,j−1), (i,j) and (i−1,j), and adjacency is symmetric. A bridge path of height h is a list of distinct vertices, consecutive ones adjacent, starting at up(0,0), ending at some down(i,h−1), with every vertex in layers 0 through h−1. Its weight is λ^L, where L is the number of vertices and λ = 1/(2cos(π/8)) is the critical activity, and its first-length weight is L·λ^L. Let bridgeMass(h) be the total weight of all bridge paths. A path is confined if every vertex has horizontal coordinate (i + j/2 for up vertices, i + j/2 + 1/2 for down vertices) of absolute value at most h(log h)², and confinedMass(h) is the total weight of confined paths. The theorem asserts summability over all bridge paths of the weight, of the first-length weight, and of the first-length weight divided by bridgeMass(h), and summability over confined paths of the weight, of the first-length weight, and of the first-length weight divided by confinedMass(h). The proof is admitted in the source, not established here.
The full formal statement gives six summability assertions, including normalized first-length weights and their corridor-confined counterparts. These are prerequisites for interpreting bridge masses and mean lengths. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Difficulty
Each strip has unbounded horizontal extent and admits paths of arbitrarily large length. Finite strip height therefore does not by itself make the path family finite.
Formalization scope
The length convention counts vertices. Confinement means horizontal coordinate bounded by h(logh)2. The target proves summability, without asserting the manuscript’s h4/3+o(1) asymptotic law. Normalized terms use the masses defined by tsum.
The shared definitions are supplied by HoneycombBridgeFiniteness. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Selected references
OpenAI, Polynomial vacuum representations and bridge mass for honeycomb walks, preprint, September 2026. Manuscript.
Integral and fractional expectation thresholds are equivalentOpen Problem
Motivation
An increasing property of a random set can be certified by small subsets. Fractional certificates allow weight to be spread across many subsets, so comparing them with ordinary certificates measures the cost of removing this relaxation. The source is OpenAI's September 2026 manuscript.
Setting
A cover is a family of generators such that every member of the increasing family contains a generator. A generator of size s costs ps. An ordinary cover and a fractional cover both have budget 1/2; a fractional cover assigns weights in [0,1] and supplies total weight at least one inside each member. The expectation thresholdsq and qf are suprema of feasible parameters in [0,1].
Formalization targets
qf(F)≤25⋅5124q(F).
For a finite nonempty ground type α and a family F of subsets of α that is nonempty, is not the entire power set, and is increasing (any superset of a member of F is again in F), the fractional threshold qf(F) is at most 25·512⁴ times the integral threshold q(F). Here q(F) is the supremum of those p in [0,1] for which F is small: some family G of sets covers F, meaning every H in F contains a member of G, with total cost Σ_{S∈G} p^{|S|} at most 1/2. The fractional threshold qf(F) is the analogous supremum of p in [0,1] for which there is a weight function g from subsets of α to [0,1] such that every H in F has Σ_{S⊆H} g(S) ≥ 1 and the fractional cost Σ_S g(S)·p^{|S|} is at most 1/2.
The comparison gives a dimension-independent bound with the same budget on both sides. It isolates certificate rounding from the separate question of locating the random-set threshold. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Difficulty
Replacing fractional weights independently can lose control of covering every member simultaneously. The constant must be independent of both ground-set size and the sizes of weighted sets.
Formalization scope
The ground type is finite and nonempty, and the family is nonempty, proper, and increasing. Costs are finite real sums and thresholds are real suprema. The exact constant in the published goal is retained; the objective is this inequality, not an unspecified equivalent comparison.
The shared definitions are supplied by TalagrandExpectationThreshold. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Selected references
OpenAI, Integral and fractional expectation thresholds are equivalent, preprint, September 2026. Manuscript.
A proof of Seymour’s second-neighborhood conjectureOpen Problem
Motivation
An oriented graph may have very uneven outdegrees, yet the second-neighborhood conjecture asks for one vertex whose new two-step reach is at least its immediate outdegree. The source manuscript presents the surrounding research claim.
Setting
An oriented graph is a loopless asymmetric relation r on a finite nonempty vertex type. First neighbors satisfy r(v,w). Second neighbors are vertices w distinct from v, not already first neighbors, but reached by some directed path v→u→w.
Formalization target
Prove that some vertex v satisfies
∣N1+(v)∣≤∣N2+(v)∣.
Every second-neighborhood vertex is counted once, irrespective of how many two-step paths reach it.
The statement covers all finite oriented graphs, including disconnected graphs and graphs whose underlying undirected graph is not complete. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Difficulty
Counting length-two walks overcounts repeated endpoints and may include first neighbors. The conclusion concerns the set of vertices at directed distance exactly two.
Formalization scope
The formal relation need not be supplied with decidability; the finite sets are formed classically. Looplessness and asymmetry are explicit hypotheses, and the vertex type is finite and nonempty. GoodVertex is exactly the finite-cardinality comparison.
Selected references
OpenAI, A proof of Seymour’s second-neighborhood conjecture, preprint, 2026. Pinned manuscript.
A classification of finite Euclidean Ramsey configurationsOpen Problem
Motivation
Euclidean Ramsey theory asks which finite shapes must occur monochromatically in a sufficiently high dimension. The scale is fixed, so an algebraic criterion must capture exact distances rather than approximate similarity. The source manuscript presents the surrounding research claim.
Setting
A Ramsey configuration a=(aᵢ) has a monochromatic congruent copy under every finite coloring in some dimension depending on the number of colors. Let F be the rational field generated by all coordinates, B=F⊗ℚF, and pᵢ=(1,aᵢ) the augmented coordinate vectors. Multiplication m:B→F sends x⊗y to xy.
Formalization target
For an injective configuration of at least two points affinely spanning ℝᵈ with d≥1, prove
Ramsey(a)⟺FieldCriterion(a).
The criterion asks for a matrix P over B with (pᵢ⊗1)ᵀP(1⊗pᵢ)=0 for every i and m(P_{αβ})=δ_{αβ} on the coordinate-coordinate block.
The criterion is necessary and sufficient for the stated configurations. Available companion targets describe spherical necessity, positive classes and concrete non-Ramsey circle configurations. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Difficulty
Applying m to the tensor identity loses information because multiplication need not be injective. Equality in the tensor ring, and arbitrary colorings without measurability, are essential.
Formalization scope
The goal uses real Euclidean coordinates and the exact generated intermediate field over ℚ. Congruence preserves all pairwise distances at their original scale. All published companion references are retained as separate groups because they repeat Ramsey definitions. Milestones state their own hypotheses and do not identify every spherical set as Ramsey.
Selected references
OpenAI, A classification of finite Euclidean Ramsey configurations, preprint, 2026. Pinned manuscript.
Polynomial mixing of the switch chain for every graphical degree sequenceOpen Problem
Motivation
Sampling a graph with a prescribed degree vector requires moving among realizations without changing degrees. The switch chain performs local edge replacements and asks whether these suffice for rapid global mixing. The source manuscript presents the surrounding research claim.
Setting
States are simple undirected labeled graphs realizing a graphical vector d on n≥4 vertices. The lazy switch chain stays put with probability one half and otherwise proposes one ordered replacement between distinct perfect matchings on four vertices, rejecting invalid proposals.
Formalization target
Prove
τTV(1/4)≤2n8,
with mixing time zero for a singleton state space. When more than one state exists, prove the spectral-gap lower bound 1/(24n²·binom(n,4)).
The goal covers every graphical degree sequence under the stated degree bound, without regularity or density restrictions. Connectivity and explicit exponential total-variation decay are available supporting targets. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Difficulty
Connectivity gives eventual communication but no polynomial rate. The estimate must be uniform across degree vectors and initial graphs.
Formalization scope
The kernel is defined by exact counts of four-vertex proposals, and total variation is the finite half-ℓ₁ distance from uniform measure. The main theorem contains the singleton case explicitly. The manuscript’s exact sampler is not an additional published target here.
Selected references
OpenAI, Polynomial mixing of the switch chain for every graphical degree sequence, preprint, 2026. Pinned manuscript.
Slope-field perturbations of the two-cylinder coveringOpen Problem
Motivation
A slope-field perturbation of a two-cylinder cover trades a reduction in projected area against the extra overlap needed to maintain coverage. The slope-field manuscript studies when the net cost becomes strictly smaller. The companion radial-sweep manuscript establishes finite triangular approximation with arbitrary tagged equal subdivisions. Both manuscripts map to the same published Lean goal, so this draft covers their shared target. The source manuscript presents the surrounding research claim.
Setting
A cylinder is a measurable finite-area planar base plus a line in its perpendicular unit direction. Ruled sets vary the segment direction over compact planar labels. Radial sweeps use p₀+ρ(a+tb)+s(e+w(t)), with 0≤ρ≤R(t), |s|≤L, and w′(t)=λ(t)(a+tb).
Formalization target
Prove the seven-part fourPaperMain conjunction: the explicit angular-area construction; C¹ hyperbolic approximation; C¹ square-zero-derivative approximation; regular-tetrahedron counterexamples with parallelogram bases and with bounded open bases; aligned radial triangular approximation; and actual-sweep projection bounds. In particular, the tetrahedron clauses require
The selected published goal is a joint endpoint shared by four related manuscripts, and therefore includes more than the slope-field application alone. Its finite covers retain both cost inequalities. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Difficulty
A local area decrease cannot guarantee a global cover. All regularity, exact coverage and error bounds in the separate conjuncts must hold in their stated regimes.
Formalization scope
Hyperbolic and nilpotent clauses use their C¹ definitions; radial data require a nonempty parameter interval, positive segment half-length, continuous nonnegative cap and alignment derivative. All tagged equal subdivisions are covered. The radial clause requires triangular-base area to converge to weightedArea(D), while actual sweep projections have eventual cost at most weightedArea(D)+ε and the corresponding limsup bound. The separate RuledApproximation.fullMain is also retained as a related reference but is not mislabeled as one of these seven conjuncts.
Finite cylinder approximation of ruled setsOpen Problem
Motivation
A continuously varying family of line segments suggests a low-cost cylinder cover, but a finite approximation must control both gaps and accumulated base area. The source manuscript presents the surrounding research claim.
Setting
A ruled set consists of segments (s,p+sv(p)) with p in a compact planar label set D and |s|≤L. The basic weighted projection cost is ∫_D(1+|v(p)|²)^(-1/2)dp. The source also defines physical rescalings, square intercept tiles and singular slope fields.
Formalization target
Prove the published FullMain conjunction. Its central finite-approximation clause gives
i∑∣Bi∣≤∫D1+∣v(p)∣2dp+ε
for every ε>0 under its C¹ hyperbolicity hypotheses. The package additionally contains physical-rescaling, logarithmic, product-cell, orthogonal-grid, smooth nilpotent and singular-tetrahedron assertions.
The chosen goal supplies a package of finite-cover results with explicit regularity and base-shape requirements. The broad fourPaperMain reference also contains a C¹ nilpotent variant. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Difficulty
Freezing directions can create gaps and a persistent area loss. The final family must be finite and cover every point while the area error is arbitrarily small.
Formalization scope
FullMain uses Euclidean planes and three-space. Some clauses require null-measure boundary or C² regularity; its NilpotentStatement requires smoothness and a square-zero derivative. The singular clause includes its stated p,γ ranges and strict tetrahedron cost below √2/2. These are the selected published clauses; the manuscript’s latest C¹ formulation is not silently substituted for them. Independent definition groups remain separate references.
Finite angular cylinder covers below the half-area boundOpen Problem
Motivation
Cylinder covers measure coverage cost by perpendicular base area. For a regular tetrahedron, the familiar half-minimum-shadow threshold is tested by a finite family of tilted triangular cylinders. The source manuscript presents the surrounding research claim.
Setting
The reference tetrahedron K has coordinates (x,y,√2t) with 0≤t≤1, |x|≤1−t and |y|≤t. Let H=√2 and A_min be its least unit-direction projection area. A triangular cylinder has a compact nondegenerate triangle in the plane perpendicular to its unit axis.
Formalization target
Prove A_min=H and construct, for every sufficiently small ε>0, 2⌈2/ε²⌉ cylinders covering K with
H∑i∣Bi∣=21−600013ε2+O(ε4),i∑∣Bi∣<2Amin.
Also prove existence of a finite cover with Σᵢ|Bᵢ|/shadowArea(uᵢ)<1/2.
The asymptotic estimate retains its explicit quadratic coefficient and uniform fourth-order error. Both absolute area and directionwise normalized cost are formal conclusions. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Difficulty
Tilting may reduce projected area but leave uncovered gaps. The target requires exact finite coverage and valid triangular bases together with the strict cost saving.
Formalization scope
Base area is two-dimensional Euclidean Hausdorff measure converted to ℝ. MainAsymptotic has fixed positive δ,C before all small ε. The broad fourPaperMain is retained as a related published reference; the selected goal remains TriangularCovering.main. Repeated definitions in independent source groups are kept separate.
Tree Constructions for the l1 Distortion of Binary Edit DistanceOpen Problem
Motivation
Embedding edit distance into ℓ₁ would permit algorithms and geometric tools for that normed space. Distortion lower bounds quantify the loss any such representation must incur. The source manuscript presents the surrounding research claim.
Setting
Edit distance is the least number of unit insertions, deletions and substitutions, with unrestricted intermediate word lengths. For a finite equal-length binary set W, c₁(W) is the infimum over all injective maps into the full real sequence space ℓ₁ of the product of the two worst distance ratios.
Formalization target
Find an absolute c>0 and d₀ such that for every d≥d₀ there are 1≤n≤d and at least two binary words of length n with
The witness exists for every sufficiently large length cap. The target bounds distortion against every injective ℓ₁ embedding, not only a particular algorithm. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Difficulty
A bad map is not a lower bound for the infimum over all maps. The finite family must force distortion uniformly while preserving its common binary word length.
Formalization scope
The chosen target uses Word Bool n and Finset witnesses. A companion binary_torus formulation is retained as a reference to the same lower-bound endpoint. Its independent source group repeats edit-distance declarations and is not combined into one import. No companion upper embedding theorem is attached.
Selected references
OpenAI, Tree Constructions for the l1 Distortion of Binary Edit Distance, preprint, 2026. Pinned manuscript.
Sharp One-Third Stability of Brenier MapsResearch Paper
Motivation
Given a source probability measure ρ and a target μ on Rd, Brenier's theorem (Brenier 1991) says that when ρ is absolutely continuous there is a unique map Tμ pushing ρ to μ that minimizes the quadratic cost ∫∣x−T(x)∣2dρ, and that it is the gradient of a convex function. Fixing ρ, the assignment μ↦Tμ embeds the space of probability measures into L2(ρ); this linearization of optimal transport is used in statistics, data analysis and machine learning to compare measures by comparing their maps. Its usefulness depends on quantitative stability: how far apart can Tμ and Tν be when μ and ν are close in Wasserstein distance? For general targets the map cannot be Lipschitz in the target, and the question is which Hölder exponent holds uniformly.
This mission asks for a machine-checked proof that, for a uniform source on a convex body, the sharp uniform exponent is exactly 1/3, as claimed in an OpenAI preprint dated September 25, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal below is open.
Timeline
1991 — Brenier proves existence and uniqueness of quadratic optimal maps as gradients of convex potentials (CPAM 1991).
2011 — Gigli reports Ambrosio's local one-half Hölder estimate along target curves near regular data (Proc. Edinb. Math. Soc. 2011, Corollary 3.4).
2020–2021 — Berman obtains stability for varying sources against fixed targets (Found. Comput. Math. 2021); Mérigot, Delalande and Chazal derive target-uniform bounds, including a W12/15 estimate for a uniform convex source (AISTATS 2020).
2023 — Delalande and Mérigot prove an L2 map bound of order W11/6 for densities bounded above and below on convex domains, with a convex-gradient interpolation inequality (Duke 2023).
2024 — Letrouit and Mérigot extend potential stability to John domains (arXiv:2411.04908).
2025 — Divol, Niles-Weed and Pooladian obtain a W21/3 map estimate for nondegenerate finite targets, with constants depending on the number, masses and geometry of the atoms (IMRN 2025).
2026 — Letrouit proves that exponents above 1/3 fail for a nonconvex source and conjectures uniform square-root stability in W2 for uniform convex sources (C. R. Math. 2026, Theorem 2 and Conjecture 3).
September 2026 — The OpenAI preprint claims the uniform W21/3 bound for every uniform convex source and shows that no larger exponent holds, disproving the square-root conjecture (Theorem 1.1, p. 2; Proposition 2.2, p. 4).
Setting
Fix d≥2, a compact convex K⊂Rd with nonempty interior, and the uniform sourceρ=1Kdx/∣K∣. Fix a nonempty compact Y⊂Rd and let Prob(Y) be the Borel probability measures with μ(Rd∖Y)=0. A coupling of μ,ν is a probability measure on Rd×Rd with marginals μ,ν, and
W2(μ,ν)=(πinf∫∣y−z∣2dπ(y,z))1/2.
For μ∈Prob(Y), Tμ is the Brenier map: a measurable T with T#ρ=μ whose graph coupling (id,T)#ρ is the unique optimal coupling of ρ and μ. Distances between maps are measured in L2(ρ): ∥T−S∥L2(ρ)=(∫∣T−S∣2dρ)1/2.
Formalization targets
Milestone: Proposition 2.2 (p. 4) — the exponent cannot be improved
For every d≥2, with K=Y=[−1,1]d and every α>1/3,
μ=ν∈Prob(Y)supW2(μ,ν)α∥Tμ−Tν∥L2(ρ)=+∞,
and the supremum stays infinite when both targets have exactly three atoms. In Lean (one_third_exponent_is_sharp): for every α>1/3 and C>0 there are distinct three-atom probability measures on the cube with unique optimal maps T,T′ and CW2α<∥T−T′∥.
For every K, Y as above there is a finite constant C(K,Y) such that for all μ,ν∈Prob(Y) the Brenier maps exist, are unique, and
∥Tμ−Tν∥L2(ρ)≤C(K,Y)W2(μ,ν)1/3.
The targets may be atomic, singular or absolutely continuous; the constant does not depend on them. In Lean this is one_third_stability. Together the two statements determine the sharp exponent in this uniform class, which is the second sentence of Theorem 1.1.
Significance
The result itself. The upper bound improves every earlier target-uniform exponent (2/15, 1/6, 1/5, 1/4 in W1 or W2) to 1/3 in W2, with a constant independent of atom counts, atom masses, separations and density bounds. The lower bound disproves Letrouit's conjectured exponent 1/2 with only three atoms on a cube. The pair gives the exact uniform stability exponent of the linearized optimal-transport embedding for uniform convex sources.
Formalizing it. Mathlib has measures, couplings and Lebesgue integration but no optimal-transport theory. A formal development would supply Wasserstein distance, existence and uniqueness of Brenier maps for semi-discrete and general targets, and Lipschitz convex potentials, all reusable. The sharpness statement is the more elementary one and is a natural first milestone.
Difficulty
The standard route bounds the difference of convex potentials and then converts it to a gradient bound by an interpolation inequality; previous potential estimates lose a power, giving exponents below 1/3. The preprint's key step is a linearW2 bound on the L2(ρ) distance of potentials, obtained by moving the sites of finite targets along an optimal coupling with fixed masses and controlling the intercept velocity through a uniform moment inequality for the cells of a maximum of affine functions (Lemma 4.1, p. 9; Proposition 5.1, p. 12). The constant must stay uniform as cell masses or faces degenerate, which rules out any argument relying on a spectral gap of the cell graph Laplacian. The final passage from finite to arbitrary Borel targets needs stability of optimal maps under approximation (Proposition 6.3, p. 16).
Formalization scope
Space is EuclideanSpace ℝ (Fin d) with Borel measures. uniformMeasure K is (volK)−1⋅vol∣K; with K compact convex with nonempty interior its volume is positive and finite.
IsSupported μ Y means μ(Yc)=0. Couplings are probability measures with the two marginals; costs are lower integrals in ℝ≥0∞; W2 is the square root of the real part of the infimal cost, finite here because supports are bounded.
IsUniqueQuadraticOptimalMap ρ μ T asserts that T is measurable, pushes ρ to μ, is cost-optimal among all couplings, and that every coupling of no larger cost equals the graph coupling. The goal must therefore also produce the Brenier maps; they are not assumed.
The constant is chosen after d, K, Y and before μ,ν, and is required to be finite and nonnegative.
The sharpness milestone fixes K=Y=[−1,1]d, requires exactly three distinct atoms with positive weights, μ=ν and W2>0, so it cannot be satisfied trivially.
Y. Brenier, Polar factorization and monotone rearrangement of vector-valued functions, Comm. Pure Appl. Math. 44 (1991), 375–417. https://doi.org/10.1002/cpa.3160440402
A. Delalande, Q. Mérigot, Quantitative stability of optimal transport maps under variations of the target measure, Duke Math. J. 172 (2023), 3321–3357. https://doi.org/10.1215/00127094-2022-0106
Q. Mérigot, A. Delalande, F. Chazal, Quantitative stability of optimal transport maps and linearization of the 2-Wasserstein space, AISTATS 2020, PMLR 108. https://proceedings.mlr.press/v108/merigot20a.html
V. Divol, J. Niles-Weed, A.-A. Pooladian, Tight stability bounds for entropic Brenier maps, IMRN 2025, rnaf078. https://doi.org/10.1093/imrn/rnaf078
C. Letrouit, Q. Mérigot, Gluing methods for quantitative stability of optimal transport maps, arXiv:2411.04908 (2024). https://arxiv.org/abs/2411.04908v3
R. J. Berman, Convergence rates for discretized Monge–Ampère equations and quantitative stability of optimal transport, Found. Comput. Math. 21 (2021), 1099–1140. https://doi.org/10.1007/s10208-020-09480-x
N. Gigli, On Hölder continuity-in-time of the optimal transport map towards measures along a curve, Proc. Edinb. Math. Soc. 54 (2011), 401–409. https://doi.org/10.1017/S001309150800117X
Counterexamples to the duality conjecture for metric entropyResearch Paper
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∘ equally hard to cover by K∘? 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 Rn with the standard pairing ⟨x,y⟩=∑ixiyi. A convex body is a compact convex set with nonempty interior; it is origin-symmetric if K=−K. Its polar is
K∘={y∈Rn:⟨x,y⟩≤1for all x∈K}.
For bounded A and a body B, the covering numberN(A,B) is the least M such that A⊆⋃j=1M(cj+B) for some c1,…,cM∈Rn (centres need not lie in A). Logarithms are natural. Let L=[−1,1]n be the cube; its polar L∘ is the cross-polytope.
The duality conjecture asks for absolute constants a,b≥1 such that, for every n and all origin-symmetric convex bodies K,L⊂Rn,
b1logN(L∘,aK∘)≤logN(K,L)≤blogN(L∘,a−1K∘).
Formalization targets
Goal: Theorem 1.1
For every a,b≥1 there are n≥1 and an origin-symmetric convex body K⊂Rn such that, with L=[−1,1]n,
logN(K,L)>blogN(L∘,a−1K∘).
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 ≤1.
Covers A B centers means every x∈A has some centre cj with x−cj∈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.
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.
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
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
Fixed Points of Nonexpansive Maps in Reflexive Banach SpacesResearch Paper
Motivation: the fixed point property in reflexive spaces
A map F is nonexpansive if ∥F(a)−F(b)∥≤∥a−b∥. Unlike strict contractions, nonexpansive maps need not have fixed points: on a bounded set, existence depends on the geometry of the norm. A Banach space has the fixed point property (FPP) if every nonexpansive self-map of every nonempty closed bounded convex subset has a fixed point. Since the mid-1960s, whether every reflexive Banach space has the FPP in its given norm has been one of the central open questions of metric fixed point theory. Many sufficient geometric conditions are known, but none of them covers all reflexive spaces. In fixed point theory, the question has been listed as unresolved as recently as 2026 (Nourouzi 2026).
Timeline
1965 — Browder and Göhde prove the FPP for uniformly convex spaces (Browder 1965; Göhde 1965). Kirk proves it for weakly compact convex sets with normal structure, in particular for closed bounded convex sets with normal structure in reflexive spaces (Kirk 1965).
1974–1975 — Bruck's common fixed point theorems for commuting families and compact convex semigroups (Bruck 1974; Bruck 1975).
1975–1976 — The Goebel–Karlovitz lemma on approximate fixed point sequences in minimal invariant sets (Goebel 1975; Karlovitz 1976). Karlovitz also shows that a norm on ℓ2 without normal structure still has the FPP, so normal structure is not necessary.
1981 — Alspach constructs a weakly compact convex subset of L1[0,1] with a fixed-point-free nonexpansive self-map, so weak compactness alone is insufficient in general Banach spaces (Alspach 1981). Maurey proves the FPP for reflexive subspaces of L1 (Maurey 1981).
1985 — Lin proves the weak FPP for spaces with a 1-unconditional basis (Lin 1985).
2006 — García-Falset, Llorens-Fuster and Mazcuñán-Navarro prove the FPP for uniformly nonsquare spaces (JFA 2006); another proof is due to Dowling, Randrianantoanina and Turett (JFA 2008).
2009 — Domínguez Benavides shows that every reflexive space admits an equivalent norm with the FPP (JMAA 2009). Changing the norm changes which maps are nonexpansive, so this does not settle the question for the original norm.
2019, 2021 — Hanebaly proposes proofs of the original-norm assertion (JP J. Fixed Point Theory Appl. 2019; preprint 2021). Later literature, such as Nourouzi (2026), still treats the question as unresolved.
2026 — An OpenAI preprint, Fixed Points of Nonexpansive Maps in Reflexive Banach Spaces (OpenAI Math Release, September 24, 2026), claims a proof for every real reflexive Banach space. It has not been peer reviewed, and the claim has not been formally verified.
Setting
Let X be a real Banach space and X∗∗ its continuous bidual. The canonical map J:X→X∗∗, J(x)(φ)=φ(x), is always a linear isometry, and X is reflexive if J is surjective. A subset C⊆X is taken nonempty, closed in the norm topology, bounded and convex. A map F:C→C is nonexpansive in the given norm of X, and a fixed point is a point a∈C with F(a)=a.
In Lean, reflexivity is the definition CanonicallyReflexive X, which says that NormedSpace.inclusionInDoubleDual ℝ X is surjective.
Formalization targets
Goal: reflexive spaces have the fixed point property (Theorem 1.1)
X real reflexive Banach,C⊆X nonempty, closed, bounded, convex,∥F(a)−F(b)∥≤∥a−b∥∀a,b∈C⟹∃a∈C:F(a)=a.
This is exactly 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. The theorem answers the reflexive-space fixed point problem for the given norm, with no extra geometric assumption (uniform convexity, normal structure, unconditional bases, uniform nonsquareness). With Bruck's 1974 theorem it gives the source's Corollary 1.2: for every commuting family of nonexpansive self-maps of C, the common fixed point set is nonempty and is a nonexpansive retract of C. Alspach's example shows that reflexivity cannot be weakened to weak compactness of C in an arbitrary Banach space.
Formalizing it. Earlier proposed proofs of the same assertion exist, and the literature has not reached a consensus, so a machine-checked proof would give unusual certainty on a disputed question. The proof relies on the minimal invariant set reduction (Zorn's lemma and weak compactness), the Goebel–Karlovitz lemma, compact semigroups of nonexpansive maps (an Ellis-type idempotent), and a tree construction with weighted telescoping estimates. Mathlib has the bidual, the weak topology, and Banach–Alaoglu, but most of the fixed-point-theoretic layer has to be built.
Difficulty
The classical route reduces a hypothetical counterexample to a minimal invariant weakly compact convex set K of diameter one. By the Goebel–Karlovitz lemma, every approximate fixed point sequence in K is asymptotically diametral. Normal-structure arguments then find a point whose radius is strictly below the diameter. In a general reflexive space there is no such geometric gain, and Karlovitz's example shows that normal structure is not necessary for the conclusion. Alspach's L1 example shows that compactness of C and nonexpansiveness alone cannot produce the contradiction: the proof has to use reflexivity of the whole space (weak compactness of the unit ball of span(K−K)), not just of the domain. A further obstacle is that F is nonlinear, so convex combinations of approximate fixed points are not mapped to convex combinations of their images.
Formalization scope
X is any real normed space with CompleteSpace X, and reflexivity is surjectivity of NormedSpace.inclusionInDoubleDual ℝ X (the continuous bidual). Completeness also follows from reflexivity, so including it is harmless. The scalar field is R; complex spaces enter as real spaces.
C is a Set X with Nonempty, IsClosed (norm topology), Bornology.IsBounded and Convex ℝ. F is a function on the subtype C → C, and nonexpansiveness is stated in the original norm of X, not in an equivalent norm.
The conclusion is the existence of a fixed point ∃ a : C, F a = a. Every hypothesis is satisfiable, so the statement is not vacuous: a trivial C is excluded only by nonemptiness, as in the source.
Infrastructure needed: the minimal invariant set reduction, the Goebel–Karlovitz lemma, compact right-topological semigroups of maps and idempotents (Ellis), and weak compactness in reflexive spaces. These would serve other fixed-point formalizations, for example Kirk's and Browder–Göhde's theorems, which are not formalized in Mathlib.
Selected references
F. E. Browder, Nonexpansive nonlinear operators in a Banach space, Proc. Natl. Acad. Sci. USA 54 (1965), 1041–1044. https://doi.org/10.1073/pnas.54.4.1041
W. A. Kirk, A fixed point theorem for mappings which do not increase distances, Amer. Math. Monthly 72 (1965), 1004–1006. https://doi.org/10.2307/2313345
L. A. Karlovitz, Existence of fixed points of nonexpansive mappings in a space without normal structure, Pacific J. Math. 66 (1976), 153–159. https://doi.org/10.2140/pjm.1976.66.153
D. E. Alspach, A fixed point free nonexpansive map, Proc. Amer. Math. Soc. 82 (1981), 423–424. https://doi.org/10.2307/2043954
J. García-Falset, E. Llorens-Fuster and E. M. Mazcuñán-Navarro, Uniformly nonsquare Banach spaces have the fixed point property for nonexpansive mappings, J. Funct. Anal. 233 (2006), 494–514. https://doi.org/10.1016/j.jfa.2005.09.002
T. Domínguez Benavides, A renorming of some nonseparable Banach spaces with the Fixed Point Property, J. Math. Anal. Appl. 350 (2009), 525–530. https://doi.org/10.1016/j.jmaa.2008.02.049
K. Nourouzi, Reflexivity of Hilbert K(H)-modules and fixed-point property for nonexpansive mappings, J. Math. 2026, Article ID 6311273. https://doi.org/10.1155/jom/6311273
The complete Crouzeix theorem: optimal similarity and a common positive boundary representationResearch Paper
Motivation
For a square matrix A, the spectrum alone does not control the size of p(A): a nonzero nilpotent matrix has spectrum {0} yet ∥A∥>0. The numerical rangeW(A)={u∗Au:∥u∥=1} is a compact convex set containing the spectrum (Toeplitz–Hausdorff), and it does retain enough information. Crouzeix's conjecture (2004) asserts that for every polynomial p,
∥p(A)∥≤2z∈W(A)max∣p(z)∣,
i.e. that W(A) is a 2-spectral set; the constant 2 would be optimal. Such bounds are used to estimate matrix functions in numerical linear algebra (for example GMRES convergence through Faber polynomials) and in operator theory. The complete version asks for the same constant when the polynomial has m×m matrix coefficients, uniformly in m; by Paulsen's theorem this is equivalent to similarity of the conformal disk image of A to a contraction with condition number at most 2.
Background
1918–1919 — Toeplitz and Hausdorff prove convexity of the numerical range (Math. Z. 1918, Math. Z. 1919).
1972, 1984 — Arveson's dilation theory (Acta Math. 128, 1972) and Paulsen's similarity theorem (Proc. AMS 92, 1984) relate complete contractivity, dilations and similarity.
1999 — Delyon and Delyon's positive integral representations (Bull. SMF 1999).
2004 — Crouzeix formulates the constant-two question (IEOT 2004); 2007 — he proves a universal complete bound 11.08 (JFA 2007).
2006 — Badea, Crouzeix and Delyon obtain the complete constant 2 for 2×2 matrices (Math. Z. 2006).
2017–2018 — Crouzeix and Palencia prove the complete bound 1+2 (SIMAX 2017); Ransford and Schwenninger simplify the argument (SIMAX 2018).
2026 — Scalar (m=1) constant-two proofs appear in preprints of Jin, Lorist–Schwenninger (arXiv:2608.03841) and Luo; Åhag, Czyż and Virtanen prove the complete inequality for base matrices of order at most three (arXiv:2608.27346).
September 2026 — Two OpenAI preprints claim the complete inequality in all dimensions: a structural proof via an optimal similarity and a common positive boundary density, extended to all bounded Hilbert-space operators (source), and a direct coefficient proof for matrices (source).
This mission asks for a formal proof of the complete Crouzeix inequality for all bounded operators on complex Hilbert spaces, with its sharpness, as stated in Corollary 6.3 of an OpenAI preprint dated September 23, 2026 (source), together with the preprint's structural theorems as milestones. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Setting
For A∈Mn(C) (n≥1) let W(A)={u∗Au:u∈Cn,u∗u=1}. A matrix polynomial of degree d with coefficient size m≥1 is P(z)=∑k=0dBkzk with Bk∈Mm(C). Its evaluation at A is
P[A]=k=0∑dAk⊗Bk∈Mn(C)⊗Mm(C),
with the base space first. All norms are Euclidean operator norms. For m=1 this is the usual p(A).
For a bounded operator A on a complex Hilbert space H={0}, W(A)={⟨x,Ax⟩:∥x∥=1} and K=W(A); P[A]=∑kAk⊗Bk acts on H⊗Cm. A bounded open convex Ω⊂C is admissible if its boundary is a regular real-analytic Jordan curve. For such Ω⊃W(A) (A a matrix) with interior conformal map f:Ω→D, put T=f(A) and
κ2=min{τ:I⪯H⪯τI,T∗HT⪯Hfor some H=H∗}.
Formalization targets
Milestone: geometry of the numerical range (Corollary 6.3, p. 16, first assertion)
For H={0}, K=W(A) is compact and convex and contains spec(A).
Milestone: the zero space (Corollary 6.3, p. 16, case H={0})
If H={0}, the numerical range is empty, every polynomial, holomorphic and rational evaluation is 0, and the corresponding inequalities read 0≤0 (with the supremum over the empty set taken to be 0).
Milestone: optimal metric and common positive representation (Lemma 1.1, Theorems 1.2–1.3, p. 2)
For admissible Ω conformal coordinates exist; for every n≥1 and A∈Mn(C) with W(A)⊂Ω, the problem defining κ2 is strictly feasible with attained minimum 1≤κ2≤4; for a minimizer H, S=H1/2 satisfies ∥S∥∥S−1∥=κ≤2 and D=Sf(A)S−1 is a contraction with ρ(D)<1; and one continuous Λ:T→Mn(C) with Λ⪰0, ∫Λdσ=I represents v[SAS−1]=∫Λ(t)⊗v(G(t))dσ(t) for every m and every Mm-valued v holomorphic near Ω, giving ∥v[A]∥≤κmaxΩ∥v∥.
Milestone: the matrix inequality (Corollary 6.1, p. 15)
For all n,m≥1, d≥0, A∈Mn(C), Bk∈Mm(C): ∥P[A]∥≤2maxW(A)∥P∥, and no smaller universal constant works.
Goal: Corollary 6.3 (p. 16)
For every complex Hilbert space H (no separability assumption) and A∈B(H): if H={0} then K is compact, convex, contains the spectrum, and for every m≥1
for matrix polynomials P, matrix functions F holomorphic on an open U⊇K (holomorphic functional calculus), and matrix rational functions R with poles off K; if H={0} the degenerate statements above hold; and the constant 2 is optimal.
Significance
The result itself. It resolves the complete Crouzeix conjecture in its operator formulation, independent of the Hilbert space, the coefficient size and the degree: W(A) is a complete 2-spectral set for every bounded operator. The structural theorems give more than the inequality: an optimal similarity, attained, with condition number at most 2, and one positive boundary density that represents every matrix-valued analytic evaluation simultaneously. These are the objects predicted abstractly by Paulsen's and Arveson's theorems, constructed here explicitly. A companion OpenAI preprint gives an independent direct proof of the matrix inequality.
Formalizing it. Mathlib has bounded operators, the holomorphic functional calculus is only partially available, and conformal mapping of analytic Jordan domains is absent. A complete development needs the Riemann mapping theorem with boundary extension, semidefinite optimization over Hermitian matrices, Haar integration on the circle, and a finite-compression argument for nonseparable spaces.
Difficulty
Two obstacles stand out. First, the passage from the scalar to the complete inequality: scalar proofs exploit commutativity that fails for matrix coefficients, so a structure valid for every coefficient size at once is needed; here it is the optimal metric chosen before any test function. Proving κ≤2 for that metric requires an endpoint extremal pair (Proposition 2.2, p. 6) and an ordered density comparison (Lemma 5.1, p. 14). Second, the passage from matrices to arbitrary operators: the numerical range of a compression lies in W(A), but one must show every vector of H⊗Cm and its image under P[A] live in a finite-dimensional compression, and treat holomorphic and rational calculi through contour integrals around the closed numerical range.
Formalization scope
H is any type with InnerProductSpace ℂ H and CompleteSpace H; operators are H →L[ℂ] H. The amplification H⊗Cm is the completion of the algebraic tensor product, and Ak⊗Bk is the completed TensorProduct.mapL.
supNorm S F = sSup (insert 0 (‖F ·‖ '' S)), so the supremum over an empty set is 0, matching the convention of Corollary 6.3.
Holomorphic evaluation is defined by a contour integral over a CalculusContour around K inside U; the goal asserts such contours exist and that the evaluation is contour-independent. Rational evaluation inverts aeval A denom; the goal asserts these denominators are units and that the rational evaluation agrees with the holomorphic one.
SharpConstant is witnessed by a 2×2 matrix with supW∣P∣=1 and ∥P[A]∥=2.
The structural milestone also includes, as an extra conjunct, that the open unit disk is admissible.
Two further published supporting statements are included as items but not milestones: existence of a finite-dimensional compression representing a given vector (a step in the proof of Corollary 6.3) and invertibility of rational denominators (the well-definedness part of the rational calculus).
M. Crouzeix, C. Palencia, The numerical range is a (1+2)-spectral set, SIAM J. Matrix Anal. Appl. 38 (2017), 649–655. https://doi.org/10.1137/17M1116672
T. Ransford, F. L. Schwenninger, Remarks on the Crouzeix–Palencia proof that the numerical range is a (1+2)-spectral set, SIAM J. Matrix Anal. Appl. 39 (2018), 342–345. https://doi.org/10.1137/17M1143757
B. Delyon, F. Delyon, Generalization of von Neumann's spectral sets and integral representation of operators, Bull. Soc. Math. France 127 (1999), 25–41. https://doi.org/10.24033/bsmf.2340
P. Åhag, R. Czyż, J. Virtanen, The complete Crouzeix conjecture in dimension three and the Clouâtre–Ostermann–Ransford conjecture, arXiv:2608.27346 (2026). https://arxiv.org/abs/2608.27346v4
A direct proof of the complete Crouzeix inequalityResearch Paper
Motivation
For a square matrix A, the spectrum alone does not control the size of p(A): a nonzero nilpotent matrix has spectrum {0} yet ∥A∥>0. The numerical rangeW(A)={u∗Au:∥u∥=1} is a compact convex set containing the spectrum (Toeplitz–Hausdorff), and it does retain enough information. Crouzeix's conjecture (2004) asserts that for every polynomial p,
∥p(A)∥≤2z∈W(A)max∣p(z)∣,
i.e. that W(A) is a 2-spectral set; the constant 2 would be optimal. Such bounds are used to estimate matrix functions in numerical linear algebra (for example GMRES convergence through Faber polynomials) and in operator theory. The complete version asks for the same constant when the polynomial has m×m matrix coefficients, uniformly in m; by Paulsen's theorem this is equivalent to similarity of the conformal disk image of A to a contraction with condition number at most 2.
Background
1918–1919 — Toeplitz and Hausdorff prove convexity of the numerical range (Math. Z. 1918, Math. Z. 1919).
1972, 1984 — Arveson's dilation theory (Acta Math. 128, 1972) and Paulsen's similarity theorem (Proc. AMS 92, 1984) relate complete contractivity, dilations and similarity.
1999 — Delyon and Delyon's positive integral representations (Bull. SMF 1999).
2004 — Crouzeix formulates the constant-two question (IEOT 2004); 2007 — he proves a universal complete bound 11.08 (JFA 2007).
2006 — Badea, Crouzeix and Delyon obtain the complete constant 2 for 2×2 matrices (Math. Z. 2006).
2017–2018 — Crouzeix and Palencia prove the complete bound 1+2 (SIMAX 2017); Ransford and Schwenninger simplify the argument (SIMAX 2018).
2026 — Scalar (m=1) constant-two proofs appear in preprints of Jin, Lorist–Schwenninger (arXiv:2608.03841) and Luo; Åhag, Czyż and Virtanen prove the complete inequality for base matrices of order at most three (arXiv:2608.27346).
September 2026 — Two OpenAI preprints claim the complete inequality in all dimensions: a structural proof via an optimal similarity and a common positive boundary density, extended to all bounded Hilbert-space operators (source), and a direct coefficient proof for matrices (source).
This mission asks for a formal proof of the complete Crouzeix inequality for matrices, with its sharpness, as stated in Theorem 1.1 of an OpenAI preprint dated September 26, 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.
Setting
For A∈Mn(C) (n≥1) let W(A)={u∗Au:u∈Cn,u∗u=1}. A matrix polynomial of degree d with coefficient size m≥1 is P(z)=∑k=0dBkzk with Bk∈Mm(C). Its evaluation at A is
P[A]=k=0∑dAk⊗Bk∈Mn(C)⊗Mm(C),
with the base space first. All norms are Euclidean operator norms. For m=1 this is the usual p(A).
Formalization targets
Milestone: the inequality (Theorem 1.1, p. 1, first assertion)
For all n,m≥1, d≥0, A∈Mn(C) and B0,…,Bd∈Mm(C),
k=0∑dAk⊗Bk≤2z∈W(A)maxk=0∑dBkzk.
Milestone: sharpness (Theorem 1.1, p. 1, second assertion)
If the inequality holds with a constant c in place of 2 for all n,m,d,A,B, then c≥2.
Goal: Theorem 1.1 (p. 1)
Both assertions together: the constant 2 is valid and no smaller universal constant is.
Significance
The result itself. It settles the complete Crouzeix conjecture in its matrix formulation, uniformly in the base dimension n, the coefficient size m and the degree, including matrices whose numerical range is a point or a segment. The scalar case m=1 had recently been proved by other authors and the complete case was known only for n≤3; a scalar argument need not survive matrix amplification because coefficient matrices do not commute. Equivalently, the numerical range is a complete 2-spectral set for every matrix, which via Paulsen's theorem gives a similarity of condition number at most 2 making the conformal disk image of A a contraction. A companion OpenAI preprint gives a separate structural proof and extends the bound to all bounded operators on Hilbert spaces.
Formalizing it. The proof uses exterior conformal maps of analytic convex domains, Faber-type coefficients, a positive double-layer kernel, and a 2×2 block positivity argument; Section 4 then approximates an arbitrary numerical range by analytic convex domains. A formal proof would provide numerical ranges, Faber polynomials and conformal collars in Lean, all reusable in matrix analysis. No machine-checked proof of any constant-2 Crouzeix bound is known.
Difficulty
The naive approach through the spectrum fails for non-normal matrices, and the classical Crouzeix–Palencia method (a positive double-layer potential plus a Cauchy transform of conjugate data) loses a factor and yields 1+2. To reach 2 in the complete setting, the argument must keep both multiplication orders FG and GF of matrix-valued test functions, since the coefficients do not commute. The preprint chooses a top singular pair (x,y) of F[A], represents three functionals through the resolvent, and must show that the resulting coefficient weights (one on the constant term, one half on the others) match exactly the Fourier weights of the diagonal compressions (Section 2, Proposition 2.2, p. 5; Theorem 3.2, p. 6). Degenerate numerical ranges with empty interior require a separate approximation step (Lemma 4.1, p. 9).
Formalization scope
Matrices are Matrix (Fin n) (Fin n) ℂ with the L2 operator norm (Matrix.Norms.L2Operator). The numerical range is the set of ⟨x,Ax⟩ over unit vectors of EuclideanSpace ℂ (Fin n).
Coefficients are B : Fin (d+1) → Matrix (Fin m) (Fin m) ℂ; the evaluation is ∑kAk⊗KronBk indexed by Fin n × Fin m, base factor first.
rangeMaximum A B is the sSup of ∥P(z)∥ over W(A). Since n≥1, W(A) is nonempty and compact, so this is the true maximum; UniversalBound C quantifies over all n,m≥1, all d, all A and B.
The goal OAI.CompleteCrouzeix.main is UniversalBound 2 ∧ ∀ C, UniversalBound C → 2 ≤ C. The two milestones state the same two clauses in the DirectCrouzeix namespace, whose definitions are identical in content.
No normality, invertibility or nonempty-interior hypothesis is imposed on A.
M. Crouzeix, C. Palencia, The numerical range is a (1+2)-spectral set, SIAM J. Matrix Anal. Appl. 38 (2017), 649–655. https://doi.org/10.1137/17M1116672
T. Ransford, F. L. Schwenninger, Remarks on the Crouzeix–Palencia proof that the numerical range is a (1+2)-spectral set, SIAM J. Matrix Anal. Appl. 39 (2018), 342–345. https://doi.org/10.1137/17M1143757
B. Delyon, F. Delyon, Generalization of von Neumann's spectral sets and integral representation of operators, Bull. Soc. Math. France 127 (1999), 25–41. https://doi.org/10.24033/bsmf.2340
P. Åhag, R. Czyż, J. Virtanen, The complete Crouzeix conjecture in dimension three and the Clouâtre–Ostermann–Ransford conjecture, arXiv:2608.27346 (2026). https://arxiv.org/abs/2608.27346v4
Backward intertwiners and a transitive commutantResearch Paper
Motivation
A closed subspace M of a Hilbert space H is hyperinvariant for a bounded operator S if AM⊆M for every operator A commuting with S. The hyperinvariant subspace problem asks whether every bounded nonscalar operator on an infinite-dimensional separable complex Hilbert space has a nonzero proper closed hyperinvariant subspace. It is a strengthening of the invariant subspace problem, closely tied to the theory of transitive operator algebras: S has no such subspace exactly when its commutant {S}′ is transitive. A related classical question asks whether every unital transitive operator algebra is strongly dense in B(H); Arveson's density theorem gives a positive answer when the algebra contains a maximal abelian self-adjoint subalgebra.
Timeline
1967. Arveson proves that a transitive algebra containing a maximal abelian self-adjoint subalgebra is strongly dense in B(H) (doi:10.1215/S0012-7094-67-03467-9).
1972. Douglas and Pearcy relate hyperinvariant subspaces to transitive algebras (doi:10.1307/mmj/1029000793).
1981–1982. Domar describes translation-invariant subspaces of weighted ℓp and Lp spaces (doi:10.7146/math.scand.a-11926); Grabiner studies unicellular shifts.
1999. Atzmon and Sodin construct completely indecomposable bilateral weighted shifts with spectrum the unit circle, leaving open whether they have proper hyperinvariant subspaces (doi:10.1006/jfan.1999.3454).
2005. Dykema observes that hyperinvariant subspaces of an operator in a von Neumann algebra have projections in that algebra (doi:10.1007/s00208-005-0669-8).
2025–2026. A preprint of Kérchy and Pearcy claiming an equivalence between the invariant and hyperinvariant problems is withdrawn after a counterexample to its Theorem 3 (arXiv:2503.13005); Kérchy studies hyperinvariant subspaces of operators containing unilateral shifts (doi:10.1007/s11785-026-02038-9).
The source of this mission is an OpenAI preprint dated September 27, 2026. A companion OpenAI preprint of the same date reaches the same existence conclusion through invariant projections in an irrational-rotation factor, by a different construction.
Setting
Let H be a complex Hilbert space and B(H) its bounded operators. For S∈B(H):
the commutant is {S}′={A∈B(H):AS=SA}, a unital subalgebra of B(H);
{S}′ is transitive if the only closed subspaces M with AM⊆M for all A∈{S}′ are {0} and H;
S is norm-quasinilpotent if ∥Sn∥1/n→0;
the strong operator topology on B(H) is the topology of pointwise norm convergence: Aλ→A iff Aλx→Ax for every x∈H.
Formalization targets
Goal: Corollary 1.2
For every infinite-dimensional separable complex Hilbert space H there is S∈B(H) with
The Lean statement OAI.BackwardIntertwiners.direct_algebra_corollary is open on the platform. The family statement OAI.Hyperinvariant.main_theorem asserts the same proposition and is included as a reference item.
Significance
Corollary 1.2 gives a negative answer to the hyperinvariant subspace problem on every separable infinite-dimensional Hilbert space, and its commutant is a proper, strongly closed, unital transitive algebra, so it also answers negatively whether every unital transitive operator algebra is strongly dense in B(H). The construction behind it (Theorem 1.1) is explicit: a weighted shift over the 2-adic odometer whose fibres have only coordinate-tail invariant subspaces, an explicit bound ∥Sn∥≤exp(−10⌊(n+1)2/4⌋), and a bounded commuting operator moving those tails backward. The operator does have many ordinary invariant subspaces, so the invariant subspace problem itself is untouched.
The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists.
Difficulty
Weighted shifts have rich lattices of invariant subspaces, so one must first pin down the invariant subspaces of each fibre (a quadratic weighted-translation criterion in the style of Domar) and then find enough operators in the commutant to destroy every candidate. Multiplication operators and the shift alone leave every fixed tail L2(X;K≥h) invariant. The essential step is a bounded operator commuting with S that moves tails backward across fibres; this requires opposite logarithmic drifts of the weights at the two ends of the bilateral sequence and one measurable normalization valid on the whole base. Arveson's theorem cannot be used, since the multiplier algebra has infinite multiplicity and is not maximal abelian.
Formalization scope
H is any type with [InnerProductSpace ℂ H] [CompleteSpace H] [SeparableSpace H] and ¬FiniteDimensional ℂ H; the claim is existential in T : H →L[ℂ] H.
commutant T is Subalgebra.centralizer ℂ {T}; TransitiveCommutant T quantifies over closed Submodules invariant under every A with A * T = T * A.
Quasinilpotence is Tendsto (fun n => ‖T ^ n‖ ^ (1 / n)) atTop (𝓝 0) (the n=0 term is irrelevant to the limit).
The strong operator topology is TopologicalSpace.induced from the pointwise (product) topology on functions H → H.
A complete development needs vector-valued L2 spaces over the 2-adic integers with Haar measure, weighted shifts and their invariant subspaces, measurable fields of projections, and transport to an arbitrary separable Hilbert space by a unitary. Contributions formalizing Theorem 1.1 (the construction), Lemma 2.1 (weighted translation criterion), Proposition 4.3 (a bounded backward intertwiner) and Lemma 5.1 (strict descent) are welcome.
A. Atzmon, M. Sodin, Completely indecomposable operators and a uniqueness theorem of Cartwright–Levinson type, J. Funct. Anal., 1999. https://doi.org/10.1006/jfan.1999.3454
L. Kérchy, C. Pearcy, Hyperinvariant subspaces of block-triangular operators on Hilbert space, withdrawn preprint, 2025. https://arxiv.org/abs/2503.13005
The entropy photon-number inequalityResearch Paper
Motivation
Shannon's entropy power inequality bounds the entropy of a sum of independent random vectors below by the entropies of the summands; it is a basic tool for classical Gaussian channel capacities. In optical communication, addition is replaced by passive mixing of bosonic modes at a beam splitter. Guha, Erkmen and Shapiro conjectured the sharp bosonic analogue, the entropy photon-number inequality (EPnI), stated in terms of the photon number of the thermal state with the same entropy (ITA 2008). If true, it settles the minimum output entropy of thermal attenuators at fixed input entropy and the capacity regions of bosonic broadcast and wiretap channels, which had been reduced to this inequality (PRA 2007).
This mission asks for a formal proof of the EPnI for finite-energy inputs in any finite number of modes, 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
1948–1965 — Shannon introduces entropy power; Stam (1959) and Blachman (IEEE IT 1965) prove the entropy power inequality.
2004 — Capacity of the pure-loss bosonic channel (PRL 2004) and the minimum-output-entropy conjecture (PRA 2004).
2007–2008 — Guha, Shapiro and Erkmen relate broadcast capacity to a minimum-output-entropy conjecture; Guha, Erkmen and Shapiro state the EPnI.
2011 — Special cases (one-mode number-diagonal inputs) by Das, Sharma and Muthukrishnan (arXiv:1107.2365).
2014 — König and Smith prove a quantum entropy power inequality, including S(ρC)≥ηS(ρA)+(1−η)S(ρB) (IEEE IT 2014); De Palma, Mari and Giovannetti prove the exponential form eS(ρC)/n≥ηeS(ρA)/n+(1−η)eS(ρB)/n (Nat. Photonics 2014).
2015 — Giovannetti, Holevo and García-Patrón solve the Gaussian optimizer conjecture for unconstrained minimum output entropy (CMP 2015).
2016–2018 — De Palma, Trevisan and Giovannetti settle one-mode constrained problems (IEEE IT 2017; PRL 2017); De Palma and Trevisan give a rigorous finite-energy conditional EPI (CMP 2018).
September 2026 — The OpenAI preprint claims the two-input EPnI for all finite-energy inputs (Theorem 1.1, p. 2).
Setting
An n-mode bosonic system has Fock space ℓ2(Nn) with number basis ∣k⟩, k∈Nn. A state is a positive trace-one operator ρ; it has finite energy if Trρ∑jaj†aj=∑k(k1+⋯+kn)⟨k∣ρ∣k⟩<∞. The von Neumann entropy is S(ρ)=−Trρlogρ (natural log). The thermal entropy per mode is
g(t)=(t+1)log(t+1)−tlogt,t≥0,
increasing from 0 to ∞, and the entropy photon number of ρ is N(ρ)=g−1(S(ρ)/n), the mean photon number per mode of the product thermal state with the same entropy. For independent inputs ρA,ρB and transmissivity 0≤η≤1, the beam-splitter outputρC is the reduced state of the modes cj=ηaj+1−ηbj after passive mixing of ρA⊗ρB. No independence among the modes within either input is assumed.
Formalization targets
Goal: Theorem 1.1 (p. 2)
For every finite n≥1, every pair of finite-energy n-mode states ρA,ρB and every 0≤η≤1,
g−1(nS(ρC))≥ηg−1(nS(ρA))+(1−η)g−1(nS(ρB)).
Thermal inputs with a common mean photon number within each port give equality.
Significance
The result itself. The EPnI is sharper than the exponential quantum entropy power inequality when the two input entropies differ, which is exactly the regime needed for constrained minimum output entropy. The preprint derives the exact minimum output entropy at fixed input entropy for every tensor power of an identical thermal attenuator, with inputs entangled across modes (Corollary 1.2, p. 2), and the exact capacity region of the degraded two-receiver pure-loss broadcast channel (Corollary 7.1, p. 26), completing the converse of Guha, Shapiro and Erkmen.
Formalizing it. The statement involves infinite-dimensional Fock space, trace-class positive operators, continuous functional calculus for the entropy, and the partial trace after a passive unitary. The Lean development builds these concretely in the number basis. A formal proof would give machine-checked infrastructure for quantum entropy on infinite-dimensional spaces, which Mathlib currently lacks. No machine-checked version of any quantum entropy power inequality is known.
Difficulty
Heat-flow (quantum Fisher information) proofs give the linear and exponential bounds, but these are attained only for equal entropies and do not recover the thermal comparison at unequal entropy levels. The preprint instead minimizes a regularized functional over pairs of inputs and must show that minimizers are thermal. This requires an interpolation theorem for diagonal form comparisons (Theorem 3.1, p. 8), attainment and Gibbs regularity of minimizers in infinite dimensions (Lemma 4.1, Proposition 4.2, pp. 15–16), a component entropy-Hessian estimate, and a stationarity identity whose cancellation forces convergence to thermal inputs (Section 6). Compactness relies on the finite-energy hypothesis; without it entropies can be infinite.
Formalization scope
Fock n is lp (fun _ : Fin n → ℕ => ℂ) 2. A State is a positive bounded operator whose diagonal in the number basis sums (HasSum) to 1.
FiniteEnergy ρ is summability of ∑k∣k∣⟨k∣ρ∣k⟩.
entropy ρ is the sum of diagonal entries of cfc(−tlogt)(ρ); for finite-energy states it is finite, so the tsum is the true entropy.
gInv s = sInf {t ≥ 0 | s ≤ g t}, the inverse of g on [0,∞).
IsBeamSplitterOutput η ρA ρB ρC requires every number-basis entry of ρC to be the (convergent) partial-trace sum of the explicitly given beam-splitter coefficients applied to ρA⊗ρB; the inputs are arbitrary density matrices, so internal entanglement is allowed.
The hypotheses are satisfiable (e.g. vacuum or thermal inputs) and the conclusion is the inequality as stated.
S. Guha, B. I. Erkmen, J. H. Shapiro, The entropy photon-number inequality and its consequences, ITA Workshop 2008, 128–130. https://doi.org/10.1109/ITA.2008.4601037
S. Guha, J. H. Shapiro, B. I. Erkmen, Classical capacity of bosonic broadcast communication and a minimum output entropy conjecture, Phys. Rev. A 76 (2007), 032303. https://doi.org/10.1103/PhysRevA.76.032303
G. De Palma, A. Mari, V. Giovannetti, A generalization of the entropy power inequality to bosonic quantum systems, Nat. Photonics 8 (2014), 958–964. https://doi.org/10.1038/nphoton.2014.252
G. De Palma, D. Trevisan, The conditional entropy power inequality for bosonic quantum systems, Comm. Math. Phys. 360 (2018), 639–662. https://doi.org/10.1007/s00220-017-3082-8
V. Giovannetti, A. S. Holevo, R. García-Patrón, A solution of Gaussian optimizer conjecture for quantum channels, Comm. Math. Phys. 334 (2015), 1553–1571. https://doi.org/10.1007/s00220-014-2150-6
V. Giovannetti, S. Guha, S. Lloyd, L. Maccone, J. H. Shapiro, H. P. Yuen, Classical capacity of the lossy bosonic channel: the exact solution, Phys. Rev. Lett. 92 (2004), 027902. https://doi.org/10.1103/PhysRevLett.92.027902
Given a group A, adjoin one new generator t and impose one relation w=1, where w is a word in t and elements of A. Can the result collapse to the trivial group when A is nontrivial? The Kervaire conjecture says no. It arose from Kervaire's 1965 characterization of high-dimensional knot groups, which involves groups normally generated by a single element, and it is one of the best-known problems about equations over groups: when does an equation w(t)=1 with coefficients in A have a solution in some group containing A?
Timeline
1962. Gerstenhaber and Rothaus prove that nonsingular systems of equations over finite groups are solvable in finite overgroups, using unitary groups and degree theory (doi:10.1073/pnas.48.9.1531); this gives the result for residually finite groups.
1965. Kervaire characterizes high-dimensional knot groups (doi:10.24033/bsmf.1624); the group-theoretic Kervaire problem is traced to this setting.
2012. Klyachko and Lurye prove injectivity for arbitrary coefficient groups after imposing wm=1, m≥2 (doi:10.1016/j.jpaa.2011.06.020).
2017. Klyachko and Thom develop new topological methods for equations over groups (doi:10.2140/agt.2017.17.331).
2024–2026. Kawauchi publishes a proposed resolution via ribbon sphere-links; Chen gives a new proof of the torsion-free case via the complexity of surfaces (arXiv:2302.09811).
The source of this mission, an OpenAI preprint dated September 24, 2026, proves unimodular coefficient injectivity for every group by a route through spectral phase and a fixed-space theorem for unitary matrices.
Setting
Let A be a group, ⟨t⟩≅Z, and H=A∗⟨t⟩ the free product. Let p:H→Z be the homomorphism that kills A and sends t to 1; p(w) is the exponent sum of t in w. A word w∈H is unimodular if p(w)=±1. Write ⟨⟨w⟩⟩H for the normal closure of w in H. The coefficient map is the composite
A↪H↠H/⟨⟨w⟩⟩H.
Its injectivity is equivalent to solvability of w(t)=1 over A: there is an overgroup B⊇A and b∈B with w(b)=1.
The Lean statement OAI.Kervaire.coefficient_injective is open on the platform.
Significance
Theorem 1.1 immediately gives the Kervaire conjecture (Corollary 1.2): if A=1 then (A∗⟨t⟩)/⟨⟨w⟩⟩=1 for every w, since for p(w)=d=±1 the quotient maps onto Z/dZ. It proves the unimodular case of the stronger Kervaire–Laudenbach conjecture with no hypothesis on A: no torsion-freeness, residual finiteness, hyperlinearity or countability. The paper's companion work extends the method to nonsingular systems of equations (Howie's conjecture).
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. The statement is short and entirely algebraic, which makes it an attractive formalization target; Mathlib already provides free products and normal closures.
Difficulty
The classical Gerstenhaber–Rothaus argument solves the equation in a unitary group and needs A to embed in (an ultraproduct of) unitary groups, which is not known for arbitrary groups. Torsion in A blocks the diagrammatic and topological arguments that work in the torsion-free case. A proof for every group therefore needs a representation available for all groups (the left regular representation, with its faithful finite trace) together with an argument that does not rely on finite-dimensional approximation of A.
Formalization scope
The free product is Monoid.Coprod A (Multiplicative ℤ); the exponent sum is Multiplicative.toAdd (Monoid.Coprod.snd w).
Unimodular w is exponentSum w = 1 ∨ exponentSum w = -1.
The quotient is by Subgroup.normalClosure {w}, and coefficientMap w is the quotient map composed with Monoid.Coprod.inl.
No hypothesis is placed on A; the group may live in any universe.
A complete development needs the group von Neumann algebra of A (or at least its trace), the spectral phase of unitaries and its subadditivity, a degree computation on a compact manifold of unitaries with fixed k-planes, and corner-labelled planar diagrams with Euler-characteristic estimates. Contributions formalizing Corollary 1.2 from Theorem 1.1, Lemma 2.1 (subadditivity of spectral phase) and Lemma 3.1 (fixed-space lemma) are welcome.
A. A. Klyachko, D. E. Lurye, Relative hyperbolicity and similar properties of one-generator one-relator relative presentations with powered unimodular relator, J. Pure Appl. Algebra, 2012. https://doi.org/10.1016/j.jpaa.2011.06.020
A CH obstruction to a prescribed categoricity thresholdResearch Paper
Motivation: categoricity transfer beyond first-order logic
A class of structures is categorical in a cardinal λ if it has exactly one model of size λ up to isomorphism. Morley's theorem (1965) says that a complete first-order theory in a countable language categorical in one uncountable cardinal is categorical in all of them. Abstract elementary classes (AECs), introduced by Shelah in the 1970s, axiomatize classes of structures with a well-behaved notion of strong substructure (closure under isomorphism, coherence, unions of chains, a Löwenheim–Skolem number) without requiring first-order axiomatizability; they cover classes defined in infinitary logics and many classes of modules. Shelah's categoricity conjecture for AECs, in its eventual form, asks whether categoricity in one sufficiently large cardinal transfers to all sufficiently large cardinals. A sharper, prescribed-threshold form names the threshold explicitly: with H(K)=ℶ(2LS(K))+ (the Hanf number for existence of arbitrarily large models), categoricity in some λ≥H(K) should imply categoricity in every μ≥H(K). Deciding which form holds is a central question in non-elementary model theory.
Timeline
1965 — Morley proves the categoricity theorem for countable first-order theories (Trans. AMS 1965).
1970s — Shelah introduces abstract elementary classes (see the survey of Boney–Vasey 2017, §2).
1990 — Hart and Shelah show categoricity in Lω1,ω can stop at ℵk while holding for ℵ0,…,ℵk−1, using finite-support group constructions (Israel J. Math. 1990).
1999 — Shelah proves categoricity transfer for AECs with amalgamation and records H(K) as the existence bound (APAL 1999).
2016 — Kolesnikov and Lambie-Hanson study Hanf numbers for amalgamation of coloring classes (JSL 2016).
2017 — Vasey proves downward transfer from a successor cardinal ≥H(K) under amalgamation and tameness (APAL 2017).
2021 — Grossberg distinguishes the prescribed-bound and eventual forms of the conjecture (A Course in Model Theory I, draft, Ch. 2 §4).
2022–2023 — Espíndola announces a proof of eventual categoricity and, for arbitrary AECs, a transfer at the prescribed bound via accessible categories (arXiv:1906.09169, arXiv:2301.13167).
2024 — Šaroch and Trlifaj state the prescribed-threshold formulation with both endpoints included (Bull. LMS 2024, §2.3).
2026 — An OpenAI preprint, A CH obstruction to a prescribed categoricity threshold (OpenAI Math Release, September 24, 2026), claims that under CH there is an AEC with LS(K)=ℵ0, categorical on a tail but with two nonisomorphic models at H(K)=ℶω2; this conflicts with the transfer claimed in Espíndola 2023 (Theorem 4.1). The preprint has not been peer reviewed and its theorem is not formally verified.
Setting
Work with relational structures in a finitary relational languageL (a set of relation symbols, each with a finite arity). An abstract elementary class is a class K of L-structures with a relation M⪯KN ("strong substructure") such that: ⪯K is a partial order on K refining substructure; K and ⪯K are closed under isomorphism; coherence holds (M0⊆M1, M0⪯KM2, M1⪯KM2 imply M0⪯KM1); unions of ⪯K-chains are in K, are ⪯K-extensions of each member, and are ⪯K-below any common strong extension (Tarski–Vaught chain axioms); and there is a Löwenheim–Skolem numberLS(K)≥ℵ0+∣L∣, the least θ such that every subset A of a model M lies in some N⪯KM with ∣N∣≤∣A∣+θ.
K is categorical in μ if it has a model of size μ and any two models of size μ are isomorphic. The beth numbers are ℶ0=ℵ0, ℶα+1=2ℶα and suprema at limits. CH is 2ℵ0=ℵ1.
Formalization targets
Goal: the CH counterexample (Theorem 1.1)
Assume CH. There is a countable finitary relational language L and an AEC K in L such that
LS(K)=ℵ0,ℶω2=H(K)=ℶ(2ℵ0)+,
K has two nonisomorphic models of cardinality ℶω2, and, with Λ=ℶ(2ℵ1)+,
Kis categorical in every cardinal μ≥Λ.
Hence Λ+>H(K) is a categoricity cardinal from which downward transfer to H(K) fails, while eventual categoricity holds for this K. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
Significance
The result itself. Combined with Gödel's relative consistency of CH, the theorem shows that, if ZFC is consistent, the prescribed-threshold form of Shelah's categoricity conjecture is not provable in ZFC (Corollary 6.1 of the source). The example has no amalgamation or joint embedding, which explains why transfer theorems that assume these properties are unaffected, and it is compatible with qualitative eventual categoricity. It also bears directly on a published claim of transfer at the prescribed bound for arbitrary AECs.
Formalizing it. Because the result contradicts a claimed theorem in the literature, an independent machine check is especially valuable. The formal statement verifies every AEC axiom explicitly, not just the two cardinal-arithmetic conclusions. Mathlib has cardinal and ordinal arithmetic, beth numbers and ZFC sets; the AEC framework built here would be reusable for further formal work in non-elementary model theory.
Difficulty
Most known non-transfer examples (Hart–Shelah) fail categoricity at small cardinals; here the failure must happen exactly at the Hanf-type bound ℶω2 while categoricity holds on a tail, with LS(K)=ℵ0. One must build two nonisomorphic models at ℶω2 and simultaneously rule out any two nonisomorphic models above Λ, without appealing to a general eventual-categoricity theorem. All AEC axioms — in particular coherence and smoothness of unions of arbitrary directed chains — must survive the exceptional sets used to separate models, which is where naive constructions break.
Formalization scope
Structures are RelModel L with carrier a ZFSet (so cardinalities are cardinals of genuine sets in universe u) and relations indexed by arity; L:N→Type with ΣnLn countable.
ClassData packages a predicate of objects and a strong-substructure relation; IsAEC lists the axioms above, including invariance under isomorphisms compatible with inclusion, coherence, and the union axioms for chains indexed by any nonzero ordinal.
HasLSNumber ℵ₀ asserts both that ℵ0 is a Löwenheim–Skolem bound and that it is the least one.
hanf κ = beth (succ (2^κ)).ord, endpoint = beth (ω_2), tailThreshold = beth (succ (2^{ℵ₁})).ord. The equality endpoint = hanf ℵ₀ is part of the goal (it follows from CH).
Categorical μ includes existence of a model of size μ; TwoModels asks for two nonisomorphic models of the given size.
CH is a hypothesis of the theorem, in the same universe; the consistency corollary is not part of the goal.
K. Gödel, The consistency of the axiom of choice and of the generalized continuum-hypothesis, Proc. Nat. Acad. Sci. USA (1938). https://doi.org/10.1073/pnas.24.12.556
B. Hart and S. Shelah, Categoricity over P for first order T or categoricity for φ∈L_{ω1ω} can stop at ℵ_k while holding for ℵ_0,…,ℵ_{k−1}, Israel J. Math. (1990). https://doi.org/10.1007/BF02807869
A. Kolesnikov and C. Lambie-Hanson, The Hanf number for amalgamation of coloring classes, J. Symb. Logic (2016). https://doi.org/10.1017/jsl.2015.48
J. Šaroch and J. Trlifaj, Deconstructible abstract elementary classes of modules and categoricity, Bull. London Math. Soc. (2024). https://doi.org/10.1112/blms.13172
C. Espíndola, A complete classification of categoricity spectra of accessible categories with directed colimits, preprint, 2023. https://arxiv.org/abs/2301.13167