Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
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 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.
Let with its flat metric and volume measure (total volume ). For a measurable , its perimeter is the De Giorgi perimeter
which equals the boundary area when is smooth, and is insensitive to null-set changes. has finite perimeter if . A minimizer at volume is a finite-perimeter with and for all finite-perimeter with .
For put and
The three expressions are the perimeters of a ball of volume , a solid circular tube of volume around a shortest closed geodesic (a coordinate circle of length ), and a slab of width between two coordinate tori. The branches cross at and .
For every :
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.
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 and 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.
The main obstruction is to rule out minimizers whose boundary is a connected surface of genus , or (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 themselves. At the cylinder–slab transition , 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).
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.ℝ≥0∞; no regularity of is assumed. Finite perimeter also requires null-measurability.CongruentAE allows any isometry of followed by a null-set change.Useful reusable infrastructure: sets of finite perimeter on flat tori, compactness and lower semicontinuity of perimeter, and the Euclidean isoperimetric inequality.
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 , the -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
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.
Let be a closed connected smooth Riemannian manifold of dimension . In local coordinates, with and the inverse matrix, the Laplace–Beltrami operator is . An eigenfunction with eigenvalue is a nonzero real with ; its nodal set is , measured by , Hausdorff measure for the Riemannian distance of .
The round metric on is the pullback of the Euclidean inner product. A neighborhood of is any set of metrics containing all whose coefficient functions, in finitely many charts and on compact subsets, have derivatives up to some order within of those of .
For every neighborhood of there are , nonzero smooth and with
Lean: OAI.YauCounterexamples.sphere_three, open on the platform.
There are a smooth metric on , nonzero smooth and with and .
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.
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 . 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.
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 such that every metric passing them lies in N. Quantifying over all such N is the topology.nodalMeasure g d u is Measure.hausdorffMeasure d of for the path distance of g itself (EMetricSpace.ofRiemannianMetric), not the distance inherited from .HasUnboundedNodalRatio g d asks for smooth nonzero eigenfunctions with positive eigenvalues tending to , finite nodal measures, and ratio . Finiteness rules out the degenerate reading where an infinite measure would become 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.
The nodal set of a Laplace eigenfunction is the set where it vanishes. On a vibrating membrane these are the curves that stay at rest (Chladni patterns), and in quantum mechanics they are the points where a stationary wave function has zero amplitude. A basic question is how large the nodal set is as the frequency grows. Yau conjectured in 1982 that on a smooth closed -dimensional Riemannian manifold the -dimensional measure of the nodal set of an eigenfunction with eigenvalue is comparable to , from above and below, with constants depending only on the manifold (Yau, Problem section, Annals of Math. Studies 102, 1982). The question is a test case for unique continuation and quantitative control of the zeros of solutions to elliptic equations.
The source of this mission, an OpenAI preprint dated September 23, 2026, claims the sharp upper bound on every smooth closed surface, which together with Brüning's lower bound would settle Yau's conjecture in dimension two.
Let be a closed (compact, without boundary) connected smooth Riemannian surface. In local coordinates write , and for the inverse matrix. The Laplace–Beltrami operator is
A Laplace eigenfunction with eigenvalue is a nonzero real function with . Its nodal set is , and its nodal length is , the one-dimensional Hausdorff measure for the Riemannian distance .
The constant depends only on the surface and its metric and is the same for every eigenfunction in every positive eigenspace. The Lean statement OAI.SharpNodal.Main asserts MainStatement M; it is open on the platform.
The order is optimal: Brüning's lower bound shows it cannot be improved, and on the round sphere spherical harmonics attain it. Before this work the best smooth-surface upper bound was . A sharp upper bound on every smooth surface, combined with the known lower bounds, would resolve Yau's conjecture for smooth closed surfaces; in dimensions three and higher the smooth upper bound remains a separate question (the companion missions in this family address it).
The theorem is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists. A formal proof would certify a long chain of quantitative estimates (Carleman inequalities, multiscale subdivision, packing), each of which is a natural target for reuse in other unique-continuation problems.
For a real-analytic metric, an eigenfunction extends holomorphically and its zeros can be counted by complex-analytic methods; this is how Donnelly and Fefferman obtain . For a merely smooth metric no such extension exists. The standard route bounds nodal length on each wavelength-sized square by the local doubling exponent (growth of the norm from a disk to a larger disk). The known bounds on individual doubling exponents are too weak: a square can have growth much larger than average, and summing worst-case local bounds loses a power of . What is needed is control of the average growth over all wavelength-scale squares, while allowing large values on individual squares.
M with [MetricSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 2)) M] [IsManifold 𝓘(ℝ, Plane) ∞ M], a smooth RiemannianBundle on the tangent bundle, and [IsRiemannianManifold 𝓘(ℝ,Plane) M], so the metric-space distance is the Riemannian distance. CompactSpace and ConnectedSpace encode closed and connected; the model space has no boundary.laplaceBeltrami is the coordinate formula above, computed through chartAt with the metric matrix obtained from mfderiv of the inverse chart. No orientability is assumed.ContMDiff … ∞ and nonzero, with at every point; smoothness is automatic by elliptic regularity, so this does not weaken the statement.nodalLength u is Measure.hausdorffMeasure 1 of for the Borel structure of the metric, valued in ℝ≥0∞; the bound is ≤ ENNReal.ofReal (C * Real.sqrt lam) with fixed before and .A complete development needs local isothermal coordinates or a coordinate-free substitute, Carleman estimates, growth bounds, and a planar comparison between growth and nodal length (Roy-Fortin's theorem). Much of this, especially Hausdorff-measure estimates for zero sets of solutions of planar elliptic equations, is reusable. Contributions formalizing the paper's intermediate results (Theorem 2.2, Proposition 3.4, Theorem 5.5, Lemma 6.2) or Roy-Fortin's planar theorem are welcome.
A Riemannian metric is Einstein if its Ricci curvature is a constant multiple of the metric, . Einstein metrics are the critical points of total scalar curvature and the vacuum solutions of general relativity in Riemannian signature, and in dimension four they are tied to gauge theory and to the topology of four-manifolds. A natural rigidity question asks which closed four-manifolds carry Einstein metrics of strictly positive sectional curvature. Three examples are known: the round sphere , the round real projective space , and the complex projective plane with its Fubini–Study metric. The classification conjecture, stated as Conjecture 1 by D. Yang in 2000, asserts that there are no others up to scaling and isometry.
All earlier results keep an additional curvature, topological or symmetry hypothesis. The source of this mission is an OpenAI preprint dated September 23, 2026, which claims the classification with no extra hypothesis and no orientability assumption.
Let be a connected, compact smooth four-manifold without boundary, with a smooth Riemannian metric . In a chart with Christoffel symbols , the curvature tensor is
the Ricci tensor is , and the sectional curvature of the plane spanned by has the sign of . The metric is Einstein if for a single constant , and positively curved if for all linearly independent . Strict positivity forces .
The three models are with distance , with distance for unit representatives, and with the Fubini–Study distance .
If is in addition oriented, then for some , is isometric to or to .
The Lean statement OAI.PositiveEinsteinFour.classification is open on the platform.
The theorem completes the four-dimensional picture for positively curved Einstein metrics: only the symmetric examples occur. It removes all the pinching, topological and symmetry hypotheses of previous results. The paper's central intermediate result, half-conformal flatness (one Weyl block vanishes, Proposition 8.1), connects the problem to Hitchin's classification of self-dual Einstein four-manifolds.
The result is stated in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. Parts of the argument rely on explicit polynomial and matrix certificates (Section 7), which are well suited to formal verification.
In dimension four the curvature of an Einstein metric splits into two Weyl blocks acting on self-dual and anti-self-dual two-forms. The Einstein equation does not force either block to vanish, and earlier arguments controlled them only under extra pinching or topological assumptions. Scalar Weyl-norm gaps (Gursky–LeBrun) control each block separately; the difficulty is the interaction of two nonzero blocks under the exact sectional-positivity condition, which is stronger than any norm bound and must be used in its tensorial form. Once one block vanishes, the classical rigidity theory finishes the proof.
ChartedSpace (EuclideanSpace ℝ (Fin 4)) with IsManifold I4 ∞, compact, connected, Hausdorff, second countable; the model has no boundary.ContMDiffRiemannianMetric; Christoffel symbols, curvature and Ricci are computed in coordinates from fderiv of the chart expression of , at the centre of the chart at each point.IsEinstein uses one constant for all points; HasPositiveSectionalCurvature requires for every linearly independent pair.ScaledIsometricTo g a d asks for a bijection with , the Riemannian distance.A complete development needs Riemannian geometry in coordinates, Weyl decomposition in dimension four, Hodge theory on two-forms, characteristic-number identities (Gauss–Bonnet–Chern, Hirzebruch signature), volume comparison, and Hitchin's classification. Contributions formalizing Proposition 8.1 (half-conformal flatness), Proposition 4.9 (balanced Weyl moments) and Lemma 8.7 (curvature of the standard models) are welcome.
A symplectic embedding preserves the standard symplectic form on , and in particular preserves volume. Gromov's nonsqueezing and two-ball theorems showed that symplectic embeddings obey constraints invisible to volume (Gromov 1985). The ball-packing problem asks exactly when finitely many balls can be embedded disjointly and symplectically into a given ball, and so measures how far symplectic rigidity goes beyond volume.
In real dimension four the answer involves infinitely many obstructions coming from pseudoholomorphic curves and algebraic geometry (McDuff–Polterovich 1994; Biran 1997). In higher dimensions Siegel and Yao conjectured that only two obstructions survive: volume and Gromov's two-ball obstruction (Conjecture A of Siegel–Yao 2025).
This mission asks for a machine-checked proof of Theorem 1.1 of an OpenAI preprint dated September 23, 2026 (source), which claims Conjecture A in every real dimension . The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.
For write
so is the capacity, the Euclidean radius is , and . An embedding of a closed ball into the open ball means a smooth map defined on an open neighbourhood of the closed ball, which is a topological embedding there, pulls back to , and sends the closed ball into the open target. A packing of is a family of such embeddings whose images of the closed balls are pairwise disjoint.
If , , and a packing exists, then
The images lie in some with by compactness, so the volume bound and Gromov's two-ball obstruction give the strict inequalities.
For integers , and positive reals , a symplectic embedding exists if and only if the two inequalities above hold.
The result itself. In every real dimension at least six, the volume and two-ball obstructions are the only obstructions to packing balls of arbitrary capacities into a ball. This contrasts with dimension four, where infinitely many further obstructions are essential, and it goes beyond packing-stability results, which concern many small balls. The theorem settles Siegel and Yao's Conjecture A.
Formalizing it. The necessity direction needs Gromov's two-ball theorem, which rests on pseudoholomorphic curve theory and has no formalization. The sufficiency direction uses Hamiltonian flows, Moser isotopies, toric domains, Kähler forms on projective degenerations and normal-cone transfer. A formal proof would require substantial new symplectic and algebro-geometric infrastructure, all of it reusable.
Sufficiency is the hard direction. The volume inequality is an integral condition, but a packing needs pointwise room; in the preprint's toric models over a surface with a handle, the unused-area profile has positive integral but need not be positive at every moment, and a Hamiltonian comparison theorem (Lemma 2.1, p. 5) is needed to rearrange it into disjoint ball layers (Lemma 3.3, p. 12). The models must then be transferred symplectically into the target ball using Kähler degenerations; three geometric cases arise (all capacities below , Proposition 5.2, p. 25; one large capacity in dimension , Proposition 5.3, p. 26; one large capacity in dimension six, Proposition 6.7, p. 39). For necessity the obvious volume argument gives only non-strict inequalities; strictness comes from compactness of the images, and the pairwise bound is genuinely symplectic.
Fin n → ℂ with capacity and .SymplecticOn U f: open, is on , is a topological embedding, and fderiv preserves at every point of .HasPacking n k R r: each closed ball lies in an open on which is symplectic, maps the closed ball into the open ball of capacity , and images of distinct closed balls are disjoint.PackingInequalities uses strict inequalities and quantifies over ordered pairs ; the goal assumes , , , , matching the source exactly.A Riemannian surface is abstract: it is given by a rule for measuring lengths and angles in local coordinates, not as a surface sitting in space. The local isometric realization problem asks whether every such surface can, near each point, be realized as an honest smooth surface in Euclidean three-space with the same lengths. The question goes back to the classical theory of surfaces. It is settled for real-analytic metrics and for smooth metrics with nonvanishing curvature, while the unrestricted smooth case is listed as open by Yau (Yau 2000, p. 236) and in Ghomi's problem survey (Ghomi 2019, §1.5, Problem 1.9).
Work in coordinates on the open square . A Riemannian metric on is a map to symmetric real matrices that are positive definite; it is if every entry is smooth. An isometric immersion of , for an open set , is a map whose differential reproduces :
equivalently . Positive definiteness forces to have rank . In Lean, Coord = Fin 2 → ℝ, Ambient = EuclideanSpace ℝ (Fin 3), square is , and LocalSmoothPositive packages smoothness of every entry and Matrix.PosDef at every point.
This is Theorem A of the source (p. 1). Because a smooth isometric immersion restricts to an embedding near any point, it also rules out local smooth isometric embeddings. The stronger statement that can be chosen with the full Euclidean Taylor jet at the origin (Corollary 5.3) is not part of the goal. The goal is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. The theorem shows that smooth local isometric realization in can fail, which answers negatively the unrestricted smooth problem recorded by Yau and Ghomi. It separates the smooth case from the analytic case (Janet–Cartan) and from finite regularity (Pogorelov, Nadirashvili–Yuan 2008). It also shows, by Corollary 5.3, that the infinite-order jet of the metric at a point does not decide realizability. It leaves open the same question under a sign condition or , since the construction uses both signs of curvature.
Formalizing it. The statement is short, but the claimed proof combines PDE estimates for Darboux's equation, hyperbolic propagation, a Baire-category argument and a boundary-saddle geometric step. The literature has disagreed about the status of the smooth question (NY2002 versus NY2008), so a machine-checked proof would remove the ambiguity. Mathlib has the manifold calculus needed to state the result (ContMDiff, mfderiv) but none of the PDE layer.
Where the Gaussian curvature is nonzero, the realization equations are elliptic or hyperbolic and can be solved locally, so any counterexample must exploit degeneracy where vanishes and changes type. Finite-regularity counterexamples (Pogorelov) do not carry over: existence at every finite order, on neighborhoods that shrink with the order, does not give one smooth map on a fixed neighborhood. Nonsolvable Monge–Ampère equations are also not enough by themselves, because the coefficients of the Darboux equation come from the same metric, so the obstruction has to be built into itself. Finally, the conclusion must hold for every neighborhood of the origin and every smooth immersion, with no a priori bounds on .
coordinateSquareOpen with values in Matrix (Fin 2) (Fin 2) ℝ. Each entry is ContMDiff … ∞ and each value is Matrix.PosDef, which includes symmetry (Hermitian over ℝ).U : Opens Coord with and , and over all maps F : U → Ambient that are ContMDiff … ∞ on the open submanifold . The isometry condition is stated with mfderiv and the Euclidean inner product: .An isometric immersion realizes an abstract Riemannian manifold as a surface in Euclidean space whose induced lengths are exactly the prescribed ones. How many dimensions are needed is a classical question. Nash showed that every compact Riemannian -manifold embeds smoothly and isometrically in some Euclidean space; for surfaces his bound is (Nash 1956). Gromov lowered the immersion dimension for closed surfaces to (Partial Differential Relations, 1986, §3.2.4). Three dimensions do not suffice even locally in the smooth category, and Gromov recorded the question whether every smooth Riemannian surface admits a smooth isometric immersion into (Gromov 2000, §I, Remark (d)), later attributing it to Chern around 1950 (Gromov 2015, p. 4).
This mission asks for a machine-checked proof of Theorem 1.1 of an OpenAI preprint dated September 23, 2026 (source), which answers the compact, boundaryless form of that question: every closed smooth Riemannian surface admits a smooth isometric immersion into . The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.
A closed surface is a compact smooth two-dimensional manifold without boundary; it need not be orientable or connected. A Riemannian metric assigns to each a positive definite inner product on , depending smoothly on . A smooth map is an isometric immersion if
Positive definiteness of forces to be injective, so is an immersion; self-intersections are allowed.
For every closed smooth Riemannian surface there is a map with , where . In Lean this is OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth_isometric_immersion.
The result itself. The theorem lowers Gromov's immersion dimension for closed surfaces from five to four, with no restriction on curvature or topology, and settles the closed case of the question Gromov attributes to Chern. Dimension four is the first codimension in which the smooth problem can have a global answer for all surfaces, since smooth metrics with no local isometric immersion into exist. The open (noncompact) case of the question is not addressed.
Formalizing it. Mathlib now has smooth manifolds, tangent bundles and smooth Riemannian metrics, so the statement is expressible without custom geometry. A complete proof would add Whitney's immersion theorem, Sard's theorem in equal dimensions, metric decompositions into rank-one terms, Nash–Moser-type smoothing estimates, and oscillatory correction schemes; none of these are formalized at this level, and all are reusable in geometric analysis.
The isometric immersion equation is a nonlinear system of three equations in four unknown functions, and its linearization loses derivatives, so a direct implicit function argument fails. Convex integration in the Nash–Kuiper style produces only solutions. Poznyak's smooth theory works on planar domains with boundary, but on a closed surface the successive local corrections must remain compatible globally. The preprint keeps a nondegenerate normal geometry (a nonzero vector-valued second fundamental form) through every step, adds the metric deficit one positive rank-one term at a time via a velocity loop in a plane normal to and (Proposition 3.1, p. 8; Proposition 7.1, p. 25), and then corrects the approximate metric exactly by a smoothing scheme that solves the linearized equation only on oscillatory modes (Proposition 5.1, p. 15). Nonorientable surfaces are handled by starting from an immersion into a small round -sphere, whose radial direction is a global normal (Lemma 9.1, p. 35).
ChartedSpace (EuclideanSpace ℝ (Fin 2)) M and IsManifold 𝓘(ℝ, ℝ²) ∞ M, assumed compact, Hausdorff and second countable. Being modeled on (not a half-space) encodes "without boundary"; no orientability or connectedness is assumed.Bundle.ContMDiffRiemannianMetric of class on the tangent bundle.ContMDiff … ∞ F and equality of the Euclidean inner product of mfderiv images with g.inner p v w for all tangent vectors; immersivity follows and is not stated separately.A norm is uniformly convex when midpoints of far-apart unit vectors are pushed strictly inside the unit ball. In infinite-dimensional Banach spaces the useful notions are asymptotic: one asks for a gain only in directions taken from a subspace of finite codimension, chosen after the center is fixed. Two such notions are compared here. Asymptotic uniform convexity (AUC) asks for growth of in every far-out unit direction ; asymptotic midpoint uniform convexity (AMUC) asks only that the average of and grows. These properties control nonlinear embeddings (for instance of countably branching diamond graphs) and are standard tools in the asymptotic geometry of Banach spaces.
Dilworth, Kutzarova, Randrianarivony, Revalski and Zhivkov (2016) asked whether AMUC and AUC are equivalent up to renorming. Baudier (2026) answered no, using subspaces of whose unit ball is compact in measure and the Daugavet-property example of Kadets and Werner. This mission asks for the exact values of both moduli in that setting.
The source of this mission is an OpenAI preprint dated September 27, 2026, which computes both moduli exactly.
All spaces are real. For a Banach space with norm , let be its closed linear subspaces of finite codimension. For and ,
The averaged midpoint modulus and the one-sided modulus are the infima of and over unit . is AUC if for all . A norm is equivalent to if with .
A space has the Daugavet property if for every rank-one bounded operator . On a probability space , convergence in measure is given by the metric
A set is totally bounded in measure if for each it is covered by finitely many -balls of radius .
Let be an infinite-dimensional closed subspace of , a probability measure, whose unit ball is totally bounded in measure and whose norm has the Daugavet property. Then for every unit and
so and , and admits no equivalent AUC norm. Lean: OAI.ExactModuli.exact_main (open on the platform).
On there is an infinite-dimensional closed subspace whose unit ball is totally bounded in measure and which has the Daugavet slice property. Lean: OAI.ExactModuli.kadets_werner_existence. The proposal also carries OAI.ExactModuli.exact_example, the combination of the two theorems for this space.
The formulas show how far apart the two moduli can be: the averaged modulus grows linearly from , while the one-sided modulus vanishes on the whole interval . They refine Baudier's qualitative AMUC statement and linear lower bound into exact curves at every unit center, and the renorming clause shows that no equivalent norm can repair the one-sided modulus. Together with Theorem 6.1, they give a concrete space realizing the separation.
The results are proved in an OpenAI preprint; they have not been peer reviewed, and no machine-checked proof exists. The Daugavet slice characterization, Bourgain's lemma on slices and weak neighborhoods (Lemma 3.2), and the construction itself are reusable pieces of Banach space theory that a formalization would supply.
The lower bound for must hold uniformly over all directions in some finite-codimensional subspace, while the hypothesis only says that the unit ball is compact in a weak metric. A compactness argument along subsequences (Baudier's route via Brézis–Lieb) gives positivity but not the exact constant. The upper bounds need directions in a prescribed finite-codimensional subspace that are almost at distance from ; the Daugavet property supplies such vectors only in weak neighborhoods, and they must then be corrected into the subspace. The renorming clause must handle an arbitrary equivalent norm, for which neither formula is available.
Cofinite F is a closed submodule with finite-dimensional quotient. H, D, averagedModulus, oneSidedModulus follow the displayed sup/inf order; H ranges over , D over .EquivalentNorm N is a Seminorm with two-sided comparison constants ; AUC N is positivity of oneSidedModulus N t for every .Daugavet X quantifies over rank-one operators written as ell.smulRight v.measureDistance is the metric on Lp ℝ 1 μ; MeasurePrecompactBall μ E requires finite -nets (centers in ) of the unit ball of ; μ is a probability measure.kwMeasure is the product of Lebesgue measures on .sSup/sInf; for infinite-dimensional the relevant sets are nonempty and bounded, so the junk values are not used.A full development needs the Daugavet slice characterization (Lemma 3.1), Bourgain's lemma (Lemma 3.2), the weak-neighborhood diameter-two property (Lemma 3.3), truncation estimates, and the Kadets–Werner iteration (Lemmas 6.2–6.3). Formalizations of these lemmas are welcome.
How well can a graph be drawn inside a Banach space without stretching some distances much more than others? The distortion of the best such drawing measures the mismatch between the graph's metric and the geometry of the space. Diamond graphs are a standard test family: each edge is repeatedly replaced by parallel two-edge paths, so the graph contains many "midpoints" between the same two endpoints at every scale. For binary diamonds, bounded distortion in a space is tied to the failure of super-reflexivity (Johnson–Schechtman 2009). For countably branching diamonds, where each edge is replaced by infinitely many paths, the relevant property is asymptotic midpoint uniform convexity (AMUC): an equivalent AMUC norm prevents uniform embeddings (Baudier et al. 2017).
This mission asks for an explicit, quantitative lower bound on the distortion of countably branching diamonds in two specific James-type tree spaces, deduced from a midpoint "lens" estimate for those spaces.
The source of this mission is an OpenAI preprint dated September 27, 2026; its lens input comes from the companion OpenAI preprint Midpoint lenses in segment spaces of the same date.
Diamonds. The normalized diamond is one edge of length . replaces every edge of by countably many internally disjoint two-edge paths with the same endpoints, each new edge having half the length of its parent. Let be the shortest-path metric. A map has distortion at most if for some scale
Tree spaces. Let (one rooted tree of each finite height, prefix order inside each tree). A segment is the set of vertices between two comparable nodes. For a finitely supported array ,
is the completion and with the dual norm. On (root included) the same formula defines , and is the closed span of the coordinate functionals.
For every and every distortion- embedding of into ,
The Lean statement OAI.DiamondDistortion.headline_all_pairs is the conjunction of the two cases. It is open on the platform.
The bound shows that the countably branching diamonds do not embed with uniformly bounded distortion into either space, with an explicit square-root growth rate. Combined with the companion results that neither space admits an equivalent asymptotically uniformly convex norm, and that the forest dual is reflexive, it shows that the diamond obstruction can hold in reflexive spaces without AUC renormability, so the unconditional-structure hypotheses in the known converses are doing real work. The constant is obtained by retaining the full quadratic budget of the lens inequality. The paper also gives direct energy proofs (Theorem 5.1, Propositions 4.2–4.3) with weaker constants, and general transfer theorems (Section 7) from lens inequalities to distortion bounds.
The theorem is proved in the OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. A formalization would certify both the metric deduction and, through its input, the tree-space lens estimate.
The input lens inequality bounds only the tail of a displacement outside a finite head. Turning it into a loss of squared edge stretch at every replacement level requires selecting, among infinitely many middle vertices, two whose head projections nearly coincide, so that their half-difference is a tail vector that still lies in the lens. Doing this simultaneously along a descending chain of edges, with the head growing at each step, and summing the losses without wasting the quadratic budget is where the constant is decided. A binary diamond argument does not transfer, because finitely many midpoints give no near-coincident projections.
Diamond.Vertex k and Diamond.Edge k are defined by recursion on the stage, each parent edge receiving new vertices indexed by ; Diamond.graph k is the undirected replacement graph and Diamond.distance k u v is SimpleGraph.dist divided by . Since distortion is scale invariant, the normalization does not affect the statement.ForestDual is the full continuous dual of the completion of the finite-height forest James space; InfinitePredual is the norm-closed span of coordinate functionals in the dual of the infinite-tree space, with the subspace norm.A complete development needs the James segment norm and its dual, coordinate projections onto finite ancestral sets, the companion lens estimate, and graph distances on the countably branching diamonds. This infrastructure is shared with the other missions of this family. Formal proofs of Theorem 7.2 (lens-to-distortion transfer) and Theorem 7.12 (AMUC prevents uniform embeddings) are welcome as reusable components.
In a uniformly convex space, if is nearly as long as and both and have length at most , then the displacement must be short. The set of such displacements,
is a symmetric lens. In infinite dimensions the right question is asymptotic: is short after discarding finitely many directions? Dilworth, Kutzarova, Randrianarivony, Revalski and Zhivkov (2016) characterized asymptotic midpoint uniform convexity (AMUC) through the measure of noncompactness of such lenses. AMUC is the property that, together with asymptotic uniform convexity (AUC), governs which countably branching graphs embed into a Banach space with bounded distortion.
This mission asks for an explicit lens estimate in two James-type tree spaces, with a bound depending only on the squared-radius deficit of the center and holding for every displacement simultaneously after one finite set of coordinates is removed.
The source of this mission is an OpenAI preprint dated September 27, 2026.
All scalars are real.
Finite-height forest. For let be the tree of words of length at most , ordered by extension (the root is the empty word). The forest is the disjoint union of one copy for each . Write if is an ancestor of in the same component. A segment is a nonempty interval . For finitely supported put and
Let be the completion of and with the dual norm. Coordinate evaluation gives functionals .
Infinite tree. Let (all finite words, root included), the completion for the same norm, and , closed in the dual norm.
A finite set of vertices is ancestral if it contains all ancestors of its elements. On either space,
For , every finite ancestral , every with , and every with and ,
The Lean statement OAI.SegmentLenses.midpoint_lens_main is the conjunction of the two cases. It is open on the platform. The displacement may have a nonzero head ; only its tail is controlled.
The estimate is uniform over the lens: one finite head controls every admissible displacement, which is exactly what is needed when a single center has infinitely many approximate midpoints. As a consequence (Corollary 7.1 of the source) both given norms are AMUC with , while Proposition 9.1 shows that neither space admits an equivalent AUC norm. In particular the infinite-height case answers Perreau's question for the specified real norm on , and the finite-height forest gives a reflexive space separating AMUC from AUC renormability. A companion preprint uses this theorem to force distortion for depth- countably branching diamonds.
The result is proved only in the OpenAI preprint; it is not peer reviewed and has no machine-checked proof. Formalizing it would certify the cancellation analysis that drives the constant .
The natural attempt is to represent a nearly norming functional for the center as a convex combination of disjoint segment functionals and read off the tail. The obstacle is cancellation: two atoms leaving the head through the same vertex can have segment sums of opposite sign, and a naive estimate loses all control. The bound must also hold for every displacement with the same , so compactness arguments that choose after do not suffice, and an independent radial approach in the source gives only the weaker .
ForestVertex is the subtype of pairs with and ; InfiniteVertex := List ℕ. Ancestry is equality of heights plus List.IsPrefix (resp. prefix only).IsInterval ancestor S asserts with , so segments are nonempty. A test family is a finite set of pairwise disjoint segments, and segmentSeminorm is the supremum of the Euclidean norms of the vectors of segment sums.X := StrongDual ℝ (UniformSpace.Completion (Test ForestVertex)); BInfinite is the closed span of the coordinate functionals inside the full dual of the infinite-tree completion, carrying the subspace (dual) norm.head H x = ∑ v ∈ H, x(e_v) • e_v^* and tail H x = x - head H x; ancestrality is Ancestral.A full development needs the James segment norm, its completion and dual, contractivity of coordinate projections, the decomposition of the tail over descendant cones (Lemma 2.2), and the atomic description of finite head balls (Section 4). This infrastructure is shared with the other missions in the same family. Formalizations of Lemma 2.1, Lemma 2.2, Corollary 7.1 and Proposition 9.1 are welcome as supporting results.
Uniform convexity of a norm says that the midpoint of two far-apart points of the unit sphere lies strictly inside the ball. In infinite dimensions there is an asymptotic version: one only asks for a gain in directions that lie far out, that is, inside some closed subspace of finite codimension. Asymptotic uniform convexity and its relatives control the large-scale geometry of a Banach space, and in particular which infinite graphs can be embedded into the space with bounded distortion.
Two such properties are compared here. Asymptotic uniform convexity (AUC) demands a gain in every far-out direction separately; asymptotic midpoint uniform convexity (AMUC), introduced by Dilworth, Kutzarova, Randrianarivony, Revalski and Zhivkov (2016), only asks for a gain when a direction and its opposite are tested together. Every AUC norm is AMUC. The question is how far apart the two notions are, both up to renorming and in terms of metric embeddings of the countably branching diamond graphs .
The source of this mission, an OpenAI preprint dated September 27, 2026, gives a reflexive example that separates the two notions and answers the reflexive diamond question negatively.
All spaces are real. For a Banach space with norm , let be the closed subspaces of finite codimension. For ,
is AUC if for every , and AMUC if for every . A norm is equivalent to if for some .
The forest. For let be the rooted tree of words of length at most , ordered by extension. The forest is the disjoint union of one copy of for every . A segment is an interval of an ancestral chain. For a finitely supported ,
Let be the completion and with the dual norm.
Diamonds. is one edge; replaces every edge of by countably many internally disjoint two-edge paths. With the shortest-path metric , a map has distortion at most if some scale gives for all .
The Lean statement OAI.ForestSpace.main_theorem is the conjunction of these six clauses. It is open on the platform.
The theorem separates AMUC from AUC renormability inside the reflexive class, which Baudier's 2026 example (non-reflexive) does not. Because AMUC is a property of the given norm while the diamond obstruction is invariant under renorming, the theorem also shows that, for general reflexive spaces, failure of AUC renormability does not force the countably branching diamonds to embed uniformly. This answers Problem 39 of Baudier–Lancien negatively and shows that the unconditional asymptotic structure hypothesis in the 2017 embedding theorem cannot simply be dropped. The quantitative modulus and distortion bounds are explicit, not merely positivity statements.
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. A formal proof would certify the full construction, including reflexivity of for a non-locally-finite forest and the square-sum distortion recursion.
Two points are delicate. First, reflexivity: the classical James tree space is not reflexive, and here reflexivity comes from using trees of finite but unbounded height together with countable branching; the full dual , not the coordinate completion, is the space. Second, the midpoint estimate: a segment test may cross from a finite ancestral set to its complement, and simply adding norming tests for the two parts produces uncontrolled positive cross terms. Non-renormability, by contrast, must be proved for every equivalent norm at once, so it cannot be read off from any computation with the given norm.
FullDual Vertex := StrongDual ℝ (J Vertex), where J V is the UniformSpace.Completion of TestVector V (finitely supported functions with norm rho). Vertex packs a height and a word in of length ; the order is equality of heights plus prefix order.IsSegment); the empty segment is allowed and contributes zero.Reflexive is surjectivity of the canonical map NormedSpace.inclusionInDoubleDual, not an abstract isomorphism with the bidual.EquivalentNorm E α β stores a Seminorm with explicit constants ; the lower bound makes it a norm. The non-renormability clause quantifies over all such structures.aucModulus and averageModulus take the inf/sup/inf order above, with sInf/sSup over real sets; for an infinite-dimensional space these sets are nonempty and bounded, so the Lean defaults are not triggered.Diamond.diamond k iterates the edge replacement starting from one edge; distances are SimpleGraph.dist of the undirected graph, and EmbeddingBound is the scaled bi-Lipschitz condition above.A complete development needs the James-type segment norm, its completion and dual, coordinate projections onto ancestral sets, and graph distances on the diamonds. The segment-norm and diamond infrastructure is shared with the other missions of this family. Contributions formalizing Lemma 2.1 (structure and reflexivity), Lemma 3.2 (bounded trees exclude AUC renorming), Lemma 4.1 (paired head–tail estimate) and Lemma 5.1 (lens lemma) are welcome.
Covering numbers measure the size of a set at a given scale: is the least number of translates of needed to cover . 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 is hard to cover by , is the polar body equally hard to cover by ? 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.
The source of this mission is an OpenAI preprint dated September 24, 2026, which disproves the dimension-free conjecture.
Work in with the standard pairing . A convex body is a compact convex set with nonempty interior; it is origin-symmetric if . Its polar is
For bounded and a body , the covering number is the least such that for some (centres need not lie in ). Logarithms are natural. Let be the cube; its polar is the cross-polytope.
The duality conjecture asks for absolute constants such that, for every and all origin-symmetric convex bodies ,
For every there are and an origin-symmetric convex body such that, with ,
The Lean statement OAI.MetricEntropyDuality.exists_entropy_duality_counterexample_with_covers is open on the platform.
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.
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 whose rows are pairwise -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 after the scale change .
RealSpace (Fin n) = Fin n → ℝ with pairing the standard dot product; cube is ; polar K uses .Covers A B centers means every has some centre with ; coveringNumber is the sInf of the admissible . The statement includes Coverable side conditions, which only certify that both infima are over nonempty sets.IsSymmetricConvexBody = compact, convex, , nonempty interior.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.
A map is nonexpansive if . 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).
Let be a real Banach space and its continuous bidual. The canonical map , , is always a linear isometry, and is reflexive if is surjective. A subset is taken nonempty, closed in the norm topology, bounded and convex. A map is nonexpansive in the given norm of , and a fixed point is a point with .
In Lean, reflexivity is the definition CanonicallyReflexive X, which says that NormedSpace.inclusionInDoubleDual ℝ X is surjective.
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.
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 , the common fixed point set is nonempty and is a nonexpansive retract of . Alspach's example shows that reflexivity cannot be weakened to weak compactness of 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.
The classical route reduces a hypothetical counterexample to a minimal invariant weakly compact convex set of diameter one. By the Goebel–Karlovitz lemma, every approximate fixed point sequence in 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 example shows that compactness of and nonexpansiveness alone cannot produce the contradiction: the proof has to use reflexivity of the whole space (weak compactness of the unit ball of ), not just of the domain. A further obstacle is that is nonlinear, so convex combinations of approximate fixed points are not mapped to convex combinations of their images.
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 ; complex spaces enter as real spaces.Set X with Nonempty, IsClosed (norm topology), Bornology.IsBounded and Convex ℝ. is a function on the subtype C → C, and nonexpansiveness is stated in the original norm of , not in an equivalent norm.∃ a : C, F a = a. Every hypothesis is satisfiable, so the statement is not vacuous: a trivial is excluded only by nonemptiness, as in the source.For a square matrix , the spectrum alone does not control the size of : a nonzero nilpotent matrix has spectrum yet . The numerical range 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 ,
i.e. that is a -spectral set; the constant 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 matrix coefficients, uniformly in ; by Paulsen's theorem this is equivalent to similarity of the conformal disk image of to a contraction with condition number at most .
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.
For () let . A matrix polynomial of degree with coefficient size is with . Its evaluation at is
with the base space first. All norms are Euclidean operator norms. For this is the usual .
For a bounded operator on a complex Hilbert space , and ; acts on . A bounded open convex is admissible if its boundary is a regular real-analytic Jordan curve. For such ( a matrix) with interior conformal map , put and
For , is compact and convex and contains .
If , the numerical range is empty, every polynomial, holomorphic and rational evaluation is , and the corresponding inequalities read (with the supremum over the empty set taken to be ).
For admissible conformal coordinates exist; for every and with , the problem defining is strictly feasible with attained minimum ; for a minimizer , satisfies and is a contraction with ; and one continuous with , represents for every and every -valued holomorphic near , giving .
For all , , , : , and no smaller universal constant works.
For every complex Hilbert space (no separability assumption) and : if then is compact, convex, contains the spectrum, and for every
for matrix polynomials , matrix functions holomorphic on an open (holomorphic functional calculus), and matrix rational functions with poles off ; if the degenerate statements above hold; and the constant is optimal.
The result itself. It resolves the complete Crouzeix conjecture in its operator formulation, independent of the Hilbert space, the coefficient size and the degree: is a complete -spectral set for every bounded operator. The structural theorems give more than the inequality: an optimal similarity, attained, with condition number at most , 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.
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 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 , but one must show every vector of and its image under live in a finite-dimensional compression, and treat holomorphic and rational calculi through contour integrals around the closed numerical range.
H is any type with InnerProductSpace ℂ H and CompleteSpace H; operators are H →L[ℂ] H. The amplification is the completion of the algebraic tensor product, and is the completed TensorProduct.mapL.supNorm S F = sSup (insert 0 (‖F ·‖ '' S)), so the supremum over an empty set is , matching the convention of Corollary 6.3.CalculusContour around inside ; 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 matrix with and .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).
For a square matrix , the spectrum alone does not control the size of : a nonzero nilpotent matrix has spectrum yet . The numerical range 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 ,
i.e. that is a -spectral set; the constant 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 matrix coefficients, uniformly in ; by Paulsen's theorem this is equivalent to similarity of the conformal disk image of to a contraction with condition number at most .
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.
For () let . A matrix polynomial of degree with coefficient size is with . Its evaluation at is
with the base space first. All norms are Euclidean operator norms. For this is the usual .
For all , , and ,
If the inequality holds with a constant in place of for all , then .
Both assertions together: the constant is valid and no smaller universal constant is.
The result itself. It settles the complete Crouzeix conjecture in its matrix formulation, uniformly in the base dimension , the coefficient size and the degree, including matrices whose numerical range is a point or a segment. The scalar case had recently been proved by other authors and the complete case was known only for ; a scalar argument need not survive matrix amplification because coefficient matrices do not commute. Equivalently, the numerical range is a complete -spectral set for every matrix, which via Paulsen's theorem gives a similarity of condition number at most making the conformal disk image of 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 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- Crouzeix bound is known.
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 . To reach in the complete setting, the argument must keep both multiplication orders and of matrix-valued test functions, since the coefficients do not commute. The preprint chooses a top singular pair of , 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).
Matrix (Fin n) (Fin n) ℂ with the L2 operator norm (Matrix.Norms.L2Operator). The numerical range is the set of over unit vectors of EuclideanSpace ℂ (Fin n).B : Fin (d+1) → Matrix (Fin m) (Fin m) ℂ; the evaluation is indexed by Fin n × Fin m, base factor first.rangeMaximum A B is the sSup of over . Since , is nonempty and compact, so this is the true maximum; UniversalBound C quantifies over all , all , all and .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.The Mazur–Ulam theorem (1932) says that every surjective isometry between real normed spaces is affine. The whole space is not always available, though: often only distances between unit vectors are known. Tingley's problem (1987) asks whether the metric of the unit sphere alone already determines the linear structure, that is, whether every surjective isometry between the unit spheres of two real Banach spaces extends to a real-linear isometry of the spaces (Tingley 1987). The question has been studied for almost four decades, mostly class by class: for sequence spaces, spaces, operator algebras and two-dimensional spaces. Nearly all known positive results depend on the structure of the particular spaces involved.
Let and be real Banach spaces, both nonzero. The unit sphere is with the metric inherited from . A map is an isometry if for all , and it is surjective if every point of is attained.
Any linear extension of is forced to be the radial extension
In Lean, UnitSphere X is the subtype and normalize x hx is as an element of it.
For nonzero real Banach spaces and every surjective isometry there is a surjective real-linear isometry such that
and is the only real-linear map that agrees with on . This is the full statement of Theorem 1.1 of the source. The goal is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. An affirmative answer turns a forty-year class-by-class programme into a single theorem: the metric of the unit sphere of any real Banach space determines the space up to linear isometry. Every space then has the Mazur–Ulam property in the sense of Cheng and Dong, with no separability, reflexivity, smoothness or strict convexity assumptions. For complex Banach spaces viewed as real spaces the conclusion is real-linearity only; complex-linearity is not claimed.
Formalizing it. The claimed proof combines classical tools (supporting functionals, Banach-space ultrapowers, Darbo's fixed-point theorem with the Kuratowski measure of noncompactness, the Mazur–Ulam theorem) with new geometric estimates on aligned chords. A machine-checked proof would certify a result whose proof has not yet been refereed. The Mazur–Ulam theorem itself is already in Mathlib (IsometryEquiv.toRealLinearIsometryEquiv); ultrapowers of Banach spaces and Darbo's theorem are not.
The radial map preserves norms and preserves distances between points of the same radius. What has to be shown is that it preserves distances between points on different spheres, for , using only distances measured on a single sphere. Once this holds, is a surjective isometry fixing and Mazur–Ulam gives linearity. The obvious attempt (extend the isometry to a neighbourhood, or use convex-set extension theorems such as Mankiewicz's) fails because the sphere has empty interior. Structural arguments (smoothness, facial structure, explicit duals) cover only special classes of spaces. In general, the maximal defect need not be attained, and no compactness is available in infinite dimensions.
NormedAddCommGroup, NormedSpace ℝ and CompleteSpace, and Nontrivial (the source's "nonzero"). Universe levels are independent, and no separability or dimension hypothesis is imposed.UnitSphere X := {x // ‖x‖ = 1} with the subtype metric; Isometry f and Function.Surjective f are the hypotheses.X ≃ₗᵢ[ℝ] Y (a bijective real-linear isometry) with the five clauses: agreement on the sphere, , the radial formula, surjectivity, and uniqueness among all X →ₗ[ℝ] Y that agree with on the sphere. No hypothesis assumes any distance between different radii, so the statement is not trivialized.A model structure on a category specifies weak equivalences, fibrations and cofibrations so that the category carries a homotopy theory. Thomason showed that the category of small categories carries a model structure Quillen equivalent to simplicial sets, so that ordinary categories model all homotopy types of spaces (Thomason 1980). Its weak equivalences are the functors whose nerves are weak homotopy equivalences.
Strict higher categories have a nerve too: Street's orientals give the Street nerve of a strict -category (Street 1987). The higher-dimensional Thomason model-structure conjecture of Ara and Maltsiniotis asks for the analogue of Thomason's theorem for strict globular -categories for every (Ara–Maltsiniotis 2014; Ara 2023, §§9.2.5–9.2.6; Guetta–Maltsiniotis 2024). Strict higher categories are already known to describe the homotopy category of spaces after localization (Gagna, below); the conjecture asks for the full model structure, with lifting and factorization on all strict -categories.
This mission asks for a machine-checked proof of Theorem 1.1 of an OpenAI preprint dated September 25, 2026 (source), which claims the conjecture in every dimension. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
A strict globular -category has a set of cells, source and target operations in each dimension, and associative, unital compositions along -dimensional boundaries satisfying the interchange law; every cell has finite dimension. A strict -category is one whose cells above dimension are identities; denotes the category of small strict -categories and strict functors ( means ). No invertibility is assumed.
The Street nerve has , with left adjoint . With barycentric subdivision set
Let and be the weak homotopy equivalences and Kan fibrations, and . Define
: a functor of strict -categories is a weak equivalence exactly when its Street nerve is a weak homotopy equivalence. This follows from being a natural weak equivalence.
For every , is a proper combinatorial model structure on , cofibrantly generated by , and
is a Quillen equivalence.
The result itself. The theorem says that strict higher categories, in every dimension, model the homotopy theory of spaces through a genuine model structure, not only after localization. It provides functorial factorizations and lifting on arbitrary strict -categories, including those that are not freely generated, which is what the small-object argument needs. The key new input is a couniversality theorem: pushouts of along sieves with a right adjoint retraction are Street weak equivalences (Theorem 5.2, p. 18), which is the remaining sufficient condition of Ara–Maltsiniotis.
Formalizing it. Mathlib has simplicial sets and model-category foundations but no strict -categories, orientals or Street nerve. A complete development adds these, Steiner's directed complexes, Gray cylinders and local presentability of , all reusable in higher category theory.
The transfer theorem reduces the model structure to a pushout condition, and that is the hard part: categorical pushouts of strict -categories can create many new composites, so the nerve of a pushout is not the pushout of nerves. Thomason controlled this in dimension 1 with Dwyer maps, but that method does not extend directly. The preprint builds explicit stationary directed prisms (Lemma 3.1, p. 10) that are constant on the old part, so contractions glue across any attachment, and then reduces general posets to finite ones via sieve covers (Corollary 4.5, p. 16; Lemma 4.6, p. 17). Properness (Proposition 7.3, p. 26) and the unit comparison after two subdivisions (Proposition 7.4, p. 27) are separate arguments.
OmegaCategory is a structure with a type of cells, source/target maps indexed by ℕ, partial compositions, the globular, unit, associativity and interchange laws, and finite dimension of each cell. Finite uses a full subcategory NCategory n.FullMain asserts: the Kan–Quillen model structure on SSet exists with the standard classes; and, for and every finite , an ExactModelEndpoint for : a ModelCategory whose weak equivalences, fibrations and cofibrations are exactly ; and ; both weak factorization systems; completeness, cocompleteness and local presentability; left and right properness; left Quillen; and the Quillen-equivalence criterion at fibrant targets.n : ℕ, including , which the source does not consider; the identity holds there by the same argument.Purely infinite -algebras are the infinite counterpart of the finite, tracial algebras: every positive element can absorb copies of itself. In the simple case they are the Kirchberg algebras, classified by K-theory. For non-simple algebras, Kirchberg and Rørdam introduced three versions of pure infiniteness (weak, ordinary, strong) and showed that the strongest one is equivalent, for separable nuclear algebras, to absorbing the Cuntz algebra tensorially, the regularity property that underlies Kirchberg's classification of non-simple purely infinite algebras. Whether the three notions coincide is Kirchberg–Rørdam's Question 9.5, listed as Problem LXXII by Schafhauser, Tikuisis and White.
The source of this mission is an OpenAI preprint dated September 25, 2026, which proves ordinary strong in general and weak ordinary for exact algebras.
All -algebras are complex and may be nonunital or nonseparable. For positive in matrices over (or in ), write (Cuntz subequivalence) if there are with in norm; matrices of different sizes are compared after zero padding. A positive is properly infinite if (zero counts as properly infinite). The paper uses two conditions:
is strongly purely infinite if for all and there are with
is exact if preserves short exact sequences of -algebras.
If satisfies (P), then for all , , there are with
in particular is strongly purely infinite.
The Lean statement OAI.WeakPureInfiniteness.exact_weaklyPurelyInfinite_stronglyPurelyInfinite is open on the platform.
Theorem 1.1 answers the ordinary-to-strong part of Problem LXXII for arbitrary algebras, and Theorem 1.2 answers the whole comparison question for exact (hence for nuclear) algebras. With Kirchberg's results, every separable nuclear algebra satisfying () absorbs (Corollary 1.3), with no unitality or simplicity assumption: a single finite amplification test characterizes this tensorial regularity. The weak-to-ordinary implication for non-exact algebras remains open.
These results are stated in an OpenAI preprint; they have not been peer reviewed, and no machine-checked proofs exist.
For non-simple algebras, comparing one positive element with itself and comparing two elements simultaneously are different demands: strong pure infiniteness must also kill a mixed entry , and earlier proofs needed control of the ideal structure (Hausdorff primitive spectrum, ideal property, topological dimension zero). Removing a fixed amplification similarly needs enough orthogonal equivalent pieces in hereditary subalgebras, which earlier work extracted from Global Glimm-type hypotheses. The difficulty is to obtain this uniformly over primitive quotients when is not Hausdorff.
NonUnitalCStarAlgebra with the order (StarOrderedRing); no unit, separability or simplicity is assumed.CStarMatrix blocks, witnessed by rectangular matrices with for every ; is diagonalCopies n h; WeaklyPurelyInfinite fixes one before quantifying over nonzero positives.Exact is stated with minimal tensor products realized inside over all pairs of Hilbert-space representations, and tests surjections in the same universe.PropertyP is (P).StronglyPurelyInfinite is the three-inequality condition above, with no norm bound on .A complete development needs Cuntz comparison, stabilizations, minimal tensor products and exactness, primitive ideal spaces and hereditary subalgebras; this is reusable for other regularity missions. Contributions formalizing Proposition 2.2-style transport lemmas and Corollary 1.3 (via Kirchberg's absorption theorem) are welcome.
Free probability treats bounded self-adjoint operators in a tracial von Neumann algebra as noncommuting random variables, and the free analogue of independence is freeness. Voiculescu introduced two candidate analogues of Shannon entropy for such tuples. The microstates free entropy measures how large the set of matrix tuples imitating the joint moments of is (Voiculescu 1994). The nonmicrostates free entropy is built instead from free Fisher information, by integrating along the addition of free semicircular noise (Voiculescu 1998). The two agree for a single variable, and whether they agree in general is part of Voiculescu's unification problem (Voiculescu 2002, Sections 3.5 and 3.8). Guionnet stated the finite-entropy formulation explicitly: does imply ? (Guionnet 2004, Conjecture 7.1).
The question matters because carries the strongest structural consequences for von Neumann algebras (it is the tool behind results such as Ge's theorem that free group factors are prime, Ge 1996), while is far more computable. Equality would let analytic computations of transfer to .
This mission asks for a machine-checked proof of Theorem 1.1 of an OpenAI preprint dated September 25, 2026 (source), which claims a tuple with . The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.
Let be a von Neumann algebra with a faithful normal tracial state , and a tuple of self-adjoint elements of .
Microstates. For , , and a matrix size , let be the set of -tuples of self-adjoint complex matrices with operator norms at most whose normalized traces of all words of length are within of the corresponding -moments of . Volume is Lebesgue measure for the unnormalized Hilbert–Schmidt inner product. Then
Free Fisher information. Vectors in the -closure of polynomials in are conjugate variables if for every noncommutative polynomial , where is the free difference quotient. Then , or if no conjugate variables exist.
Nonmicrostates entropy. With a standard free semicircular family free from ,
There exist and a bounded self-adjoint tuple in a von Neumann algebra with faithful normal tracial state such that
The Lean goal OAI.FiniteEntropySeparation.main asserts exactly this, with the semicircular family required to lie in the same algebra.
The result itself. The theorem answers the finite-entropy equality question negatively: finiteness of does not force , so the matrix-approximation and Fisher-information definitions are genuinely different invariants even in the finite regime. Known equality results therefore cannot be extended by finiteness alone; any equality theorem must use structure such as convexity of a potential. The preprint notes that it does not settle the question for each fixed small number of variables.
Formalizing it. No formal definitions of free entropy, free Fisher information or free semicircular systems are known to exist in a proof assistant. A complete development would formalize both entropies, the comparison in the form needed, Gaussian asymptotic freeness, cumulant calculus and matrix-volume estimates, all reusable across free probability.
Both entropies are hard to compute for any non-free tuple, and the gap must survive two limits that interact badly: the over matrix size in and the integral over noise time in . The preprint's tuple couples free semicirculars with a commuting discrete variable that creates spectral blocks; after perturbing by small semicircular noise, is finite (Lemma 4.2, p. 9). The analytic side needs a Fisher-information bound in terms of higher cumulants (Proposition 3.2, p. 6), which makes nearly Gaussian at a suitable noise scale, while the matrix side must show that microstates, after GUE evolution, retain detectable block structure that independent GUE matrices of the same variances lack (Lemma 6.1, p. 12). Matching the two requires a finite-time entropy-production comparison along one fixed sequence of matrix laws (Lemma 5.1, p. 10); a naive application of loses exactly the deficit being sought.
VonNeumannAlgebra H on a complex Hilbert space ; the trace is a vector state given by a unit vector that is tracial on and separating for (so the state is faithful and normal).Fin n-indexed self-adjoint elements of . FreeStandardNoise requires each to have the semicircle moments (Catalan numbers) and the unital algebras generated by and by each to be free.ℝ≥0∞, equal to when no conjugate system exists.EReal built from the positive and negative parts of the integrand as lower Lebesgue integrals over .EReal logarithms (volume zero gives ).A von Neumann algebra is a unital algebra of bounded operators on a Hilbert space that is closed under adjoints and in the weak operator topology. For a set of operators, denotes the smallest von Neumann algebra containing . The generator problem, going back to Kadison's 1967 list of problems, asks whether every von Neumann algebra with separable predual is singly generated, for a single bounded operator ; equivalently, whether two self-adjoint operators always suffice. It is one of the oldest structural questions about von Neumann algebras, and by classical reductions everything comes down to type II factors.
The source of this mission is an OpenAI preprint dated September 23, 2026, which claims single generation for every II factor with separable predual.
Let be a complex Hilbert space and a unital -subalgebra closed in the weak operator topology. is a factor if its centre is ; it is finite if every isometry () is unitary; it is diffuse if every nonzero projection has a proper nonzero subprojection. A nonzero finite diffuse factor is a type II factor; it carries a unique faithful normal tracial state , with . has separable predual if is isometrically the dual of a separable Banach space; this does not require or to be norm-separable.
An inclusion of factors is irreducible if . denotes the unitary group.
For an irreducible inclusion of II factors with of separable predual,
The Lean statement OAI.Generator.single_generation_of_II1_separable_predual is open on the platform.
Combined with Willig's reduction and the known type I and properly infinite cases, Theorem 1.2 gives single generation of every von Neumann algebra with separable predual, an affirmative answer to the generator problem. The paper also deduces that the generator invariants and of Dykema–Sinclair–Smith–White vanish for every such factor, and that Voiculescu's free entropy dimensions are not invariants of the generated algebra (Corollary 6.1), since has both a free semicircular -tuple and a self-adjoint pair as generators. Theorem 1.1 is of independent interest: it shows that relative generators are generic, not merely existent.
These results are stated in an OpenAI preprint; they have not been peer reviewed, and no machine-checked proofs exist.
Earlier positive results all relied on extra structure (Cartan subalgebras, property , tensor decompositions, sequential commutation) to build a generator. Without such structure one must show that a unitary generates over , which requires detecting every vector of through words in and . Perturbing along a long word changes it many times, and operator-norm bounds on the accumulated perturbation grow with the word length; a length-uniform estimate is needed. The Baire-category step also needs the projection onto to vary semicontinuously in .
StarSubalgebra ℂ (H →L[ℂ] H); WOTClosed uses Mathlib's weak operator topology, and wstar s is the infimum of WOT-closed star-subalgebras containing (unital by construction).IsII1Factor = nonzero Hilbert space, WOT-closed, trivial centre, finite (isometries are unitary), diffuse. No trace is assumed.HasSeparablePredual asks for a separable Banach space in the same universe with a conjugate-linear isometric equivalence between its dual and the algebra; this is equivalent to the usual condition.IsNormalizedTrace: normalized, positive, faithful, tracial, ultraweakly continuous), the topology on unitary large is generated by trace 2-distance balls, and the locus is .A complete development needs the standard theory of II factors (trace, , conditional expectations, ultrapowers), Popa's free independence in ultraproducts and irreducible hyperfinite subfactors, Haagerup's inequality for free groups, and the Baire category theorem on the unitary group. This infrastructure is reusable across operator-algebra missions. Contributions formalizing Proposition 3.2 (perturbation bounds) and Popa's irreducible hyperfinite embedding (Theorem 5.1) are welcome.
A closed subspace of a Hilbert space is hyperinvariant for a bounded operator if for every operator commuting with . 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: has no such subspace exactly when its commutant is transitive. A related classical question asks whether every unital transitive operator algebra is strongly dense in ; Arveson's density theorem gives a positive answer when the algebra contains a maximal abelian self-adjoint subalgebra.
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.
Let be a complex Hilbert space and its bounded operators. For :
For every infinite-dimensional separable complex Hilbert space there is 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.
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 . 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 , 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.
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 invariant. The essential step is a bounded operator commuting with 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.
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.Tendsto (fun n => ‖T ^ n‖ ^ (1 / n)) atTop (𝓝 0) (the term is irrelevant to the limit).TopologicalSpace.induced from the pointwise (product) topology on functions H → H.A complete development needs vector-valued 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.
The invariant subspace problem asks whether every bounded operator on a separable infinite-dimensional complex Hilbert space has a nontrivial closed invariant subspace. Inside a finite von Neumann algebra there is a sharper, algebra-relative version: given in a type factor , is there a projection with and , i.e. a nontrivial -invariant subspace whose projection lies in ? The Brown measure, built from the Fuglede–Kadison determinant, gives such projections whenever it is not a point mass (Haagerup–Schultz). The open territory is therefore operators whose Brown measure is a point mass, in particular quasinilpotent ones.
Zhu, Fang and Shi (2017) studied the weighted irrational rotations in the hyperfinite factor and asked whether must have a nontrivial invariant projection when is nonzero almost everywhere, is nonconstant and the determinant of is zero. This mission formalizes a negative answer for every prescribed irrational angle.
The source of this mission is an OpenAI preprint dated September 27, 2026.
Fix an irrational . Let be the von Neumann algebra generated by unitaries with and trace for , ; it is the hyperfinite factor. Concretely, on , shifts the coordinate and multiplies the -th coordinate at by . For a continuous set . A projection is invariant for if ; it is nontrivial if . The Fuglede–Kadison determinant of is , with the normalized Haar measure.
For every irrational there is a continuous with
such that every projection with equals or ; moreover , , and .
The goal OAI.Invariant233.Results.prescribed_irrational_counterexample is open on the platform.
Theorem 1.1 answers the Zhu–Fang–Shi question negatively, with the angle fixed in advance and no Diophantine condition. Combined with Dykema's observation that hyperinvariant subspaces of have projections in , it yields (Corollary 1.4) a nonzero quasinilpotent operator on every separable infinite-dimensional Hilbert space with no nontrivial hyperinvariant subspace, so its commutant is a proper, strongly closed, transitive unital algebra. It also shows that, at determinant zero, the Haagerup–Schultz method cannot be supplemented by any invariant projection in the factor for these operators. The conclusion concerns projections in ; ordinary invariant subspaces of the Hilbert-space representation are not excluded.
The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists.
Brown-measure methods give nothing here: at determinant zero the Brown measure is , so Haagerup–Schultz projections are trivial, and point-mass Brown measure does not by itself exclude invariant projections (Dykema–Haagerup, Tucci). One must show directly that a hypothetical invariant projection, viewed as a measurable field of projections, contradicts weighted orthogonality identities along rotation orbits. The weight's logarithmic drops must be rare enough to keep a finite window under control yet strong enough to suppress the infinite tail, and this must work at an arbitrary prescribed angle, which forces large divisible frequencies. Passing from a measurable weight to a continuous one with a single zero requires an intertwining multiplier that may be unbounded.
AddCircle (1:ℝ) with Haar probability; the zero of is at , which corresponds to .Lp (lp (fun _ : ℤ => ℂ) 2) 2 circleMeasure; Rotation.U is the fibrewise shift and Rotation.V θ multiplies by ; Rotation.algebra θ is the double commutant of .HasOnlyTrivialInvariantProjections M T quantifies over self-adjoint idempotents with ; no commutation with is required.NormQuasinilpotent T is ; the determinant is the vector-state Fuglede–Kadison determinant , avoiding .A complete development needs crossed-product (group-measure-space) von Neumann algebras, measurable fields of projections, the Fuglede–Kadison determinant, and uniform averaging under irrational rotation. Contributions formalizing Theorem 5.2 (the measurable-weight obstruction), Lemma 5.1 (conditional convolution obstruction), Corollary 6.2 (quasinilpotence) and Lemma A.4 (the product algebra is a factor) are welcome.
The classification programme for simple nuclear -algebras identifies a class of algebras that are determined by K-theory and traces. Membership in that class is governed by regularity properties: finite nuclear dimension, absorption of the Jiang–Su algebra , and strict comparison. Uniform property , introduced by Castillejos, Evington, Tikuisis, White and Winter, is a central divisibility condition: it asks for projections in a central sequence algebra that cut every trace exactly in half, uniformly across the whole trace space, while preserving trace values against fixed coefficients. Together with strict comparison it is equivalent to -stability for simple separable unital nuclear algebras (Castillejos–Evington–Tikuisis–White). Schafhauser, Tikuisis and White asked (Problem XXI of their problem list) whether real rank zero of the uniform tracial ultrapower of the tracial completion already forces uniform property .
The source of this mission is an OpenAI preprint dated September 23, 2026, which answers Problem XXI affirmatively (and, by separate arguments, also treats the unital Toms–Winter conjecture).
Let be a unital -algebra with nonempty set of tracial states. The uniform 2-seminorm is
The uniform tracial completion consists of bounded sequences in that are Cauchy for , modulo those tending to zero; each extends to a designated trace on . For a free ultrafilter on , the uniform tracial ultrapower is the algebra of bounded sequences in modulo those whose uniform 2-norm tends to zero along . Its limit traces are
and denotes the set of these. embeds in as constant sequences.
A unital -algebra has real rank zero if every self-adjoint element is a norm limit of self-adjoint elements with finite spectrum. is stably finite if every isometry in every matrix algebra over is unitary, and nuclear if its algebraic tensor product with any -algebra carries a unique -norm.
Let be unital, separable, simple, infinite-dimensional, nuclear and stably finite with , and let be a free ultrafilter. If has real rank zero, then there is a projection with
This is the halving formulation of uniform property used in Problem XXI. The Lean statement OAI.ComparatorModel.CurrentMain.main is open on the platform.
The theorem shows that real rank zero at the level of the tracial ultrapower is enough to produce uniform property , with no restriction on the trace space; the paper also deduces that every trace on is a designated extension (Corollary 1.2). Since uniform property plus strict comparison gives -stability, this links projection structure in tracial ultrapowers to the Toms–Winter regularity theory. The equivalence between the halving formulation and the usual all- formulation is due to Carrión et al.
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.
Real rank zero supplies many projections in , but nothing makes them central, and halving must hold simultaneously for every limit trace and every coefficient . Divisibility results derived from real rank zero (Vaccaro) give tracially large order-zero maps without centrality; uniform property needs commutation with all of and exact coefficient identities. Equality of the scalar traces alone is not enough. Nuclearity by itself does not suffice either, as Toms' AH example shows, so the real rank zero hypothesis must be used in an essential way.
TracialState A is a positive linear functional with and ; the order on is the order (StarOrderedRing).U, computed with the designated traces .TopologicallySimple, StablyFinite (via CStarMatrix), IsNuclear (subsingleton of -norms on algebraic tensor products, in a fixed universe) and RealRankZero (finite-spectrum self-adjoint approximation) are defined directly.UniformPropertyGammaAt A U asserts a star projection commuting with the image of and halving familyLimitTrace … s for every sequence of traces s : ℕ → TracialState A.MainClaim existentially packages five auxiliary Prop classes (quotient -norm, closure properties of null and Cauchy sequences, existence of ultralimits, and vanishing of limit traces on null sequences). They are true general facts that a proof must establish; they are not assumptions.A complete development needs ultrapowers and tracial completions of -algebras, nuclearity and completely positive approximation, and real rank zero; all of this is reusable for the other regularity missions of this family. Contributions formalizing Theorem 1.3 (finite-set central splitting) and Corollary 1.2 are welcome.
How rigid is a von Neumann algebra inside ? If two algebras have unit balls that are uniformly close, must they be the same algebra up to a small change of coordinates? Kadison and Kastler introduced the distance between the unit balls in 1972 (Amer. J. Math. 1972) and asked whether sufficiently close algebras are spatially isomorphic, implemented by a unitary close to the identity. The positive answer for a class of algebras is called (strong) Kadison–Kastler stability. The problem connects perturbation theory, Hochschild cohomology, and Kadison's similarity problem, and it was settled previously only for injective (amenable) algebras, type I algebras, and specific nonamenable examples.
This mission asks for a formal proof of the uniform strong Kadison–Kastler stability theorem stated in an OpenAI preprint dated September 23, 2026 (source): a single tolerance works for all von Neumann algebras on all Hilbert spaces. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Let be a complex Hilbert space and the bounded operators with the operator norm. A von Neumann algebra is a unital -subalgebra equal to its double commutant (in particular it contains the identity ). Write for its unit ball. The Kadison–Kastler distance is the Hausdorff distance of unit balls,
A unitary conjugates to if .
For every there is such that for every complex Hilbert space and all von Neumann algebras with , there is a unitary with
The tolerance depends only on : not on the algebras, their type, their representations, or the size of .
The result itself. It answers the Kadison–Kastler perturbation question in its strongest uniform form for von Neumann algebras, including all nonamenable and type III cases and non-separable Hilbert spaces. Consequences include that every algebraic or analytic invariant preserved by unitary conjugacy (type, factoriality, property , Cartan subalgebras) is locally constant in the Kadison–Kastler metric. The analogous C*-algebra statement fails in its uniform-unitary form by Johnson's examples, so the theorem is specific to von Neumann algebras.
Formalizing it. The statement uses only Mathlib's VonNeumannAlgebra, unitary operators and Hausdorff distance, so it is fully expressible today. The proof, however, draws on free probability, tracial ultraproducts, Tomita–Takesaki theory, crossed products, Poisson boundaries and measurable cocycles, most of which are absent from Mathlib. Formalizing even the amenable (injective) case would be a substantial reusable contribution.
Closeness of unit balls supplies nearby elements but no linear or multiplicative correspondence between the algebras, and it gives no control at matrix levels, where perturbation arguments naturally live. For nonamenable algebras the classical route through vanishing Hochschild cohomology is unavailable. The preprint proceeds by cases. For finite factors it proves a uniform bound on all matrix amplifications of commutator maps (Theorem 3.1, p. 11) and corrects nearby unitaries to a measurable cocycle over an amenable boundary action (Section 4). Infinite factors require comparing modular groups through Tomita graphs (Proposition 6.5, p. 41) and aligning the modular action (Proposition 7.1, p. 45) before passing to crossed products (Theorem 8.4, p. 59). General algebras then require aligning centers and passing from separable to arbitrary Hilbert spaces (Section 9) without losing uniformity.
NormedAddCommGroup, InnerProductSpace ℂ, CompleteSpace) in a fixed universe u; is chosen before , so the uniformity over Hilbert spaces is part of the statement.VonNeumannAlgebra H is Mathlib's notion; these algebras contain the identity, so "unital with identity " is built in.kkDistance M N is Metric.hausdorffDist of the closed unit balls. Both balls contain and are bounded, so the Hausdorff distance is finite and the definition is exactly (1.1).NearConjugacy M N ε asks for a unitary with as sets and .A quantum channel models how a physical system, used to carry information, is corrupted by its environment. The classical capacity of a channel is the largest rate, in bits per use, at which classical messages can be sent with vanishing error when the sender may encode into arbitrary — possibly entangled — states of many uses and the receiver may measure all outputs jointly. The Holevo–Schumacher–Westmoreland coding theorem (Holevo 1998; Schumacher–Westmoreland 1997) expresses this capacity as a regularized limit of the Holevo information over ever larger blocks of uses. Since Holevo information is not additive in general (Hastings 2009), computing the capacity of any specific channel requires a channel-specific additivity argument, and exact formulas are known only for a few families.
Generalized amplitude damping is the standard model of a qubit relaxing toward a thermal state: it loses or gains an excitation with probabilities set by a damping strength and a stationary excited population , and its coherences decay. It is one of the basic noise models of quantum information theory.
For the generalized amplitude-damping channel acts on a qubit density matrix by
and independent uses act as on matrices. With , the Holevo information in bits is
over all finite ensembles of input states (entangled across uses when ). The classical capacity is the supremum of rates for which there are -use codes — arbitrary input states for each of equiprobable messages and one joint measurement of all outputs — with average error tending to zero and ; there is no shared entanglement or feedback. Write for binary entropy in nats, and .
For all and every ,
the maximum is attained, , and for every maximizer the equiprobable independent products of the two signals attain at every block length. The goal is published on the platform with status Open.
The result itself. The theorem gives a closed one-variable formula for the classical capacity of every generalized amplitude-damping channel, removing the regularization over block lengths: entangled input signals across uses give no advantage, and a simple product code with two signals per use is optimal. This settles the ordinary amplitude-damping case listed as open by LKDW 2018 and extends beyond the pure-output criterion of Tang et al. to the thermal regime, where the channel has no pure output. The source further proves additivity of Holevo capacity, minimum output entropy and classical capacity when the channel is used in parallel with any finite-dimensional partner channel (Corollary 1.2); that corollary is not part of this goal.
Formalizing it. The goal ties together an operational capacity (codes and error probabilities), an entropic quantity (a supremum over unrestricted ensembles on -dimensional matrices), and a scalar optimization. A machine-checked proof would certify both the matrix entropy inequality at the heart of the argument and the converse direction of the coding theorem. Mathlib does not currently contain quantum channel capacity theory, so the definitions here are new infrastructure.
Optimizing a single use gives a lower bound on capacity; the difficulty is the matching upper bound for all simultaneously, where an input may be entangled across all uses. Holevo additivity is false for general channels, so no abstract argument applies, and for interior thermal occupation with the channel has no pure output, which rules out the recent pure-output criterion. The proof needs a lower bound on the entropy of the output of an arbitrary entangled block input, i.e. a matrix entropy inequality for block-structured states that is tight on product inputs. Identifying the capacity with the regularized Holevo quantity also requires the full coding theorem and a Fano-type converse.
Fin n → Fin 2; the -use channel is given by tensor products of the four standard Kraus operators of generalized amplitude damping, which reproduce the displayed action exactly.Tr (cfc negMulLog P) (nats, ); Holevo values are divided by (bits). holevo γ ν n is the sSup over all finite ensembles of arbitrary -dimensional states, with no product or purity restriction.capacity is the sSup of operationally achievable rates: codes with any positive number of messages, arbitrary state encodings, an arbitrary POVM decoder, average error tending to , and the liminf rate condition. It is defined operationally, not by regularization, so the identity includes the coding theorem.Real.binEntropy (nats); the maximizer is over . The final clause also asserts that the phase-product signals are states.