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?
Semidefinite representations may be smaller than linear descriptions of a polytope. Lower bounds for their matrix size require a factorization obstruction that applies to arbitrary positive-semidefinite factors. The source manuscript presents the surrounding research claim.
For even n, columns are perfect matchings of the complete graph. Rows comprise edges and odd vertex subsets. The unshifted slack matrix has edge-incidence entries and odd-cut entries |M∩δ(U)|−1. Its real PSD rank is the least positive r admitting trace products of positive-semidefinite r×r factors.
Prove that every positive real power is eventually exceeded:
The separate lift target gives the same superpolynomial lower bound for every exact affine PSD lift.
The selected formal target is OAI.PerfectMatchingPSD.main.
The selected formal goal excludes polynomial-size factorizations. The manuscript dated October 5 states exponential bounds for positively shifted matching matrices; that stronger shifted statement is not the existing published target. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Factors are unrestricted real PSD matrices, with no rank-one or symmetry requirement. Lower bounds for nonnegative rank alone do not rule them out.
The target concerns the full unshifted row set and uses real exponentiation with C fixed before n₀. The affine-lift companion quantifies over affine sections and affine images of PSD cones. Independent definition groups are retained separately. The description deliberately makes no exponential or positive-shift claim for these references.
adc7f1241b42. Goal source.Inversion gates create domains of definition as well as nonzero-value conditions. A rational hitting list must find a point where every inverse exists and where the final value is invertible. The source manuscript presents the surrounding research claim.
A noncommutative rational formula over ℚ has variables, constants, sums, ordered products and inverse gates, with tree-node size. Evaluation is a relation requiring genuine two-sided inverses. Admissible means defined at some positive-dimensional rational matrix tuple; nonzero means one such defined value is nonzero.
Construct one deterministic finite-state Turing machine and positive integers C,k which, on unary n,s≥1, outputs a list H of common positive-dimensional rational tuples with
and every admissible nonzero size-s formula has a defined invertible value at some tuple in H.
The selected formal target is OAI.RationalHitting.main.
The output-length bound controls the full binary representation, including rational entries and all tuples. No separate inverse-depth or coefficient-height parameter is added. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
A tuple detecting one rational expression may encounter a singular inverse in another. Definedness and invertibility must be guaranteed at a list point for every eligible formula.
Matrices and constants are rational; scalars use the algebra map. The fixed TM0 alphabet and state space, self-delimiting binary output and unary parameter input are explicit. The matrix dimension is shared across the entire list and required positive.
adc7f1241b42. Goal source.Testing a noncommutative polynomial at scalar points can lose its ordered-word structure. Matrix evaluation preserves noncommutativity and permits a single prescribed tuple to test an entire bounded-size formula class. The source manuscript presents the surrounding research claim.
A division-free formula has scalar and variable leaves and addition or ordered multiplication gates. Its size counts every tree node. Nonzero means that at least one coefficient of its word series is nonzero. The published generator is an explicit tuple of rational matrices depending only on n and s.
For all n,s≥1, every characteristic-zero field F and every formula f of size at most s, prove
where the rational tuple T is coerced into F and has dimension 2ns², except for the specified one-variable size-one case.
The selected formal target is OAI.NCHitting.universal_hitting.
One tuple is universal for the whole size class and every characteristic-zero coefficient field. The formal goal establishes its hitting property. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Nonzero word coefficients must survive the same matrix substitution uniformly across all formulas. Choosing a point separately for each f would reverse the required quantifiers.
Formula coefficients are defined by word convolution; evaluation uses scalar matrices and the explicit rational generator. The theorem asserts nonzero matrix output, not invertibility. The manuscript’s deterministic construction-time claim is not a separate statement in this selected Lean target.
adc7f1241b42. Goal source.Online selection must commit before all values arrive, while the offline optimum sees the full vector. The mission asks how much one independent sample per item can recover under a matroid feasibility constraint. The source manuscript presents the surrounding research claim.
A matroid on Fin n specifies feasible independent subsets. An online rule sees the full initial sample vector, a finite random seed and the arriving label/value prefix. Sample and value coordinates are jointly independent, corresponding marginals agree, and the seed is independent of all of them.
For every labeled matroid, construct a distribution-independent rule and seed law such that every prefix is feasible and, for every measurable arrival permutation,
The arrival order may depend on all samples, all values and the entire seed. Reward integrability is also required.
The selected formal target is OAI.MatroidProphet.one_sample.
The rule and its seed distribution depend only on the known matroid. The allowed adversary is stronger than an order chosen before the values or random seed are revealed. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Independence of the input coordinates does not imply independence of the adversarial order. The guarantee must survive an order selected with full information while decisions remain irrevocable.
Values are nonnegative almost surely, and only the actual offline optimum is assumed integrable. The hidden-vector target with ratio 2⁻²⁹³ provides an available supporting milestone. The duplicated one-sample formulation and secretary consequence remain references in their independent source group.
adc7f1241b42. Goal source.Hyperbolic polynomials define convex optimization regions through real-rooted line restrictions. A spectrahedral representation would describe the same region by one finite symmetric positive-semidefinite matrix inequality. The source manuscript presents the surrounding research claim.
The formal ambient space consists of two real symmetric 4×4 matrices X,Z and a vector y∈ℝ³. A fixed determinant expression defines a multivariate polynomial p. At e=((I,I),0), the cone consists of x for which every complex root of t↦p(te−x) is real and nonnegative.
Prove dim(ambient)=23, p(e)=1, and
with every line polynomial real-rooted. For every N>0 and linear symmetric pencil L, prove
The selected formal target is OAI.Paper256.main_result.
The formal target rules out every finite homogeneous real symmetric pencil size. It also verifies the algebraic and root properties of its fixed polynomial. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Excluding one determinantal expression is weaker than excluding all matrix-inequality representations of the cone. The final universal quantifier ranges over all positive dimensions and all real linear pencils.
The published Lean formula has asserted degree 20. The manuscript abstract describes degree 16; this draft follows the actual published degree-20 statement rather than substituting the manuscript number. Symmetric matrices use selfAdjoint, and positivity is Matrix.PosSemidef. No affine pencil or projected semidefinite lift is asserted here.
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.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.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.Birational anabelian geometry studies how much of a function field is determined by a small quotient of its absolute Galois group. This mission isolates uniqueness in the reconstruction correspondence. The source manuscript presents the surrounding research claim.
Fix a prime ℓ. The fields K/k and L/l are essentially finite type extensions of algebraically closed constant fields, have transcendence degree at least two, and have characteristic different from ℓ. The abelian-by-central datum records the pro-ℓ abelian quotient and the commutator pairing. IsomF consists of constant-preserving perfect-closure isomorphisms modulo Frobenius; IsomCUnits quotients bracket-compatible Galois isomorphisms by the encoded ℓ-adic unit relation.
For field-isomorphism classes a and a′ and a Galois-isomorphism class b, prove
PhiGraph is the relation induced by representatives and a compatible extension to algebraic closures.
The selected formal target is OAI.BogomolovPop.main_graph_injective.
This establishes uniqueness of the field class whenever two representatives produce the same Galois class. The manuscript states a full reconstruction bijection; the selected published Lean target is its graph-injectivity assertion. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Equality is required after two different quotient constructions, one generated by Frobenius and one by ℓ-adic scalar limits. Recovering equality of classes must respect both ambiguities and the contravariant Galois action.
The definition block constructs topological pro-ℓ quotients, closed commutator subgroups, perfect closures and the pullback graph. The theorem quantifies over arbitrary field types with the stated algebraic instances. It does not assert existence, surjectivity or functionality of PhiGraph, and those broader manuscript conclusions are not attached as proved results. Only the existing injectivity target and its definition block are referenced.
adc7f1241b42. Goal source.Compatibility between reassociation and braiding imposes equations on formal Lie expressions. The question is whether those equations leave precisely the free family of odd-weight generators predicted by the Deligne–Drinfeld conjecture. The source manuscript presents the surrounding research claim.
Let L be the free Lie algebra over ℚ on x and y, each of weight one. The solution space W satisfies antisymmetry, the three-term relation, and the pentagon equation in the four-strand infinitesimal braid algebra. Its operation is the Ihara bracket {p,q}=Dₚq−D_qp+[p,q]. The free algebra F has generators indexed by k ≥ 0 with weights 2k+3.
Establish a graded bracket-preserving linear equivalence
together with mutually inverse continuous maps on the products of weight pieces. The completed maps must preserve the bracket degree by degree, including the finite convolution sum defining its weight-n component.
The selected formal target is OAI.DeligneDrinfeld.main.
The target simultaneously expresses freeness and exhaustion of the full equation space. Finding a free subalgebra alone leaves the exhaustion assertion unresolved. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
The pentagon relation couples substitutions in the braid Lie algebra. Constructing odd-weight solutions does not by itself show that all solutions are generated by them, nor that the completed bracket has the required compatibility.
The published definition block specifies the braid quotient, tangent construction of D, weighted Lie words, rational submodules and product completions. Generator k has weight 2k+3. The factor spaces carry the explicitly supplied discrete topology. The goal is exactly MainStatement, including its inverse, continuity and completed-bracket clauses. The available reference set supplies the definition block and one target, so no unsupported paper lemmas are attached as milestones.
adc7f1241b42. Goal source.An isotropic elastic body is described by two spatially varying Lamé moduli: the shear modulus and the parameter (the bulk modulus is ). The elastic inverse problem asks whether static boundary measurements, the boundary tractions produced by all prescribed boundary displacements, determine both moduli inside the body. It is the elasticity analogue of Calderón's conductivity problem, with applications to elastography and nondestructive testing, and it is harder because two coefficients are coupled through a vector-valued system rather than a scalar equation.
Without smallness, analyticity or symmetry hypotheses, three-dimensional global uniqueness was not established. The source of this mission is an OpenAI preprint dated September 24, 2026, which claims it for all smooth moduli satisfying the energy-positivity conditions.
Let be a bounded connected domain with boundary, and let satisfy
For a displacement , the strain is , the stress , and the elasticity system is . For boundary data let be the unique weak solution with trace . The displacement-to-traction map is
For admissible pairs , on ,
The Lean statement OAI.Elasticity.global_uniqueness is open on the platform.
The theorem settles the smooth three-dimensional isotropic elastic Calderón uniqueness question under the natural energy-positivity assumptions, with no analyticity, no closeness to constants, and no prior agreement near the boundary. It identifies both moduli from the full zero-frequency boundary operator. It does not give a reconstruction algorithm or stability estimates, which remain natural follow-up questions.
The result is stated in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.
The scalar complex-geometric-optics method does not apply directly to the Lamé system. Earlier reductions to auxiliary systems ran into two problems documented in the Nakamura–Uhlmann erratum: the planar matrix transport equation with prescribed initial data need not be solvable, and the corrected solutions lead to a pseudodifferential rather than a differential identity. The Eskin–Ralston reduction from auxiliary fields to physical displacements is not injective, so equality of physical boundary maps does not by itself give equality of auxiliary Cauchy data. A proof must work with exact physical solutions and keep track of their actual divergences.
Domain Ω: open, connected, bounded, with smooth boundary given by local diffeomorphisms of flattening .Admissible Ω λ μ: both moduli smooth on an open neighbourhood of , with and on .DN Ω λ μ f g is the energy pairing of a weak solution with trace against any representative of ; the goal assumes equality of these two-variable functions and concludes pointwise equality of the moduli on .A complete development needs vector-valued Sobolev spaces, Korn's inequality, the weak Dirichlet problem for the Lamé system, Carleman estimates and complex geometric optics for elliptic systems. These tools are reusable for other inverse problems. Contributions formalizing Lemma 2.1 (common exterior extension), Proposition 2.2 (transfer of physical solutions) and Proposition 3.2 (supported Carleman estimate) are welcome.
Liouville theorems say that certain nonlinear elliptic equations have no positive solutions on the whole space. Beyond their own interest, they are the key input in blow-up and rescaling arguments that give a priori bounds, existence results and singularity estimates for equations on bounded domains (Gidas–Spruck 1981; Polačik–Quittner–Souplet 2007). For the scalar equation , Gidas and Spruck proved nonexistence in the whole subcritical range. For the coupled Lane–Emden system , , the corresponding statement — no positive solutions below the critical hyperbola — is the Lane–Emden conjecture; before the source, it had been proved only in dimensions and in partial ranges. The weighted Hénon–Lane–Emden version, with factors and , asks the same question for the weighted hyperbola.
Fix an integer , exponents and real weights . The Hénon–Lane–Emden system is
where is the Laplacian. A solution in the sense of the source is a pair with and for every , including the origin, satisfying both equations at every . The exponents are subcritical if
In Lean, Space n = EuclideanSpace ℝ (Fin n), IsSolution n p q A B u v packages continuity, ContDiffOn ℝ 2 off the origin, strict positivity everywhere and the two equations with Mathlib's Laplacian and real powers, and Subcritical is the displayed inequality.
This is exactly Theorem 1.1 of the source. Taking gives the unweighted Lane–Emden conjecture (Corollary 1.2) for . The goal is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. If the source's proof is correct, the theorem gives a positive answer to Huang and Zou's Conjecture B and, with , to the Lane–Emden conjecture in every dimension. It needs no radial symmetry, boundedness, integrability, finite energy, stability or growth condition at infinity. Combined with the radial existence theorem of Bidaut-Véron and Giacomini, it also settles Phan's Conjecture C for and , including existence on the critical hyperbola (Corollary 6.2). Through the blow-up method, Liouville theorems of this type give a priori bounds and singularity and decay estimates for Lane–Emden-type systems on bounded domains.
Formalizing it. The statement is elementary: classical derivatives, the Euclidean Laplacian and real powers. The proof uses potential estimates, a localized virial (Rellich–Pohozaev type) identity, a geometric interval inequality and a dilation argument. All of these are within reach of Mathlib's analysis library, which makes the theorem a realistic test of large-scale PDE formalization.
The weighted statement does not follow from the unweighted one at the same exponents. For example, , , is weighted-subcritical, while is unweighted-supercritical. Weighted subcriticality also does not give the unweighted input in Phan's transfer argument. Translations do not preserve the weighted equation, so moving-plane and translation-based compactness arguments are unavailable. The level sets have endpoint values that vary with , which breaks the unweighted interval comparison. Finally, since no energy, decay or stability bound is assumed, the localized energy has to be bounded from the subcritical gap alone.
EuclideanSpace ℝ (Fin n) with , and are real with . Weights are Real.rpow ‖x‖ A, used only at , so the junk value of rpow at never enters. The nonlinearities Real.rpow (v x) p are evaluated at strictly positive arguments.Continuous on all of and ContDiffOn ℝ 2 on . Positivity is required at every point, including the origin, as in the source; differentiability at the origin is not assumed.Heat in an insulated planar plate evolves by the heat equation with Neumann boundary condition. For generic initial temperature, after a long time the temperature minus its average is dominated by an eigenfunction of the first positive Neumann eigenvalue. Rauch asked in 1974 where the hottest and coldest points of the plate end up, and conjectured that they move to the boundary (Rauch 1975). In spectral form, the hot spots conjecture asks whether a first nonconstant Neumann eigenfunction attains its maximum and minimum only on the boundary. The question links spectral geometry, reflected Brownian motion and elliptic PDE, and it is known to depend on topology: it fails for some domains with holes.
This mission asks for a machine-checked proof of the strict form of the conjecture for all smooth bounded simply connected planar domains, as claimed in an OpenAI preprint dated September 24, 2026 (source): every nonzero first-positive Neumann eigenfunction has no interior critical point at all. The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal below is open.
Let be a nonempty bounded open simply connected set with boundary. The first positive Neumann eigenvalue is
counting only positive eigenvalues (many sources call it ). The first positive Neumann eigenspace consists of the with and
This weak formulation encodes in with on . Eigenspace functions are smooth up to the boundary.
For every nonzero ,
This holds for every member of the eigenspace, also when is a multiple eigenvalue. In Lean this is OAI.StrictHotSpots.main_theorem.
The result itself. It resolves Burdzy's simply connected planar hot spots conjecture in its strongest form: not only do the extrema lie on the boundary, but there are no interior saddle points either, for every eigenfunction in the eigenspace. Combined with the Burdzy–Werner and Burdzy one-hole counterexamples, it shows that simple connectivity is exactly the dividing line among smooth planar domains. The intermediate kernel theorem (Theorem 5.1, p. 12), a conditional negativity statement for reciprocal Green kernels of the disk, is stated independently of the eigenfunction problem.
Formalizing it. A complete development needs Sobolev spaces on smooth planar domains, the Riemann mapping theorem with boundary regularity, Neumann elliptic regularity, and the theory of conditionally negative definite kernels. Each is reusable. No machine-checked proof of any hot spots result, including the triangle case, is known to exist.
Each Cartesian derivative of an eigenfunction solves the same Helmholtz equation, but its boundary values have no fixed sign, so a maximum-principle argument on one directional derivative fails on a general domain with no preferred direction. Coupling methods need convexity or symmetry. The preprint instead uses the Neumann condition jointly on both derivatives (the gradient is tangent to the boundary), via a nonnegative quadratic form whose null space consists exactly of eigenfunction gradients (Proposition 3.1, p. 7). The central difficulty is to build enough scalar boundary multipliers preserving that null space; this requires proving that a reciprocal kernel is conditionally negative semidefinite (Theorem 5.1, p. 12), through regularized Green kernels, a complete Nevanlinna–Pick-type matrix property, and a boundary limit.
EuclideanSpace ℝ (Fin 2): nonempty, open, bounded, IsSimplyConnected (which includes path-connectedness), with a smooth local defining function with nonzero derivative at every boundary point.HasH1Gradient Ω v g: and is the weak gradient of against smooth test functions compactly supported in . is the sInf of Rayleigh quotients over mean-zero nonzero functions; this set is nonempty and bounded below by .InFirstNeumannEigenspace Ω u requires , mean zero, and the weak eigen-equation for all test pairs. The smoothness-up-to-the-boundary clause is a standard regularity fact for Neumann eigenfunctions on smooth domains (the preprint cites Showalter for it), so it does not exclude any eigenfunction.sInf/sSup of on frontier Ω, which is compact and nonempty, so these are the true minimum and maximum.Calderón's inverse conductivity problem asks whether the electrical conductivity inside a body is determined by voltage and current measurements on its boundary. Mathematically, a conductivity on a domain defines the elliptic equation , and the boundary data are encoded by the Dirichlet-to-Neumann (DN) operator , which maps a boundary voltage to the resulting boundary current. The problem underlies electrical impedance tomography and is the model case of a large family of inverse boundary-value problems. Calderón (1980) posed it for bounded measurable conductivities bounded away from zero; how much regularity uniqueness requires has been a central question since.
In dimension , uniqueness for merely bounded measurable scalar conductivities remained unresolved. The source of this mission is an OpenAI preprint dated September 23, 2026, which constructs a counterexample in dimension three.
Let . A conductivity is a measurable with almost everywhere. Let be the Sobolev space, the closure of compactly supported smooth functions, and the trace space, with dual . For a trace , let be the unique function with trace such that
The DN operator is
There are and with
The Lean statement OAI.ScalarConductivity.main_nonuniqueness is open on the platform.
The theorem shows that scalar Calderón uniqueness fails in the bounded measurable class in dimension three, in contrast with the planar theorem of Astala–Päivärinta and the Lipschitz and uniqueness results in higher dimensions. It locates the regularity threshold for uniqueness strictly between and the known positive classes. By Corollary 1.2, counterexamples can be localized: any finite family of disjoint balls inside any Lipschitz domain supports distinct conductivities with the same DN map.
The result is stated in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.
Matrix-valued counterexamples exist, but they do not transfer to scalar conductivities: scalar coefficients can approximate matrix ones only in the sense of - or -convergence, and Rondi's example shows that exact realization of a full boundary map by a scalar coefficient can fail. Moreover, Daudé–Kamran–Nicoleau note an obstruction for full-boundary data: a weakly harmonic factor with constant full boundary trace is constant. One must therefore match the entire DN operator (every boundary input) exactly, with a scalar coefficient, and with uniform ellipticity bounds; the paper does so with a nested family of scalar blocks realizing prescribed current triples exactly.
IsDirichletToNeumann γ Λ requires existence and uniqueness of the weak -harmonic extension of every trace and the weak flux identity against every .EqualOneNearBoundary asks for with a.e. on ; bounds and measurability are stated almost everywhere on the ball.A complete development needs Sobolev spaces on a ball, weak solutions of divergence-form equations (Lax–Milgram), trace spaces, and the paper's block constructions (convex-integration-type scalarization). Contributions formalizing Theorem 3.1 (exact finite-field scalarization), Proposition 4.1 (branching block) and Corollary 1.2 are welcome.
The Boltzmann equation describes a dilute gas through a density of particles at position with velocity , evolving by free transport and binary collisions. For hard spheres, the collision rate is proportional to the normal relative speed. In 1989 DiPerna and Lions constructed global renormalized solutions for all initial data with finite mass, energy and entropy, and weak stability holds at the same level. Existence and stability do not give uniqueness, though: the physical bounds do not even make the quadratic collision term locally integrable, and the uniqueness of general renormalized solutions is a basic question in kinetic theory (Silvestre 2022, §2). Uniqueness is known only under much stronger assumptions, such as Maxwellian upper bounds or closeness to equilibrium.
Phase space is , with . For incoming velocities and a collision normal , put , , . The hard-sphere collision operator is
with ordinary surface measure on ; the two terms are the gain and the loss. The Cauchy problem is , . An initial datum has finite entropy if it is nonnegative and .
A solution is admissible (Definition 2.1 of the source) if, with :
There is a nonnegative finite-entropy datum with bounded velocity support, two admissible global solutions with initial datum , and a time such that
This is Theorem 1.1 of the source (p. 3), with the difference placed in the common interval of strong continuity, which is where the source establishes it. 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 shows that the DiPerna–Lions framework, even with local mass conservation, momentum conservation and the energy and entropy inequalities retained, does not determine the evolution uniquely. The example is spatially inhomogeneous and periodic, and the two solutions start from exactly the same datum, unlike ill-posedness results that compare nearby data. On the interval where they differ, both solutions satisfy the unrenormalized equation. The datum has bounded velocities but unbounded amplitudes concentrated at smaller and smaller spatial scales, which points to the kind of extra control a uniqueness theorem has to impose.
Formalizing it. The statement fixes a long list of admissibility conditions. Its definitions are a useful contribution in their own right: renormalized solutions, entropy dissipation and kinetic test functions on the torus are not in Mathlib. The 65-page proof (colored decompositions, Carleman representation, velocity averaging, a dilation limit and a branching analysis) is a long-term target. Its propositions are natural milestones.
Constructing two different weak limits is not the hard part: approximations with and without a small "hot seed" give two candidate solutions. The difficulty is to show that they really differ. A vanishing seed can produce a hit on the a priori cap that carries arbitrarily little mass, and weak compactness can erase it in the limit. The source must rule out this loss of information uniformly as the cold velocity distributions collapse onto an axis, where the weight controlling the hot density is singular. At the same time every admissibility condition, including the entropy-dissipation inequality and local mass conservation, has to survive the limits. Energy-increasing constructions (Wennberg) and homogeneous examples do not meet these constraints.
EuclideanSpace ℝ (Fin 3), positions in Fin 3 → AddCircle 1, and densities are real functions on phase space. The sphere carries (volume).toSphere, which is ordinary surface area, not a probability measure.gain and loss are Bochner integrals. To prevent them from silently returning on non-integrable fibers, AdmissibleGlobal requires fiberwise integrability and space-time integrability of the renormalized gain and loss.AdmissibleGlobal f₀ F encodes Definition 2.1: finite entropy at each time, a.e. initial value, weak continuity against bounded measurable tests, uniform moment bounds, the renormalized equation for all Renormalization and all smooth periodic KineticTest , local mass conservation against MassTest, total momentum conservation, the energy inequality, and the entropy inequality in ℝ≥0∞ with the lower semicontinuous extension of .StrongEarly T F adds , strong continuity on via eLpNorm, and integrability of gain and loss on . Distinctness is ¬ (F t =ᵐ G t) for some .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.