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?
Cutoff means that a Markov chain’s transition from far from equilibrium to near equilibrium occurs in a negligible fraction of its mixing time. The source studies heat-bath dynamics for a disordered mean-field Ising model. The source is OpenAI's September 2026 manuscript.
The Sherrington–Kirkpatrick model has independent centered Gaussian pair couplings with variance and zero external field. One discrete update picks a site uniformly and resamples its spin from its conditional Gibbs law. Mixing time uses worst-case total variation distance.
For real parameters β with 0 ≤ β < 1/2, ε with 0 < ε < 1/2, and η > 0, two things hold for the Sherrington–Kirkpatrick model with n spins, where a disorder g is a real coupling for each pair i < j of sites and the Gibbs measure at zero external field has weight proportional to exp((1/2) Σᵢ Σⱼ σᵢ gᵢⱼ σⱼ) on spin configurations σ ∈ {±1}ⁿ (couplings symmetrized, diagonal zero). The dynamics is a heat-bath single-site chain: choose a site uniformly at random, then keep or flip its spin with probabilities proportional to the Gibbs masses of the two configurations (for n = 0 the transition matrix is the identity). The distance after k steps is the maximum over starting configurations of the total variation distance (half the ℓ¹ distance) between the k-step distribution and the Gibbs measure, and mixingTime(g, δ) is the least k whose distance is at most δ (the infimum of the set, so 0 if that set is empty). The disorder law makes the couplings independent centered Gaussians with variance β²/n. First, the probability under this law that the ratio mixingTime(g, ε) / mixingTime(g, 1 − ε) exceeds 1 + η tends to 0 as n → ∞. Second, for all sufficiently large n, every disorder g satisfies mixingTime(g, 1 − ε) > 0.
The goal is OAI.SKRatio.ratio_cutoff.
The available target gives ratio cutoff in probability over the disorder and eventual positivity of the denominator for every disorder. It isolates a precise mixing-time comparison. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Fast relaxation estimates alone do not prove that all fixed total-variation thresholds become asymptotically equivalent. The worst starting configuration and the random couplings both enter the comparison.
The attached range is , narrower than the full high-temperature range discussed in the manuscript. The target does not specify the cutoff location. Dynamics is discrete single-site updating; the exceptional transition is the identity.
The shared definitions are supplied by SKRatio. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
The Ising perceptron weights binary configurations by their projections onto random patterns. The paper develops a variational description of its pressure; the available formal target checks that the proposed variational value is finite. The source is OpenAI's September 2026 manuscript.
An overlap path is an almost-everywhere class on with a monotone representative taking values in . The variational expression combines a Gaussian pattern functional with an Ising entropy, defined as a supremum over monotone nonnegative field steps.
For every real α ≥ 0 and every continuous function f : ℝ → ℝ that is bounded (there is K with |f(x)| ≤ K for all x), the variational value of the Ising perceptron model is a finite real number, i.e. variationalValue(α,f) equals the extended real (p : EReal) for some real p. Here variationalValue(α,f) is the infimum, over all admissible overlap paths q (almost-everywhere-defined functions on (0,1) that agree a.e. with a monotone function taking values in [0,1]), of α times the pattern functional of f at q plus the Ising entropy of q. The pattern functional is the limit as n→∞ of uniformPattern, a nested Gaussian transform over a uniform grid with n+1 cells built from cell averages of q and applied to f at 0, where each transform is either a Gaussian average or a log-exponential-moment average divided by d, depending on whether d is zero. The Ising entropy is the supremum, over field steps (a partition of [0,1] with nonnegative monotone step values), of the field recursion value plus half the integral of the step function against q. The statement asserts that this infimum is neither +∞ nor −∞.
The goal is OAI.IsingPerceptron.variationalValue_real_of_continuous.
The goal rules out both infinite extended-real values for continuous bounded potentials. This is a well-definedness component needed before a real-valued limit formula can be used. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
The entropy is a supremum over an unbounded family of fields and the outer expression is an infimum over paths. Boundedness of the input potential alone does not syntactically make this extended-real expression finite.
The target is variationalValue_real_of_continuous, with nonnegative density and continuous bounded potential. It does not assert convergence of finite-system pressure or the manuscript’s broader bounded-Borel result. Gaussian recursion and almost-everywhere path conventions are kept as published.
The shared definitions are supplied by IsingFiniteness. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
A diluted spin glass has finitely many interactions per spin on average. The source seeks the exact thermodynamic pressure using a hierarchy of random local-field laws. The source is OpenAI's September 2026 manuscript.
The pressure is the expected logarithm of the partition function divided by the number of Ising spins. A Poisson number of even-arity interactions and independent external fields define the model. The cavity functional uses nested probability laws and iterated logarithmic power means.
For every model of a diluted p-spin glass with Ising spins in {+1,-1} that satisfies the standing admissibility hypotheses, the free-energy density F_N converges, as N tends to infinity, to a variational value, so existence of the thermodynamic limit is part of the conclusion. A model consists of a density α ≥ 0, a probability law on interaction samples (θ, a, b, f), where θ is a real function on spin configurations in {±1}^p, a and b are reals and f assigns to each of the p slots a real function on spins, and a probability law for the external field on ℝ. Admissibility means: p is even and at least 2; α > 0; ‖θ‖ = max_s |θ(s)| and |h| are integrable under the disorder and field laws; almost surely a > 0 and, for every configuration s, exp θ(s) = a(1 + b ∏_l f_l(s_l)) with |b ∏_l f_l(s_l)| < 1; the functions f_1,…,f_p are independent and identically distributed, b is independent of the vector f, every power (−b)^n with n ≥ 1 is integrable, and E[(−b)^n] ≥ 0. No boundedness of interactions, fields or messages is added. F_N is (1/N) times the expectation of log Σ_σ exp(−H), where the number k of interactions is Poisson with mean αN, the k interactions are independent disorder samples, the N fields are independent field samples, and each interaction is placed on p index choices in {1,…,N} (repetitions allowed) averaged uniformly over all choices; here the log-weight of σ is Σ_j θ_j(σ at the chosen indices) + Σ_i h_i σ_i. The limit is the infimum over depths r ≥ 0 of φ_r, itself the infimum, over a nested law ζ in the r-fold hierarchy of probability measures (each level with the weak topology and its Borel σ-field) and exponents 0 < m_1 < … < m_r < 1, of the cavity functional B_r. B_r equals log 2 plus the Poisson(αp)-averaged expectation of the site term, a logarithm of an average over spin ε of exp(hε + Σ_j message_j(ε)), minus α(p−1) times the expectation of the log of the edge weight, with both terms evaluated through iterated log power-means in the exponents m_i.
The goal is OAI.DilutedSpinGlass.mezard_parisi.
The equality identifies the limit with the infimum over all finite hierarchy depths. Existence of the thermodynamic limit is part of the conclusion, not an assumption. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Upper bounds at each hierarchy depth do not yield equality with the infinite-size model. Unbounded disorder requires retaining integrability hypotheses through nested expectations.
The admissibility predicate requires positive density, even arity at least two, first moments, the specified interaction factorization, and positivity and integrability of the relevant powers. The statement adds no boundedness restriction on interactions, fields, or trial messages.
The shared definitions are supplied by DilutedSpin. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
On an expanding infinite graph, the appearance of an infinite open cluster and the appearance of a unique one can occur at different densities. The source seeks a nonempty interval where infinitely many infinite clusters coexist. The source is OpenAI's September 2026 manuscript.
In bond percolation, edges are independently retained with probability . The critical threshold records appearance of infinite clusters; records uniqueness. The intermediate operator threshold records boundedness on of the two-point connection kernel.
For a bond graph G, given by a map from an edge type E to unordered pairs of vertices in an infinite vertex type V, that is connected, locally finite (each vertex lies in finitely many edges) and quasi-transitive (finitely many vertex representatives such that every vertex is the image of one under an automorphism of G acting on vertices and edges), and whose vertex isoperimetric constant hV(G), the infimum over nonempty finite vertex sets A of |outer vertex boundary of A|/|A|, is strictly positive, the MainConclusion holds for Bernoulli bond percolation on G. Writing pc for the infimum of parameters p at which an infinite cluster occurs with positive probability, pu for the infimum of p at which there is almost surely exactly one infinite cluster, ptwo for the supremum of p at which the two-point function τ_p(x,y)=P_p(x connected to y) is the matrix kernel of a bounded operator on ℓ²(V), and operatorNorm(p) for the infimum of operator norms of such operators, valued in [0,∞], the conclusion has four parts. First, the supremum of operatorNorm(p) over p<pc equals operatorNorm(pc). Second, operatorNorm(pc) is finite. Third, pc<ptwo≤pu. Fourth, there exist p₁<p₂<1 with pc<p₁ such that, for almost every i.i.d. uniform [0,1] edge labelling, for every p in [p₁,p₂] the configuration of edges with label at most p has infinitely many infinite clusters. The proof is omitted (sorry) in the source.
The goal is OAI.Percolation.BenjaminiSchramm.full_main. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The full goal also identifies the critical norm as the supremum from below and supplies simultaneous nonuniqueness over a fixed interval under the uniform-label coupling. Supporting statements cover critical laws and Cayley graphs. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
A separate almost-sure statement at each parameter does not establish one event valid for every parameter in an interval. Critical operator control must also survive the passage to the threshold itself.
The graph has infinitely many vertices, is connected and locally finite, has finitely many vertex orbits, and has positive vertex isoperimetric constant. Thresholds lie in the unit interval; operator norms may take extended nonnegative values. The independent Cayley definition group is retained separately.
The shared definitions are supplied by BenjaminiSchramm, CayleyPercolation. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Multiplicity measures the growth of infinitesimal neighborhoods in a local ring. The manuscript addresses Lech’s flat-local-map inequality; the available formal target isolates its complete-domain Frobenius-complex component. The source is OpenAI's September 2026 manuscript.
For a local domain of dimension , Hilbert–Samuel multiplicity is the limit of . A short complex has finite free terms in degrees through zero, finite-length homology, and nonzero zeroth homology. Its Frobenius scalar extensions define a normalized Euler-characteristic sequence.
The defined proposition DuttaDomainClaim holds, in universe u. That claim says: let D be a commutative Noetherian local domain (in universe u) that is complete in the adic topology of its maximal ideal, with prime characteristic p, and let F be a cochain complex of D-modules indexed by the integers that is a short complex. Short means every term F^i is free and finitely generated, F^i is zero whenever i < -dim D or i > 0, every homology module of F has finite length, and the homology of F in degree 0 is nonzero. Here dim is the Krull dimension (taken as 0 if it is the bottom value). Let F_n denote F after extending scalars along the n-fold iterate of the Frobenius map of D. The conclusion has three parts. First, every homology module of every F_n has finite length. Second, the sequence a_n = p^(-n dim D) * chi(F_n) converges as n tends to infinity, where chi(G) is the alternating sum, over i from 0 to dim D, of (-1)^i times the length of the homology of G in degree -i; this limit is the Dutta multiplicity of F. Third, the Hilbert-Samuel multiplicity of D, defined as the limit of (dim D)! times the length of D/m^N divided by N^(dim D) as N tends to infinity, is at most the Dutta multiplicity of F.
The goal is OAI.Lech.dutta_domain.
The goal formalizes the lower bound by Dutta multiplicity together with the convergence and finite-length statements needed to interpret it. This is a precise component of the paper’s multiplicity program. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Lengths of homology after Frobenius extension must be controlled before normalized Euler characteristics can be used. A definition by a chosen limit does not by itself establish convergence.
The ring is a complete Noetherian local domain in prime characteristic. The goal is DuttaDomainClaim, not the unrestricted flat local homomorphism inequality. Dimensions and lengths use the natural-number conversions in the supplied definitions, and convergence is an explicit conclusion.
The shared definitions are supplied by DuttaDomain. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Random triangle deletion constructs a partial triangle packing. Its terminal uncovered edges measure how efficiently this process covers pairs, and the source seeks the leading constant rather than only the growth exponent. The source is OpenAI's September 2026 manuscript.
Start from the complete graph on vertices. At each step choose a remaining triangle uniformly and remove its three edges. A triangle-free state stays fixed. The terminal leave is the edge count at the end.
For the random triangle-removal process, three limits hold as n tends to infinity. The process starts from the complete graph on n vertices, with graphs represented as sets of 2-element subsets of Fin n. At each step, if the current graph G contains triangles (3-subsets all of whose pairs are edges of G), one triangle is chosen uniformly at random and its three edges are deleted; if there is no triangle, the graph stays unchanged. Running this for C(n,2) steps gives the terminal law on graphs, and expectation and probability are taken with respect to it. Writing normalizedLeave(G) = |E(G)| / n^(3/2) and sharpConstant c = 1/(2√2), the theorem asserts: first, the expected value of (normalizedLeave(G) − c)² tends to 0; second, for every ε > 0, the probability that |normalizedLeave(G) − c| > ε tends to 0; and third, the expected number of edges of the terminal graph divided by n^(3/2) tends to c.
The goal is OAI.SharpTerminalLeave.sharp_terminal_leave.
The three conclusions record mean-square concentration, concentration in probability, and the limiting normalized expectation. The exact leading constant is part of the target. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Early evolution estimates need to remain informative near termination, where triangles become scarce. A high-probability estimate alone need not control the second moment required here.
Graphs are finite sets of pairs from Fin n, with transitions given by probability mass functions. Running for the initial edge count guarantees that the absorbing terminal law is reached. Expectations are finite sums and all limits are along natural tending to infinity.
The shared definitions are supplied by TriangleRemoval. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
A measure-preserving system may have low information production yet fail to admit a smooth realization. The target asks for a single ergodic system excluding every finite-dimensional smooth positive-volume model. The source manuscript presents the surrounding research claim.
The system is a measurable equivalence T of a standard nonatomic probability space. Standard nonatomic is expressed by an isomorphism with the unit interval after removing null sets. A smooth model is a compact smooth manifold, a smooth diffeomorphism and an invariant probability measure with strictly positive smooth local coordinate density.
Construct a system satisfying
The formal finite-entropy predicate requires every finite-partition entropy rate to converge, with one finite real upper bound.
The selected formal target is OAI.SmoothObstruction.main.
The obstruction ranges over every finite dimension, nonorientable manifolds and positive-dimensional smooth boundary models. The manuscript asserts zero entropy; the selected published theorem requires finite entropy only. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Failure of a particular embedding does not exclude all measure-theoretic conjugacies and all dimensions. Conjugacy is allowed after discarding invariant null sets.
The goal quantifies over measurable equivalences and uses conull measurable conjugacy, not topological conjugacy. Entropy is measured in bits by the supplied finite-partition definition. Closed models include dimension zero, boundary models require positive dimension, and no orientation hypothesis is imposed.
adc7f1241b42. Goal source.Sampling costs can be measured by potential and gradient queries independently of the computation between them. This model isolates the information needed for a well-conditioned log-concave distribution. The source manuscript presents the surrounding research claim.
The admissible potentials V on ℝᵈ are C², satisfy V(0)=0 and ∇V(0)=0, and have Hessian between I and 2I. Their Gibbs law has density proportional to exp(−V). A measurable adaptive algorithm receives exact (V(x),∇V(x)) replies.
For the least query budget q(d) achieving total-variation error at most 1/10, prove
plus q(d)≥c log d eventually for some c>0, and optimal dimension exponent γ*=0.
The selected formal target is OAI.LogConcaveSampling.exact_source_main.
The target gives both a subpolynomial upper bound and a logarithmic lower bound. It leaves computation between queries unrestricted. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
The sampler must work uniformly across every admissible potential and use a deterministic query budget on every execution. A dimension-dependent condition number or merely expected budget would change the problem.
Algorithms have measurable query/output maps driven by private randomness and finite transcripts. Query complexity lies in ℕ∞, retaining infeasibility as infinity. Total variation is the specified supremum-style bound on measurable sets, and the upper/lower comparisons use ENNReal.
adc7f1241b42. Goal source.Rectangular matrix products arise when the two outer dimensions are much larger than the inner dimension. The dual exponent records the largest inner growth rate compatible with arithmetic exponent two. The source manuscript presents the surrounding research claim.
For k∈[0,1], ω_ℂ(1,k,1) is the infimum of exponents for multiplying an n×⌈nᵏ⌉ matrix by a ⌈nᵏ⌉×n matrix over ℂ. The dual exponent α is the supremum of k for which this infimum equals two.
Prove the strict bound
The additional published rectangular endpoint asserts ω_ℂ(1,709/1000,1)<523/250=2.092.
The selected formal target is OAI.MatrixMultiplication.complex_alpha_gt_93_div_200.
Strictness is part of both statements. The supplied goal concerns the complex dual exponent; the manuscript title’s square bound and broader field claims are not attached formal targets. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
An algorithm for one size does not establish an asymptotic exponent. The definition quantifies over every positive slack and all positive sizes with one bound constant for each slack.
Algorithms are division-free arithmetic programs with constants and input gates of cost zero and addition, subtraction and multiplication of cost one. Correctness is quantified over all input matrices. The dual exponent is a real supremum of exact exponent-two shapes, using the prescribed inner-dimension ceiling.
adc7f1241b42. Goal source.The worst covering density over convex bodies measures how much overlap is unavoidable when translations must cover all of space. Comparing unrestricted centers with a single lattice separates two geometric constraints. The source manuscript presents the surrounding research claim.
The translative density θ_T(K) is the infimum of volume(K) times the upper intensity of locally finite covering center sets. Intensity is measured in expanding centered cubes. The lattice density θ_L(K) takes the corresponding infimum over discrete full-rank lattice coverings.
For each of the four suprema Aₙ, over all or centrally symmetric convex bodies and using θ_T or θ_L, prove common positive constants c,C and a threshold n₀ with
The selected formal target is OAI.CoveringOrder.optimal_order.
The selected endpoint asserts the same asymptotic order for all four worst-case quantities. The manuscript’s new translative lower-bound claim is part of this broader packaged endpoint. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
A lower bound for lattice centers does not exclude a more efficient nonlattice cover. The unrestricted lower bound ranges over every locally finite covering set.
The definitions retain extended nonnegative real densities and suprema, so a finite upper bound also asserts finiteness. Central symmetry may have any center. The theorem concerns suprema over bodies, not a lower bound on every individual body.
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.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.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.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.
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.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.
A Riemannian metric is Einstein if its Ricci curvature is a constant multiple of the metric, . Einstein metrics are the critical points of total scalar curvature and the vacuum solutions of general relativity in Riemannian signature, and in dimension four they are tied to gauge theory and to the topology of four-manifolds. A natural rigidity question asks which closed four-manifolds carry Einstein metrics of strictly positive sectional curvature. Three examples are known: the round sphere , the round real projective space , and the complex projective plane with its Fubini–Study metric. The classification conjecture, stated as Conjecture 1 by D. Yang in 2000, asserts that there are no others up to scaling and isometry.
All earlier results keep an additional curvature, topological or symmetry hypothesis. The source of this mission is an OpenAI preprint dated September 23, 2026, which claims the classification with no extra hypothesis and no orientability assumption.
Let be a connected, compact smooth four-manifold without boundary, with a smooth Riemannian metric . In a chart with Christoffel symbols , the curvature tensor is
the Ricci tensor is , and the sectional curvature of the plane spanned by has the sign of . The metric is Einstein if for a single constant , and positively curved if for all linearly independent . Strict positivity forces .
The three models are with distance , with distance for unit representatives, and with the Fubini–Study distance .
If is in addition oriented, then for some , is isometric to or to .
The Lean statement OAI.PositiveEinsteinFour.classification is open on the platform.
The theorem completes the four-dimensional picture for positively curved Einstein metrics: only the symmetric examples occur. It removes all the pinching, topological and symmetry hypotheses of previous results. The paper's central intermediate result, half-conformal flatness (one Weyl block vanishes, Proposition 8.1), connects the problem to Hitchin's classification of self-dual Einstein four-manifolds.
The result is stated in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. Parts of the argument rely on explicit polynomial and matrix certificates (Section 7), which are well suited to formal verification.
In dimension four the curvature of an Einstein metric splits into two Weyl blocks acting on self-dual and anti-self-dual two-forms. The Einstein equation does not force either block to vanish, and earlier arguments controlled them only under extra pinching or topological assumptions. Scalar Weyl-norm gaps (Gursky–LeBrun) control each block separately; the difficulty is the interaction of two nonzero blocks under the exact sectional-positivity condition, which is stronger than any norm bound and must be used in its tensorial form. Once one block vanishes, the classical rigidity theory finishes the proof.
ChartedSpace (EuclideanSpace ℝ (Fin 4)) with IsManifold I4 ∞, compact, connected, Hausdorff, second countable; the model has no boundary.ContMDiffRiemannianMetric; Christoffel symbols, curvature and Ricci are computed in coordinates from fderiv of the chart expression of , at the centre of the chart at each point.IsEinstein uses one constant for all points; HasPositiveSectionalCurvature requires for every linearly independent pair.ScaledIsometricTo g a d asks for a bijection with , the Riemannian distance.A complete development needs Riemannian geometry in coordinates, Weyl decomposition in dimension four, Hodge theory on two-forms, characteristic-number identities (Gauss–Bonnet–Chern, Hirzebruch signature), volume comparison, and Hitchin's classification. Contributions formalizing Proposition 8.1 (half-conformal flatness), Proposition 4.9 (balanced Weyl moments) and Lemma 8.7 (curvature of the standard models) are welcome.
A symplectic embedding preserves the standard symplectic form on , and in particular preserves volume. Gromov's nonsqueezing and two-ball theorems showed that symplectic embeddings obey constraints invisible to volume (Gromov 1985). The ball-packing problem asks exactly when finitely many balls can be embedded disjointly and symplectically into a given ball, and so measures how far symplectic rigidity goes beyond volume.
In real dimension four the answer involves infinitely many obstructions coming from pseudoholomorphic curves and algebraic geometry (McDuff–Polterovich 1994; Biran 1997). In higher dimensions Siegel and Yao conjectured that only two obstructions survive: volume and Gromov's two-ball obstruction (Conjecture A of Siegel–Yao 2025).
This mission asks for a machine-checked proof of Theorem 1.1 of an OpenAI preprint dated September 23, 2026 (source), which claims Conjecture A in every real dimension . The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.
For write
so is the capacity, the Euclidean radius is , and . An embedding of a closed ball into the open ball means a smooth map defined on an open neighbourhood of the closed ball, which is a topological embedding there, pulls back to , and sends the closed ball into the open target. A packing of is a family of such embeddings whose images of the closed balls are pairwise disjoint.
If , , and a packing exists, then
The images lie in some with by compactness, so the volume bound and Gromov's two-ball obstruction give the strict inequalities.
For integers , and positive reals , a symplectic embedding exists if and only if the two inequalities above hold.
The result itself. In every real dimension at least six, the volume and two-ball obstructions are the only obstructions to packing balls of arbitrary capacities into a ball. This contrasts with dimension four, where infinitely many further obstructions are essential, and it goes beyond packing-stability results, which concern many small balls. The theorem settles Siegel and Yao's Conjecture A.
Formalizing it. The necessity direction needs Gromov's two-ball theorem, which rests on pseudoholomorphic curve theory and has no formalization. The sufficiency direction uses Hamiltonian flows, Moser isotopies, toric domains, Kähler forms on projective degenerations and normal-cone transfer. A formal proof would require substantial new symplectic and algebro-geometric infrastructure, all of it reusable.
Sufficiency is the hard direction. The volume inequality is an integral condition, but a packing needs pointwise room; in the preprint's toric models over a surface with a handle, the unused-area profile has positive integral but need not be positive at every moment, and a Hamiltonian comparison theorem (Lemma 2.1, p. 5) is needed to rearrange it into disjoint ball layers (Lemma 3.3, p. 12). The models must then be transferred symplectically into the target ball using Kähler degenerations; three geometric cases arise (all capacities below , Proposition 5.2, p. 25; one large capacity in dimension , Proposition 5.3, p. 26; one large capacity in dimension six, Proposition 6.7, p. 39). For necessity the obvious volume argument gives only non-strict inequalities; strictness comes from compactness of the images, and the pairwise bound is genuinely symplectic.
Fin n → ℂ with capacity and .SymplecticOn U f: open, is on , is a topological embedding, and fderiv preserves at every point of .HasPacking n k R r: each closed ball lies in an open on which is symplectic, maps the closed ball into the open ball of capacity , and images of distinct closed balls are disjoint.PackingInequalities uses strict inequalities and quantifies over ordered pairs ; the goal assumes , , , , matching the source exactly.A Riemannian surface is abstract: it is given by a rule for measuring lengths and angles in local coordinates, not as a surface sitting in space. The local isometric realization problem asks whether every such surface can, near each point, be realized as an honest smooth surface in Euclidean three-space with the same lengths. The question goes back to the classical theory of surfaces. It is settled for real-analytic metrics and for smooth metrics with nonvanishing curvature, while the unrestricted smooth case is listed as open by Yau (Yau 2000, p. 236) and in Ghomi's problem survey (Ghomi 2019, §1.5, Problem 1.9).
Work in coordinates on the open square . A Riemannian metric on is a map to symmetric real matrices that are positive definite; it is if every entry is smooth. An isometric immersion of , for an open set , is a map whose differential reproduces :
equivalently . Positive definiteness forces to have rank . In Lean, Coord = Fin 2 → ℝ, Ambient = EuclideanSpace ℝ (Fin 3), square is , and LocalSmoothPositive packages smoothness of every entry and Matrix.PosDef at every point.
This is Theorem A of the source (p. 1). Because a smooth isometric immersion restricts to an embedding near any point, it also rules out local smooth isometric embeddings. The stronger statement that can be chosen with the full Euclidean Taylor jet at the origin (Corollary 5.3) is not part of the goal. The goal is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. The theorem shows that smooth local isometric realization in can fail, which answers negatively the unrestricted smooth problem recorded by Yau and Ghomi. It separates the smooth case from the analytic case (Janet–Cartan) and from finite regularity (Pogorelov, Nadirashvili–Yuan 2008). It also shows, by Corollary 5.3, that the infinite-order jet of the metric at a point does not decide realizability. It leaves open the same question under a sign condition or , since the construction uses both signs of curvature.
Formalizing it. The statement is short, but the claimed proof combines PDE estimates for Darboux's equation, hyperbolic propagation, a Baire-category argument and a boundary-saddle geometric step. The literature has disagreed about the status of the smooth question (NY2002 versus NY2008), so a machine-checked proof would remove the ambiguity. Mathlib has the manifold calculus needed to state the result (ContMDiff, mfderiv) but none of the PDE layer.
Where the Gaussian curvature is nonzero, the realization equations are elliptic or hyperbolic and can be solved locally, so any counterexample must exploit degeneracy where vanishes and changes type. Finite-regularity counterexamples (Pogorelov) do not carry over: existence at every finite order, on neighborhoods that shrink with the order, does not give one smooth map on a fixed neighborhood. Nonsolvable Monge–Ampère equations are also not enough by themselves, because the coefficients of the Darboux equation come from the same metric, so the obstruction has to be built into itself. Finally, the conclusion must hold for every neighborhood of the origin and every smooth immersion, with no a priori bounds on .
coordinateSquareOpen with values in Matrix (Fin 2) (Fin 2) ℝ. Each entry is ContMDiff … ∞ and each value is Matrix.PosDef, which includes symmetry (Hermitian over ℝ).U : Opens Coord with and , and over all maps F : U → Ambient that are ContMDiff … ∞ on the open submanifold . The isometry condition is stated with mfderiv and the Euclidean inner product: .An isometric immersion realizes an abstract Riemannian manifold as a surface in Euclidean space whose induced lengths are exactly the prescribed ones. How many dimensions are needed is a classical question. Nash showed that every compact Riemannian -manifold embeds smoothly and isometrically in some Euclidean space; for surfaces his bound is (Nash 1956). Gromov lowered the immersion dimension for closed surfaces to (Partial Differential Relations, 1986, §3.2.4). Three dimensions do not suffice even locally in the smooth category, and Gromov recorded the question whether every smooth Riemannian surface admits a smooth isometric immersion into (Gromov 2000, §I, Remark (d)), later attributing it to Chern around 1950 (Gromov 2015, p. 4).
This mission asks for a machine-checked proof of Theorem 1.1 of an OpenAI preprint dated September 23, 2026 (source), which answers the compact, boundaryless form of that question: every closed smooth Riemannian surface admits a smooth isometric immersion into . The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.
A closed surface is a compact smooth two-dimensional manifold without boundary; it need not be orientable or connected. A Riemannian metric assigns to each a positive definite inner product on , depending smoothly on . A smooth map is an isometric immersion if
Positive definiteness of forces to be injective, so is an immersion; self-intersections are allowed.
For every closed smooth Riemannian surface there is a map with , where . In Lean this is OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth_isometric_immersion.
The result itself. The theorem lowers Gromov's immersion dimension for closed surfaces from five to four, with no restriction on curvature or topology, and settles the closed case of the question Gromov attributes to Chern. Dimension four is the first codimension in which the smooth problem can have a global answer for all surfaces, since smooth metrics with no local isometric immersion into exist. The open (noncompact) case of the question is not addressed.
Formalizing it. Mathlib now has smooth manifolds, tangent bundles and smooth Riemannian metrics, so the statement is expressible without custom geometry. A complete proof would add Whitney's immersion theorem, Sard's theorem in equal dimensions, metric decompositions into rank-one terms, Nash–Moser-type smoothing estimates, and oscillatory correction schemes; none of these are formalized at this level, and all are reusable in geometric analysis.
The isometric immersion equation is a nonlinear system of three equations in four unknown functions, and its linearization loses derivatives, so a direct implicit function argument fails. Convex integration in the Nash–Kuiper style produces only solutions. Poznyak's smooth theory works on planar domains with boundary, but on a closed surface the successive local corrections must remain compatible globally. The preprint keeps a nondegenerate normal geometry (a nonzero vector-valued second fundamental form) through every step, adds the metric deficit one positive rank-one term at a time via a velocity loop in a plane normal to and (Proposition 3.1, p. 8; Proposition 7.1, p. 25), and then corrects the approximate metric exactly by a smoothing scheme that solves the linearized equation only on oscillatory modes (Proposition 5.1, p. 15). Nonorientable surfaces are handled by starting from an immersion into a small round -sphere, whose radial direction is a global normal (Lemma 9.1, p. 35).
ChartedSpace (EuclideanSpace ℝ (Fin 2)) M and IsManifold 𝓘(ℝ, ℝ²) ∞ M, assumed compact, Hausdorff and second countable. Being modeled on (not a half-space) encodes "without boundary"; no orientability or connectedness is assumed.Bundle.ContMDiffRiemannianMetric of class on the tangent bundle.ContMDiff … ∞ F and equality of the Euclidean inner product of mfderiv images with g.inner p v w for all tangent vectors; immersivity follows and is not stated separately.