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.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
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?
Finite patterns fit inside positive-measure sets after a sufficiently small affine change. The dyadic similarity problem asks whether one particular infinite pattern can be excluded even from compact sets of nearly full measure. The source manuscript presents the surrounding research claim.
The dyadic sequence is D={2⁻ⁿ:n≥1}. Its affine copies are x+sD with arbitrary x∈ℝ and nonzero signed scale s. The ambient measure is Lebesgue measure on the real line.
For every 0<η<1, construct a compact E⊆[0,1] with
The same E must avoid every translation and both signs of dilation.
The selected formal target is OAI.Problem310.dyadic_affine_avoidance.
The result concerns the dyadic sequence specifically, with a stronger near-full-measure conclusion than merely finding one positive-measure avoiding set. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Excluding a countable collection of copies does not handle the continuum of scales and centers. Finite initial segments cannot replace the entire sequence.
The definition dyadicPoint accepts n=0, but the theorem explicitly chooses n≥1. Measure is ENNReal-valued and compares with ENNReal.ofReal(1−η). Compactness and interval containment are required conclusions. General infinite sets are outside this selected target.
adc7f1241b42. Goal source.Choosing real signs in a polynomial controls how much its values can peak around the unit circle. The target seeks asymptotically optimal maximum modulus at every sufficiently large length. The source manuscript presents the surrounding research claim.
A real Littlewood polynomial has consecutive coefficients εₖ∈{−1,1}: P_N(z)=Σₖ₌₀ᴺ⁻¹ εₖzᵏ. The coefficient family may depend on both its length and the requested accuracy.
Prove
All sufficiently large integer lengths are required, rather than a subsequence.
The selected formal target is OAI.AsymptoticallyMinimalLittlewood.main.
The selected target is the uniform maximum-modulus assertion. The companion finite-flatness target gives one sign family whose normalized modulus tends to one in every positive finite Lᵖ moment. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Control at finitely many sample points does not directly give a bound on the full circle. Uniformity in the circle variable and coverage of all large lengths are separate obligations.
Coefficients are real-valued Fin N functions explicitly constrained to ±1 and evaluated as complex polynomials. The companion theorem uses Haar probability on UnitAddCircle and a single family for every p>0. Both independent definition groups are referenced; finite-flatness is a related endpoint rather than a claimed prerequisite.
adc7f1241b42. Goal source.Integral-means spectra record the worst derivative concentration among normalized conformal maps. A strict bound at exponent −1 tests a specific predicted value of that spectrum. The source manuscript presents the surrounding research claim.
For a normalized univalent disk map f, M(−1,f,r) is the average of |f′|⁻¹ on the circle of radius r. The bounded spectrum B_b uses the extended-real limsup growth exponent, then takes its supremum over maps with bounded image.
Prove that there exist real ε and C with 0<ε<1/4 such that
for every normalized univalent f and 1/2≤r<1. Also prove B_b(−1)<1/4 and the failure of the defined Kraetzer prediction to equal B_b at every real exponent.
The selected formal target is OAI.StrictInverseFirstPower.main.
A strictly positive uniform ε is the content of the improvement. The target explicitly includes the spectrum consequence and the negation of the full predicted formula. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
An exponent arbitrarily close to 1/4 from above does not give a strict gap below 1/4. The same ε and C must precede the quantification over f and r.
The circle estimate covers all normalized univalent maps, whereas the spectrum uses the bounded-image subclass. Complex derivatives, real interval integrals and EReal suprema are the supplied representations. The prediction is the specified piecewise quadratic/linear function.
adc7f1241b42. Goal source.The size of the derivative of a conformal map can concentrate near a domain boundary. Brennan-type integrability and inverse-square integral means quantify how severe that concentration can be. The source manuscript presents the surrounding research claim.
A schlicht function is an injective holomorphic map f on the unit disk with f(0)=0 and f′(0)=1. M(f,t,r) is the circle average of |f′|ᵗ at radius r, and B(t) is the supremum of the associated extended-real boundary growth exponents.
Prove the four-part MainStatement, including
uniformly for schlicht f and 1/2 ≤ r < 1. For conformal bijections φ:W→𝔻 on the specified simply connected domains, prove area integrability of |φ′|ˢ for 4/3<s<4; for univalent disk maps prove integrability of |f′|ᵗ for −2<t<2/3.
The selected formal target is OAI.Brennan.main_theorem.
The goal packages the uniform circle bound, exact spectrum value and both area-integrability formulations. A separate endpoint target records sharp failure for the Koebe map and its inverse. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
A growth bound with a constant depending on f does not supply the stated uniform estimate. Boundary behavior must also support the precise open exponent intervals.
Planar Lebesgue area, a left-hand limit r→1, and extended-real spectra are fixed. W must be open, connected, simply connected and have nontrivial spherical boundary. Main and sharp-endpoint definitions are independent published groups with repeated names, so references coexist without one aggregate import.
adc7f1241b42. Goal source.Algebraic ampleness and positivity of a smooth Hermitian metric are different kinds of positivity for a vector bundle. The target asks for one concrete family where they separate. The source manuscript presents the surrounding research claim.
The quadric surface is ℙ¹×ℙ¹. Rank-two algebraic bundles are specified by principal affine charts and regular 2×2 transition matrices. For a bundle G, E(m) is its coordinatewise m-th-power pullback twisted by the polarization O(1,1).
Construct G and a family E(m) such that
for one positive integer m₀, with the required pullback-twist identities for every positive m.
The selected formal target is OAI.QuadricCounterexample.main_theorem.
The assertion compares two precise positivity conditions on the same family. The goal is existential and does not provide a numerical threshold m₀. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Proving ampleness supplies projective sections, whereas excluding every positive metric is a quantified differential-geometric obstruction. Testing one candidate metric cannot settle nonexistence.
The reference defines ℙ¹ as the one-point compactification of ℂ, bundles by cocycles, ampleness through symmetric sections giving a closed projective embedding, and strict positivity by a matrix Hessian expression. SourceMainTheorem retains all of these conventions. Only the published definition block and target are attached.
adc7f1241b42. Goal source.A hypersurface can be abstractly affine space without its defining equation being an ambient coordinate. Distinguishing these two properties is the embedding question behind the Abhyankar–Sathaye problem. The source manuscript presents the surrounding research claim.
For n ≥ 4, let R=ℂ[X₀,…,Xₙ₋₁]. A polynomial F is a coordinate if a ℂ-algebra automorphism of R sends some variable Xᵢ to F. Its zero fiber is represented by the quotient R/(F).
For every n ≥ 4, find F with
The source supplies an explicit construction, while this selected goal asks for existence.
The selected formal target is OAI.AbhyankarSathaye.exists_noncoordinate_polynomial.
The target separates the intrinsic affine-space quotient from ambient polynomial equivalence in every dimension at least four. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
An isomorphism of the quotient rings need not extend to an automorphism of the ambient ring. Both the quotient isomorphism and the failure of every possible coordinate automorphism must be established.
The goal uses multivariate polynomials indexed by Fin n, a principal ideal, and ℂ-algebra equivalences. A separate published derivation target and its explicit polynomial definitions are retained as related references. That target concerns n−1 commuting locally nilpotent derivations, their common kernel and ordinary extra-variable partial derivatives; it is not asserted as a logical dependency of the existence goal.
adc7f1241b42. Goal source.Logarithmic Kodaira dimension measures the supply of pluricanonical forms allowed poles along a boundary. Its behavior in a fibration depends especially on the case where a general fiber has no such nonzero forms. The source manuscript presents the surrounding research claim.
A stratum-smooth fibration is a surjective connected-fiber morphism of smooth projective complex varieties with reduced simple-normal-crossing boundaries E and D. The pullback of the base boundary is supported in E; the total space and every boundary stratum are smooth away from D.
Very generally on the base, the point lies outside D and every supplied fiber model F satisfies
with every positive-degree logarithmic pluriform section on the total space equal to zero.
The selected formal target is OAI.ReverseLogKodaira.SmoothProjectiveVariety.veryGenerally_fiber_negative_branch.
This is the fiber-negative branch of the manuscript’s wider additivity claim. Its vanishing assertion is part of the goal, not merely explanatory background. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
The conclusion concerns all positive tensor degrees and every fiber model over very general points. One fixed fiber or one vanishing space of sections would not suffice.
The definitions use schemes over ℂ, ideal-sheaf boundaries, exterior powers of Kähler differentials, and rational pluriform lattices. Kodaira dimension takes values in WithBot ℕ∞. Very generally means outside a countable family of proper closed subsets. The nonnegative branches and full reverse inequality are not additional attached targets.
adc7f1241b42. Goal source.A planar prime walk can go around a gap that would block a walk on a line. The Gaussian moat problem therefore asks for an obstruction to every possible bounded-step route through distinct Gaussian primes. The source manuscript presents the surrounding research claim.
A Gaussian prime is an irreducible element of ℤ[i]. For D ∈ ℝ, two distinct primes are adjacent when their Euclidean distance is at most D. A component contains every prime reachable by a finite path.
Prove the conjunction
The second clause also bounds the length of every finite injective D-step prime chain by B and asserts component finiteness.
The selected formal target is OAI.GaussianMoat.fullMain.
The same B must work for every starting prime at a fixed step bound. The theorem makes no numerical claim about this bound. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Showing that each component is finite does not give a uniform bound across starting points. Every route in two dimensions and primes on the axes remain within the quantification.
The formal graph uses Mathlib Gaussian integers and complex Euclidean distance. Step bounds range over all real numbers. MainEndpoint and UniformEndpoint are both mandatory clauses of fullMain. Only that published target and its definitions are supplied.
adc7f1241b42. Goal source.Birational anabelian geometry studies how much of a function field is determined by a small quotient of its absolute Galois group. This mission isolates uniqueness in the reconstruction correspondence. The source manuscript presents the surrounding research claim.
Fix a prime ℓ. The fields K/k and L/l are essentially finite type extensions of algebraically closed constant fields, have transcendence degree at least two, and have characteristic different from ℓ. The abelian-by-central datum records the pro-ℓ abelian quotient and the commutator pairing. IsomF consists of constant-preserving perfect-closure isomorphisms modulo Frobenius; IsomCUnits quotients bracket-compatible Galois isomorphisms by the encoded ℓ-adic unit relation.
For field-isomorphism classes a and a′ and a Galois-isomorphism class b, prove
PhiGraph is the relation induced by representatives and a compatible extension to algebraic closures.
The selected formal target is OAI.BogomolovPop.main_graph_injective.
This establishes uniqueness of the field class whenever two representatives produce the same Galois class. The manuscript states a full reconstruction bijection; the selected published Lean target is its graph-injectivity assertion. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Equality is required after two different quotient constructions, one generated by Frobenius and one by ℓ-adic scalar limits. Recovering equality of classes must respect both ambiguities and the contravariant Galois action.
The definition block constructs topological pro-ℓ quotients, closed commutator subgroups, perfect closures and the pullback graph. The theorem quantifies over arbitrary field types with the stated algebraic instances. It does not assert existence, surjectivity or functionality of PhiGraph, and those broader manuscript conclusions are not attached as proved results. Only the existing injectivity target and its definition block are referenced.
adc7f1241b42. Goal source.Compatibility between reassociation and braiding imposes equations on formal Lie expressions. The question is whether those equations leave precisely the free family of odd-weight generators predicted by the Deligne–Drinfeld conjecture. The source manuscript presents the surrounding research claim.
Let L be the free Lie algebra over ℚ on x and y, each of weight one. The solution space W satisfies antisymmetry, the three-term relation, and the pentagon equation in the four-strand infinitesimal braid algebra. Its operation is the Ihara bracket {p,q}=Dₚq−D_qp+[p,q]. The free algebra F has generators indexed by k ≥ 0 with weights 2k+3.
Establish a graded bracket-preserving linear equivalence
together with mutually inverse continuous maps on the products of weight pieces. The completed maps must preserve the bracket degree by degree, including the finite convolution sum defining its weight-n component.
The selected formal target is OAI.DeligneDrinfeld.main.
The target simultaneously expresses freeness and exhaustion of the full equation space. Finding a free subalgebra alone leaves the exhaustion assertion unresolved. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
The pentagon relation couples substitutions in the braid Lie algebra. Constructing odd-weight solutions does not by itself show that all solutions are generated by them, nor that the completed bracket has the required compatibility.
The published definition block specifies the braid quotient, tangent construction of D, weighted Lie words, rational submodules and product completions. Generator k has weight 2k+3. The factor spaces carry the explicitly supplied discrete topology. The goal is exactly MainStatement, including its inverse, continuity and completed-bracket clauses. The available reference set supplies the definition block and one target, so no unsupported paper lemmas are attached as milestones.
adc7f1241b42. Goal source.An isotropic elastic body is described by two spatially varying Lamé moduli: the shear modulus and the parameter (the bulk modulus is ). The elastic inverse problem asks whether static boundary measurements, the boundary tractions produced by all prescribed boundary displacements, determine both moduli inside the body. It is the elasticity analogue of Calderón's conductivity problem, with applications to elastography and nondestructive testing, and it is harder because two coefficients are coupled through a vector-valued system rather than a scalar equation.
Without smallness, analyticity or symmetry hypotheses, three-dimensional global uniqueness was not established. The source of this mission is an OpenAI preprint dated September 24, 2026, which claims it for all smooth moduli satisfying the energy-positivity conditions.
Let be a bounded connected domain with boundary, and let satisfy
For a displacement , the strain is , the stress , and the elasticity system is . For boundary data let be the unique weak solution with trace . The displacement-to-traction map is
For admissible pairs , on ,
The Lean statement OAI.Elasticity.global_uniqueness is open on the platform.
The theorem settles the smooth three-dimensional isotropic elastic Calderón uniqueness question under the natural energy-positivity assumptions, with no analyticity, no closeness to constants, and no prior agreement near the boundary. It identifies both moduli from the full zero-frequency boundary operator. It does not give a reconstruction algorithm or stability estimates, which remain natural follow-up questions.
The result is stated in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.
The scalar complex-geometric-optics method does not apply directly to the Lamé system. Earlier reductions to auxiliary systems ran into two problems documented in the Nakamura–Uhlmann erratum: the planar matrix transport equation with prescribed initial data need not be solvable, and the corrected solutions lead to a pseudodifferential rather than a differential identity. The Eskin–Ralston reduction from auxiliary fields to physical displacements is not injective, so equality of physical boundary maps does not by itself give equality of auxiliary Cauchy data. A proof must work with exact physical solutions and keep track of their actual divergences.
Domain Ω: open, connected, bounded, with smooth boundary given by local diffeomorphisms of flattening .Admissible Ω λ μ: both moduli smooth on an open neighbourhood of , with and on .DN Ω λ μ f g is the energy pairing of a weak solution with trace against any representative of ; the goal assumes equality of these two-variable functions and concludes pointwise equality of the moduli on .A complete development needs vector-valued Sobolev spaces, Korn's inequality, the weak Dirichlet problem for the Lamé system, Carleman estimates and complex geometric optics for elliptic systems. These tools are reusable for other inverse problems. Contributions formalizing Lemma 2.1 (common exterior extension), Proposition 2.2 (transfer of physical solutions) and Proposition 3.2 (supported Carleman estimate) are welcome.
Liouville theorems say that certain nonlinear elliptic equations have no positive solutions on the whole space. Beyond their own interest, they are the key input in blow-up and rescaling arguments that give a priori bounds, existence results and singularity estimates for equations on bounded domains (Gidas–Spruck 1981; Polačik–Quittner–Souplet 2007). For the scalar equation , Gidas and Spruck proved nonexistence in the whole subcritical range. For the coupled Lane–Emden system , , the corresponding statement — no positive solutions below the critical hyperbola — is the Lane–Emden conjecture; before the source, it had been proved only in dimensions and in partial ranges. The weighted Hénon–Lane–Emden version, with factors and , asks the same question for the weighted hyperbola.
Fix an integer , exponents and real weights . The Hénon–Lane–Emden system is
where is the Laplacian. A solution in the sense of the source is a pair with and for every , including the origin, satisfying both equations at every . The exponents are subcritical if
In Lean, Space n = EuclideanSpace ℝ (Fin n), IsSolution n p q A B u v packages continuity, ContDiffOn ℝ 2 off the origin, strict positivity everywhere and the two equations with Mathlib's Laplacian and real powers, and Subcritical is the displayed inequality.
This is exactly Theorem 1.1 of the source. Taking gives the unweighted Lane–Emden conjecture (Corollary 1.2) for . The goal is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. If the source's proof is correct, the theorem gives a positive answer to Huang and Zou's Conjecture B and, with , to the Lane–Emden conjecture in every dimension. It needs no radial symmetry, boundedness, integrability, finite energy, stability or growth condition at infinity. Combined with the radial existence theorem of Bidaut-Véron and Giacomini, it also settles Phan's Conjecture C for and , including existence on the critical hyperbola (Corollary 6.2). Through the blow-up method, Liouville theorems of this type give a priori bounds and singularity and decay estimates for Lane–Emden-type systems on bounded domains.
Formalizing it. The statement is elementary: classical derivatives, the Euclidean Laplacian and real powers. The proof uses potential estimates, a localized virial (Rellich–Pohozaev type) identity, a geometric interval inequality and a dilation argument. All of these are within reach of Mathlib's analysis library, which makes the theorem a realistic test of large-scale PDE formalization.
The weighted statement does not follow from the unweighted one at the same exponents. For example, , , is weighted-subcritical, while is unweighted-supercritical. Weighted subcriticality also does not give the unweighted input in Phan's transfer argument. Translations do not preserve the weighted equation, so moving-plane and translation-based compactness arguments are unavailable. The level sets have endpoint values that vary with , which breaks the unweighted interval comparison. Finally, since no energy, decay or stability bound is assumed, the localized energy has to be bounded from the subcritical gap alone.
EuclideanSpace ℝ (Fin n) with , and are real with . Weights are Real.rpow ‖x‖ A, used only at , so the junk value of rpow at never enters. The nonlinearities Real.rpow (v x) p are evaluated at strictly positive arguments.Continuous on all of and ContDiffOn ℝ 2 on . Positivity is required at every point, including the origin, as in the source; differentiability at the origin is not assumed.Heat in an insulated planar plate evolves by the heat equation with Neumann boundary condition. For generic initial temperature, after a long time the temperature minus its average is dominated by an eigenfunction of the first positive Neumann eigenvalue. Rauch asked in 1974 where the hottest and coldest points of the plate end up, and conjectured that they move to the boundary (Rauch 1975). In spectral form, the hot spots conjecture asks whether a first nonconstant Neumann eigenfunction attains its maximum and minimum only on the boundary. The question links spectral geometry, reflected Brownian motion and elliptic PDE, and it is known to depend on topology: it fails for some domains with holes.
This mission asks for a machine-checked proof of the strict form of the conjecture for all smooth bounded simply connected planar domains, as claimed in an OpenAI preprint dated September 24, 2026 (source): every nonzero first-positive Neumann eigenfunction has no interior critical point at all. 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 be a nonempty bounded open simply connected set with boundary. The first positive Neumann eigenvalue is
counting only positive eigenvalues (many sources call it ). The first positive Neumann eigenspace consists of the with and
This weak formulation encodes in with on . Eigenspace functions are smooth up to the boundary.
For every nonzero ,
This holds for every member of the eigenspace, also when is a multiple eigenvalue. In Lean this is OAI.StrictHotSpots.main_theorem.
The result itself. It resolves Burdzy's simply connected planar hot spots conjecture in its strongest form: not only do the extrema lie on the boundary, but there are no interior saddle points either, for every eigenfunction in the eigenspace. Combined with the Burdzy–Werner and Burdzy one-hole counterexamples, it shows that simple connectivity is exactly the dividing line among smooth planar domains. The intermediate kernel theorem (Theorem 5.1, p. 12), a conditional negativity statement for reciprocal Green kernels of the disk, is stated independently of the eigenfunction problem.
Formalizing it. A complete development needs Sobolev spaces on smooth planar domains, the Riemann mapping theorem with boundary regularity, Neumann elliptic regularity, and the theory of conditionally negative definite kernels. Each is reusable. No machine-checked proof of any hot spots result, including the triangle case, is known to exist.
Each Cartesian derivative of an eigenfunction solves the same Helmholtz equation, but its boundary values have no fixed sign, so a maximum-principle argument on one directional derivative fails on a general domain with no preferred direction. Coupling methods need convexity or symmetry. The preprint instead uses the Neumann condition jointly on both derivatives (the gradient is tangent to the boundary), via a nonnegative quadratic form whose null space consists exactly of eigenfunction gradients (Proposition 3.1, p. 7). The central difficulty is to build enough scalar boundary multipliers preserving that null space; this requires proving that a reciprocal kernel is conditionally negative semidefinite (Theorem 5.1, p. 12), through regularized Green kernels, a complete Nevanlinna–Pick-type matrix property, and a boundary limit.
EuclideanSpace ℝ (Fin 2): nonempty, open, bounded, IsSimplyConnected (which includes path-connectedness), with a smooth local defining function with nonzero derivative at every boundary point.HasH1Gradient Ω v g: and is the weak gradient of against smooth test functions compactly supported in . is the sInf of Rayleigh quotients over mean-zero nonzero functions; this set is nonempty and bounded below by .InFirstNeumannEigenspace Ω u requires , mean zero, and the weak eigen-equation for all test pairs. The smoothness-up-to-the-boundary clause is a standard regularity fact for Neumann eigenfunctions on smooth domains (the preprint cites Showalter for it), so it does not exclude any eigenfunction.sInf/sSup of on frontier Ω, which is compact and nonempty, so these are the true minimum and maximum.Calderón's inverse conductivity problem asks whether the electrical conductivity inside a body is determined by voltage and current measurements on its boundary. Mathematically, a conductivity on a domain defines the elliptic equation , and the boundary data are encoded by the Dirichlet-to-Neumann (DN) operator , which maps a boundary voltage to the resulting boundary current. The problem underlies electrical impedance tomography and is the model case of a large family of inverse boundary-value problems. Calderón (1980) posed it for bounded measurable conductivities bounded away from zero; how much regularity uniqueness requires has been a central question since.
In dimension , uniqueness for merely bounded measurable scalar conductivities remained unresolved. The source of this mission is an OpenAI preprint dated September 23, 2026, which constructs a counterexample in dimension three.
Let . A conductivity is a measurable with almost everywhere. Let be the Sobolev space, the closure of compactly supported smooth functions, and the trace space, with dual . For a trace , let be the unique function with trace such that
The DN operator is
There are and with
The Lean statement OAI.ScalarConductivity.main_nonuniqueness is open on the platform.
The theorem shows that scalar Calderón uniqueness fails in the bounded measurable class in dimension three, in contrast with the planar theorem of Astala–Päivärinta and the Lipschitz and uniqueness results in higher dimensions. It locates the regularity threshold for uniqueness strictly between and the known positive classes. By Corollary 1.2, counterexamples can be localized: any finite family of disjoint balls inside any Lipschitz domain supports distinct conductivities with the same DN map.
The result is stated in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.
Matrix-valued counterexamples exist, but they do not transfer to scalar conductivities: scalar coefficients can approximate matrix ones only in the sense of - or -convergence, and Rondi's example shows that exact realization of a full boundary map by a scalar coefficient can fail. Moreover, Daudé–Kamran–Nicoleau note an obstruction for full-boundary data: a weakly harmonic factor with constant full boundary trace is constant. One must therefore match the entire DN operator (every boundary input) exactly, with a scalar coefficient, and with uniform ellipticity bounds; the paper does so with a nested family of scalar blocks realizing prescribed current triples exactly.
IsDirichletToNeumann γ Λ requires existence and uniqueness of the weak -harmonic extension of every trace and the weak flux identity against every .EqualOneNearBoundary asks for with a.e. on ; bounds and measurability are stated almost everywhere on the ball.A complete development needs Sobolev spaces on a ball, weak solutions of divergence-form equations (Lax–Milgram), trace spaces, and the paper's block constructions (convex-integration-type scalarization). Contributions formalizing Theorem 3.1 (exact finite-field scalarization), Proposition 4.1 (branching block) and Corollary 1.2 are welcome.
The relativistic Vlasov–Maxwell system is the basic kinetic model of a collisionless plasma: a cloud of charged particles, described by a phase-space density, moves under the electromagnetic field it generates, and the field evolves by Maxwell's equations with the particles as sources. Whether smooth, compactly supported data in three dimensions always produce a solution that stays smooth for all time has been the central question about the Cauchy problem for this system since the 1980s. Weak solutions exist globally, but they come without regularity or uniqueness, and every previous global classical result required smallness, a dimensional reduction, symmetry, or a nearby global reference solution.
This mission asks for a machine-checked proof of global existence and uniqueness of classical solutions for arbitrary smooth admissible data, as claimed in an OpenAI preprint dated September 23, 2026 (source). The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal below is open.
For momentum let and (the relativistic velocity, ). The unknowns are a particle density and fields , with charge and current densities and . In the one-species normalization the system is
A smooth admissible datum has , , smooth with every derivative bounded and , and satisfies , . A classical solution on is a triple solving the system pointwise, with continuous in time with values in , and with supported in a fixed compact set on each bounded time interval.
Every smooth admissible datum generates a classical solution on with the given initial values; for every finite the solution is on (respectively for the fields) with compact phase-space support on ; and any other classical solution with the same datum agrees with it at every . This is OAI.RVM.global_classical_solution.
The result itself. It settles the large-data global classical regularity problem for three-dimensional relativistic Vlasov–Maxwell, with no size, symmetry or neutrality assumption; nonzero total charge with its Coulomb tail is allowed. Global well-posedness at this level is the starting point for questions about long-time behaviour, scattering and stability of plasma equilibria that previously could only be posed for small or symmetric data.
Formalizing it. The proof combines the Glassey–Strauss representation of fields along backward light cones, energy-flux estimates, a delicate signed bootstrap, and local well-posedness and continuation theory. None of this PDE infrastructure (wave-equation representation formulas, characteristics of transport equations in phase space, Sobolev local theory) is currently available in a proof assistant at the needed level, so each component is reusable.
By the Glassey–Strauss criterion it suffices to bound the momentum support on finite time intervals. The natural approach estimates the absolute value of the force along a characteristic using the retarded field representation and energy flux through light cones. At receiver energy this loses a factor relative to what is needed (Section 1.2, p. 4); the loss comes from sources whose velocity is much closer to the light ray than the receiver's. The preprint instead estimates the signed momentum increment , integrating the retarded force along source trajectories before taking norms (Proposition 2.1, p. 5; Lemma 6.1, p. 24), controls direction changes (Lemma 7.1, p. 29), and closes a bootstrap whose time-to-double lower bounds have a divergent sum (Section 9).
EuclideanSpace ℝ (Fin 3); derivatives are Fréchet derivatives in coordinate directions; the time derivative is derivWithin on , so is one-sided.Admissible encodes with compact support and nonnegativity for ; ContDiff ℝ ∞ with all iterated derivatives bounded and MemLp 2 for ; and both Gauss constraints pointwise.Classical requires regularity on the closed half-spaces, , continuity of into on , compact phase support on each , all five equations pointwise for (including both constraints), and the initial values.In optimal transport on a Riemannian manifold with the quadratic cost , the regularity of optimal maps is governed by a fourth-order curvature quantity of the cost, the Ma–Trudinger–Wang (MTW) tensor. Its nonnegativity on orthogonal pairs, the weak MTW condition (A3w), is necessary for continuity of optimal maps, and together with convexity of the tangent injectivity domains it yields the global geometric "supporting" properties used in regularity theory. Whether weak MTW by itself forces those injectivity domains to be convex was proposed by Villani and proved previously only under a nonfocality assumption, which excludes cut points that are also conjugate points.
Let be a smooth, connected, compact Riemannian manifold without boundary, of dimension , with geodesic distance and exponential map . The open tangent injectivity domain at is
the set of velocities whose geodesic is still minimizing slightly beyond time one. With , the MTW quantity at is
and weak MTW means whenever , for all and . No nonfocality, strict positivity, or prior convexity is assumed.
In Lean, is a Mathlib Riemannian manifold modelled on EuclideanSpace ℝ (Fin n) (so without boundary), with CompactSpace, ConnectedSpace and IsRiemannianManifold linking the metric-space distance to the Riemannian metric. exp x v is the time-one point of a smooth curve with initial point , initial velocity , and locally constant-speed distance-realizing behaviour; mtw is the iterated one-variable derivative formula above.
If satisfies weak MTW, then for every , every and ,
i.e. is convex. This is Theorem 1.1 of the source. The goal is published on the platform with status Open.
The result itself. Combined with the Figalli–Rifford–Villani supporting principle, convexity of injectivity domains under weak MTW alone removes an extra geometric hypothesis from the regularity theory of optimal transport on compact manifolds, and covers focal manifolds where minimizing geodesics may reach conjugate cut points. The source also proves a global supporting property, convexity of lifted gap sections, and uniform intermediate-time geometry (Theorem 1.2), which feed the companion preprint on bi-Hölder regularity of transport maps.
Formalizing it. The statement uses only geodesics, distance and a four-fold derivative of the squared distance, so it can be phrased with current Mathlib Riemannian infrastructure. A proof needs nonsmooth analysis of the distance function near the cut locus, semiconvex potentials and their subdifferentials, and a continuity (degree) argument; this layer would be reusable for other cut-locus results.
The cost is smooth only before the cut locus, while convexity of concerns segments whose interior points might a priori leave the region where is defined. Weak MTW controls the cost Hessian only in directions perpendicular to a velocity segment and gives no strict inequality. Smooth-cost concavity arguments therefore cannot be applied beyond their domain, and nonfocality — the assumption that cut points are reached strictly before conjugate points — is exactly what earlier proofs used to keep the cost smooth along the segment.
exp is defined through complete geodesics with prescribed initial data (ContMDiff curve, mfderiv at equal to , locally ); on a compact manifold such a geodesic exists and is unique, so the Classical.choose fallback is never used.injectivityDomain matches exactly; mtw uses iterated deriv, which is the true fourth derivative wherever the cost is smooth (the case , near ).Convex ℝ (injectivityDomain x) for every .Along a geodesic of a Riemannian manifold, a Jacobi field describes how nearby geodesics spread apart. Two points of a geodesic are conjugate if some nonzero Jacobi field vanishes at both; a metric has no conjugate points if this never happens. Nonpositive sectional curvature implies no conjugate points (by the Rauch comparison), and the two conditions share many consequences: the universal cover is diffeomorphic to via the exponential map, and the fundamental group controls the geometry. For a single metric the converse fails: Gulliver (1975) produced metrics without conjugate points that have regions of positive curvature. The existence question is subtler: must a closed manifold that carries some metric without conjugate points also carry some metric of nonpositive curvature? Ivanov and Kapovitch (2014) and the Burns–Matveev survey (2021) ask this, explicitly including dimension three.
In dimension two the answer is positive (Euler characteristic and uniformization), so dimension three is the first case. The source of this mission is an OpenAI preprint dated September 24, 2026, which answers the question negatively in dimension three.
Let be a closed (compact, boundaryless) connected smooth 3-manifold with a smooth Riemannian metric . In a chart, with Christoffel symbols , a curve is a geodesic if . With covariant derivative along and curvature , a Jacobi field is a smooth vector field along with
has no conjugate points if every Jacobi field vanishing at two distinct times vanishes identically. has nonpositive sectional curvature if for all tangent vectors .
The Lean statement OAI.ThreeManifold.main_theorem is open on the platform.
The theorem shows that, starting in dimension three, the existence of a metric without conjugate points is strictly weaker than the existence of a nonpositively curved metric, answering the Ivanov–Kapovitch question. The same manifold carries no locally CAT(0) length metric and, by the Ivanov–Kapovitch equivalence, no metric without focal points, so it separates "no conjugate points" from "no focal points" as well. The example is a graph manifold glued from two copies of (punctured torus), exactly the test case Ivanov and Kapovitch proposed.
The result is stated in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.
Two separate problems must be solved. The obstruction side (no nonpositively curved metric) follows from Leeb's graph-manifold criterion and is group-theoretic. The construction side is analytic: one must build a metric across the gluing neck and prove that every complete geodesic, including those that enter and leave the neck infinitely often at arbitrary angles, has no conjugate points. Nonpositive curvature is not available in the neck, so the Rauch comparison does not apply; the index form must be controlled with endpoint terms uniformly in entry angle, turning height and excursion time.
ChartedSpace (Fin 3 → ℝ) with IsManifold 𝓘(ℝ, Fin 3 → ℝ) ∞, compact, connected, Hausdorff, second countable; orientability is OrientedAtlas (all transition maps have positive Jacobian determinant).ContMDiffRiemannianMetric; Christoffel symbols and curvature are computed in every atlas chart from fderiv of the coordinate metric.IsGeodesicOn g γ U asks for a smooth curve satisfying the geodesic equation in every chart on the open interval U; IsJacobiFieldOn asks for chart-smooth fields satisfying the Jacobi equation.NoConjugatePoints g: for every open interval U, geodesic and Jacobi field on U, vanishing at two distinct times forces vanishing on U.NonpositiveSectionalCurvature g: for all chart points and vectors; the goal asserts no smooth metric on the same smooth manifold has this property.A complete development needs Riemannian geometry in coordinates, geodesic flows and Jacobi fields, the index form, Cartan–Hadamard/flat torus theorems and the group theory of graph manifolds. Contributions formalizing Theorem 2.1 (no proper cocompact CAT(0) action), Lemma 6.2 (index-form criterion) and Proposition 6.1 (assembly of passage estimates) are welcome.
On a smooth Riemannian manifold, an upper bound on the Hessian of a function immediately bounds the second derivative of along every geodesic: . In non-smooth geometry this step breaks down. On metric measure spaces with Ricci curvature bounded below in the synthetic sense — the spaces — Hessians exist only weakly: inequalities are tested against the reference measure , whereas a single prescribed geodesic can lie in a set of measure zero. Passing from a distributional Hessian bound to a statement about every individual geodesic is a recurring need, for example in characterizing lower bounds on sectional curvature synthetically (in the same release the preprint accompanies an OpenAI preprint on Gigli's distributional-curvature characterization of Alexandrov spaces). Earlier results get this passage only under extra regularity.
is a complete separable metric space with a Borel measure that charges every nonempty open set and is finite on bounded sets. , for and , means the (unreduced) Lott–Sturm–Villani curvature-dimension condition for optimal transport between absolutely continuous probability measures with finite second moment, together with a quadratic Cheeger energy (infinitesimal Hilbertianity).
The minimal weak upper gradient is defined through test plans (probability measures on absolutely continuous curves with bounded compression and finite kinetic energy). Polarization gives , and the Laplacian is the nonpositive generator, . The test class consists of bounded, globally Lipschitz in the domain of with . For such compactly supported and nonnegative compactly supported Lipschitz , the weak Hessian evaluation of is
A constant-speed minimizing geodesic is a curve with , where . All of these notions are defined from scratch in the Lean development (IsTestPlan, weakGradient, gamma, IsLaplacian, IsTestFunction, weakHessian, CurvatureDimension, RCD).
Let be a full-support space with . Let be bounded and globally Lipschitz and bounded and continuous, and assume
for all compactly supported test functions and all nonnegative . Then every constant-speed minimizing geodesic of length satisfies in distributions on :
The goal is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. If the source's proof is correct, the theorem makes a measure-theoretic Hessian inequality usable on every prescribed geodesic, including geodesics that are invisible to almost-everywhere statements. For constant it says that is concave on every geodesic. Compared with earlier results, needs only to be bounded and Lipschitz (no second-order Sobolev or Laplacian-domain regularity), may vary in space, and may have infinite total mass. Such geodesic convexity statements feed into synthetic characterizations of sectional-curvature lower bounds and into rigidity arguments on spaces.
Formalizing it. The statement depends on a large definitional layer: test plans, weak upper gradients, Cheeger energy, the Laplacian, Lott–Sturm–Villani and the weak Hessian. None of these is in Mathlib. Formalizing them faithfully is reusable infrastructure for the whole theory of metric measure spaces with Ricci bounds. The proof itself relies on deep inputs (Savaré's self-improvement, the Ambrosio–Gigli–Savaré and Braun–Habermann–Sturm equivalences, Deng's non-branching theorem), so the realistic path is to state those inputs as milestones.
A weak Hessian bound holds only after integration against . A naive argument would average the bound over a family of geodesics and then localize, but a fixed geodesic can carry zero measure, and almost-everywhere statements about transport geodesics say nothing about it. The natural fix — change the measure to and use entropy convexity — requires the weighted Bochner inequality on the weighted test class. A Lipschitz weight does not preserve that class: the drift term need not be Sobolev, as an explicit Euclidean example in the source shows (Remark 4.2). Localizing to one geodesic also needs uniqueness of geodesics between nearby endpoints, which in this generality comes from non-branching of finite-dimensional spaces.
MetricSpace with Borel σ-algebra, CompleteSpace and SeparableSpace; is a Measure X with FullSupport and FiniteOnBoundedSets. RCD m K N is the unreduced CurvatureDimension with the coefficients for all , plus QuadraticCheegerEnergy (the parallelogram law for Cheeger energy).IsTestFunction requires the function itself (not merely a representative) to be bounded and globally Lipschitz, in the Laplacian domain, with Sobolev Laplacian. WeakHessianUpperBound m F G quantifies over compactly supported test functions and compactly supported nonnegative Lipschitz .Set.Icc 0 1 → X with , so constant curves are included (the conclusion is then trivial). The conclusion CurveSecondDerivativeBound integrates over against smooth nonnegative with tsupport φ ⊆ Ioo 0 1.weakGradient, laplacian) return when the object does not exist. The hypotheses on (bounded Lipschitz) and the test-function requirements ensure that the relevant gradients and Laplacians exist, so the hypothesis is not vacuous.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 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.
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.
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.