The affine Bernstein theorem in dimensions three through nineOpen Problem
Motivation
Affine maximal graphs satisfy a nonlinear fourth-order geometric equation. The target asks whether completeness forces such a locally uniformly convex graph to be a paraboloid. The pinned manuscript supplies the research context.
Setting
The dimension is between three and nine. The domain is nonempty, open and convex, the function is smooth with positive-definite Hessian, and completeness uses intrinsic Euclidean graph length.
The theorem states that, for every integer dimension 3 ≤ n ≤ 9, a nonempty open convex set Ω ⊆ ℝⁿ and a function u : ℝⁿ → ℝ that is smooth on Ω satisfy the following conclusion under three hypotheses. First, the Hessian H = D²u is positive definite at every point of Ω. Second, u satisfies the affine maximal equation ∑ᵢⱼ Uᵢⱼ ∂ᵢ∂ⱼw = 0 throughout Ω, where U = (det H)H⁻¹ and w = (det H)^{−(n+1)/(n+2)}. Third, the graph is complete for its intrinsic Euclidean path distance: the distance between x and y in Ω is the infimum over C¹ paths γ in Ω joining them of ∫₀¹ √(‖γ′(t)‖² + (Du(γ(t))γ′(t))²) dt, and every Cauchy sequence for this distance has a limit in Ω for the same distance. Then Ω = ℝⁿ and there exist a symmetric positive definite real n × n matrix A, a vector b ∈ ℝⁿ, and c ∈ ℝ such that u(x) = ½xᵀAx + b·x + c for every x ∈ ℝⁿ. Moreover, an invertible affine map of ℝⁿ × ℝ carries the standard paraboloid {(x, ‖x‖²)} onto the graph {(x, u(x)) : x ∈ Ω}.
Significance and status
The goal also gives an invertible affine map from the standard paraboloid to the graph. The wider immersed-hypersurface formulation is not included as a separate target. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Difficulty
The domain is not initially assumed to be all of space. Both global domain exhaustion and the quadratic form must follow from the equation and completeness.
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 affine Bernstein theorem in dimensions three through nine, preprint, 2026. Manuscript.
Power-law violations of Yau's nodal upper boundOpen Problem
Motivation
Nodal sets are the zero loci of Laplace eigenfunctions. Their size probes how geometry constrains high-frequency oscillation. The pinned manuscript supplies the research context.
Setting
The encoded manifold is S4×S1 with one smooth Riemannian metric. The sequence consists of nonzero smooth real eigenfunctions with positive eigenvalues tending to infinity.
The theorem states that the defined proposition MainTarget holds, i.e. that there exist a smooth Riemannian metric g on the 5-manifold S⁴ × S¹ (the unit sphere in ℝ⁵ times the circle, modelled on ℝ⁴ × ℝ¹), a sequence of positive reals λₖ, and a sequence of smooth real functions uₖ on this manifold, each not identically zero, such that the following hold. At every point x, in the extended chart at x, the coordinate Laplacian of uₖ, namely (1/√det G) Σᵢ ∂ᵢ(√det G Σⱼ Gⁱʲ ∂ⱼ(uₖ∘chart⁻¹)), where G is the matrix of g in the chart's coordinate frame and Gⁱʲ its inverse, satisfies −Δ_g uₖ(x) = λₖ uₖ(x), so each uₖ is a Laplace eigenfunction with eigenvalue λₖ. Moreover λₖ → ∞, and the 4-dimensional Hausdorff measure (taken with respect to the distance induced by g) of the nodal set {uₖ = 0}, divided by √λₖ, tends to +∞ as k → ∞. Thus the nodal-set size grows faster than the order √λₖ, which is a counterexample to a Yau-type upper bound on nodal sets in this setting. The theorem is admitted in the source and not proved there.
Significance and status
The selected target is divergence relative to the square-root eigenvalue scale. It does not specify the fixed additional power ε0 asserted by the manuscript title and abstract. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Difficulty
The same smooth metric must support the whole eigenfunction sequence, and the nodal measure uses the distance induced by that metric.
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.
Taming implies compatibility on four-manifoldsOpen Problem
Motivation
A symplectic form can be positive on complex lines without being invariant under the almost complex structure. The target asks whether some compatible form nevertheless exists in four dimensions. The pinned manuscript supplies the research context.
Setting
The manifold is smooth, compact, connected, Hausdorff and second countable, modeled on real four-space. The almost complex structure squares to minus the identity.
The theorem states that, for a smooth manifold X modeled on four-dimensional Euclidean space ℝ⁴ (charted with smooth transition maps) that is Hausdorff, second countable, compact and connected, and for an almost complex structure J on X, if some symplectic two-form α tames J, then there exists a symplectic two-form η that is compatible with J. Here a two-form assigns to each point x a continuous alternating real bilinear form on the tangent space at x, and an almost complex structure J is a smooth field of continuous linear endomorphisms of the tangent spaces with J(Jv) = −v for every tangent vector v. A two-form is symplectic when it is smooth (its pullbacks along smooth maps from open subsets of ℝ⁴ are smooth), closed (the exterior derivative of each such pullback vanishes), and nondegenerate (a tangent vector v with α(v,w) = 0 for all w must be zero). The form α tames J when α(v, Jv) > 0 for every nonzero tangent vector v at every point. The form η is compatible with J when it tames J and is J-invariant, meaning η(Ju, Jv) = η(u, v) for all tangent vectors u and v at every point. This is a formal statement admitted without proof.
Significance and status
The conclusion supplies a possibly different symplectic form. It does not assert that the original taming form is compatible or prescribe its cohomology class. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Difficulty
A pointwise compatibility adjustment need not preserve closedness. The conclusion requires both global symplectic structure and positivity.
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, Taming implies compatibility on four-manifolds, preprint, 2026. Manuscript.
Generalized Cartan–Hadamard isoperimetry and Euclidean equality rigidityOpen Problem
Motivation
Sharp filling inequalities compare the mass of a cycle with the least mass needed to fill it. The selected formulation extends a Euclidean coefficient to proper CAT(0) metric spaces. The pinned manuscript supplies the research context.
Setting
Integral currents are encoded metric currents with integer-multiplicity chart decompositions and integral boundary. The input is a compactly supported n-cycle for n at least two. In the displayed coefficient, σ_n=(n+1)ω_{n+1}, where ω_{n+1} is the Euclidean volume of the unit ball in dimension n+1; this is the published sphereArea convention.
The theorem states that, for a proper metric space X with its Borel σ-algebra that is CAT(0), meaning there is a choice of geodesic parametrization segment(x,y,t) from x to y (with segment(x,y,0)=x, segment(x,y,1)=y, and dist(segment(x,y,s),segment(x,y,t))=|s−t|·dist(x,y) for s,t in [0,1]) satisfying the comparison inequality dist(segment(o,x,s),segment(o,y,t))² ≤ (s·d(o,x) − t·d(o,y))² + s·t·(d(x,y)² − (d(o,x) − d(o,y))²), the following filling property holds for every integer n ≥ 2. Let T be an integral n-current on X, that is, a metric current (a multilinear functional on a bounded Lipschitz function and n Lipschitz functions, with locality, continuity and finite mass) that is a countable sum of disjointly supported integer-multiplicity bi-Lipschitz chart pieces and whose boundary has the same properties, and suppose T is compactly supported and a cycle, meaning its boundary is zero. Then there exists a compactly supported integral (n+1)-current S on X whose boundary is T and whose mass satisfies mass(S) ≤ c_n · mass(T)^((n+1)/n), where c_n = 1/((n+1)·(σ_n)^(1/n)), σ_n = (n+1)·ω_{n+1} is the area of the unit n-sphere and ω_{n+1} is the volume of the unit ball in Euclidean (n+1)-space. This is an admitted theorem statement, not a verified proof.
Significance and status
The goal is the CAT(0) integral-current filling inequality. Euclidean coefficient optimality is an additional reference. The manifold perimeter comparison and equality-rigidity statements in the manuscript are not separate attached targets. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Difficulty
The sharp coefficient must hold without a smooth manifold model, while preserving integrality, compact support and the exact boundary.
Formalization scope
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
Additional published targets are included as separate references:
A counterexample to Naimark's problem in ZFCOpen Problem
Motivation
Uniqueness of irreducible representations is a strong condition on a C*-algebra. The target asks for a counterexample to the expected compact-operator characterization without added set-theoretic hypotheses. The pinned manuscript supplies the research context.
Setting
Representations are nonzero star homomorphisms on complete complex inner product spaces. Irreducibility is expressed by closed invariant subspaces, and equivalence by an intertwining linear isometry.
The theorem states that, for every universe level choice, there exists a type A carrying a C*-algebra structure (over ℂ) with the following five properties. First, A is simple in the sense that it is nontrivial and its only closed two-sided ideals are {0} and A itself. Second, A is not finite-dimensional as a complex vector space. Third, there is a continuous linear functional τ : A → ℂ that is a faithful tracial state: τ has norm 1, τ(aa) is a nonnegative real number for every a, τ(ab) = τ(ba) for all a and b, and τ(aa) > 0 whenever a ≠ 0. Fourth, A has a unique irreducible representation up to unitary equivalence: whenever π and ρ are nonzero star-homomorphisms (non-unital algebra homomorphisms preserving star) from A into the bounded operators on complete complex inner product spaces H and K, taken in the stated universe levels, and each has no closed invariant subspace other than 0 and the whole space, there is a linear isometric isomorphism U : H → K with U(π(a)x) = ρ(a)(Ux) for all a and x. Fifth, for every complete complex inner product space H in the stated universe, A is not isomorphic to the algebra of compact operators on H, meaning there is no injective star-homomorphism φ : A → B(H) whose range is exactly the set of compact operators on H.
Significance and status
The target explicitly requires simplicity, infinite dimension, a faithful tracial state and failure of all compact-operator isomorphisms in the stated universes. No additional set-theoretic hypothesis appears in its binders. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Difficulty
The construction must combine infinite dimension, a faithful trace and uniqueness across the specified representation universes.
Formalization scope
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
Selected references
OpenAI, A counterexample to Naimark's problem in ZFC, preprint, 2026. Manuscript.
Vanishing of higher bounded Hochschild cohomologyOpen Problem
Motivation
Hochschild cohomology measures whether a cocycle equation admits a primitive. In an operator algebra the boundedness requirement is part of the mathematical problem. The pinned manuscript supplies the research context.
Setting
Cochains are continuous complex multilinear maps into the von Neumann algebra itself, with its natural left and right multiplication actions.
The theorem states that, for a complex von Neumann algebra M (a C*-algebra with a partial order making it star-ordered, equipped with the W*-algebra structure), and any natural number n, every bounded Hochschild cocycle of degree n+2 with values in M is a coboundary. Here a cochain of degree m is a continuous complex m-linear map from M^m to M. The Hochschild differential of a cochain f of degree m, evaluated at (v_0,...,v_m), is v_0 f(v_1,...,v_m) plus the sum over j from 0 to m-1 of (-1)^(j+1) f(v_0,...,v_j v_{j+1},...,v_m), where the j-th and (j+1)-th inputs are multiplied into one, plus (-1)^(m+1) f(v_0,...,v_{m-1}) v_m. The hypothesis is that f has degree n+2 and its differential vanishes at every (n+3)-tuple of elements of M. The conclusion is that there exists a continuous multilinear cochain g of degree n+1 whose differential equals f at every (n+2)-tuple of elements of M.
Significance and status
The goal covers every natural n, hence degrees at least two. It does not include a separately referenced degree-one inner-derivation theorem. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Difficulty
An algebraic primitive is insufficient: the lower-degree cochain must remain continuous and bounded in the encoded operator-norm sense.
Formalization scope
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
Selected references
OpenAI, Vanishing of higher bounded Hochschild cohomology, preprint, 2026. Manuscript.
An explicit obstruction to nuclear norm-ultrapower embeddingsOpen Problem
Motivation
Norm ultrapowers permit approximations along a free ultrafilter. An explicit algebra excluded from every nuclear target ultrapower tests the limits of this embedding mechanism. The pinned manuscript supplies the research context.
Setting
The group is the stated dyadic semidirect product. Its full group C*-algebra is specified by a universal property, and the ultrapower is bounded sequences modulo norm-null sequences along the ultrafilter.
The theorem states that, working in universe level 0, there exist a nonzero unital complex C*-algebra A and a group homomorphism ι from G into the unitary group of A such that the following hold. Here G is the semidirect product of the additive group of 3-vectors over the dyadic rationals Z[1/2] by SL₃(ℤ) × ℤ, where a matrix acts linearly on the vectors and the integer n acts by multiplication by 2ⁿ. First, (A, ι) is the full group C*-algebra of G: the span of ι(G) is dense in A, and every homomorphism of G into the unitaries of a nonzero unital C*-algebra D extends uniquely to a unital -homomorphism A → D. Second, A is separable as a topological space. Third, for every nonzero unital C-algebra B that is nuclear in the tensor-norm sense (minimal and maximal C*-tensor norms agree on B ⊗ C for every C*-algebra C) and every free ultrafilter ω on ℕ (one containing no finite set), there is no injective unital -homomorphism from A into the norm ultrapower of B, namely bounded B-valued sequences modulo those tending to 0 along ω. Fourth, there exist a nonzero unital C-algebra O and two elements s₀, s₁ of O satisfying the Cuntz relations (each sᵢsᵢ = 1 and s₀s₀ + s₁s₁* = 1), with O universal for these relations, such that for every free ultrafilter ω there is likewise no injective unital *-homomorphism from A into the norm ultrapower of O. The theorem is admitted in the source, not proved.
Significance and status
The goal includes separability, the full group universal property, nonembedding and the Cuntz-algebra corollary in the stated base universe. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Difficulty
A single source algebra must obstruct all nuclear targets and free ultrafilters. Universal full-group and Cuntz-algebra constructions are part of the target.
Formalization scope
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
Selected references
OpenAI, An explicit obstruction to nuclear norm-ultrapower embeddings, preprint, 2026. Manuscript.
Kadison's similarity theorem through uniform derivation estimatesOpen Problem
Motivation
A bounded algebra representation need not visibly preserve adjoints. The similarity problem asks whether one bounded change of Hilbert-space coordinates restores that structure. The pinned manuscript supplies the research context.
Setting
Representations are continuous unital complex algebra homomorphisms into bounded operators on a complete complex inner product space. The conjugating operator must have a bounded inverse.
The theorem states that, for every C*-algebra A in universe u and every complex inner product space K in universe v that is complete (a Hilbert space), every bounded unital representation of A on K is similar to a star representation. Here a bounded unital representation is a continuous ℂ-algebra homomorphism π from A into the algebra of bounded linear operators on K; being an algebra homomorphism of unital algebras, it preserves the identity. Similarity to a star representation means that there is an invertible bounded operator S on K, with bounded inverse, such that for every a in A, S π(a*) S⁻¹ equals the adjoint of S π(a) S⁻¹. Equivalently, the conjugated map a ↦ S π(a) S⁻¹ commutes with the involution. This is the Kadison similarity statement as a defined proposition SimilarityTheorem, and the source declares it as a theorem whose proof is admitted rather than supplied.
Significance and status
Similarity is the selected goal. The two commutator formulations and explicit hyperreflexivity estimate remain distinct references with their own constants and universes. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Difficulty
One operator S must work simultaneously for every algebra element. Uniform matrix-amplification estimates cannot acquire a dimension-dependent constant.
Formalization scope
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
Additional published targets are included as separate references:
An isomorphism of the free group factorsOpen Problem
Motivation
Group von Neumann algebras encode a free group's regular representation as an operator algebra. Whether the rank remains visible in that algebra is the motivating isomorphism problem. The pinned manuscript supplies the research context.
Setting
The parameter runs over extended nonnegative reals greater than one. Integer ranks use group factors, infinity uses countably many generators, and other parameters use the encoded stabilized corner model.
The theorem states that for any two extended nonnegative real parameters r and s, both strictly greater than 1 (so either may be infinite), the interpolated factors attached to r and s are isomorphic as C*-algebras with trace and topology, meaning the type of normal tracial equivalences between them is nonempty. The interpolated factor at a parameter is chosen by cases: for r = ∞ it is the group von Neumann algebra of the free group on countably many generators; for r equal to a natural number n it is the group von Neumann algebra of the free group on n generators; otherwise it is the corner pAp of the stabilization of the rank-two free group algebra, cut down by a selected star projection p whose stabilized projection trace is the real number 1/√(r−1), with the trace being the stabilized trace rescaled by the inverse of that value. Each carries its canonical trace or this rescaled trace and an ultraweak-type topology. A NormalTracialEquiv between two such models consists of a ℂ-linear star-algebra isomorphism that preserves the traces and is continuous in both directions for the given topologies.
Significance and status
The goal is a nonempty type of normal tracial equivalences between the precise interpolated models. Statements about fundamental groups are not separate attached targets. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Difficulty
The required equivalence must preserve the algebra, involution and trace, and be continuous in both directions for the specified topologies.
Formalization scope
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
Selected references
OpenAI, An isomorphism of the free group factors, preprint, 2026. Manuscript.
A Fock-space inequality and the Laughlin spectral gapOpen Problem
Motivation
A known zero-energy vector does not by itself give a uniform positive gap above it. The Laughlin problem asks for a lower bound controlling every competing antisymmetric state. The pinned manuscript supplies the research context.
Setting
At N particles set Q=3(N−1). States are complex functions on finite configurations, with antisymmetry under exchanging particles. The energy is a sum of squared pair-annihilation amplitudes.
The theorem states that there is a threshold N₀ ≥ 2 such that for every N ≥ N₀ and every antisymmetric complex-valued state ψ on N particles, each with local levels 0,…,Q where Q = 3(N−1), one has (1/25)·d(ψ)² ≤ E(ψ). Here a state assigns a complex number to each configuration a : Fin N → {0,…,Q}, and antisymmetric means that swapping the values at two distinct positions i and j negates ψ. The energy E(ψ) sums, over pairs i<j, over p = 0,…,2Q−2, and over configurations a with a_i = a_j = 0, the squared modulus of the pair amplitude, which is the sum over x,y of pairCoefficient(Q,p,x,y)·ψ(a with a_i replaced by x and a_j by y). The pair coefficient vanishes unless x+y = p+1, in which case it equals (x−y)/√2 times the square root of Q^{(x)}·Q^{(y)}·p! divided by Q·(2Q−2)^{(p)}·x!·y!, where m^{(k)} is the descending factorial. The Laughlin vector is built from the polynomial ∏{i<j}(x{i,0}x_{j,1} − x_{j,0}x_{i,1})³ in variables indexed by particle and a Boolean: its coefficient at the monomial with exponent a_i on x_{i,1} and Q−a_i on x_{i,0} is divided by ∏_i √C(Q,a_i). The quantity d(ψ)² is the infimum over complex c of the sum over configurations of |ψ(a) − c·Laughlin(a)|², the squared distance from ψ to the line spanned by the Laughlin vector, with no normalization of ψ assumed.
Significance and status
The selected goal has constant 1/25 and no normalization requirement on the state. The Fock-space inequality, the earlier 1/100 formulation and the planar endpoint are separate references; they retain their own representations and constants. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Difficulty
The bound must be uniform for all sufficiently large particle numbers and for every state, rather than a variational estimate on a selected excitation.
Formalization scope
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
Additional published targets are included as separate references:
Area-controlled end replacement and the Bondi Penrose inequality in the CKS classOpen Problem
Motivation
Replacing a hyperboloidal end by an asymptotically flat end can connect Bondi mass with ADM mass. The source seeks a replacement that preserves interior geometry, the energy condition, and almost all enclosing area. The source is OpenAI's September 2026 manuscript.
Setting
A CKS exterior datum describes a three-dimensional hyperboloidal end and its mass aspect. Its Bondi charge is energy-momentum (E,P), assumed strictly future timelike. An enclosing cut is a surface in the supplied geometric class; its area is computed from the metric.
For a connected, Hausdorff, second countable smooth 3-manifold N with boundary and a smooth Riemannian metric g with a smooth symmetric tensor field K, such that N is orientable, the boundary is compact and nonempty, g is complete, and (g,K) satisfies the pointwise local-chart physical dominant energy condition PhysicalDEC, the following holds. Suppose d is a CKS exterior-end datum for (g,K): a coordinate end outside radius d.chart.radius in which g and K are represented by smooth perturbations, together with a smooth mass aspect function on the sphere and the tensor patches realizing it. If the Bondi charge (energy, momentum) of d's mass aspect, (E,P), is timelike, meaning |P|<E, then there exist another such datum d', a radius R₀ with d'.chart.radius<R₀ and 12≤R₀, and a function ε with ε(R)→0 as R→∞, such that d' has Bondi charge (√(E²−|P|²),0), and the minimal enclosing area of g is finite. Moreover, for every R≥R₀ one has 0≤ε(R)<1 and there are a complete smooth metric gR, a smooth symmetric tensor field kR, spatial tensor fields G and k on Euclidean 3-space, and a number η with these properties. The pair (gR,kR) agrees with (g,K) at every point outside the chart domain or with chart coordinate norm at most R, and satisfies PhysicalDEC and integrable constraints. Also gR≥(1−ε(R))g as quadratic forms. On the end, gR and kR equal the end metrics built from G and k in d'.chart. Each Cartesian component of G minus the identity satisfies the order-1 Symbol condition from CKSADM, and k vanishes where ‖x‖>2R². As r→∞ the spatial ADM energy of G tends to √(E²−|P|²)+η and the ADM momentum of (G,k) tends to 0, with 0≤η≤2R^(−1/2). Finally, gR has finite minimal enclosing area, (1−ε(R)) times the minimum enclosing area of g is at most that of gR, and for every outer domain D the cut areas of g and gR are finite and satisfy (1−ε(R))·cutArea(g,D)≤cutArea(gR,D).
The selected goal constructs end replacements with zero limiting ADM momentum and quantitative area comparison, including minimum enclosing area. The Schwarzschild equality examples are attached as a separate target. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Difficulty
Changing the end can create a cheaper enclosing surface or violate the dominant energy condition. Agreement on each retained interior region does not alone prevent either problem.
Formalization scope
The manifold is a connected Hausdorff second-countable smooth three-manifold with compact nonempty boundary, and the original complete data satisfy the physical dominant energy condition. The main target is end replacement; it does not itself state the final Bondi–Penrose inequality. The equality-example target keeps its stronger boundary and no-additional-horizon hypotheses.
The shared definitions are supplied by CKSBondiPenrose, CKSBondiPenrose_002. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Selected references
OpenAI, Area-controlled end replacement and the Bondi Penrose inequality in the CKS class, preprint, September 2026. Manuscript.
Parabolic intersections in Artin groupsOpen Problem
Motivation
Standard generator subsets define natural subgroups in an Artin group. The source asks whether arbitrary conjugates of these subgroups remain in the same class after intersection. The source is OpenAI's September 2026 manuscript.
Setting
A standard parabolic subgroup is generated by a subset of the standard generators. A parabolic subgroup is any conjugate of one. There is no requirement that its Coxeter subgroup be finite.
Formalization targets
gAXg−1∩hAYh−1=kAZk−1for some Z⊆S,k∈AM.
The theorem, which is admitted in the source with a placeholder proof, states the following for a Coxeter matrix M on a finite, linearly ordered index set S, with Artin(M) the Artin group presented on generators S by the braid relations: the word of alternating generators s,t,s,... of length M(s,t) equals the alternating word beginning with t, for each pair s,t. For any two subsets X and Y of S and any two elements g and h of Artin(M), there exist a subset Z of S and an element k of Artin(M) such that the intersection of the two conjugate subgroups g P_X g⁻¹ and h P_Y h⁻¹ equals k P_Z k⁻¹. Here P_T is the standard parabolic subgroup generated by the images of the generators in T, and conjugation by g is the subgroup whose members x satisfy g⁻¹xg in P. There is no spherical-type or other restriction on M, so the intersection of two conjugates of standard parabolic subgroups is itself a conjugate of a standard parabolic subgroup.
The selected goal is closure under binary intersection. Attached results also give arbitrary intersections controlled by at most the rank many members, unique parabolic closure, and dynamics for irreducible non-clique groups. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Difficulty
Conjugation obscures the standard generating subsets, so intersecting X and Y alone does not describe the subgroup intersection. The target must produce both a new subset and a new conjugating element.
Formalization scope
The generating type is finite and linearly ordered. The Coxeter-matrix convention encodes an infinite label by zero. The dynamics milestone has additional irreducibility and non-clique assumptions; those are not imposed on the intersection theorem.
The shared definitions are supplied by ArtinParabolicIntersections. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Selected references
OpenAI, Parabolic intersections in Artin groups, preprint, September 2026. Manuscript.
Harmonic heights and the Artin K(pi,1) conjectureOpen Problem
Motivation
A classifying-space problem asks whether a natural complex captures a group without additional higher homotopy. The source addresses the finite-rank Artin problem through the lifted spherical-cell complex. The source is OpenAI's September 2026 manuscript.
Setting
An Artin group is presented by alternating braid relations from a Coxeter matrix. A subset of generators is spherical when its associated Coxeter parabolic subgroup is finite. Lifted cells pair a group element with such a subset, with incidence determined by reduced coset words.
Formalization targets
ContractibleSpace(SalvettiCover(M))for every Coxeter matrix M on finite S.
For every Coxeter matrix M indexed by a finite type S of standard generators, the topological space SalvettiCover(M) is contractible. The Artin group Artin(M) is the free group on S modulo the braid relators, one for each ordered pair (s,t): the alternating word s t s t ... of length M(s,t) times the inverse of the alternating word t s t s ... of the same length. A subset T of S is spherical when the standard parabolic subgroup of the Coxeter group generated by the simple reflections in T is finite. A lifted cell is a pair (a,T) of an Artin group element and a spherical subset. One lifted cell (a,T) is a face of (b,U) when T is contained in U and there is a word w in letters of U that is reduced in the Coxeter group (its Coxeter length equals the word length), is of minimal length in its coset with respect to the parabolic subgroup generated by T, and satisfies a = b times the image of w in the Artin group. The preorder on lifted cells is the reflexive transitive closure of this face relation, and SalvettiCover(M) is the geometric realization, as a topological space, of the nerve of that preorder viewed as a category.
The goal makes the full topological realization contractible, rather than only asserting vanishing of a selected homotopy group. It supplies a precise target for the covering-space component of the source. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Difficulty
Local spherical pieces need not automatically fit into a globally contractible realization. The face relation and its transitive closure must retain the interaction between Artin words and Coxeter length.
Formalization scope
SalvettiCover is the geometric realization of the nerve of the lifted-cell preorder. The generator type is finite but need not be equipped with a chosen enumeration. The mission preserves this published model instead of substituting a different complex.
The shared definitions are supplied by HarmonicArtin. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Selected references
OpenAI, Harmonic heights and the Artin K(pi,1) conjecture, preprint, September 2026. Manuscript.
All-temperature pressure for orthogonally invariant Ising spin glassesOpen Problem
Motivation
An Ising spin system probes a quadratic form only on cube vertices. The source asks whether random orthogonal eigenvectors allow its pressure to be determined by the limiting eigenvalue distribution at every positive temperature. The source is OpenAI's September 2026 manuscript.
Setting
The pressure is the normalized logarithm of the average Boltzmann weight under the uniform spin prior. Eigenvectors are Haar orthogonal, and the deterministic empirical eigenvalue laws converge weakly to a compactly supported probability law. The variational formula uses an edge-extended spectral transform.
Formalization targets
EPN(β)→Vβ,PN(β)→Vβalmost surely(β>0).
For a spin system on N Ising spins σ ∈ {−1,1}^N, the rotated pressure for eigenvalues λ₁,…,λ_N, an orthogonal rotation U and a field c is (1/N) times the log of the average over all 2^N spin configurations of exp(H(σ)), where H(σ) = (1/2)∑ᵢ λᵢ (Uσ)ᵢ² + ∑ᵢ cᵢσᵢ. The theorem states that, for any probability space (Ω,P), random N×N orthogonal matrices U_N that are measurable and whose laws are right-invariant under multiplication (Haar-type), and any deterministic eigenvalue arrays (eig_N,i), the following holds under these assumptions: ν is a probability measure on ℝ whose support lies in [a,b] and contains both a and b; for every ε>0, eventually in N all eigenvalues lie in [a−ε,b+ε]; the empirical spectral laws (1/N)∑ᵢ δ_{eig_N,i} converge weakly to ν; and the inverse temperature β is strictly positive. Then, with eigenvalues β·eig_N,i, rotation U_N(ω)⁻¹ and zero external field, the expected rotated pressure ∫ pressure dP converges as N → ∞, and the pressure itself converges for P-almost every ω, in both cases to the real part of the variational functional of the measureR transform of the β-rescaled law of ν, evaluated at the edge β·b.
The selected goal is the all-positive-temperature zero-field pressure theorem. The attached results also cover field laws, random spectra, Gaussian-pattern pressure and ground energy, and related norm limits under their stated assumptions. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Difficulty
Weak spectral convergence does not control rare extreme eigenvalues. The explicit no-outlier condition is essential to the selected statement’s comparison with the limiting spectral functional.
Formalization scope
The spin prior is uniform probability, and temperature is implemented by multiplying eigenvalues by β. The no-outlier condition holds eventually within every enlargement of the limiting support interval. Almost-sure convergence and expectation convergence are both conclusions; other attached variants keep their own uniform-integrability and field hypotheses.
The shared definitions are supplied by InvariantIsing. 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, All-temperature pressure for orthogonally invariant Ising spin glasses, preprint, September 2026. Manuscript.
An explicit exact Hausdorff gauge for SLEOpen Problem
Motivation
Hausdorff dimension identifies a critical power of scale but need not give a positive measure at that power. The source proposes an iterated-logarithm correction for ordinary chordal SLE curves. The source is OpenAI's September 2026 manuscript.
Setting
A Hausdorff gauge is continuous, nondecreasing on nonnegative radii, zero at zero, and positive at positive radii. Its metric measure charges a covering set according to its diameter. Chordal SLE is represented by a capacity-two Loewner trace driven by scaled Brownian motion.
Formalization targets
h(r)=r1+κ/8(loglog(1/r))(1−κ/8)/2for small r>0,Hh(γ([s,t]))>0(0<s<t).
For every probability space (Ω, P) and every κ with 0<κ<8, if γ is an ordinary chordal SLE_κ family of curves on Ω, then almost surely the explicit Hausdorff gauge measure of every positive-time segment of the curve is positive. Here γ being an ordinary chordal SLE_κ means that each γ(ω,t) is measurable in ω and that there is a standard real Brownian motion B on (Ω,P) such that, for almost every ω, the curve t↦γ(ω,t)∈ℂ with driving function U(t)=√κ·B_t(ω) is a capacity-two trace: γ is continuous, starts at 0, stays in the closed upper half-plane, and there are conformal-type maps G_t from the unbounded component of the upper half-plane minus γ[0,t] to the upper half-plane and inverse maps F_t back, holomorphic, mutually inverse, with G_0 the identity, satisfying the Loewner equation ∂_t G_t(z)=2/(G_t(z)−U(t)) (one-sided at t=0), the normalization z(G_t(z)−z)→2t as z→∞, and F_t(U(t)+iy)→γ(t) as y→0⁺. The gauge h:ℝ→ℝ is any function that is continuous, nondecreasing on [0,∞), zero at 0 and positive for r>0, and that coincides, for all sufficiently small r>0, with r^{1+κ/8}·(log log(1/r))^{(1−κ/8)/2}. The gauge measure is the Hausdorff-type metric measure on ℂ built from r↦h(r) (with the ENNReal-valued radius cast through its real part). The conclusion is that, for almost every ω, simultaneously for all times 0<s<t, this measure of the image set γ(ω)([s,t]) is strictly positive.
The formal goal establishes simultaneous positivity for every nontrivial positive-time compact segment. It is the lower-positivity component of the manuscript’s exact-gauge claim. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Difficulty
A dimension statement only determines a critical exponent; it does not decide the effect of a slowly varying correction. Positivity must hold for all segment times on one probability-one event.
Formalization scope
The parameter satisfies 0<κ<8. The goal does not assert finite measure, finite expected disk mass, or non-sigma-finiteness for a different gauge. The name sourceLowerMain_proved is a declaration name; its current theorem status is Open.
The shared definitions are supplied by SLELowerPositivity. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Selected references
OpenAI, An explicit exact Hausdorff gauge for SLE, preprint, September 2026. Manuscript.
Cutoff throughout the high-temperature Sherrington–Kirkpatrick phaseOpen Problem
Motivation
Cutoff means that a Markov chain’s transition from far from equilibrium to near equilibrium occurs in a negligible fraction of its mixing time. The source studies heat-bath dynamics for a disordered mean-field Ising model. The source is OpenAI's September 2026 manuscript.
Setting
The Sherrington–Kirkpatrick model has independent centered Gaussian pair couplings with variance β2/n and zero external field. One discrete update picks a site uniformly and resamples its spin from its conditional Gibbs law. Mixing time uses worst-case total variation distance.
For real parameters β with 0 ≤ β < 1/2, ε with 0 < ε < 1/2, and η > 0, two things hold for the Sherrington–Kirkpatrick model with n spins, where a disorder g is a real coupling for each pair i < j of sites and the Gibbs measure at zero external field has weight proportional to exp((1/2) Σᵢ Σⱼ σᵢ gᵢⱼ σⱼ) on spin configurations σ ∈ {±1}ⁿ (couplings symmetrized, diagonal zero). The dynamics is a heat-bath single-site chain: choose a site uniformly at random, then keep or flip its spin with probabilities proportional to the Gibbs masses of the two configurations (for n = 0 the transition matrix is the identity). The distance after k steps is the maximum over starting configurations of the total variation distance (half the ℓ¹ distance) between the k-step distribution and the Gibbs measure, and mixingTime(g, δ) is the least k whose distance is at most δ (the infimum of the set, so 0 if that set is empty). The disorder law makes the couplings independent centered Gaussians with variance β²/n. First, the probability under this law that the ratio mixingTime(g, ε) / mixingTime(g, 1 − ε) exceeds 1 + η tends to 0 as n → ∞. Second, for all sufficiently large n, every disorder g satisfies mixingTime(g, 1 − ε) > 0.
The available target gives ratio cutoff in probability over the disorder and eventual positivity of the denominator for every disorder. It isolates a precise mixing-time comparison. 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
Fast relaxation estimates alone do not prove that all fixed total-variation thresholds become asymptotically equivalent. The worst starting configuration and the random couplings both enter the comparison.
Formalization scope
The attached range is 0≤β<1/2, narrower than the full high-temperature range discussed in the manuscript. The target does not specify the cutoff location. Dynamics is discrete single-site updating; the exceptional n=0 transition is the identity.
The shared definitions are supplied by SKRatio. 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, Cutoff throughout the high-temperature Sherrington–Kirkpatrick phase, preprint, September 2026. Manuscript.
Complex Matrix Multiplication Below 2.258 and Rectangular BoundsOpen Problem
Motivation
Rectangular matrix products arise when the two outer dimensions are much larger than the inner dimension. The dual exponent records the largest inner growth rate compatible with arithmetic exponent two. The source manuscript presents the surrounding research claim.
Setting
For k∈[0,1], ω_ℂ(1,k,1) is the infimum of exponents for multiplying an n×⌈nᵏ⌉ matrix by a ⌈nᵏ⌉×n matrix over ℂ. The dual exponent α is the supremum of k for which this infimum equals two.
Formalization target
Prove the strict bound
αC>20093=0.465.
The additional published rectangular endpoint asserts ω_ℂ(1,709/1000,1)<523/250=2.092.
Strictness is part of both statements. The supplied goal concerns the complex dual exponent; the manuscript title’s square bound and broader field claims are not attached formal targets. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Difficulty
An algorithm for one size does not establish an asymptotic exponent. The definition quantifies over every positive slack and all positive sizes with one bound constant for each slack.
Formalization scope
Algorithms are division-free arithmetic programs with constants and input gates of cost zero and addition, subtraction and multiplication of cost one. Correctness is quantified over all input matrices. The dual exponent is a real supremum of exact exponent-two shapes, using the prescribed inner-dimension ceiling.
Riesz transforms and uniform rectifiability in higher codimensionOpen Problem
Motivation
Singular integral estimates can detect geometric regularity in a measure whose support has no given parametrization. The mission turns a uniform Riesz-transform bound into uniform pieces of Lipschitz images. The source manuscript presents the surrounding research claim.
Setting
Let μ be a regular measure in ℝᵈ, with d≥4 and 2≤n≤d−2. Ahlfors–David regularity means that μ(B(x,r)) is comparable to rⁿ on its support at admissible radii. Hard-truncated Riesz transforms use the kernel (x−y)/|x−y|^(n+1), excluding distances at most ε.
Formalization target
With fixed dimension and bounds C_AD,C_R, prove that there exist θ>0 and M≥0 such that every eligible μ satisfies
μ(B(x,r)∩rangeg)≥θrn
for some M-Lipschitz map g from the open n-dimensional radius-r ball, at every support point and admissible radius.
The constants θ and M are uniform across the entire class of measures with the prescribed analytic bounds. This is the exact quantitative ball-image conclusion. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Difficulty
Individual rectifiable pieces with constants depending on μ do not yield this quantifier order. The Riesz bound ranges over every positive hard truncation and every scalar L² input.
Formalization scope
Ambient space is EuclideanSpace ℝ (Fin d). Radii are positive and bounded by the extended support diameter. The hypothesis uses μ.Regular, nonnegative Riesz constants, MemLp and eLpNorm; the conclusion uses the actual measure of the intersection with a Lipschitz image. No endpoint codimensions are included.
Selected references
OpenAI, Riesz transforms and uniform rectifiability in higher codimension, preprint, 2026. Pinned manuscript.
An unconditional first moment for cubic Gauss sumsOpen Problem
Motivation
Cubic Gauss sums oscillate even after normalization. Their first moment asks whether this cancellation retains a precise lower-order bias when averaged over arithmetic primes. The source manuscript presents the surrounding research claim.
Setting
Work in the Eisenstein integers ℤ[ω], with ω=exp(2πi/3). A primary prime p is a prime element congruent to one modulo three. N(p)=|p|², G(p) is the normalized cubic Gauss sum, and c*=(2π)^(2/3)/(3Γ(2/3)).
Formalization target
At the real sharp cutoff X, establish
p primary primeN(p)≤X∑G(p)=56c∗logXX5/6+o(logXX5/6).
The two supporting targets compare each fixed angular mode to its explicit model and give cancellation for every nonzero mode.
The coefficient and scale specify the first moment, rather than only an order-of-magnitude estimate. Both conjugate prime elements are included when they satisfy the primary-prime predicate. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Difficulty
Pointwise estimates on G(p) do not isolate the X^(5/6)/log X bias. The error must be little-o at that scale with the exact arithmetic normalization.
Formalization scope
The published definitions use residue-class representatives, the cubic residue symbol, the trace exponential phase, and complex-valued cutoff sums. Little-o is taken as real X tends to positive infinity. Angular modes are integers held fixed before the limit.
Selected references
OpenAI, An unconditional first moment for cubic Gauss sums, preprint, 2026. Pinned manuscript.
Equidistribution of Prime-Degree Torus Packets with Arbitrary Local TypeOpen Problem
Motivation
Closed diagonal orbits encode lattices in totally real number fields. Their distribution tests whether arithmetic families fill the space of unimodular lattices as their discriminants grow. The source manuscript presents the surrounding research claim.
Setting
For a fixed prime n=d+1 ≥ 5, Xₙ is the quotient of SLₙ(ℝ) by its integral lattice subgroup. A packet consists of normalized full lattices of one local homothety type, including the specified sign translates. Its measure averages orbital probabilities with orbit-volume weights.
Formalization target
For any sequence of totally real degree-n fields and full lattices whose multiplier discriminants tend to infinity, prove
∃ν,ν is Haar probability,μi⇒ν,
and tightness of the entire family {μᵢ}. Weak convergence uses every bounded continuous real test function and includes the probability normalization of every μᵢ.
The conclusion addresses arbitrary local types and includes absence of escape of mass. The fixed-Haar formulation is also available as a supporting target. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Difficulty
Convergence on compactly supported tests alone would not establish the requested probability convergence on a noncompact quotient. The packet normalization and tightness must be justified uniformly through the discriminant limit.
Formalization scope
The source definitions use completed lattices over ℤₚ, diagonal-flow period covolumes and volume-weighted sums over distinct orbits. The theorem fixes prime degree at least five and allows both fields and local types to vary. Both published formulations and their shared definitions are referenced.
Selected references
OpenAI, Equidistribution of Prime-Degree Torus Packets with Arbitrary Local Type, preprint, 2026. Pinned manuscript.
Uniform exclusion of Landau–Siegel zerosOpen Problem
Motivation
Real zeros of Dirichlet L-functions close to one obstruct uniform estimates for primes in arithmetic progressions. A conductor-independent logarithmic gap is the precise quantitative issue addressed here. The source manuscript presents the surrounding research claim.
Setting
A Dirichlet character χ modulo an integer q is primitive, nonprincipal, and real-valued when its complex values have zero imaginary part. Its analytically continued L-function is denoted L(s,χ). The zero β is real and lies strictly between zero and one; log is the natural logarithm.
Formalization target
Prove that one positive real constant works for every allowed modulus, character and zero:
This is the uniform zero-gap conclusion itself, not a statement for a bounded family of conductors. The source dated October 1, 2026 states this as its principal result. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Difficulty
A bound whose constant varies with the character cannot establish this quantifier order. The arithmetic and analytic estimates must retain one positive constant across every conductor and every real primitive character.
Formalization scope
The goal uses Mathlib’s actual Dirichlet characters and L-functions over ℂ, with q : ℕ, a nonzero instance and q ≥ 3. Both available published formulations are referenced. The second formulation merely groups the zero hypotheses differently and is not presented as an independent milestone. The manuscript’s interpolation and determinant lemmas have no supplied published theorem IDs and are not attached as milestones.
Selected references
OpenAI, Uniform exclusion of Landau–Siegel zeros, preprint, 2026. Pinned manuscript.
Global classical solutions of the three-dimensional relativistic Vlasov–Maxwell systemResearch Paper
Motivation
The relativistic Vlasov–Maxwell system is the basic kinetic model of a collisionless plasma: a cloud of charged particles, described by a phase-space density, moves under the electromagnetic field it generates, and the field evolves by Maxwell's equations with the particles as sources. Whether smooth, compactly supported data in three dimensions always produce a solution that stays smooth for all time has been the central question about the Cauchy problem for this system since the 1980s. Weak solutions exist globally, but they come without regularity or uniqueness, and every previous global classical result required smallness, a dimensional reduction, symmetry, or a nearby global reference solution.
This mission asks for a machine-checked proof of global existence and uniqueness of classical solutions for arbitrary smooth admissible data, as claimed in an OpenAI preprint dated September 23, 2026 (source). The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal below is open.
Timeline
1984 — Wollman proves local existence and uniqueness of classical solutions (CPAM 1984).
1986 — Glassey and Strauss show that a classical solution continues as long as the momentum support stays bounded (ARMA 1986); in 1987 they prove global existence for initially dilute plasmas (CMP 1987).
1985–1998 — Glassey and Schaeffer obtain global classical solutions for symmetric relativistic Vlasov–Poisson (CMP 1985) and for reduced Vlasov–Maxwell models in one and one-half, two and one-half, and two dimensions (1990, 1997, 1998).
1989 — DiPerna and Lions prove global existence of weak solutions for large data (CPAM 1989); Rein treats the relativistic case directly (CMS 2004).
1990 — Rein proves stability of global existence near suitable global solutions (CMP 1990).
2002–2003 — New proofs of the continuation criterion by Klainerman–Staffilani (CPAA 2002) and Bouchut–Golse–Pallard (ARMA 2003).
2004–2016 — Refined continuation criteria: Schaeffer's small-data theorem with momentum tails (IUMJ 2004), Pallard (IUMJ 2005), Luk and Strain's two-dimensional projection criterion (CMP 2014) and moment bounds (ARMA 2016).
2020–2025 — Small-particle global results with large fields: Bigorgne (CMP 2020; APDE 2025), Wei–Yang (CMP 2021).
September 2026 — The OpenAI preprint claims the general large-data result without symmetry (Theorem 1.1, p. 3).
Setting
For momentum v∈R3 let q(v)=1+∣v∣2 and u(v)=v/q(v) (the relativistic velocity, ∣u∣<1). The unknowns are a particle density f(t,x,v)≥0 and fields E(t,x),B(t,x)∈R3, with charge and current densities ρf=∫fdv and jf=∫u(v)fdv. In the one-species normalization the system is
A smooth admissible datum(f0,E0,B0) has f0∈Cc∞(Rx3×Rv3), f0≥0, E0,B0 smooth with every derivative bounded and E0,B0∈L2, and satisfies ∇⋅E0=ρf0, ∇⋅B0=0. A classical solution on [0,∞) is a C1 triple solving the system pointwise, with E,B continuous in time with values in L2, and with f(t,⋅,⋅) supported in a fixed compact set on each bounded time interval.
Formalization targets
Goal: Theorem 1.1 (p. 3)
Every smooth admissible datum generates a classical solution on [0,∞) with the given initial values; for every finite T the solution is C∞ on [0,T]×R6 (respectively [0,T]×R3 for the fields) with compact phase-space support on [0,T]; and any other classical solution with the same datum agrees with it at every t≥0. This is OAI.RVM.global_classical_solution.
Significance
The result itself. It settles the large-data global classical regularity problem for three-dimensional relativistic Vlasov–Maxwell, with no size, symmetry or neutrality assumption; nonzero total charge with its Coulomb tail is allowed. Global well-posedness at this level is the starting point for questions about long-time behaviour, scattering and stability of plasma equilibria that previously could only be posed for small or symmetric data.
Formalizing it. The proof combines the Glassey–Strauss representation of fields along backward light cones, energy-flux estimates, a delicate signed bootstrap, and local well-posedness and continuation theory. None of this PDE infrastructure (wave-equation representation formulas, characteristics of transport equations in phase space, Sobolev local theory) is currently available in a proof assistant at the needed level, so each component is reusable.
Difficulty
By the Glassey–Strauss criterion it suffices to bound the momentum support on finite time intervals. The natural approach estimates the absolute value of the force along a characteristic using the retarded field representation and energy flux through light cones. At receiver energy w this loses a factor w relative to what is needed (Section 1.2, p. 4); the loss comes from sources whose velocity is much closer to the light ray than the receiver's. The preprint instead estimates the signed momentum increment VX(t2)−VX(t1), integrating the retarded force along source trajectories before taking norms (Proposition 2.1, p. 5; Lemma 6.1, p. 24), controls direction changes (Lemma 7.1, p. 29), and closes a bootstrap whose time-to-double lower bounds have a divergent sum (Section 9).
Formalization scope
Space and momentum are EuclideanSpace ℝ (Fin 3); derivatives are Fréchet derivatives in coordinate directions; the time derivative is derivWithin on [0,∞), so t=0 is one-sided.
Admissible encodes C∞ with compact support and nonnegativity for f0; ContDiff ℝ ∞ with all iterated derivatives bounded and MemLp 2 for E0,B0; and both Gauss constraints pointwise.
Classical requires C1 regularity on the closed half-spaces, f≥0, continuity of t↦E(t),B(t) into L2 on [0,∞), compact phase support on each [0,T], all five equations pointwise for t≥0 (including both constraints), and the initial values.
The conclusion asserts existence, smoothness on every finite horizon, and uniqueness within the same classical class; uniqueness is pointwise equality at all t≥0. The hypotheses are satisfiable (e.g. f0=0, E0=B0=0), so the statement is not vacuous.
ρ and j are Bochner integrals in v; for compactly supported f these are the genuine moments.
R. T. Glassey, W. A. Strauss, Singularity formation in a collisionless plasma could occur only at high velocities, Arch. Ration. Mech. Anal. 92 (1986). https://doi.org/10.1007/BF00250732
R. T. Glassey, W. A. Strauss, Absence of shocks in an initially dilute collisionless plasma, Comm. Math. Phys. 113 (1987). https://doi.org/10.1007/BF01223511
J. Luk, R. M. Strain, A new continuation criterion for the relativistic Vlasov–Maxwell system, Comm. Math. Phys. 331 (2014). https://doi.org/10.1007/s00220-014-2108-8
F. Bouchut, F. Golse, C. Pallard, Classical solutions and the Glassey–Strauss theorem for the 3D Vlasov–Maxwell system, Arch. Ration. Mech. Anal. 170 (2003). https://doi.org/10.1007/s00205-003-0265-6
X. Wang, Large data global solution of the 3D RVM system with cylindrical symmetry, arXiv:2203.01199 and arXiv:2607.14685 (2026). https://arxiv.org/abs/2607.14685v1
Uniform Bi-Holder Transport from Weak MTWResearch Paper
Motivation: when are optimal transport maps continuous?
Given two probability densities ρ0,ρ1 on a compact Riemannian manifold, optimal transport with the quadratic cost c(x,y)=d(x,y)2/2 seeks the map T pushing ρ0vol to ρ1vol at least total cost. McCann proved that such a map exists and is unique almost everywhere (McCann 2001). Whether it is continuous when the densities are merely bounded above and below depends on the geometry of the cost: the Ma–Trudinger–Wang (MTW) condition, a sign condition on a fourth derivative of c, is the decisive curvature hypothesis, and its weak form is known to be necessary. The question is whether weak MTW is also sufficient on every compact manifold, with estimates that do not degenerate as transport graphs approach conjugate points.
Background
1992 — Caffarelli's regularity theory for maps with convex potentials, based on sections and contact-volume comparison (Caffarelli 1992).
2001 — McCann's polar factorization on Riemannian manifolds (McCann 2001).
2005 — Ma, Trudinger and Wang introduce the curvature condition (MTW 2005).
2009 — Loeper links MTW to supporting cost functions and shows its necessity for continuity (Loeper 2009).
2010 — Loeper and Villani: uniform estimates under strict MTW and nonfocality (Loeper–Villani 2010).
2011 — Figalli, Rifford and Villani: transport continuity implies convex injectivity domains and weak MTW; on surfaces continuity is equivalent to their conjunction, and the equivalence with weak MTW alone is posed (FRV 2011).
2013 — Figalli, Kim and McCann: Hölder continuity and injectivity of optimal maps under weak MTW with cost-convexity hypotheses (FKM 2013), and products of round spheres (FKM 2013).
2015 — Figalli, Gallouët and Rifford: weak MTW implies convex injectivity domains on nonfocal manifolds (FGR 2015).
2019 — Lebedeva, Petrunin and Zolotov list the convexity and continuity questions (LPZ 2019, Questions 8.6–8.7).
2026 — Two OpenAI preprints (OpenAI Math Release, September 25, 2026): a companion proving that weak MTW forces convex injectivity domains and global support, and Uniform Bi-Hölder Transport from Weak MTW (this mission), claiming uniform bi-Hölder optimal maps for every density-bounded class. Neither is peer reviewed, and the theorem is not formally verified.
Setting
Let (M,g) be a smooth, connected, compact Riemannian manifold without boundary, of dimension n≥2, with distance d and volume vol. Put c(x,y)=21d(x,y)2 and let
I(x)={p∈TxM:d(x,expx(ap))=a∣p∣ for some a>1}
be the open injectivity domain. Weak MTW: for every p∈I(x) and ξ⊥η in TxM,
−23∂s2∂t2∂4c(expx(tξ),expx(p+sη))s=t=0≥0.
For 0<λ≤Λ, the density class consists of measurable ρ with ∫ρdvol=1 and λ≤ρ≤Λ almost everywhere. An optimal map from ρ0 to ρ1 is a measurable T with T#(ρ0vol)=ρ1vol minimizing ∫c(x,T(x))ρ0(x)dvol among such maps.
In Lean, metricVolume n is the n-dimensional Hausdorff measure normalized to agree with Lebesgue measure on Rn (which equals Riemannian volume), riemannianExp is defined from complete geodesics, and WeakMTW uses iteratedDeriv 2 twice.
Formalization targets
Goal: uniform bi-Hölder optimal maps
Fix (M,g) satisfying weak MTW and 0<λ≤Λ with a nonempty density class. There are α∈(0,1] and C<∞, depending only on (M,g),λ,Λ, such that for all densities ρ0,ρ1 in the class, the almost-everywhere unique optimal map has a homeomorphic representative T with
d(Tx,Tx′)≤Cd(x,x′)α,d(T−1y,T−1y′)≤Cd(y,y′)α.
This is Theorem 1.1 of the source. The goal is published on the platform with status Open.
Significance
The result itself. The constants are common to the whole density class; they do not depend on the densities or their derivatives, and the theorem allows conjugate cut points without nonfocality, strict MTW, or cut avoidance. Combined with the necessity result of Figalli–Rifford–Villani it gives the equivalence of weak MTW with transport continuity for bounded densities on compact manifolds, with uniform estimates in the forward direction. No explicit exponent is obtained (the positive exponent comes from a contradiction argument).
Formalizing it. The Lean statement packages existence, almost-everywhere uniqueness, homeomorphic regularity and uniform bi-Hölder bounds in one assertion over all density pairs, making precise what "class-uniform" means. A proof requires the companion geometric results (convex injectivity domains, global support), McCann's theorem, and Caffarelli-type section estimates on manifolds — none currently in Mathlib.
Difficulty
Hölder estimates obtained after localizing near a smooth part of the cost give a density-dependent exponent and localization scale; they do not give a common scale or constant for a family whose transport graphs approach conjugate pairs, where the cost stops being smooth. Weak MTW constrains the cost only where it is smooth and only for orthogonal directions. Earlier uniform results needed strict MTW and nonfocality, or special geometry (products of spheres).
Formalization scope
Volume is the normalized Hausdorff measure euclideanVolumeFactor n • μH[n]; densities are AEMeasurable, integrable, of mass one, and between lam and cap almost everywhere; nonemptiness of the class is a hypothesis, as in the source.
IsOptimalMap requires measurability, the pushforward identity for withDensity measures, and minimality among all measurable maps with that pushforward; uniqueness is almost everywhere for ρ0vol.
The conclusion requires one α∈(0,1] and one C≥0 before quantifying over densities, and a homeomorphism M ≃ₜ M with the same exponent and constant for T and T−1; a trivializing choice is excluded because T must itself be optimal.
Weak MTW is a hypothesis only at p∈I(x) and orthogonal ξ,η.
Needed infrastructure: Riemannian geodesics and cut locus, semiconvex potentials, Kantorovich duality and McCann's theorem, Hausdorff measure versus Riemannian volume, Caffarelli-type sections.
R. J. McCann, Polar factorization of maps on Riemannian manifolds, Geom. Funct. Anal. 11 (2001), 589–608. https://doi.org/10.1007/PL00001679
X.-N. Ma, N. S. Trudinger and X.-J. Wang, Regularity of potential functions of the optimal transportation problem, Arch. Ration. Mech. Anal. 177 (2005), 151–183. https://doi.org/10.1007/s00205-005-0362-9
G. Loeper and C. Villani, Regularity of optimal transport in curved geometry: the nonfocal case, Duke Math. J. 151 (2010), 431–485. https://doi.org/10.1215/00127094-2010-003
A. Figalli, L. Rifford and C. Villani, Necessary and sufficient conditions for continuity of optimal transport maps on Riemannian manifolds, Tohoku Math. J. 63 (2011), 855–876. https://doi.org/10.2748/tmj/1325886291
A. Figalli, Y.-H. Kim and R. J. McCann, Hölder continuity and injectivity of optimal maps, Arch. Ration. Mech. Anal. 209 (2013), 747–795. https://doi.org/10.1007/s00205-013-0629-5
A. Figalli, Y.-H. Kim and R. J. McCann, Regularity of optimal transport maps on multiple products of spheres, J. Eur. Math. Soc. 15 (2013), 1131–1166. https://doi.org/10.4171/JEMS/388
A. Figalli, T. O. Gallouët and L. Rifford, On the convexity of injectivity domains on nonfocal manifolds, SIAM J. Math. Anal. 47 (2015), 969–1000. https://doi.org/10.1137/140961821
The Isoperimetric Conjecture for the Cubic Flat Three-TorusResearch Paper
Motivation
The isoperimetric problem asks, for each prescribed volume, for the regions of least boundary area. In Euclidean space the answer is the round ball. In a compact space with topology the answer changes with the volume: small regions still look like balls, but larger regions can save area by wrapping around the space. The unit cubic flat three-torus R3/Z3 is the simplest compact example in three dimensions, and the periodic isoperimetric problem on it is equivalent, by reflection, to the relative isoperimetric problem in a cube. It is a standard test case for how local Euclidean geometry interacts with global topology, and it has been studied in connection with periodic minimal and constant-mean-curvature surfaces (Hauswirth–Pérez–Romon–Ros 2004; Ros 2005).
The conjectured answer is a sequence of three phases: balls, solid circular tubes around shortest closed geodesics, and slabs between parallel coordinate tori, followed by their complements. This mission asks for a machine-checked proof of that conjecture, including the classification of every minimizer, as claimed in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal below is open.
Timeline
1972 — Hadwiger proves that a coordinate cut minimizes at half volume for the cube (Monatsh. Math. 1972).
1992–1996 — Ritoré and Ros develop stability and structure results for constant-mean-curvature surfaces in flat three-manifolds (Comment. Math. Helv. 1992; Trans. AMS 1996); Ritoré's thesis records Hsiang's coordinate reflection symmetry (1994).
2000 — Barthe and Maurey recover Hadwiger's half-volume result by Gaussian comparison (Ann. IHP 2000). Morgan and Johnson's small-volume comparison implies that balls minimize for sufficiently small volume on compact flat manifolds (Indiana Univ. Math. J. 2000, Theorem 4.4).
2004 — Hauswirth, Pérez, Romon and Ros state the ball–tube–slab prediction and prove that a nonstandard minimizing boundary is connected of genus 2, 3 or 4, with curvature–area bounds (Trans. AMS 2004).
2005 — Ros's survey records the conjecture for the cubic torus and cube (Clay Math. Proc. 2, 2005, Section 1.6).
2013 — Acerbi, Fusco and Morini prove that slabs are the only minimizers near half volume (Comm. Math. Phys. 2013, Theorem 5.3), without effective ranges.
2026 — Milman obtains effective ranges for the phases, including the ball phase up to volume fraction 0.120582…, and reduces the profile conjecture to the two transition volumes 4π/81 and 1/π (Comm. Pure Appl. Math. 2026, Theorems 1.2–1.3).
September 2026 — The OpenAI preprint claims the full conjecture with all equality cases (Theorem 1.1, p. 1).
Setting
Let T=R3/Z3 with its flat metric and volume measure ∣⋅∣ (total volume 1). For a measurable E⊆T, its perimeter is the De Giorgi perimeter
P(E)=sup{∫EdivF:F a smooth vector field on T,∣F∣≤1}∈[0,∞],
which equals the boundary area when ∂E is smooth, and is insensitive to null-set changes. E has finite perimeter if P(E)<∞. A minimizer at volume V is a finite-perimeter E with ∣E∣=V and P(E)≤P(F) for all finite-perimeter F with ∣F∣=V.
For 0<V<1 put v=min(V,1−V) and
I(V)=min{(36π)1/3v2/3,2πv,2}.
The three expressions are the perimeters of a ball of volume v, a solid circular tube of volume v around a shortest closed geodesic (a coordinate circle of length 1), and a slab of width v between two coordinate tori. The branches cross at V1=4π/81 and V2=1/π.
Formalization targets
Goal: Theorem 1.1 (p. 1)
For every V∈(0,1):
a minimizer at volume V exists;
every minimizer has perimeter exactly I(V);
a set E is a minimizer at volume V≤1/2 if and only if, up to an isometry of T and a null set, it is a ball of radius (3V/(4π))1/3 when V≤4π/81, a solid tube of radius V/π about a shortest closed geodesic when 4π/81≤V≤1/π, or a slab of width V between coordinate tori when 1/π≤V; for V>1/2 the minimizers are exactly the complements of those at volume 1−V.
The ranges are closed, so at each transition volume both adjacent types are minimizers and there are no others. This is OAI.CubicTorus.unit_cubic_isoperimetric.
Significance
The result itself. It determines the isoperimetric profile of the cubic three-torus and the reflected relative profile of the unit cube at every volume, settling a conjecture explicitly posed by Hauswirth–Pérez–Romon–Ros and Ros. The equality classification at the transitions is new even granting Milman's reduction, which classifies minimizers on the open branches once the endpoint values are known but leaves extra co-minimizers at 4π/81 and 1/π to be excluded.
Formalizing it. The proof combines geometric measure theory (existence and regularity of minimizers), structure theorems for stable CMC surfaces, a differential inequality for the profile, and certified one-variable numerics. A formal proof would certify the whole chain; existence and regularity of isoperimetric regions in a flat torus are themselves substantial missing library pieces. No machine-checked version of the result, or of the Euclidean isoperimetric inequality for finite-perimeter sets in this generality, is known to exist.
Difficulty
The main obstruction is to rule out minimizers whose boundary is a connected surface of genus 2, 3 or 4 (Theorem 2.1, p. 3, quoting Hauswirth–Pérez–Romon–Ros). The general curvature–area bound and the profile differential inequality (Lemma 2.3, p. 4) exclude such surfaces away from the transitions but not at V1,V2 themselves. At the cylinder–slab transition V2=1/π, the planar isoperimetric inequality applied to horizontal sections leaves a deficit in a central curvature range; the preprint closes it with a calibration of a corner section, a nesting argument for planar sections, and a Jensen estimate (Section 6, Proposition 6.7, p. 19), supplemented by certified numerical bounds (Appendix B).
Formalization scope
The torus is PiLp 2 (fun _ : Fin 3 => AddCircle 1), whose metric is the flat torus metric; volume is the pushforward of Lebesgue measure on the half-open unit cube.
Perimeter is the De Giorgi supremum over C∞Z3-periodic vector fields on R3 with ∣F∣≤1, valued in ℝ≥0∞; no regularity of E is assumed. Finite perimeter also requires null-measurability.
Minimizers are global: the comparison ranges over all finite-perimeter sets of the same volume.
The canonical ball is the metric ball about 0; the tube is {x:∥x1∥2+∥x2∥2<V/π} around the x0-direction geodesic; the slab is {x:∥x0∥<V/2}. CongruentAE allows any isometry of T followed by a null-set change.
The phase ranges are closed, so both types are included at ties, matching the source. The statement is not vacuous: existence is part of the conclusion, and the profile value is a concrete real number.
Useful reusable infrastructure: sets of finite perimeter on flat tori, compactness and lower semicontinuity of perimeter, and the Euclidean isoperimetric inequality.
E. Milman, Isoperimetric inequalities on slabs with applications to cubes and Gaussian slabs, Comm. Pure Appl. Math. 79 (2026), 1012–1072. https://doi.org/10.1002/cpa.70020
E. Acerbi, N. Fusco, M. Morini, Minimality via second variation for a nonlocal isoperimetric problem, Comm. Math. Phys. 322 (2013), 515–557. https://doi.org/10.1007/s00220-013-1733-y
M. Ritoré, A. Ros, Stable constant mean curvature tori and the isoperimetric problem in three space forms, Comment. Math. Helv. 67 (1992), 293–305. https://doi.org/10.1007/BF02566501
Smooth counterexamples to Yau's nodal upper bound in dimensions three and fourResearch Paper
Motivation
The nodal set of a Laplace eigenfunction is the set where it vanishes. In 1982 Yau asked whether, on a fixed smooth closed Riemannian manifold of dimension d, the (d−1)-dimensional measure of the nodal set of every eigenfunction with eigenvalue λ is comparable to λ from above and below (Yau, Problem section, Annals of Math. Studies 102, 1982). The conjectured two-sided bound
cgλ≤Hgd−1(Zu)≤Cgλ,
with constants depending only on the metric, has organized several decades of work on unique continuation and quantitative zero sets of elliptic equations. The lower and upper inequalities are logically separate, and a fixed metric must be distinguished from a metric chosen anew for each eigenvalue.
After Logunov, the smooth upper bound was known to be polynomial in λ but not of order λ. The source of this mission, an OpenAI preprint dated September 23, 2026, claims that the upper bound fails for fixed smooth metrics in dimensions three and four.
Setting
Let (M,g) be a closed connected smooth Riemannian manifold of dimension d. In local coordinates, with ∣g∣=det(gij) and (gij) the inverse matrix, the Laplace–Beltrami operator is Δgu=∣g∣−1/2∂i(∣g∣1/2gij∂ju). An eigenfunction with eigenvalue λ>0 is a nonzero real u with −Δgu=λu; its nodal set is Zu={u=0}, measured by Hgd−1, Hausdorff measure for the Riemannian distance of g.
The round metricg∗ on S3⊂R4 is the pullback of the Euclidean inner product. A C∞ neighborhood of g∗ is any set of metrics containing all g whose coefficient functions, in finitely many charts and on compact subsets, have derivatives up to some order within ε of those of g∗.
Formalization targets
Goal: Theorem 1.1 (three-sphere)
For every C∞ neighborhood N of g∗ there are g∞∈N, nonzero smooth uj and λj>0 with
−Δg∞uj=λjuj,λj→∞,λjHg∞2(Zuj)→∞.
Lean: OAI.YauCounterexamples.sphere_three, open on the platform.
Milestone: Theorem 1.2 (four-manifold)
There are a smooth metric g∞ on S2×T2, nonzero smooth uj and λj→∞ with −Δg∞uj=λjuj and Hg∞3(Zuj)/λj→∞.
Significance
Theorem 1.1 disproves the upper-bound half of Yau's conjecture for smooth metrics already in dimension three, with metrics arbitrarily close to the round sphere, where the bound does hold. Neither theorem asserts a power-law excess, and neither contradicts the lower bound. Together with the companion preprints of this family (a sharp λ upper bound on smooth surfaces, and power-law violations in dimension at least five) it would locate the boundary of validity of the upper bound by dimension. The result is claimed in an OpenAI preprint that has not been peer reviewed, and no machine-checked proof exists.
Difficulty
Approximate eigenfunctions (quasimodes) with large nodal sets are comparatively easy to build locally. The obstacle is to replace each quasimode by an exact eigenfunction of an ordinary Laplace–Beltrami operator of one fixed metric, while keeping every sign change that witnesses nodal measure, and to do this for infinitely many eigenvalues at once with corrections that converge in C∞. A scalar potential or conductivity correction would be easy, but the operator must be a genuine metric Laplacian, which imposes a determinant identity between conductivity and density; the paper uses different, dimension-specific repairs in dimensions three and four. Also, the nodal set is not assumed regular, so its measure must be bounded below by a stable, lower semicontinuous count of sign changes.
Formalization scope
SmoothMetric E M is Mathlib's ContMDiffRiemannianMetric on the tangent bundle. Sphere 3 is the unit sphere of EuclideanSpace ℝ (Fin 4) with its standard charts; the four-manifold is Sphere 2 × (Circle × Circle).
laplaceBeltrami g u x is the coordinate formula above, in the chart at x with coordinates from Module.finBasis; only values in the open chart target are used.
IsSmoothNeighborhood g₀ N: some finite list of compact-chart derivative tests and one ε>0 such that every metric passing them lies in N. Quantifying over all such N is the C∞ topology.
nodalMeasure g d u is Measure.hausdorffMeasure d of {u=0} for the path distance of g itself (EMetricSpace.ofRiemannianMetric), not the distance inherited from R4.
HasUnboundedNodalRatio g d asks for smooth nonzero eigenfunctions with positive eigenvalues tending to ∞, finite nodal measures, and ratio Hd−1/λ→∞. Finiteness rules out the degenerate reading where an infinite measure would become 0 under toReal; it holds for every eigenfunction of a smooth metric on a compact manifold (Hardt–Simon).
A complete development needs elliptic regularity and perturbation theory for simple eigenvalues of metric Laplacians, WKB-type quasimode constructions, and Hausdorff-measure lower bounds from sign changes along segments. Contributions formalizing the named propositions (Proposition 2.6 spherical profiles, Proposition 3.6 simultaneous wave realization, Proposition 4.4 exactification, Proposition 6.2 one construction step) are welcome.
A. Logunov, Nodal sets of Laplace eigenfunctions: proof of Nadirashvili's conjecture and of the lower bound in Yau's conjecture, Ann. of Math., 2018. https://doi.org/10.4007/annals.2018.187.1.5
A. Logunov, E. Malinnikova, Nodal sets of Laplace eigenfunctions: estimates of the Hausdorff measure in dimensions two and three, 2018. https://doi.org/10.1007/978-3-319-59078-3_17
H. Hezari, Upper bounds on the size of nodal sets for Gevrey and quasianalytic Riemannian manifolds, Commun. Math. Phys., 2023. https://doi.org/10.1007/s00220-023-04853-z