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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
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?
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.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.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.How rigid is a von Neumann algebra inside ? If two algebras have unit balls that are uniformly close, must they be the same algebra up to a small change of coordinates? Kadison and Kastler introduced the distance between the unit balls in 1972 (Amer. J. Math. 1972) and asked whether sufficiently close algebras are spatially isomorphic, implemented by a unitary close to the identity. The positive answer for a class of algebras is called (strong) Kadison–Kastler stability. The problem connects perturbation theory, Hochschild cohomology, and Kadison's similarity problem, and it was settled previously only for injective (amenable) algebras, type I algebras, and specific nonamenable examples.
This mission asks for a formal proof of the uniform strong Kadison–Kastler stability theorem stated in an OpenAI preprint dated September 23, 2026 (source): a single tolerance works for all von Neumann algebras on all Hilbert spaces. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Let be a complex Hilbert space and the bounded operators with the operator norm. A von Neumann algebra is a unital -subalgebra equal to its double commutant (in particular it contains the identity ). Write for its unit ball. The Kadison–Kastler distance is the Hausdorff distance of unit balls,
A unitary conjugates to if .
For every there is such that for every complex Hilbert space and all von Neumann algebras with , there is a unitary with
The tolerance depends only on : not on the algebras, their type, their representations, or the size of .
The result itself. It answers the Kadison–Kastler perturbation question in its strongest uniform form for von Neumann algebras, including all nonamenable and type III cases and non-separable Hilbert spaces. Consequences include that every algebraic or analytic invariant preserved by unitary conjugacy (type, factoriality, property , Cartan subalgebras) is locally constant in the Kadison–Kastler metric. The analogous C*-algebra statement fails in its uniform-unitary form by Johnson's examples, so the theorem is specific to von Neumann algebras.
Formalizing it. The statement uses only Mathlib's VonNeumannAlgebra, unitary operators and Hausdorff distance, so it is fully expressible today. The proof, however, draws on free probability, tracial ultraproducts, Tomita–Takesaki theory, crossed products, Poisson boundaries and measurable cocycles, most of which are absent from Mathlib. Formalizing even the amenable (injective) case would be a substantial reusable contribution.
Closeness of unit balls supplies nearby elements but no linear or multiplicative correspondence between the algebras, and it gives no control at matrix levels, where perturbation arguments naturally live. For nonamenable algebras the classical route through vanishing Hochschild cohomology is unavailable. The preprint proceeds by cases. For finite factors it proves a uniform bound on all matrix amplifications of commutator maps (Theorem 3.1, p. 11) and corrects nearby unitaries to a measurable cocycle over an amenable boundary action (Section 4). Infinite factors require comparing modular groups through Tomita graphs (Proposition 6.5, p. 41) and aligning the modular action (Proposition 7.1, p. 45) before passing to crossed products (Theorem 8.4, p. 59). General algebras then require aligning centers and passing from separable to arbitrary Hilbert spaces (Section 9) without losing uniformity.
NormedAddCommGroup, InnerProductSpace ℂ, CompleteSpace) in a fixed universe u; is chosen before , so the uniformity over Hilbert spaces is part of the statement.VonNeumannAlgebra H is Mathlib's notion; these algebras contain the identity, so "unital with identity " is built in.kkDistance M N is Metric.hausdorffDist of the closed unit balls. Both balls contain and are bounded, so the Hausdorff distance is finite and the definition is exactly (1.1).NearConjugacy M N ε asks for a unitary with as sets and .A random configuration on the vertices of a graph is a factor of IID if it can be produced by a measurable rule from independent uniform labels at the vertices, where the rule commutes with the graph's automorphisms. On trees this notion connects ergodic theory (which invariant processes are "Bernoulli-like"), local algorithms on sparse random graphs (factors of IID are limits of what local algorithms can produce), and statistical mechanics. The free Ising state on the -regular tree is the basic test case. It is easy to sample from a chosen root by broadcasting spins outward, but a factor rule may not use a root. Lyons asked for which inverse temperatures it is a factor of IID (Lyons 2017), and Nam, Sly and Zhang conjectured the answer after proving it for large below a non-explicit constant (Nam–Sly–Zhang 2022).
This mission asks for a formal proof of the exact threshold, including equality, as stated in an OpenAI preprint dated September 26, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Let be the infinite -regular tree with vertex set ; concretely, is the set of finite words over with no two equal consecutive letters, and is adjacent to . Put for . The free zero-field Ising law on is determined by its marginals on finite connected subtrees :
Equivalently, a fair spin at one vertex is broadcast along edges, each child agreeing with its parent with probability . A spin law is a factor of IID if it is the law of for i.i.d. uniform labels and a measurable such that, for each fixed automorphism , almost surely, where .
For every integer and every ,
The result itself. It answers the ferromagnetic case of Lyons's question and proves the Nam–Sly–Zhang conjecture for every . The threshold coincides with the reconstruction (extremality) threshold of the free state, and the result holds at equality, where non-reconstruction alone gives no factor rule (a weak limit of factors need not be a factor). The preprint also shows that, in this range, the factor can be chosen to commute with every automorphism on every input (Lemma 8.5, p. 46). The converse direction ( excludes a factor) is known from Sly's obstruction via the Backhausz–Szegedy–Virág bound and is reproved on p. 2.
Formalizing it. The preprint's construction uses Brownian observation processes, stochastic localization, innovation equations of nonlinear filtering, and conditional-copy coupling arguments. Mathlib has Brownian motion only in early form and no stochastic calculus for infinitely many coupled SDEs; a formal proof would build reusable stochastic-analysis infrastructure. The converse needs the BSV correlation bound for factors of IID. No machine-checked factor-of-IID result for a non-trivial Gibbs measure is known.
Rooted sampling is easy; the obstacle is to remove the root while keeping the output a measurable function of the labels. Finite-cluster constructions only work in the uniqueness range . The Nam–Sly–Zhang approach observes and expresses the posterior through innovations , which are independent Brownian motions; but being Brownian does not make a function of , and that is the central step (pp. 2–3). At criticality the field-response sums in the innovation equation are only borderline integrable near time zero, so infinite sums must be justified with an exact covariance-energy identity rather than with a contraction estimate (Section 1.2, p. 3).
TreeVertex d is the set of words in Fin d with distinct consecutive letters, treeAdj appends or removes one letter, and TreeAut d is the group of adjacency-preserving bijections.Measure.infinitePi of Lebesgue measure on ; spins take values in a two-element type with the discrete σ-algebra, and configurations carry the product σ-algebra.HasFreeIsingLaw θ μ prescribes on every cylinder over a finite connected Finset by the product formula above; these cylinders determine the law.IsFactorOfIID d θ asks for a measurable Phi with pushforward law HasFreeIsingLaw θ and, for each automorphism g, Phi (relabel g U) = relabel g (Phi U) for almost every U (null set may depend on g), matching (1.1).θ = Real.tanh β with and ; at both sides hold trivially (i.i.d. spins), which is consistent with the source. The stronger everywhere-equivariant version is not part of the goal.In Bernoulli bond percolation on a graph , each edge is kept (open) independently with probability . As grows, an infinite connected component of open edges appears at the critical probability . The criticality problem asks whether an infinite cluster can already exist at . A negative answer means the phase transition is continuous. Benjamini and Schramm (1996) conjectured that, on every graph with a large symmetry group and , there is no infinite cluster at . The question contains the famous open case of and connects percolation to geometric group theory, since Cayley graphs of finitely generated groups are the main examples.
The source of this mission is an OpenAI preprint dated September 24, 2026, which treats the remaining subexponential-growth case for all quasi-transitive graphs.
A graph here has vertex set and a set of labelled bonds, each with a pair of endpoints; loops and parallel bonds are allowed. It is locally finite if each vertex lies in finitely many bonds, connected if any two vertices are joined by a path, and quasi-transitive if its automorphism group (bijections of vertices and of bonds respecting endpoints) has finitely many orbits on . Examples include and every Cayley graph of a finitely generated group.
For , let be the law of a random set containing each bond independently with probability . The cluster of is the set of vertices joined to by a finite path of bonds in (including ). Define
For every infinite, connected, locally finite, quasi-transitive graph ,
The hypothesis is necessary, since at every infinite connected graph percolates. The Lean statement OAI.CriticalPercolation.BondGraph.no_percolation_at_criticality is open on the platform.
Theorem 1.1 resolves the Benjamini–Schramm criticality conjecture for Bernoulli bond percolation, and in particular gives on for every (Corollary 10.1, p. 39), including the long-open case . With Hutchcroft's exponential-growth theorem, the remaining work is the subexponential case, divided into superpolynomial growth and growth bounded by a polynomial along a sequence of scales. As a consequence the percolation probability is continuous at on every such graph.
The result is proved in an OpenAI preprint that has not been peer reviewed. No machine-checked proof of the general quasi-transitive statement exists; the reported Lean formalization concerns only nearest-neighbour . A formal proof would also certify the structural input (Tessera–Tointon's finitary structure theorem) as used here.
The obvious strategy, renormalization from large finite boxes, needs a gluing inequality to connect independently found large clusters, and it needs coordinates: on a general quasi-transitive graph there is no lattice to place boxes in. Planar duality is unavailable, the lace expansion needs high dimension, and Hutchcroft's argument uses exponential growth essentially. In the superpolynomial case one must rule out two large distinct clusters adjacent across an edge; in the polynomial case one needs nilpotent-group coordinates (Gromov, Trofimov, Tessera–Tointon) and a two-direction corridor exploration in which conditional failure probabilities stay uniformly small. Neither uniqueness of the infinite cluster nor independence across coarse blocks can be assumed.
BondGraph V E stores ends : E → Sym2 V; loops and parallel bonds are allowed. LocallyFinite counts bonds at each vertex. Clusters use SimpleGraph.fromEdgeSet of the open bonds, so loops are discarded and parallel bonds collapse; reachability includes the zero-length path.Aut consists of a vertex bijection and a bond bijection that commute with ends; QuasiTransitive says some finite set of vertices meets every orbit.law p is ProbabilityTheory.setBernoulli Set.univ p on Set E: each bond retained independently with probability p : unitInterval.criticalProbability is sInf in unitInterval of ; if the set were empty this would be , which hpc excludes.percolates is the event that some cluster is infinite; the conclusion says it has measure at .A complete development needs Bernoulli product measures, Harris–FKG and conditional correlation inequalities, Hutchcroft's exponential-growth theorem, volume-growth theory of quasi-transitive graphs, and the Gromov–Trofimov–Tessera–Tointon structure theory. Each of these is reusable well beyond this mission. Contributions formalizing Proposition 3.1 (two-cluster bound), Theorem 6.1 (joint gluing), Theorem 7.1 (criticality with a nilpotent quotient action) or Proposition 9.3 (subcritical exploration), or the cited Theorem 2.2 (Hutchcroft), are welcome.
The irreducible complex representations of the symmetric group are indexed by partitions and written (Specht modules). Decomposing a tensor product (with the diagonal action) into irreducibles is governed by the Kronecker coefficients
which have no known positive combinatorial formula and are a central open topic in algebraic combinatorics and geometric complexity theory. A basic test of how far tensor products spread is the tensor square conjecture: in every degree (with a few exceptions) some single irreducible representation has a tensor square containing every irreducible representation.
For a Young diagram with cells, fix a bijection between and the cells (a tableau). The Lean development realizes inside the space of functions on words ( = number of rows), with acting by permuting letters: the polytabloid is the signed sum, over the column group of , of the permuted indicator of the row word of , and Specht t is the -span of the -orbit of . The Kronecker coefficient kronecker a b t is finrank of the space of -intertwining maps from spechtRep t to the tensor product spechtRep a ⊗ spechtRep b. canonicalTableau λ is a fixed tableau of shape .
For every positive integer with there is a partition such that
so the tensor square contains every irreducible representation of . The Lean statement asserts, for one Young diagram with cells: positivity of kronecker for every target diagram with cells; irreducibility of spechtRep for ; and that every finite-dimensional irreducible complex representation of admits an injective intertwining map into . This is Theorem 1.1 of the source together with its "thus" sentence. The goal is published on the platform with status Open.
The result itself. The theorem settles the tensor square conjecture of Pak, Panova and Vallejo, including all nontriangular degrees. Since the sign representation occurs, the chosen must be self-conjugate. Via Letellier's results it also gives tensor squares of unipotent characters of that contain every unipotent character (Corollary 1.2 of the source). The companion cyclic Saxl theorem is used as input at staircase degrees.
Formalizing it. The proof combines representation-theoretic constructions with exact finite computations (Murnaghan–Nakayama recursion for all eligible , and capacity calculations), which the source certifies by included programs. A formal proof would replace these with checked computation and would require building Specht modules, Kronecker coefficients and branching rules in Lean, infrastructure Mathlib currently lacks.
Knowing that a smaller staircase square contains every constituent does not transfer to an enlarged diagram: constituents must survive a map from the actual enlarged tensor square, and the attached cells introduce alternating terms that can cancel. Almost-all or higher-power results (Luo–Sellke, Harman–Ryba) do not give a universal square. Small degrees cannot be handled by asymptotic estimates and require exact Kronecker computations, and are genuine exceptions.
YoungDiagrams with card = n; the representation space is (Fin n → Fin d) → ℂ, and Specht t is the cyclic span of one polytabloid. kronecker is Module.finrank ℂ of Representation.IntertwiningMap, so it is the genuine multiplicity of in the tensor square.A thin spanning tree of a graph is a spanning tree that uses only a small fraction of the edges of every cut. Thin trees were introduced for the asymmetric traveling salesman problem: Asadpour, Goemans, Mądry, Oveis Gharan and Saberi showed that a thin tree of low cost can be augmented into a cheap tour, giving an -approximation (doi:10.1287/opre.2017.1603). Goddyn conjectured that high edge connectivity forces thin trees; the strong thin tree conjecture asks for thinness in every -edge-connected multigraph. For applications one wants not just existence but an efficient algorithm that finds such a tree, also when parallel-edge multiplicities are huge and written in binary.
Background. The maximum-entropy rounding of Asadpour et al. constructs -thin trees. Oveis Gharan and Saberi constructed -thin trees on planar and bounded-genus graphs (2011, doi:10.1137/1.9781611973082.75). Anari and Oveis Gharan proved existence of -thin trees in general (2015, arXiv:1411.4613), without a polynomial-time construction. Klein and Olver (2023, doi:10.1109/FOCS57990.2023.00011) and Klein, Olver and Yeoh (2026, doi:10.4230/LIPIcs.ICALP.2026.129) handled laminar families and near-minimum cuts. A companion OpenAI preprint claims the existence statement of the strong conjecture.
The source of this mission, an OpenAI preprint dated September 23, 2026, claims a deterministic polynomial-time construction.
Graphs are finite undirected loopless multigraphs; parallel copies count separately. For , is the multiset of edges with exactly one endpoint in , and is -edge-connected if for every such . A spanning tree is -thin if for all such . Two input formats are allowed: an explicit list of labelled edge copies, or a list of endpoint pairs with multiplicities written in binary (so the number of edges can be exponential in the input length). Running time is measured in the total binary input length.
There is an absolute constant and a deterministic algorithm that, given and a -edge-connected multigraph on at least one vertex (in either format), returns in time polynomial in the input length a spanning tree with
returning the empty tree for a one-vertex graph. Lean: OAI.AlgorithmicThinTrees.algorithmic_strong_thin_trees, open on the platform.
The theorem would give an algorithmic resolution of the strong thin tree conjecture: not only do -thin trees exist, they can be found deterministically in polynomial time, even for exponentially many parallel edges. It also yields simultaneous cost-and-cut rounding (Corollary 7.1): from a fractional point whose mass on every cut is at least one, a tree in its support with every cut load and total cost within constant factors, with no metric assumption on costs. The order is optimal. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.
Existence proofs for thin trees go through the Marcus–Spielman–Srivastava interlacing-families theorem and a fixed-point argument, neither of which is constructive: they show that some choice works without locating it. The algorithm must replace these by explicit, rational, polynomially sized computations (checked signings, rational positive semidefinite decompositions, bounded denominators) and must work with binary multiplicities, where even listing the edges is exponential. Certifying thinness on all exponentially many cuts must also be done without enumerating them.
StrongThinTree.MultiGraph n m (vertices Fin n, edges Fin m, loopless). Inputs are ExplicitInput or BinaryInput (ordered, distinct endpoint pairs with multiplicities); a binary input's edge copies are Σ i, Fin (multiplicity i).Valid x: , and EdgeConnected k.CurrentKS.Machine: a deterministic machine with finitely many binary stacks and a finite instruction table, run for a fuel bound. Inputs and outputs are self-delimiting binary encodings (CurrentKS.encodeNat).AlgorithmicStrongThinTrees: ∃ C > 0, ∃ M a degree, 0 < a ∧ ∀ x, Valid x → after a * (len + 1)^degree steps M has halted and its output stack encodes a duplicate-free edge list forming a ThinTree C k; for the output is empty.Needed infrastructure: the existence theory of the companion mission, a model of deterministic computation with polynomial-time bounds, exact rational linear algebra, and constructive spectral sparsification. Contributions formalizing Proposition 2.5, Proposition 3.1, Lemma 6.1, Theorem A.1 (rational rank-one signing) or Corollary 7.1 are welcome.
The chromatic symmetric function of a graph, introduced by Stanley, records all proper colorings of the graph with infinitely many colors as a symmetric function; it refines the chromatic polynomial. Whether it expands with nonnegative coefficients in the basis of elementary symmetric functions ("-positivity") is a central question in algebraic combinatorics. The Stanley–Stembridge conjecture (1993) predicted -positivity for incomparability graphs of -free posets; it arose from positivity questions for immanants of Jacobi–Trudi matrices. Shareshian and Wachs introduced a -graded refinement, the chromatic quasisymmetric function, which tracks ascents of colorings along edges, and conjectured that for natural unit interval graphs its elementary coefficients are polynomials in with nonnegative integer coefficients. The -refinement is tied to geometry: it describes the graded representation of the symmetric group on the cohomology of regular semisimple Hessenberg varieties.
Let be weakly increasing with . The natural unit interval graph has vertices and edges with . A proper coloring gives different colors to adjacent vertices, and counts edges with . The chromatic quasisymmetric function is
For a partition , with . Let be the set of permutations (as words ) such that every adjacent descent is an edge, and the number of inversions , , with an edge.
In Lean (namespace OAI.ElementaryPositivity), NaturalUnitIntervalGraph n stores a monotone extensive h : Fin n → Fin n; chromatic r is in variables as an MvPolynomial (Fin r) (Polynomial ℕ); Nondescent and graphInversions define and ; a PermutationWitness is a map together with the identity below in every number of variables, using Mathlib's MvPolynomial.esymmPart.
For every and every natural unit interval graph on there is a map with
In particular every elementary coefficient of lies in . The goal is published on the platform with status Open.
The result itself. The theorem resolves the elementary-positivity part of the Shareshian–Wachs conjecture, and at , via Guay-Paquet's reduction, recovers the Stanley–Stembridge conjecture first proved by Hikita. It is stronger than positivity: it gives a combinatorial witness, assigning each permutation of an elementary partition while preserving its graph-inversion weight. Through the Brosnan–Chow/Guay-Paquet identity, it implies that each graded piece of the cohomology of a regular semisimple Hessenberg variety is a direct sum of Young permutation modules with multiplicities counted by the witness (Corollary 1.2). Elementary unimodality, the other part of the Shareshian–Wachs conjecture, is not addressed.
Formalizing it. The statement is a finite polynomial identity for each , and , fully expressible with Mathlib's multivariate polynomials and elementary symmetric polynomials. A machine-checked proof would certify a long bijective argument (walls, triangle moves, witness completion) with many case distinctions.
The coloring definition already has nonnegative coefficients in the monomial basis, but rewriting in the elementary basis involves subtraction, so positivity is not visible from the definition. Earlier positive formulas (Schur expansions, power-sum expansions, the acyclic-orientation formula) group partitions or work at , and Hikita's probabilistic formula has rational -weights that are only positive at real , not coefficientwise. A proof over must produce, for each elementary partition and each power of , a nonnegative integer count, uniformly over all graphs.
h : Fin n → Fin n monotone with i ≤ h i (zero-indexed); edges are in either order.Fin r and the identity is required for every , which is equivalent to the identity of symmetric functions since both sides are homogeneous of degree .Polynomial ℕ, so nonnegativity in is built into the statement; the witness theta is an arbitrary function on the finite set . The source's additional assertion that is produced by a deterministic terminating procedure is not encoded, but any such function on a finite set is computable by search, so nothing of mathematical substance is lost.A vertex cover of a hypergraph is a set of vertices meeting every edge; the covering number is the minimum size of a cover, and the matching number is the maximum number of pairwise disjoint edges. In an -partite -uniform hypergraph the vertices are split into parts and every edge contains exactly one vertex from each part. Ryser's covering conjecture asserts
For it is Kőnig's theorem, so it proposes a higher-dimensional analogue of the most basic min–max theorem of bipartite matching theory. In the intersecting case () it asks for a cover of size , and it is equivalent to Gyárfás's conjecture that monochromatic trees cover any -edge-coloured complete graph.
Background. An equivalent formulation appears in Henderson's 1971 thesis (doi:10.7907/J1Z1-SK19). Aharoni proved the case in 2001 (doi:10.1007/s004930170001); Gyárfás and Tuza settled the intersecting case through ; Haxell and Scott (2012) proved for (doi:10.37236/1175); Francetić, Herke, McKay and Wanless (2017) handled linear intersecting hypergraphs through rank nine (doi:10.1016/j.ejc.2016.10.004); Bishnoi, Das, Morris and Szabó (2021) treated -intersecting hypergraphs (doi:10.1016/j.jcta.2020.105366). Truncated projective planes give equality whenever is a prime power; equality examples were studied by Mansour, Song and Yuster (2009, doi:10.1007/s00373-008-0821-9), Aharoni, Barát and Wanless (2016, doi:10.1007/s00373-015-1575-9) and Abu-Khazneh, Barát, Pokrovskiy and Szabó (2019, doi:10.1016/j.jcta.2018.07.011). Clow, Haxell and Mohar disproved Lovász's stronger matching-reduction conjecture at (doi:10.1007/s00493-026-00220-3), without contradicting Ryser's inequality.
The source of this mission, an OpenAI preprint dated September 23, 2026, claims intersecting counterexamples for ranks .
A finite hypergraph is a finite set of edges, each a finite set of vertices. It is -partite -uniform if there is a map assigning each vertex one of parts such that every edge contains exactly one vertex of each part. It is intersecting if it is nonempty and any two distinct edges share a vertex, so . Every edge of an intersecting hypergraph is itself a cover, so always; a counterexample to Ryser's conjecture in the intersecting case needs .
There are a prime with and such that for every prime , , an intersecting -partite -uniform hypergraph with and exists.
There is such that for every prime with there is such that for every odd , with , there is a finite intersecting -partite -uniform hypergraph with
In particular infinitely many ranks fail. Lean: OAI.RyserOdd.eventualOddFailures_and_infinite, open on the platform.
The theorem would disprove Ryser's conjecture in its intersecting case, and through the standard transfer (Corollary 1.2) also Gyárfás's monochromatic tree-cover conjecture, for the ranks . The value is the maximum possible. A companion preprint of the same family covers a different range of ranks (prime , with balanced parts); the two constructions are independent apart from three elementary estimates. Thresholds are not numerical. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.
The truncated-plane examples sit exactly at , and covers may mix vertices from different parts, so enlarging individual parts does not help. One must insert exceptional edges that destroy every cover of size while preserving the intersecting property. Ruling out all small covers requires showing that any small cover contains almost a full pencil of lines, which over needs an incidence bound with a power saving (a Bourgain–Katz–Tao-type sum–product estimate) valid in fields whose proper subfields are small. This is where odd exponents and the congruence enter.
Hypergraph V := Finset (Finset V) over a finite type V with decidable equality.RPartiteUniform r H: some part : V → Fin r with exactly one vertex of each part in every edge. Uniform r H: every edge has r vertices.Intersecting: distinct edges meet. matchingNumber is the maximal size of a pairwise disjoint subfamily; coverNumber is sInf of cover sizes, and existence of a cover is asserted separately so the sInf is not the empty-set default.ExplicitFailureAt r packages all of these with , and ; the goal asserts it for the stated ranks and that the set of failing ranks is infinite.Needed infrastructure: finite fields and their projective planes, incidence and sum–product estimates, and probabilistic selection arguments. Contributions formalizing Theorem 2.1 (uniform incidence saving), Lemma 3.2 (line covers after random deletions) or Theorem 4.1 (compatible translates from independent pools) are welcome.
In metric -median, a finite set (or ) of clients and a finite set of candidate facilities lie in a common finite metric with rational distances. Given an integer , one opens a nonempty set with and pays
Candidate facilities are part of the input and need not coincide with the clients. It is one of the basic clustering and facility-location objectives, and its approximability has been a testing ground for LP rounding, primal-dual methods and local search. The hard part of the problem is the facility budget: a solution with small connection cost is much easier to find if a few extra facilities may be opened, and every approximation algorithm must eventually enforce on its output.
This mission concerns two tools for enforcing that budget and their combination into a randomized approximation strictly below factor on arbitrary finite rational metrics, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Write and . A comparison solution of size assigns each client to a nearest member of (ties broken by fixed priorities); is the cluster of and , with . An anchor is a supplied feasible with . A certificate partitions into good and bad centres and gives distinct proxies for the good centres. A randomized polynomial-time algorithm is a polynomial-time multi-stack Turing machine that reads the encoded instance together with a string of fair random bits whose length is a fixed polynomial in the input length.
Let be disjoint, with distances between distinct indices positive integers bounded by a fixed polynomial in . Fix , and a rational . There is a randomized algorithm that, given an anchor with and a failure parameter , always returns with , runs in time polynomial in and , and, whenever some comparison solution of size and cost admits a certificate with
satisfies with probability at least . The algorithm is not given , or the certificate.
There is an absolute constant such that for every fixed some randomized polynomial-time algorithm for metric -median always returns a feasible (nonempty, , ) and satisfies
The result itself. Theorem 1.1 makes the running time single-exponential in the number of clusters without accurate proxies, so logarithmically many exceptions are tractable; FPT methods with dependence do not give this by setting . Combined with a new proof of bounded-price strictness for one compatible execution of the logarithmic-surplus construction of Cohen-Addad, Grandoni, Lee, Schwiegelshohn and Svensson (Lemma 8.1, p. 43), it yields Theorem 1.2: a randomized approximation strictly below , both with high probability and in expectation, that opens at most facilities on every output. A companion preprint proves a stronger deterministic bound by an independent route; Theorem 1.2's interest is the way recovery and payment accounting together enforce the budget.
Formalizing it. The statements are fully explicit about the machine model, the random bits, and the input encoding. A formal proof would need local-search anchoring (Theorem 3.3), leader/ball sampling with amortized radius guesses (Section 4), a finite categorical continuous-greedy algorithm with explicit error (Lemma 5.1, p. 21), the surplus construction as an external interface (Theorem 7.1, p. 35), and metric rounding and transfer (Lemma 2.1, p. 6). The submodular-optimization and local-search components are reusable.
Every factor- dual-fitting argument charges to a client set served by a comparison facility, which gives exactly ; improving the constant requires saving on connection cost while still paying for all regular openings with one final price, one set of copy lengths and the budgets of one actual replay of the construction (Section 1.2, p. 3). On the recovery side, guessing a good solution from an anchor naively costs ; keeping the dependence single-exponential in the number of bad clusters requires interleaving leader sampling and removals and amortizing radius guesses over disjoint client sets (Section 4). Theorem 1.1 holds only for normalized integral metrics; the global application must construct its anchors after normalization and transfer the final cost bound back (Lemma 2.1, p. 6).
RationalMetricInput: points Fin pointCount, a rational pseudometric table (zero on the diagonal, symmetric, triangle inequality), client and facility Finsets covering all points (they may overlap, so clients and facilities may share locations), a nonempty facility set and a positive budget . Feasible S is , , and nonempty when there are clients; optimum minimizes over nonempty subsets of size .BinaryRandomizedAlgorithm is a TM2ComputableInPolyTime function of (input bits, random bits) with finite alphabets, using randomBits.eval (input length) fair bits; probabilities and expectations are uniform averages over all seeds.Real.rpow); the same algorithm must also satisfy the expectation bound.Input adds disjointness of and , integral distances, positivity between distinct indices, and an anchor with anchor.card = budget; Bounded bound caps distances by a fixed polynomial in ; ζ is passed in unary precision , and PolynomialWork bounds work by . A Certificate encodes with , , the good set, injective proxies into the anchor, the proxy-cost promise with lexicographic tie-breaking, and at most bad centres.A set of unit-length jobs with precedence constraints is to be run on a fixed number of identical machines so that all jobs finish as early as possible. For two machines this was solved in 1969–1972; for a number of machines given as part of the input the problem is NP-complete (Ullman, 1975). Whether the problem is polynomial-time solvable for three machines, written , is problem OPEN8 in the appendix of Garey and Johnson's 1979 book and is one of the best-known open questions on the complexity of scheduling.
The source of this mission, an OpenAI preprint dated September 24, 2026, claims a deterministic polynomial-time algorithm.
The input is a directed acyclic graph on , , given as an explicit list of arcs, and optionally an integer deadline with . A feasible schedule with makespan at most is a map
such that each value is taken at most three times (three machines) and for every arc (precedence). Slot means execution during . There are no release dates, communication delays or other resources. The input length is the length of the binary encoding of the graph and deadline.
There is a single deterministic multitape Turing machine and a constant such that, on every such input of length , halts within
steps and
The exponent is the one stated in the paper and is not optimized; the content of the theorem is that a fixed polynomial bound exists. The Lean statement OAI.ThreeMachine.main_theorem is open on the platform.
The theorem resolves the polynomial-time side of Garey and Johnson's OPEN8: unit-job makespan scheduling with arbitrary precedence constraints on three identical machines lies in P. Previous exact algorithms were either restricted to special precedence structures (forests, bounded height) or subexponential, and approximation schemes did not decide the optimum. The structural statement behind the algorithm, that feasible schedules admit recursive decompositions whose interval job sets have descriptions of bounded size, may be of independent use for other fixed-machine scheduling problems. No practical running time is claimed.
The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. A formal proof would also certify the running-time analysis in an explicit machine model, which is rarely done for algorithmic results of this size.
Removing selected slots from a feasible schedule leaves gaps that can be rescheduled independently, which suggests a recursive search over the job sets of gaps. The obstacle is their number: naming a gap by its two boundary triples does not determine its job set, and intersecting descriptions inherited from ancestors can make the descriptions grow without bound along a recursion of linear depth. The subexponential decomposition of Nederlof–Swennenhuis–Węgrzycki controls the number of subproblems only up to ; a polynomial bound needs every subproblem to have a global description of constant size.
Instance n is a list of arcs on Fin n; acyclic forbids a Relation.TransGen cycle. Jobs are Fin n (shifted to in the encoding).Feasible G T τ: slots in , at most three jobs per slot, strict precedence.CorrectOutput distinguishes the optimization mode (none) and the decision mode (some T).Machine k q g over Fin (g+3) with tapes; input on tape 0 encoded by encodeInput (self-delimiting binary numbers), output read from tape 0 after halting. The time bound is with the encoded length.A complete development needs the combinatorics of the decomposition (separators and bounded global descriptions), a dynamic program over polynomially many descriptions, and its implementation and time analysis on the given Turing machine model. Contributions formalizing the purely combinatorial structure theorem, independently of the machine model, are welcome.
In the -server problem, labelled servers occupy points of a metric space, requests arrive online, and each request is served by moving one server onto it; the cost is the total distance moved, compared with the offline optimum through the competitive ratio. A companion OpenAI preprint claims that on every metric there exists a randomized policy with ratio against oblivious requests, matching the known worst-case lower bound. That result is an existence statement: it gives no procedure for computing the policy's probabilities.
This mission asks whether the bound can be realized by one uniform algorithm with explicit bit complexity on all finite rational metrics, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Fix and . A rational metric on is a table that is nonnegative, zero exactly on the diagonal, symmetric, and satisfies the triangle inequality. An initial labelled tuple may have repetitions. For a request word , is the algorithm's total movement and the minimum over all choices of serving labels with knowledge of . denotes the total binary length of the encoding of .
The computational model is a bit machine: a finite control with an input tape, finitely many work tapes over , an output channel, and one fresh unbiased random bit per step. At each request the input tape is replaced by the encoded request, the internal state is retained, and the output after the step budget names the server to move.
There are an absolute constant and a polynomial such that a single uniform randomized online algorithm, on every instance as above,
with independent of and of its length.
The result itself. It converts the existence theorem into an algorithm whose ratio is independent of , using only unbiased random bits and polynomial work per request in the input length and the bit length of the request counter. The price is an additive constant with no size bound: the algorithm may serve a very long initial stretch with a fixed label while its constructor runs. Coester and Cosson obtain stronger time and randomness guarantees but with ratio on general metrics; the two results are incomparable.
Formalizing it. The goal is stated in an explicit machine model, so a formal proof certifies both the competitive bound and the bit-complexity bound. It needs the companion existence theorem (Theorem 2.1 here, p. 4) as an input; a full development therefore also requires formalizing that theorem or taking it as a separate milestone. Exact rational linear algebra (Fourier–Motzkin elimination), dyadic rounding of probabilities, and step-counted machine simulation are reusable.
Knowing that a good policy exists does not give its probabilities, and a finite horizon alone does not control a long input on which the optimum barely moves. The preprint (pp. 3–4) solves a rational linear system for each horizon, then filters requests so that only those missed by some strongly lazy service with bounded moves are retained, which bounds the retained word length; a marking fallback pays for trajectories exceeding the move cap. The constructor's running time is uncontrolled, so the algorithm simulates it for only steps at request (Proposition 4.2, p. 14), and the delayed activation is absorbed into .
RationalMetric n is a Fin n → Fin n → ℚ table with the metric axioms; configurations are Fin k → Fin n; offlineCost is the sInf over label histories matching the request word (a finite, nonempty set of costs).BitMachine has finitely many controls and tapes and a transition consuming one coin per step. Preprocessing (boot) runs steps with all coins , so it is deterministic; this is satisfied by the source's deterministic constructor, and Theorem 1.1 does not require randomness there.requestBudget c e L t steps (Nat.clog 2 (t+1)) and must have yielded with output value for every reachable state and every coin string; requests are encoded by a fixed self-delimiting binary code.machineExpectedCost averages over all coin strings of the step budget, i.e. uniformly random bits; the bound is required for every request list w, with chosen after and before w.Multiplying two matrices by the schoolbook method costs about operations. The matrix-multiplication exponent of a field is the infimum of exponents such that matrices over can be multiplied with additions, subtractions and multiplications. It governs the asymptotic cost of a central bilinear operation and of the many algorithms built from it (determinants, inversion, linear systems). Bounding has driven algebraic complexity theory since 1969. In recent years the bounds have moved in the third and fourth decimal place, with each improvement coming from a finer analysis of the same tensor-power framework.
Fix a field . An arithmetic program is a straight-line sequence of gates, each a constant from , an input entry, or the sum, difference or product of two earlier gates. Its cost counts the addition, subtraction and multiplication gates. A program multiplies matrices if designated registers equal the entries of for every pair of input matrices over . A real number is admissible if for every there is such that for every some correct program has cost at most , and
In Lean this is MatrixAllFields.MatrixMultiplication.Arithmetic.omega F, defined for every F : Type u with [Field F].
The Lean statement also contains the numerical comparison , which carries no mathematical content (the source writes the comparison as ). This is Theorem 1.1 of the source. The goal is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. If the source's argument and certificate are correct, the theorem lowers the best stated bound on from (Dupont et al.) to , and it does so uniformly over all fields, with exact algorithms in every positive characteristic. Any improvement in lowers the exponent of every algorithm reducible to matrix multiplication. The method — pooling directional capacities across extraction depths and staggering lots so that one lot sits at each splitting stage — shows that combination losses in the asymmetric framework can be traded across depths.
Formalizing it. Bounds of this type rest on long chains of tensor-power constructions, recovery arguments and large rational parameter tables, checked in the source by an accompanying verifier with interval certificates for logarithms. A machine-checked proof would certify the whole chain from the arithmetic model to the final rational inequality. It would also give Mathlib the asymptotic sum inequality and Coppersmith–Winograd machinery, which every future bound on needs.
Every recent improvement fights extraction losses. Restricting a tensor power to a direct sum of independent matrix products wastes variables whenever whole blocks must be disjoint, while the final products only need disjoint subsets. Prescribed marginals may also allow several joint distributions. Earlier analyses take the minimum of three directional capacities separately at each depth, so a shortage on one side at one depth is lost. Using capacity across depths requires that variables deleted in earlier extractions (to resolve conflicts or impose type conditions) can still be recovered exactly, over the original field and with only subexponentially many extra copies. Positive characteristic rules out arguments that divide by small integers or rely on characteristic-zero identities.
F : Type u, with free constants from and unit cost for add, sub and mul. This matches the source's "scalar additions and multiplications".AdmissibleExponent F τ asks, for each , for one constant that works for every . omega F is the sInf of the admissible set, which is nonempty (schoolbook algorithm) and bounded below by the output size, so a junk value cannot make the strict inequality true.A projection game (label cover) asks for labels on the two sides of a bipartite multigraph so that, on each edge, the right label is the image of the left label under a prescribed map. In a 2-to-1 game the left alphabet has labels, the right alphabet , and every edge map has exactly two preimages of each right label. Khot introduced the 2-to-1 and Unique Games conjectures in 2002 (STOC 2002) as hypotheses that yield tight hardness of approximation. The 2-to-1 Games Conjecture with perfect completeness asserts that, for every fixed , it is NP-hard to tell satisfiable 2-to-1 games from games in which every labeling satisfies at most a fraction of edges. Perfect completeness matters for problems whose YES instances must be exactly satisfiable, such as graph coloring: hardness with completeness does not imply it.
This mission asks for a formal proof of the conjecture, as stated in an OpenAI preprint dated September 23, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
For an integer , a 2-to-1 instance has finite left and right vertex sets and a nonempty list of edge occurrences , where is given by an explicit table with for every . Parallel occurrences, possibly with different maps, are allowed and counted with multiplicity; there are no weights. A labeling assigns and and satisfies when . The value is the maximum, over labelings, of the fraction of satisfied occurrences. 3-SAT inputs are bit strings that decode to conjunctions of three-literal clauses (repetitions allowed); malformed inputs count as unsatisfiable.
For every fixed rational there are an integer and a deterministic polynomial-time reduction from 3-SAT to 2-to-1 instances with alphabets and such that
The running time is polynomial in the binary input length, with degree and constants depending only on .
The result itself. It removes the conditional hypothesis from perfect-completeness reductions. The preprint derives NP-hardness for maximum -colorable subgraph at soundness through Guruswami and Sinop's reduction (Corollary 1.2, p. 3), and recovers satisfiable Not-Two and three-query PCP hardness (Corollary 1.3, p. 4), the latter already known unconditionally by Håstad (SICOMP 2014). A companion preprint uses it for hardness of finding large independent sets in three-colorable graphs.
Formalizing it. No PCP-style hardness result of this strength has been machine-checked. A complete development needs a perfect-completeness PCP gap (Theorem 2.1, p. 5), projection-game parallel repetition (Theorem 2.2, p. 6), the Grassmann expansion theorem (Theorem 2.3, p. 7) and inverse shortcode estimates (Theorem 2.6, p. 9), on top of a polynomial-time Turing-machine framework. These components are shared with the Unique Games formalization and would be reusable.
Near-perfect completeness does not give perfect completeness: the reductions need not produce any finite satisfiable game. Amplifying a constant-soundness perfect-completeness game by parallel repetition destroys the 2-to-1 structure, since -fold repetition gives preimages per right label. The preprint therefore builds a new tree-structured construction (Section 3) whose joint-partition questions keep two-element fibers and satisfy exact identities, and the soundness analysis must decode labelings through a rank test whose tested rows depend on the decoded form itself (Sections 5–6), before projection-game repetition gives the contradiction (Section 7).
ProjectionTable q is a Vector (Fin q) (2*q) with exactly two preimages of every b : Fin q. Instance q lists edges as a List with a nonemptiness proof, so value = maxSatisfied / edges.length never divides by zero; maxSatisfied is a Finset.sup over all labelings.BinaryGapReduction δ fixes alphabet ≥ 2, a construct map, a Turing.TM2ComputableInPolyTime witness from raw input bits (identity encoding) to the explicit bit encoding gameBits, finite tape alphabets, completeness value = 1 on encodings of satisfiable formulas, and soundness value ≤ δ on all other inputs.value = 1 requires a labeling satisfying every edge.How densely can equal disks be packed in the plane? The hexagonal arrangement, with centers on the triangular lattice, covers a fraction of the plane, and Thue's theorem says no packing does better. In 2003 Cohn and Elkies introduced a linear programming bound for sphere packing: a single auxiliary function whose values are nonpositive outside a ball and whose Fourier transform is nonnegative certifies an upper bound on packing density. Viazovska (dimension 8) and Cohn, Kumar, Miller, Radchenko and Viazovska (dimension 24) found auxiliary functions for which the bound is sharp, solving sphere packing in those dimensions. Cohn and Elkies conjectured that a sharp function exists also in dimension 2 (Conjecture 7.3 of their paper). The planar packing problem itself is classical; the question here is whether the Fourier method certifies it exactly.
The source of this mission, an OpenAI preprint dated September 23, 2026, claims an explicit sharp planar certificate.
Scale disks to radius , so a packing is a set of centers with for distinct centers. The Fourier transform is
A Schwartz function is smooth with all derivatives decaying faster than any inverse power of . A function is radial if depends only on ; for real radial integrable , is real and radial. The Cohn–Elkies theorem says that if is admissible, for and , then every packing of radius- disks has density at most .
There is a real radial Schwartz function with
Lean: OAI.sharp_fourier_certificate, open on the platform.
With the Cohn–Elkies bound equals , the hexagonal density, so the theorem answers the two-dimensional case of Cohn–Elkies Conjecture 7.3 affirmatively and gives a Fourier-analytic proof of Thue's theorem for arbitrary (not only periodic) packings. Its zero structure also recovers uniqueness of the triangular lattice among periodic optimal packings. The certificate does not satisfy the additional zero-set requirement of Cohn–Elkies Conjecture 8.1, which remains a separate question. The construction methods feed into the companion work on universal optimality of the triangular lattice in the same family. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists. By contrast, Viazovska's dimension-8 theorem has been the subject of formalization efforts, so a planar certificate would be a natural low-dimensional companion.
In dimensions 8 and 24 the magic functions come from modular forms, whose symmetries control a function and its Fourier transform at once. No such modular construction is known to produce the planar certificate, and Sardari's nonuniqueness theorem shows that prescribing values and derivatives on the lattice shells does not pin a function down. Numerical Laguerre–Gaussian searches (Cohn–Elkies) approach the bound but do not attain it. The hard part is an exact construction together with rigorous sign control of both (for ) and (everywhere), including between interpolation nodes and in the tails.
EuclideanSpace ℝ (Fin 2); the function is a SchwartzMap Plane ℝ.SharpPlanar.fourier f ξ is the Bochner integral of ; for a Schwartz function it is the usual transform.SharpCertificate f: Radial f, fourier f 0 = 1, f 0 = 2 / √3, for every ξ the transform has zero imaginary part and nonnegative real part, and f x ≤ 0 when 1 ≤ ‖x‖.A complete development needs Fourier transforms of radial functions in the plane (Hankel transforms, Gaussian pairings) and rigorous interval or Bernstein-polynomial sign certification. Formalizing the Cohn–Elkies bound itself (certificate implies density bound) would be a valuable reusable companion. Contributions formalizing Proposition 2.2, Proposition 3.4 or Proposition 4.3 are welcome.
Which arrangement of points in the plane minimizes interaction energy? For many repulsive interactions the expected answer is the triangular (hexagonal) lattice. Universal optimality, formulated by Cohn and Kumar (2007, doi:10.1090/S0894-0347-06-00546-7), asks for a single configuration that minimizes energy simultaneously for every completely monotone potential of squared distance, which includes all Gaussians and all inverse powers. It was proved in dimensions 8 and 24 for and the Leech lattice; in dimension two it was a conjecture. The question matters in mathematical physics (crystallization, vortex lattices, Coulomb and Riesz gases) and in the theory of Fourier interpolation.
The source of this mission, an OpenAI preprint dated September 26, 2026, claims the full planar statement against all locally finite configurations of density one. A companion OpenAI preprint reaches the same energy conclusion by a different (modulo-12) interpolation construction.
Let and , the triangular lattice of covolume one. Let be the closed disk of radius about the origin. A set is locally finite if each is finite, and has centered disk density one if , where .
A smooth is completely monotone if for all , . The lower energy per particle is
summing over ordered pairs. The Fourier transform is and is the dual lattice.
For every there is a real radial Schwartz with
given for by the paper's explicit atomic interpolation construction.
For every smooth nonnegative completely monotone and every locally finite of centered disk density one,
Lean: OAI.AtomicTriangular.universal_energy_minimum, open on the platform.
Theorem 1.1 would settle the planar case of the Cohn–Kumar universal-optimality conjecture in a density-based competitor class with no periodicity or perturbation assumption, for every completely monotone potential including those (such as with ) whose lattice sums diverge. By Bernstein's theorem such potentials are mixtures of Gaussians, so the sharp Gaussian certificates of Theorem 1.2 are the analytic core. The theorem identifies the minimum value; it does not classify minimizers. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists. A formalization would also produce reusable Fourier-analytic tools in Lean (Poisson summation for lattices, linear-programming energy bounds).
Lattice-restricted results (Rankin, Montgomery) compare only lattices; a competitor here may be nonperiodic, have arbitrarily close pairs, and have large local clustering. The Fourier linear-programming method handles general competitors but needs, for each Gaussian, an auxiliary function that is simultaneously a pointwise minorant, has nonnegative Fourier transform, and is sharp: it must touch the Gaussian on every lattice shell and its transform must vanish on every dual shell. Constructing such functions for all at once, with rigorous sign control between the interpolation nodes, is the central obstacle. A second issue is passing from the density hypothesis alone (no averaging over translates) to the energy inequality.
EuclideanSpace ℝ (Fin 2); A is Set.range triangularPoint.AdmissiblePotential g: ContDiffOn ℝ ⊤ g (Ioi 0), and iteratedDeriv r g t for .energy g C is the liminf over of diskEnergy, valued in ℝ≥0∞; latticeEnergy g is a tsum in ℝ≥0∞, so divergent sums are allowed and no summability hypothesis is needed.C and the equality latticeEnergy g = energy g A.realFourier is Mathlib's 𝓕 (kernel ) applied to the complexified function; the clause names the paper's explicit coefficients (R, R0, Yf, Uplus, Uminus) and error bounds.Contributions formalizing Lemma 2.1 (reciprocal Gaussian parameters), Proposition 2.3 (density-only linear programming), Lemma 4.1 (finite certificate) and Proposition 5.1 (exact interpolation and approximation) are welcome.
Seshadri constants measure the local positivity of a line bundle at a point or a configuration of points: how much of an ample class survives after blowing up the points and subtracting equal multiples of the exceptional curves. For points on a surface with ample , a dimension count gives the universal upper bound . Nagata's 1959 conjecture, which came out of his counterexample to Hilbert's fourteenth problem, says that this bound is attained at very general points of the projective plane. On an arbitrary polarized surface, the qualitative Nagata–Biran(–Szemberg) conjecture predicts that the bound is attained at very general points for every sufficiently large . On the symplectic side, the conjecture corresponds to packing stability: large numbers of equal balls fill a four-manifold.
Let be a smooth integral complex projective surface and an ample line bundle, with self-intersection . For a tuple of distinct points, the multipoint Seshadri constant is
the infimum over integral curves through at least one . If is the blow-up at with exceptional curves , then is the largest such that is nef (nonnegative on every integral curve), and always . Let be the set of tuples of distinct points. A property holds at very general tuples if it fails only on a countable union of proper Zariski-closed subsets of .
For every such there is such that for each there is a countable union of proper Zariski-closed subsets of , with , such that for every
The threshold may depend on and is not explicit. The goal statement is published on the platform with status Open.
The result itself. Theorem 1.1 settles the qualitative Nagata–Biran conjecture for all polarized complex surfaces, with no assumption that is a square or that a plane constant is maximal (the hypotheses needed by Harbourne, Roé and Roé–Ross). Because the conclusion is nefness of the square-zero boundary class, it rules out every curve whose degree-to-multiplicity ratio is below , including curves with unequal multiplicities. Via Eckl's Kähler packing correspondence, it gives the algebraic counterpart of packing stability. The sharp plane case ( in ) is a separate companion result.
Formalizing it. The statement is built from scheme-theoretic foundations: projective surfaces, line bundles, sheaf cohomology, blow-ups by universal property, intersection numbers through Euler characteristics. A complete proof would be among the first machine-checked results about the birational geometry of surfaces. Much of the required infrastructure, such as Riemann–Roch on surfaces, finite-dimensionality of coherent cohomology and the existence of blow-ups, is not yet in Mathlib.
The upper bound is an elementary jet count. Equality requires showing that no curve on the surface has too large multiplicity at the chosen points, for all multiplicity orders simultaneously. Degenerating the points to a special configuration, the usual approach in the plane, fails because the threshold in must be uniform in the jet order: the asymptotic interpolation theorems (Alexander–Hirschowitz) give thresholds depending on a fixed multiplicity bound. Arbitrary surfaces also lack the toric coordinates available on . The source transfers the problem to finite interpolation on an algebraic torus through a nodal divisor in .
Surface: an integral scheme, smooth of relative dimension over , with a closed immersion into some compatible with the structure maps. LineBundle: a locally free sheaf of rank one. IsAmple: the nonvanishing loci of sections of positive powers that are affine form a neighbourhood basis.Ext^n(𝒪, M) in the category of sheaves of modules, and dimensions are finrank ℂ. Then and , by Riemann–Roch. If cohomology were infinite-dimensional, finrank would return ; finite-dimensionality for projective schemes is part of what a solver must prove.IsClosed, ≠ univ, with a point outside all of them).sInf over integral curves with positive total multiplicity.PointBlowup, characterized by its universal property, and the exceptional ideal sheaves . The inequality is for every integral curve on the blow-up.Euler's totient counts the integers in coprime to . Many integers share a totient, and most integers are not totients at all, so counting the distinct values of is much harder than counting integers with a given factorization. Let
The size of was studied by Pillai, Erdős, Hall, Pomerance, Maier and Ford over most of the twentieth century; Ford's 1998 estimate determines up to a bounded multiplicative factor but leaves open whether has an asymptotic equivalent, and Erdős and Hall's question whether .
This mission asks for a formal proof of the explicit asymptotic formula and the Erdős–Hall regular-variation property, as stated in an OpenAI preprint dated September 25, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Logarithms are natural and is the -fold iterate. For let , let be the unique root of , and set
For large put , , the phase , and ; the factor is Ford's counting scale.
For each the preprint defines an explicit arithmetic coefficient , , from a finite set of "tail witnesses" (tuples of primes , , and a cofactor , subject to explicit size and recurrence constraints, ) by inclusion–exclusion over witnesses with a common totient , weighted by (formula (2.8), p. 5). Here is the least preimage, and when the limit exists. The coefficient is defined without reference to .
for .
uniformly on , with , and
For let and . Then converges uniformly and ; if some totient has then and , and otherwise and . The positive alternative holds for .
The result itself. The formula replaces Ford's bounded uncertainty by an explicit function of the phase , built from finite arithmetic data, and answers the Erdős–Hall question: is regularly varying of index . Theorem 2.2 answers, in weighted form, Erdős's question on how least preimages are distributed in intervals , reducing it to the existence of a "seed" totient with . Whether such seeds exist for every (equivalently, whether is unbounded) is not settled by the preprint.
Formalizing it. This is analytic number theory at full strength: Ford's structure theorems for totient preimages, sieve bounds for two or three linear forms in shifted primes, simplex volume computations and an inclusion–exclusion limit. Mathlib has the totient and the prime number theorem in some forms but not these sieve and distribution results. The definitions in this mission (the renewal root , the witnesses, ) are explicit and can be checked independently of any proof.
Counting integers with a typical factorization is a volume computation, but counts values, and different can have the same totient. The preprint must show that, outside a negligible set, distinct long prime prefixes give distinct values (Proposition 5.1, p. 22, and Proposition 5.3, p. 27), which needs a uniform comparison estimate for products of shifted primes (Proposition 4.2, p. 17), while short discrete tails that may collide are kept exactly and handled by inclusion–exclusion (Lemma 6.4, p. 30). The limits are taken in a specific order ( with fixed, then ), and no continuity of is available, so all errors must be uniform in the phase.
IsTotient v means for some ; V x counts totients in ; ell v is Nat.find of the least preimage (junk value for non-totients, never used on them).rho is the sInf of roots in of ; the root is unique, so this is the source's .AH H f s is formula (2.8) with finsum over totients and over nonempty finite sets of witnesses with ; the witness set is finite for each , so the finsums are genuine finite sums. A f s is limUnder atTop; the goal asserts uniform convergence, so the junk value is never used.mainTerm x = x / log x * G x (m x) * A 1 (theta x); asymptotic equivalence is Tendsto (V x / mainTerm x) atTop (𝓝 1).coefficient_nonnegative is stated for every , while the source states it for sufficiently large ; for small the witness set is empty or the inclusion–exclusion is still a probability, so this is a harmless strengthening.companion_zero_case restates alternative (ii) of Theorem 2.2 in a separate definition file (TotientCompanionZero) with identical definitions.For a positive integer , Jacobsthal's function is the least such that every run of consecutive integers contains an integer coprime to . Equivalently, is the longest interval that can be covered by choosing one residue class modulo each prime divisor of (the classes shifted by the interval's start). Its maximum over integers with at most prime divisors,
governs how long a stretch can be sieved out by primes. It is linked to gaps between consecutive primes (long covered intervals produce large prime gaps, as in the Erdős–Rankin and Ford–Green–Konyagin–Maynard–Tao constructions) and to the limits of the linear sieve. Jacobsthal asked, and Erdős recorded, whether .
The source of this mission is an OpenAI preprint dated September 25, 2026.
Both are stated in Lean as the existence, for each , of a length satisfying IsJacobsthalBound k m with the displayed size bound. The goal OAI.Erdos970.Erdos970Final.erdos_970_iterated_log is open on the platform.
Theorem 1.1 answers Jacobsthal's question affirmatively, uniformly over all prime sets and interval positions, and removes the logarithmic losses in the bounds of Vaughan and Iwaniec, going slightly below the quadratic scale. It shows that the linear sieve can be pushed to its limiting parameter , where the lower sieve function vanishes, by retaining a boundary contribution. The gap to the best lower bound (roughly ) remains large; Vaughan suggested .
The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists. The constant is not made explicit.
The linear sieve gives a lower bound for the number of uncovered integers only when the sieving range is below the square root of the interval length, which is exactly where the exponent 2 comes from; at the critical parameter the main term of the lower-bound sieve vanishes, so the standard argument yields nothing and a loss appears. One must keep the boundary term that the leading linear-sieve calculation discards, and then show that the actual prescribed residue classes do not deviate much from a reference calculation. Positivity of the reference calculation alone does not suffice: the comparison requires an inverse estimate for a witnessing edge of a decreasing-prime tree, variance bounds, and stopping-time counts for hard endpoints.
IsJacobsthalBound k m: for every n : ℕ with 0 < n and n.primeFactors.card ≤ k, and every a : ℤ, some i < m has (a + i).natAbs.Coprime n.JacobsthalQuadratic: ∃ C > 0, ∀ k > 0, ∃ m, IsJacobsthalBound k m ∧ m ≤ C k^2.JacobsthalIteratedLog: the same with bound C k^2 / (log (log (3k)))^2; for the denominator is positive.IsJacobsthalBound identically.A complete development needs the fundamental lemma of the sieve, Buchstab-type functions of the linear sieve, prime number theorem estimates in short ranges and progressions, the additive large sieve, a lattice-point count on plane curves, and renewal-type arguments for a continuous path process. Contributions formalizing Theorem 1.2 (the quantitative covering estimate), Lemma 2.1 (fundamental lemma of the sieve), Proposition 6.3 (positive reference margin), Proposition 8.2 (inverse estimate for an edge) and Corollary 9.3 are welcome.
Large service systems such as call centers and hospital wards are modelled as many-server queues: identical servers, customers arriving according to a general process, service requirements drawn independently from a general distribution , and a single first-come-first-served queue. When is not exponential the number of customers in system is not Markov, and a tractable state must keep track of how long each customer in service has been served. Kaspi and Ramanan (Ann. Appl. Probab. 21 (2011)) take as state the number in system together with the age measure, the point measure of the ages of the customers in service, and prove a functional law of large numbers: scaled by , these processes converge to the unique solution of a deterministic system, the fluid equations. Earlier fluid and diffusion analyses of the queue worked with other state descriptors (Reed, Ann. Appl. Probab. 19 (2009); Whitt, Oper. Res. 54 (2006)); the measure-valued description records the elapsed service time of every customer in service, which is the information a non-exponential service distribution requires.
This mission covers the deterministic half of that result: the fluid equations are well posed, and their solution is given in closed form.
Service requirements have a density that vanishes on , , and the mean is normalized to one, . Let and let be the hazard rate on ; is locally integrable on but not integrable on it. For a measure and a function write , and for the constant one.
The data are a triple in
where is the cumulative arrival process, the initial number in system and the initial age measure (per server, so the total capacity is one). A càdlàg pair , with a sub-probability measure on in the weak topology, solves the fluid equations if for every : (3.4); for every test function
(3.6); and the nonidling condition (3.7). Here is the cumulative departure process and the cumulative entry into service. Equation (3.5) is a weak form of a transport equation: mass moves to the right at unit speed, is killed at rate , and enters at age at rate .
For every :
Uniqueness of the fluid solution is what turns tightness of the scaled -server processes into convergence: every subsequential limit solves the fluid equations, so all coincide (the paper's Theorem 3.7). The representation (3.11) reduces the measure-valued equation to the scalar process , and the continuity estimate of Theorem 4.6 says the fluid solution is a Lipschitz function of the arrival process. Both are used in the paper's study of long-time behaviour, where converges to the measure with density , and (3.12) is the form of the entry rate used there.
The results are proved in the paper. None of them, and no part of the measure-valued fluid model, has a machine-checked proof. Formalizing them produces a checked weak-solution theory for a transport equation with an unbounded killing rate and a measure-valued boundary input, which is a reusable piece of infrastructure for other age- and residual-time-based queueing models.
The central step is Theorem 4.1. The naive approach treats (4.2) as a first-order PDE and integrates along characteristics, but the solution is only a càdlàg path of measures, is merely locally integrable and blows up near , and may jump, so classical characteristics are not available; the test functions must not vanish on the boundary , since that is where the entry term lives. The second difficulty is in Theorem 4.6: the entry process is defined implicitly through the nonidling condition, and comparing two solutions requires a first-crossing argument that distinguishes whether the system is below, at or above capacity at that time.
The service law is its density (ServiceLaw), with below , and mean one. Time is read on ; every condition is stated for . Measures of the fluid model are FiniteMeasure ℝ carried by , whose topology is weak convergence, so càdlàg paths are càdlàg in with the weak topology. The paths of Theorem 4.1 and Lemma 4.5 are ℝ → Measure ℝ with values Radon on (possibly infinite) and càdlàg in the vague topology. is an extended number. The integral in (3.4) is a lower integral in , and , are its real value. is the Lebesgue–Stieltjes measure of , with no atom at . A function of bounded variation is a difference of nondecreasing càdlàg functions vanishing at .
Explicit choices: compact support of test functions is relative to , so need not vanish (with supports taken in the entry term of (3.5) would vanish identically); and equal to the datum are clauses of the fluid equations, but not of the age equation, where is arbitrary; functions in , and are represented by functions on of the same class, of which only values on are read; norms in Lemma 4.5 are computed in , since may be infinite. Two printed statements are corrected: in Theorem 3.5 the paper's right-hand side of the equivalence lists (3.6) and (3.11); the nonidling condition (3.7), part of the fluid equations on the left, is kept on the right, as the proof requires. In (4.10), is replaced by , which is what Lemma 4.5 and (4.9) give.
A fluid solution is defined by the weak transport equation (3.5), never by the representation (3.11) or by a formula for in terms of ; with such a definition the equivalence of the goal would be an unfolding of definitions.
A complete development needs Lebesgue–Stieltjes integration by parts for càdlàg functions of bounded variation, the Riesz description of the vague topology, and uniqueness for weak solutions of transport equations; these are reusable beyond this mission. Proofs of any milestone, and of the parts of Theorem 3.5 separately, are welcome. The paper's Section 4.3 machinery (the abstract and simplified age equations, Lemmas 4.12–4.13, Propositions 4.15–4.16) is not posed here and may be formalized as supporting lemmas.
A random conductance model puts a random conductivity on every edge of the lattice . It is the simplest discrete model of diffusion in a heterogeneous medium, and its generator is the generator of a random walk in a random environment. Classical stochastic homogenization shows that on large scales the random operator behaves like a constant-coefficient elliptic operator whose homogenized coefficient is deterministic. The characterization of , however, involves an equation on the whole lattice for every realization of the coefficients. In practice one computes a spatial average over a box of size of the energy density of an approximate corrector, as in Gloria and Otto (arXiv:1104.1291, §1). The random part of the error of this procedure is a variance. Its size as a function of determines how large a computational box must be.
Timeline:
Fix and . Sites are and is the canonical basis. An edge carries a conductivity ; such a field belongs to the class . The discrete gradients are and , and .
The conductivities are i.i.d.: they are distributed according to the product over all edges of one probability law on . No density is assumed, so atomic laws are allowed. is the expectation and the variance.
For a direction with and a cut-off , the approximate corrector solves
The zero-order term introduces the length scale . The Green's function is the solution of in weak form.
A mask is supported in the box , sums to and satisfies . The averaged energy density is
There are an exponent and a threshold , depending only on , and for each mask constant a constant , such that for every law on , every unit , every , every and every mask :
The statement fixes the shape of the bound, not the value of or , which is why it is the goal.
The milestones follow the paper's proof:
The result. The estimate says that smooth averages of the energy density fluctuate as if the density were independent from site to site, at the rate . That rate is the best possible, since the coefficients themselves are independent. In the error analysis of approximations of , this controls the random error and separates it from the systematic error caused by the cut-off . Proposition 2.1, a byproduct, shows that the approximate corrector has all moments bounded uniformly in when , which yields a stationary corrector (Corollary 2.1 of the paper).
Formalizing it. The theorem has been proved since 2011, and no machine-checked version is known. A formal proof would combine three components that are reusable well beyond this paper:
The obvious argument fails because the energy density is not independent from site to site: the corrector couples all conductivities through the inverse of a random elliptic operator. Bounding the variance needs the sensitivity of to each single conductivity, and that sensitivity is expressed through gradients of the Green's function. Pointwise bounds on that are uniform in the coefficients do not exist: the continuum counterpart fails, by examples from quasi-conformal mappings. Only averaged decay on dyadic annuli and a small gain of integrability are available, which is why the proof needs the moment bounds of Proposition 2.1. In the Green's function does not decay, so only BMO-type control is available, and a logarithm of is lost.
Statements follow the arXiv v1 reprint (arXiv:1104.1291v1) of the Annals of Probability article; theorem and page numbers refer to it.
Fin d → ℤ. An edge is the pair (z, i), and a coefficient field is a real function on edges; the theorems assume it takes values in .Measure.infinitePi of one probability measure on with .Ruling out a trivial formalization. If the constant were allowed to depend on the law or on the mask, the goal would follow from the boundedness of the energy average alone. If the variance were taken of a function that is not square-integrable, it would be by convention. The goal fixes before and and requires square-integrability as part of the conclusion.
Not formalized:
Welcome contributions are proofs of any milestone and reusable infrastructure: infinite-product variance inequalities, discrete integration by parts, and discrete maximum principles.