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?
Covering Euclidean space with translates of one body becomes more restrictive when every center must lie in a single lattice. The mission asks for a density bound with the optimal-order n log n shape claimed in the manuscript. The source manuscript presents the surrounding research claim.
A convex body is compact and convex with nonempty interior. A full lattice L is a discrete integer submodule spanning the real coordinate space. It covers by K when K+L=ℝⁿ, and its covering density is volume(K)/covolume(L).
Establish one absolute constant C>0 with
The lattice may depend on K and n.
The selected formal target is OAI.SingleLatticeCovering.single_lattice_covering.
The centers form one full-rank lattice. The target includes no symmetry or boundary smoothness assumption on K. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
A union of a few lattice cosets is not itself the required single lattice. Density control must accompany exact coverage of every point.
The formal theorem explicitly supplies DiscreteTopology L and IsZLattice ℝ L in addition to the integer submodule. It uses Mathlib lattice covolume, real volume and the natural logarithm. Dimension starts at two, and the universal C is chosen before K and n.
adc7f1241b42. Goal source.The volume of a symmetric convex body multiplied by the volume of its polar is unchanged by invertible linear coordinates. Its extremizers are therefore classified up to linear equivalence. The source manuscript presents the surrounding research claim.
For an origin-symmetric compact convex K⊆ℝⁿ with nonempty interior, the polar body K° consists of p with Σpᵢxᵢ≤1 for every x∈K. Hanner bodies are generated from centered nondegenerate intervals by products and convex joins; linear Hanner bodies also allow invertible linear images.
For n≥1, prove the equality classification
The lower-bound inequality is retained as a separate supporting target.
The selected formal target is OAI.SymmetricMahler.symmetric_mahler_equality.
The goal identifies every equality case, not only one minimizing example. The manuscript’s inequality and equality assertions appear as distinct published statements. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Showing that the recursively constructed examples attain the value gives only one implication. The reverse implication must classify arbitrary symmetric convex bodies, including nonpolyhedral inputs.
Points are functions Fin n→ℝ and polarity uses the coordinate dot product. Volumes are converted from ENNReal to ℝ in the product. The two definition groups both declare coordinatePolar; they remain separate references rather than an aggregate module.
adc7f1241b42. Goal source.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.Singular integral estimates can detect geometric regularity in a measure whose support has no given parametrization. The mission turns a uniform Riesz-transform bound into uniform pieces of Lipschitz images. The source manuscript presents the surrounding research claim.
Let μ be a regular measure in ℝᵈ, with d≥4 and 2≤n≤d−2. Ahlfors–David regularity means that μ(B(x,r)) is comparable to rⁿ on its support at admissible radii. Hard-truncated Riesz transforms use the kernel (x−y)/|x−y|^(n+1), excluding distances at most ε.
With fixed dimension and bounds C_AD,C_R, prove that there exist θ>0 and M≥0 such that every eligible μ satisfies
for some M-Lipschitz map g from the open n-dimensional radius-r ball, at every support point and admissible radius.
The selected formal target is OAI.RieszRectifiability.quantitative_higher_codimension_riesz_rectifiability.
The constants θ and M are uniform across the entire class of measures with the prescribed analytic bounds. This is the exact quantitative ball-image conclusion. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Individual rectifiable pieces with constants depending on μ do not yield this quantifier order. The Riesz bound ranges over every positive hard truncation and every scalar L² input.
Ambient space is EuclideanSpace ℝ (Fin d). Radii are positive and bounded by the extended support diameter. The hypothesis uses μ.Regular, nonnegative Riesz constants, MemLp and eLpNorm; the conclusion uses the actual measure of the intersection with a Lipschitz image. No endpoint codimensions are included.
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.Cubic Gauss sums oscillate even after normalization. Their first moment asks whether this cancellation retains a precise lower-order bias when averaged over arithmetic primes. The source manuscript presents the surrounding research claim.
Work in the Eisenstein integers ℤ[ω], with ω=exp(2πi/3). A primary prime p is a prime element congruent to one modulo three. N(p)=|p|², G(p) is the normalized cubic Gauss sum, and c*=(2π)^(2/3)/(3Γ(2/3)).
At the real sharp cutoff X, establish
The two supporting targets compare each fixed angular mode to its explicit model and give cancellation for every nonzero mode.
The selected formal target is OAI.CubicFirstMoment.patterson_firstMoment.
The coefficient and scale specify the first moment, rather than only an order-of-magnitude estimate. Both conjugate prime elements are included when they satisfy the primary-prime predicate. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Pointwise estimates on G(p) do not isolate the X^(5/6)/log X bias. The error must be little-o at that scale with the exact arithmetic normalization.
The published definitions use residue-class representatives, the cubic residue symbol, the trace exponential phase, and complex-valued cutoff sums. Little-o is taken as real X tends to positive infinity. Angular modes are integers held fixed before the limit.
adc7f1241b42. Goal source.Closed diagonal orbits encode lattices in totally real number fields. Their distribution tests whether arithmetic families fill the space of unimodular lattices as their discriminants grow. The source manuscript presents the surrounding research claim.
For a fixed prime n=d+1 ≥ 5, Xₙ is the quotient of SLₙ(ℝ) by its integral lattice subgroup. A packet consists of normalized full lattices of one local homothety type, including the specified sign translates. Its measure averages orbital probabilities with orbit-volume weights.
For any sequence of totally real degree-n fields and full lattices whose multiplier discriminants tend to infinity, prove
and tightness of the entire family {μᵢ}. Weak convergence uses every bounded continuous real test function and includes the probability normalization of every μᵢ.
The selected formal target is OAI.DukePrimeDegree.prime_degree_packet_measure_equidistribution_unconditional.
The conclusion addresses arbitrary local types and includes absence of escape of mass. The fixed-Haar formulation is also available as a supporting target. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Convergence on compactly supported tests alone would not establish the requested probability convergence on a noncompact quotient. The packet normalization and tightness must be justified uniformly through the discriminant limit.
The source definitions use completed lattices over ℤₚ, diagonal-flow period covolumes and volume-weighted sums over distinct orbits. The theorem fixes prime degree at least five and allows both fields and local types to vary. Both published formulations and their shared definitions are referenced.
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.Real zeros of Dirichlet L-functions close to one obstruct uniform estimates for primes in arithmetic progressions. A conductor-independent logarithmic gap is the precise quantitative issue addressed here. The source manuscript presents the surrounding research claim.
A Dirichlet character χ modulo an integer q is primitive, nonprincipal, and real-valued when its complex values have zero imaginary part. Its analytically continued L-function is denoted L(s,χ). The zero β is real and lies strictly between zero and one; log is the natural logarithm.
Prove that one positive real constant works for every allowed modulus, character and zero:
The constant must be independent of q and χ.
The selected formal target is OAI.SiegelZeros.WeightedTorusJets.exists_absolute_real_zero_gap.
This is the uniform zero-gap conclusion itself, not a statement for a bounded family of conductors. The source dated October 1, 2026 states this as its principal result. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
A bound whose constant varies with the character cannot establish this quantifier order. The arithmetic and analytic estimates must retain one positive constant across every conductor and every real primitive character.
The goal uses Mathlib’s actual Dirichlet characters and L-functions over ℂ, with q : ℕ, a nonzero instance and q ≥ 3. Both available published formulations are referenced. The second formulation merely groups the zero hypotheses differently and is not presented as an independent milestone. The manuscript’s interpolation and determinant lemmas have no supplied published theorem IDs and are not attached as milestones.
adc7f1241b42. Goal source.Given a source probability measure and a target on , Brenier's theorem (Brenier 1991) says that when is absolutely continuous there is a unique map pushing to that minimizes the quadratic cost , and that it is the gradient of a convex function. Fixing , the assignment embeds the space of probability measures into ; this linearization of optimal transport is used in statistics, data analysis and machine learning to compare measures by comparing their maps. Its usefulness depends on quantitative stability: how far apart can and be when and are close in Wasserstein distance? For general targets the map cannot be Lipschitz in the target, and the question is which Hölder exponent holds uniformly.
This mission asks for a machine-checked proof that, for a uniform source on a convex body, the sharp uniform exponent is exactly , as claimed in an OpenAI preprint dated September 25, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal below is open.
Fix , a compact convex with nonempty interior, and the uniform source . Fix a nonempty compact and let be the Borel probability measures with . A coupling of is a probability measure on with marginals , and
For , is the Brenier map: a measurable with whose graph coupling is the unique optimal coupling of and . Distances between maps are measured in : .
For every , with and every ,
and the supremum stays infinite when both targets have exactly three atoms. In Lean (one_third_exponent_is_sharp): for every and there are distinct three-atom probability measures on the cube with unique optimal maps and .
For every , as above there is a finite constant such that for all the Brenier maps exist, are unique, and
The targets may be atomic, singular or absolutely continuous; the constant does not depend on them. In Lean this is one_third_stability. Together the two statements determine the sharp exponent in this uniform class, which is the second sentence of Theorem 1.1.
The result itself. The upper bound improves every earlier target-uniform exponent (, , , in or ) to in , with a constant independent of atom counts, atom masses, separations and density bounds. The lower bound disproves Letrouit's conjectured exponent with only three atoms on a cube. The pair gives the exact uniform stability exponent of the linearized optimal-transport embedding for uniform convex sources.
Formalizing it. Mathlib has measures, couplings and Lebesgue integration but no optimal-transport theory. A formal development would supply Wasserstein distance, existence and uniqueness of Brenier maps for semi-discrete and general targets, and Lipschitz convex potentials, all reusable. The sharpness statement is the more elementary one and is a natural first milestone.
The standard route bounds the difference of convex potentials and then converts it to a gradient bound by an interpolation inequality; previous potential estimates lose a power, giving exponents below . The preprint's key step is a linear bound on the distance of potentials, obtained by moving the sites of finite targets along an optimal coupling with fixed masses and controlling the intercept velocity through a uniform moment inequality for the cells of a maximum of affine functions (Lemma 4.1, p. 9; Proposition 5.1, p. 12). The constant must stay uniform as cell masses or faces degenerate, which rules out any argument relying on a spectral gap of the cell graph Laplacian. The final passage from finite to arbitrary Borel targets needs stability of optimal maps under approximation (Proposition 6.3, p. 16).
EuclideanSpace ℝ (Fin d) with Borel measures. uniformMeasure K is ; with compact convex with nonempty interior its volume is positive and finite.IsSupported μ Y means . Couplings are probability measures with the two marginals; costs are lower integrals in ℝ≥0∞; is the square root of the real part of the infimal cost, finite here because supports are bounded.IsUniqueQuadraticOptimalMap ρ μ T asserts that is measurable, pushes to , is cost-optimal among all couplings, and that every coupling of no larger cost equals the graph coupling. The goal must therefore also produce the Brenier maps; they are not assumed.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.Given two probability densities on a compact Riemannian manifold, optimal transport with the quadratic cost seeks the map pushing to at least total cost. McCann proved that such a map exists and is unique almost everywhere (McCann 2001). Whether it is continuous when the densities are merely bounded above and below depends on the geometry of the cost: the Ma–Trudinger–Wang (MTW) condition, a sign condition on a fourth derivative of , is the decisive curvature hypothesis, and its weak form is known to be necessary. The question is whether weak MTW is also sufficient on every compact manifold, with estimates that do not degenerate as transport graphs approach conjugate points.
Let be a smooth, connected, compact Riemannian manifold without boundary, of dimension , with distance and volume . Put and let
be the open injectivity domain. Weak MTW: for every and in ,
For , the density class consists of measurable with and almost everywhere. An optimal map from to is a measurable with minimizing among such maps.
In Lean, metricVolume n is the -dimensional Hausdorff measure normalized to agree with Lebesgue measure on (which equals Riemannian volume), riemannianExp is defined from complete geodesics, and WeakMTW uses iteratedDeriv 2 twice.
Fix satisfying weak MTW and with a nonempty density class. There are and , depending only on , such that for all densities in the class, the almost-everywhere unique optimal map has a homeomorphic representative with
This is Theorem 1.1 of the source. The goal is published on the platform with status Open.
The result itself. The constants are common to the whole density class; they do not depend on the densities or their derivatives, and the theorem allows conjugate cut points without nonfocality, strict MTW, or cut avoidance. Combined with the necessity result of Figalli–Rifford–Villani it gives the equivalence of weak MTW with transport continuity for bounded densities on compact manifolds, with uniform estimates in the forward direction. No explicit exponent is obtained (the positive exponent comes from a contradiction argument).
Formalizing it. The Lean statement packages existence, almost-everywhere uniqueness, homeomorphic regularity and uniform bi-Hölder bounds in one assertion over all density pairs, making precise what "class-uniform" means. A proof requires the companion geometric results (convex injectivity domains, global support), McCann's theorem, and Caffarelli-type section estimates on manifolds — none currently in Mathlib.
Hölder estimates obtained after localizing near a smooth part of the cost give a density-dependent exponent and localization scale; they do not give a common scale or constant for a family whose transport graphs approach conjugate pairs, where the cost stops being smooth. Weak MTW constrains the cost only where it is smooth and only for orthogonal directions. Earlier uniform results needed strict MTW and nonfocality, or special geometry (products of spheres).
euclideanVolumeFactor n • μH[n]; densities are AEMeasurable, integrable, of mass one, and between lam and cap almost everywhere; nonemptiness of the class is a hypothesis, as in the source.IsOptimalMap requires measurability, the pushforward identity for withDensity measures, and minimality among all measurable maps with that pushforward; uniqueness is almost everywhere for .M ≃ₜ M with the same exponent and constant for and ; a trivializing choice is excluded because must itself be optimal.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.