Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
The Johnson–Lindenstrauss lemma (1984) says that any points of a Hilbert space can be placed in -dimensional Euclidean space with distortion at most any prescribed . This dimension reduction is used throughout analysis, geometry and algorithm design. Johnson and Lindenstrauss also asked what analogues hold in other Banach spaces. For the spaces with the question splits into several versions: whether one needs the map to be linear, whether one discretizes a whole subspace or only a finite set, and whether the target is a coordinate space with the same exponent. This mission concerns the finite-set, coordinate-target, nonlinear version: how many coordinates are needed so that every -point subset of embeds into with distortion at most ?
The source of this mission, an OpenAI preprint dated September 23, 2026, claims that for every fixed , , and the dimension is .
All spaces are real. Fix , an integer and . Let be the least integer such that for every measure space and every distinct points there are and a scale with
The map is arbitrary, not required to be linear. Put
For fixed , :
Since , the upper bound is . The Lean statement OAI.SubpolynomialLp.source_main is open on the platform.
For the best previous finite-set bounds were polynomial in (linear for ), and for logarithmic dimension is impossible. The theorem places at for every fixed , in contrast with exact embeddings, where the dimension is of order . Thus the exponent jumps from at to for every . The upper exponent and the logarithmic lower bound are not claimed to be optimal. The theorem is existential; no embedding algorithm is asserted.
The result is claimed in an OpenAI preprint and has not been peer reviewed; no machine-checked proof exists. A formal proof would include a probabilistic construction (stable laws, Poisson sampling, Rosenthal-type moment inequalities), an electrical-flow localization estimate, and a convex-separation argument.
Linear maps cannot work: fixed-distortion linear maps on some configurations need dimension proportional to when . Subspace discretization theorems apply to the span of the points, which has dimension up to , so they also give only polynomial bounds. The Johnson–Lindenstrauss approach relies on Gaussian rotation invariance, which has no analogue in . One needs a single random scalar map whose increments have nearly equal normalized -th moments simultaneously for all pairs, with relative (not additive) error control.
coordinateDistance p y z is on Fin d → ℝ.GoodDimension p n D d quantifies over every measure space (Ω, mΩ, μ) in a fixed universe and every injective x : Fin n → Lp ℝ (ENNReal.ofReal p) μ; the target is Fin d → ℝ with the distance and a scale .dimension p n D is the sInf of the good dimensions in ℕ. The goal also asserts that this infimum is good, so the default value of sInf ∅ cannot make the bounds trivial.gamma p is as above; the exact-embedding lower bound uses natural-number division, i.e. the floor.Tendsto statement along n : ℕ for each .A complete development needs spaces, -stable random variables, Poisson sampling and moment inequalities, effective resistance and electrical flows on complete graphs, and Carathéodory's theorem for the exact-embedding upper bound. Contributions formalizing the exact-embedding bounds (Ball's upper bound and the antipodal lower bound) and the weighted moment criterion are welcome.
The Brunn–Minkowski inequality is a cornerstone of convex geometry, with consequences ranging from the isoperimetric inequality to concentration of measure. The Brunn–Minkowski theory of Firey and Lutwak replaces the Minkowski combination, whose support function is , by a -mean of support functions. As the -mean becomes the geometric mean , giving the logarithmic combination of two bodies. In 2012 Böröczky, Lutwak, Yang and Zhang conjectured that, for origin-symmetric convex bodies, the logarithmic combination already satisfies the multiplicative Brunn–Minkowski bound. This would be a strict strengthening of the classical inequality in the symmetric case. The conjecture is equivalent to a logarithmic Minkowski inequality for cone-volume measures and, by work of Saroglou, implies the (B)-conjecture for even log-concave measures. Symmetry is essential: the inequality fails for general bodies.
A convex body is a compact convex set with nonempty interior; it is origin-symmetric if , in which case is an interior point. Its support function is
which is strictly positive for origin-symmetric bodies. For a positive function on the sphere, the Wulff body is
The logarithmic combination of with parameter is . In general is not itself a support function, which is why the Wulff body is needed. denotes Lebesgue measure.
For , origin-symmetric convex bodies and ,
The goal statement is published on the platform with status Open.
The result itself. By the arithmetic–geometric mean inequality, , so the theorem strengthens the multiplicative Brunn–Minkowski inequality for symmetric bodies. It implies the symmetric Brunn–Minkowski inequality for every (Corollary 1.2 of the source), the logarithmic Minkowski inequality for cone-volume measures, and, through Saroglou's transfer, the (B)-conjecture: is log-concave for every even log-concave measure and origin-symmetric convex body (Corollary 8.1 of the source).
Formalizing it. The statement uses only Euclidean space, support functions and Lebesgue measure, all in Mathlib. The proof uses smooth approximation of polytopes, moment coordinates, a variance bound and a tensor estimate. A formal proof would put a long-standing conjecture of convex geometry on a machine-checked footing; Mathlib does not yet contain the classical Brunn–Minkowski inequality in this generality, and that would be a natural reusable milestone.
The classical proofs of Brunn–Minkowski (Prékopa–Leindler, mass transport) apply to Minkowski sums, but the logarithmic combination is not a Minkowski sum and is not a support function, so these tools give only the weaker inclusion bound. Local (second-variation) approaches reduce the problem to a spectral gap for the Hilbert–Brunn–Minkowski operator on even functions, but local-to-global arguments had only been completed near the ball, for zonoids, or under extra symmetry. Without symmetry the inequality is false, so any argument must use the evenness of the bodies.
EuclideanSpace ℝ (Fin n) with ; convex bodies are compact, convex, with nonempty interior; symmetry is x ∈ K ↔ -x ∈ K.sSup of over , nonempty and bounded for a convex body, so it is the true maximum. Real powers rpow are applied to positive support values (positivity follows from symmetry and nonempty interior).volume in ℝ≥0∞, with ℝ≥0∞-valued powers and . At the inequality reduces to (resp. ), so the edge cases are consistent.A finite metric embeds into exactly when it is a nonnegative combination of cut metrics . This makes distortion the right measure for the flow–cut gap: given edge capacities and pairwise demands, the ratio between the sparsest cut value and the maximum concurrent flow . Linial, London and Rabinovich (1995) and Aumann and Rabani (1998) developed this connection, and Gupta, Newman, Rabinovich and Sinclair (2004) proved that the worst flow–cut gap on a fixed graph equals the worst distortion of its weighted shortest-path metrics. They conjectured that every proper minor-closed family embeds into with uniformly bounded distortion (the GNRS conjecture). Graphs of bounded treewidth form one of its basic cases.
Let be a finite connected graph with edge lengths . The shortest-path metric is the least total length of a path from to .
A tree decomposition of is a finite tree with bags () such that the bags cover , each edge has both endpoints in some bag, and for each vertex the nodes whose bag contains induce a connected subtree. In this mission, as in the source, bounds the bag cardinality , so the treewidth bound is .
A map has distortion at most if .
For every integer there is a constant such that for every nonempty finite connected graph with a tree decomposition of bag size at most and every , there are and with
is independent of the number of vertices, the decomposition and all ratios of edge lengths; the goal asserts only its existence. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. The theorem settles the bounded-treewidth case of the GNRS conjecture. Through the GNRS equivalence, it gives for every multicommodity instance on graphs of treewidth less than . By the Robertson–Seymour excluded-planar-minor theorem it also covers every family excluding a fixed planar minor. Combined with known approximation algorithms for the minimum distortion (Gupta–Talwar–Witmer 2013; Cohen-Addad–Mömke–Verdugo 2024), it yields fixed-parameter-time embeddings of distortion . With the planar companion preprint it covers the almost-embeddable families of Lee and Sidiropoulos.
Formalizing it. The proof constructs cut measures directly on a tree decomposition and combines them with padded random partitions from the literature. A formal proof would certify that the constants depend only on , the point at which earlier approaches lost uniformity.
The successful pathwidth approach embeds the graph stochastically into dominating trees, but that route cannot work here: some series-parallel metrics require expected tree distortion (GNRS 2004, Theorem 5.6). Local-consistency approaches assume that small vertex sets admit compatible isometric cut representations, which a general bounded-treewidth metric need not provide. Multiscale constructions from padded partitions give good separation at each scale, but summing their contributions loses a factor growing with the number of scales. The construction must handle arbitrary branching of the decomposition tree and arbitrary edge-length ratios without such accumulation.
V is any nonempty Fintype with decidable equality; G : SimpleGraph V is connected.HasTreeDecomposition G k: a tree T on Fin n, bags Fin n → Finset V covering all vertices and all edges, with the bags containing each vertex inducing a connected subgraph of T, and all bags of cardinality at most k.ℓ : G.edgeSet → ℝ, strictly positive. shortestPathDistance is the sInf of lengths of paths (IsPath) from to ; this set is finite and nonempty for a connected finite graph, so the infimum is the true distance.PiLp 1 (Fin m → ℝ) with chosen per graph; this is the source's remark (p. 2) that the target can be taken to be finite-dimensional , and it is at least as strong as an target.C depends only on k and is quantified before the graph.A finite metric space embeds into exactly when its metric is a nonnegative combination of cut metrics . For this reason the least distortion with which a graph metric embeds into governs the gap between multicommodity flow and sparsest cut: Linial, London and Rabinovich (1995) and Aumann and Rabani (1998) connected metric embeddings to the approximate max-flow/min-cut theorem, and Gupta, Newman, Rabinovich and Sinclair (2004) proved that the worst flow–cut gap on a fixed graph equals the worst distortion of its weighted shortest-path metrics. They conjectured (the GNRS conjecture) that every proper minor-closed graph family embeds into with uniformly bounded distortion. The planar case has been the central open instance.
Let be a finite connected simple graph on vertex set with symmetric edge lengths on edges. The graph metric is the infimum of over walks from to . is planar if it has a drawing in : distinct points for vertices and, for each edge, an injective arc between its endpoints whose interior avoids every vertex and meets the interior of no other edge.
A map into the real space of some measure space has distortion at most if for all .
There is a constant such that for every , every connected planar graph on vertices and every symmetric positive edge-length function , there are a measure space and with
The constant is not fixed: the goal asserts only existence, so any improvement of the constant is compatible with it. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. The theorem settles the planar case of the GNRS conjecture. By the Gupta–Newman–Rabinovich–Sinclair equivalence it gives a universal constant bound on the fractional flow–cut gap for arbitrary demands in planar graphs. With the bounded-treewidth companion preprint it also yields constant distortion for the fixed-parameter almost-embeddable families of Lee and Sidiropoulos (Corollary 10.1 of the source). The general clique-sum closure needed for the full GNRS conjecture is not established.
Formalizing it. The statement is elementary (finite graphs, arcs in the plane, an space), yet the proof combines a geometric column model of planar graphs, random multiscale cut constructions and packing estimates. A formal proof would certify every scale-combination step, where errors in uniformity are easy to make.
Standard random-partition methods for planar graphs separate pairs at each distance scale with good probability, but naive summation over scales costs a factor proportional to the number of scales, which is unbounded when edge lengths vary. Embedding first into Euclidean space cannot work: Newman–Rabinovich show Euclidean distortion is necessary already for series-parallel graphs. The difficulty is to combine separations at different scales while keeping a single uniform upper bound on every edge.
Fin n; the graph is a SimpleGraph (Fin n) with G.Connected (so ). Singletons are allowed.IsPlanar G asks for an injective vertex placement in ℝ × ℝ and, for each ordered adjacent pair, an injective continuous arc on the unit interval with the right endpoints, whose interior avoids all vertex points and meets the interior of another arc only if it is the same unoriented edge.Fin n → Fin n → ℝ, symmetric, and positive on adjacent pairs; values on non-adjacent pairs are irrelevant. graphDistance is the sInf of walk lengths; for a connected graph with nonnegative edge lengths the set of walk lengths is nonempty and bounded below, so the infimum is the genuine shortest-path distance.MeasureTheory.Lp Ω ℝ 1 μ for an existentially chosen measure space, and the inequalities are stated without a rescaling factor (the rescaling is absorbed into ).The projection body of a convex body is the convex body whose support function in a unit direction is the -dimensional volume of the shadow of on . Petty showed that is affinely covariant, so the normalized volume
is invariant under invertible affine maps, and its extremal values are natural affine isoperimetric questions. Petty's conjecture concerns the minimum (ellipsoids). For the maximum, Brannen conjectured in 1996 that simplices maximize among all convex bodies (Mathematika 1996); the simplex value is .
This mission asks for a formal proof of an explicit counterexample in dimension , 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.
A convex body in is compact and convex with nonempty interior, and is -dimensional volume. For the brightness is , and
Let be the standard simplex and
The benchmark constant is , which equals of every -simplex (Proposition 5, p. 4).
It is not true that for every convex body .
is a convex body and
The result itself. Brannen's conjecture fails: in dimension the simplex is not the maximizer of normalized projection-body volume. The mechanism is the product identity for polytopes (Proposition 3, p. 3), which shows that is a lower bound for any universal upper constant in dimension ; iterating it gives an exponential excess for all large (Corollary 6, p. 6). The counterexample in dimensions was obtained independently by Feng, Hu, Liu and Xu; the contribution here is an explicit product witness with an exact rational value. The optimal upper constant and its maximizers remain separate questions.
Formalizing it. Every ingredient is elementary: the facet formula for projection bodies of polytopes (Cauchy's formula, Lemma 2, p. 2), the facet structure of a Cartesian product, affine covariance (Lemma 4, p. 3), and a fiber computation of . A formal proof would supply Mathlib with projection bodies of polytopes and Cauchy's projection formula, both reusable. The final comparison is an exact rational identity.
There is no shortcut through general inequalities: the statement is a strict comparison of two explicit volumes in dimension , so both and must be computed exactly. Computing of a product directly from shadow volumes is unwieldy; the efficient route goes through facet area-normal vectors, which requires proving that, up to a null set, each point of a shadow lies over exactly two facet interiors, and that the facets of are exactly and . The simplex value needs the volume of a cube plus a segment.
EuclideanSpace ℝ (Fin 20). In the goal, projectionVolume is the induced Lebesgue measure on the submodule of the orthogonal projection of ; brightness u = ‖u‖ * projectionVolume, so the support-function inequality is imposed for all (the homogeneous extension).productWitness is the set of whose first and last ten coordinates both lie in standardSimplex 10; the goal includes that it is compact, convex, with nonempty interior.simplexConstant 20 is the explicit number , not ; the goal states the exact ratio, its reduced fraction, the strict inequality, and .euclideanHausdorffMeasure (d-1) of the image under the orthogonal projection, and compares with ratio (simplex 20), so it implicitly needs Proposition 5.toReal; all bodies involved are bounded, so no infinite value is hidden.The projection body of a convex body packages the areas of all shadows of into a single convex body: its support function in direction is the -dimensional volume of the orthogonal projection of onto . The normalized volume is invariant under translations and invertible linear maps, so asking for its extremizers is an affine isoperimetric problem. Petty's projection-volume conjecture (Petty, 1971) predicts that this ratio is minimized exactly by ellipsoids. It is related to, but distinct from, Petty's projection inequality for the polar body , which is a classical theorem; inequalities in this family underlie affine Sobolev inequalities and isoperimetric inequalities in normed spaces.
This mission asks for a formal proof of the conjecture in every dimension , 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.
A convex body is a compact convex set with nonempty interior, and denotes -dimensional Lebesgue volume. For a unit vector , let be the orthogonal projection of onto the hyperplane and the Lebesgue measure on that hyperplane. The projection body is
the convex body with support function . Write for the volume of the Euclidean unit ball . An ellipsoid is a set with and an invertible linear map. Since , the ball has ratio .
For every integer and every convex body ,
with equality if and only if is an ellipsoid.
The result itself. Together with the separately proved three-dimensional case, it settles Petty's conjecture for all (in dimension the ratio is constant up to the standard identification). The preprint derives from it the Lutwak–Petty lower-degree inequalities, a mixed determinant-gradient inequality strengthening the Sobolev–Zhang affine inequality, and the sharp Holmes–Thompson isoperimetric inequality in normed spaces (Corollaries 7.1–7.3, pp. 27–29). Those corollaries for rely on the external three-dimensional theorem.
Formalizing it. The proof uses the first variation of volume, spherical harmonics with explicit cosine and Funk transform multipliers, a strict harmonic estimate for arbitrary norms, a variational representation of support functionals, and Brouwer's fixed-point theorem. Mathlib has Brouwer-type results only in limited forms and has no spherical-harmonic decomposition of ; these would be reusable. No machine-checked proof of any case of the conjecture is known.
Previous results are local: they require the body, after a linear change of variables, to be close to the ball, because the harmonic analysis of the projection operator only controls perturbations of the ball. A global argument must handle arbitrary bodies without symmetry or regularity. In the preprint (pp. 2–3) the degree-two spherical harmonic component is not a zero mode of the relevant sign-test operator and has to be removed by choosing affine coordinates; this needs a continuous family of variational minimizers extended to singular matrices and a fixed-point argument (Proposition 5.5, p. 23). Harmonics of degree at least four are controlled by a strict norm estimate valid for every norm (Theorem 4.1, p. 12). The equality case must come out of the same estimates.
Space n is EuclideanSpace ℝ (Fin n); IsConvexBody K is compact, convex, nonempty interior; .shadowVolume K u is the measure, in the induced Euclidean volume on the submodule , of the image of under orthogonalProjectionOnto. projectionBody K is the intersection of half-spaces over unit vectors, which has support function shadowVolume K because that function is itself a support function.projectionRatio K = volume.real (projectionBody K) / volume.real K ^ (n - 1); for a convex body both volumes are finite and the denominator is positive.pettyConstant n = kappa (n-1) ^ n * kappa n ^ (2 - n) with an integer exponent, the volume of the closed unit ball.IsEllipsoid K: for a linear equivalence .iff equality characterization; neither part is vacuous for .Place a convex body in the position coordinates and its polar in the momentum coordinates of the standard symplectic space . The resulting Lagrangian product links two problems. Its volume is the Mahler volume product , and its symplectic capacities measure how large a round ball can be squeezed into it by a symplectic map. Since symplectic maps preserve volume, a ball of capacity inside forces . Artstein-Avidan, Karasev and Ostrover showed that the Hofer–Zehnder capacity of equals for every origin-symmetric and connected Viterbo's volume–capacity conjecture to Mahler's conjecture (Duke 2014). Whether actual balls of capacity close to fit, i.e. whether the Gromov width also equals , was open.
This mission asks for a formal proof that it does, as claimed in an OpenAI preprint dated September 22, 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.
An origin-symmetric convex body is compact, convex, has nonempty interior, and satisfies . Its polar is . On put , and let
A symplectic embedding of an open set into is a map on that is a topological embedding, maps into , and whose derivative preserves at every point. The Gromov width is the supremum of capacities for which embeds symplectically into .
For every and origin-symmetric convex body , .
For every and every origin-symmetric convex body ,
and for every there is a symplectic embedding . No embedding at capacity exactly is asserted.
The result itself. It answers the symmetric-polar-product width question with no smoothness, strict convexity or unconditionality assumptions, and through volume preservation it implies the symmetric Mahler inequality in every dimension (Corollary 5.3). For it also transports finite ball packings satisfying strict volume and pairwise-capacity conditions into (Corollary 5.5, p. 17). It is specific to symmetric polar products: the general Viterbo conjecture is false.
Formalizing it. Mathlib has smooth manifolds and differential forms but no symplectic capacities, nonsqueezing, or Moser's deformation method. A formal proof would need these, together with a conformal map of the disk with explicit boundary estimates. These components are reusable across symplectic geometry. No machine-checked computation of a Gromov width of a non-trivial domain is known.
The upper bound follows from Gromov nonsqueezing and a supporting-cylinder argument (or from the Hofer–Zehnder computation). The lower bound is the hard direction: knowing does not produce any ball, and explicit embeddings were previously known only for special families ( balls, the cube). The preprint's route (Sections 2–4) needs balls of capacity close to from holomorphic maps vanishing to order , and a momentum scale that is uniform up to the tips of a conformal lens, where slice heights approach as grows; a non-uniform estimate does not suffice.
EuclideanSpace ℝ (Fin n); phase space is their product. polar uses the real inner product; polarProduct K is interior K ×ˢ interior (polar K).capacityBall n c is the open ball , so a ball of radius has capacity .HasSymplecticEmbedding U V: some e with ContDiffOn ℝ ∞ e U, IsEmbedding on the subtype U, MapsTo e U V, and for all .gromovWidth is an sSup in ℝ≥0∞ of the admissible capacities, so an unbounded set would give ⊤; the goal asserts the value 4 and separately every capacity below .Welcome contributions: a Lean notion of symplectic embedding between open subsets of , Gromov nonsqueezing (as an axiom-free target in its own right), and volume preservation for symplectic maps.
The Hardy–Littlewood maximal function replaces a function by the largest of its averages around each point. It is the basic tool for differentiation theorems and singular integrals, and it is bounded on for but not on . Kinnunen showed that it also preserves first-order Sobolev regularity: it is bounded on for , because pointwise (Kinnunen 1997). At this argument breaks, since is unbounded on . Hajłasz and Onninen asked whether the gradient estimate nevertheless holds (Question 1 in Ann. Acad. Sci. Fenn. Math. 2004). The question is a test of whether maximal operators improve or destroy regularity at the endpoint, where the usual machinery is unavailable.
This mission asks for a formal proof of the planar centered-disk case, 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.
Identify with the Euclidean plane and write for the open disk of radius centered at . For a locally integrable real function , the centered disk maximal function is
The space consists of integrable whose distributional gradient is represented by an integrable vector field , i.e. for all . Norms of gradients are Euclidean: . For the signed estimate, put and .
There is an absolute constant such that for every real and with a power of two (including ),
with independent of , and the number of dyadic scales.
There is an absolute constant such that for every real , is finite almost everywhere, locally integrable, belongs to , and has a globally integrable weak gradient with
The result itself. It resolves the planar centered-disk case of the Hajłasz–Onninen question with no radiality or support assumption. As a consequence (Corollary 6.3, p. 39) the bound extends to inputs and yields a co-area type perimeter bound for level sets of . The constant is absolute but not optimized. Higher dimensions, other centered maximal operators, and continuity of in remain separate questions.
Formalizing it. Mathlib has Lebesgue integration, weak derivatives only in limited form, and no maximal-function regularity theory. A formal proof would need distributional gradients, Poincaré inequalities on squares, dyadic multiscale decompositions and a vector-measure representation of bounded distributional derivatives (the preprint's Appendix A). These pieces are reusable across harmonic analysis.
For one bounds and uses the strong maximal inequality, which fails for . One-dimensional proofs order the optimizing intervals, and that ordering has no analogue for families of centered disks. Fractional-order proofs use that optimizing balls overlap little, a mechanism that degenerates at order zero. The preprint (Sections 2–5) instead proves the signed finite-band estimate uniformly in the number of scales: it uses a vanishing first moment at interior maximizing radii, a concentration-in-a-thin-shell lemma (Lemma 2.4, p. 8), and two multiscale constructions that pay for direction changes in scale and space. A variation bound alone would leave a possibly singular derivative measure; removing the singular part needs the signed form of Proposition 1.2 applied to locally mean-subtracted inputs (Section 6).
EuclideanSpace ℝ (Fin 2). maximal f x is an ℝ≥0∞-valued supremum over all real of lower Lebesgue integrals of over Metric.ball x r divided by ; the goal asserts it is finite a.e. before passing to maximalReal = toReal.HasWeakGradient f g is the integration-by-parts identity against every compactly supported test function, coordinatewise; the input is Integrable f, Integrable g, HasWeakGradient f g, which is exactly with weak gradient g. The bound is stated against this g, so it does not depend on a choice of representative.InW11Loc asks for local integrability and a locally integrable weak gradient; the goal also asks for one integrable weak gradient G with ∫ ‖G‖ ≤ C * ∫ ‖g‖, C ≥ 0 chosen before f.sSup over the closed radius band ; the band envelope is continuous in , so the supremum is finite. Inputs are ContDiff ℝ ∞ with compact support.If a complex manifold is a product , its tangent bundle splits as the sum of the pulled-back tangent bundles of the factors, and each summand is integrable: the bracket of two local holomorphic vector fields tangent to a summand stays in that summand. Conversely, given a holomorphic decomposition , one wants to know whether it comes from a product. Integrability of the summands is the necessary local condition, and it can fail: Höring exhibited a non-integrable summand on the product of an abelian surface with (Höring 2007, Example 2.14). For rationally connected projective manifolds — those in which two general points lie on a rational curve, a class including all Fano manifolds — Höring showed that integrability of one summand already yields a compatible product decomposition, which made automatic integrability the remaining question.
A complex manifold of dimension is a Hausdorff, second-countable space with a holomorphic atlas to . is projective if it admits an injective holomorphic immersion into a complex projective space ; for compact this is a closed embedding.
A rational curve in is a holomorphic map . A compact connected projective manifold is rationally connected if there is a nonempty Zariski-open set such that every pair lies on the image of a rational curve. Here Zariski-open is measured through the projective embedding: is the complement of the common zero set of a family of bihomogeneous polynomials in the two sets of homogeneous coordinates.
A holomorphic splitting is given by a holomorphic field of idempotent linear maps on the tangent spaces, with and , both of positive rank at every point. A family of subspaces is integrable if for every open and every pair of holomorphic vector fields on with values in , the Lie bracket takes values in .
Let be a smooth connected projective complex manifold of dimension at least two which is rationally connected. For every holomorphic decomposition into subbundles of positive rank,
for every open , where denotes holomorphic sections over . The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. The theorem has no rank or positivity hypothesis, and it settles the smooth rationally connected case of Höring's conjecture. Combined with Höring's product theorem it gives Corollary 1.2: every holomorphic splitting of the tangent bundle of a smooth rationally connected projective manifold comes from an isomorphism identifying with the factor tangent bundles. It also applies to general fibers of the rationally connected quotient of a uniruled compact Kähler manifold, supplying the integrability premise in Höring's structure theorems (Corollary 5.1). Together with the companion preprint on universal-cover splitting for compact Kähler manifolds, it covers both the integrability question and the global product question.
Formalizing it. The statement involves projective embeddings, Zariski-open sets of pairs, rational curves and holomorphic distributions, all expressed from first principles over Mathlib's manifold library. A machine-checked proof would certify a classical-looking but new geometric argument; the compatible product (Corollary 1.2) is not part of this goal.
The bracket of two sections of , projected to , is a tensor , and the task is to show it vanishes. The natural approach is to restrict to rational curves and use positivity, as in the Fano and low-rank cases, but without positivity or rank assumptions the restricted bundles can have summands of either sign and no vanishing follows directly. Smoothness cannot be dropped: a singular rationally connected example with a non-integrable summand exists (Höring 2026, Example 4.3), so the argument must use the manifold structure in an essential way. Rational connectedness is also needed: Höring's example on an abelian surface times is a smooth projective manifold with a non-integrable summand.
ComplexManifold carries its dimension, a Hausdorff second-countable topology, and an analytic (ω) atlas modeled on Fin dim → ℂ. The theorem assumes ConnectedSpace, CompactSpace and 2 ≤ X.dim.ProjectiveEmbedding X is an injective map to ℙ ℂ (Fin (N+1) → ℂ) that is holomorphic and immersive in every affine patch.RationalCurve X is a holomorphic map from given by two holomorphic maps agreeing via ; RationallyConnected e asks for a nonempty, dense, Zariski-open set of pairs (bihomogeneous polynomial complement) all joined by rational curves. Density is automatic for a nonempty Zariski-open subset of the irreducible variety , so stating it does not narrow the class.TangentSplitting X is a holomorphic idempotent field on the tangent bundle with range and kernel of positive rank at every point. Integrable uses VectorField.mlieBracketWithin for sections that are holomorphic on an open set.If a complex manifold is a product , its holomorphic tangent bundle is the direct sum of the tangent bundles of the factors. The converse question asks when a given holomorphic decomposition of the tangent bundle of a compact manifold comes from a product decomposition of its universal cover, with the product realizing the specified summands rather than some other splitting. This is the complex-analytic counterpart of the de Rham decomposition theorem for Riemannian manifolds with parallel complementary distributions (de Rham 1952), but a holomorphic splitting supplies no complete metric making the distributions parallel, so de Rham's argument does not apply. The question sits between foliation theory, Kähler geometry and the classification of projective manifolds with split tangent bundle.
A complex manifold of dimension is a Hausdorff, second-countable space with holomorphic charts to . A Kähler metric is a smooth Riemannian metric on the real tangent bundle that is Hermitian ( for multiplication by ) and whose fundamental form is closed.
A holomorphic splitting of with ranks is given by a field of -linear idempotents , holomorphic in charts, with and ; then , and . A subbundle is integrable if its local holomorphic sections are closed under the Lie bracket. The ordinary universal cover is a connected, simply connected covering space carrying the lifted complex structure.
Let be a compact connected Kähler manifold of complex dimension and a holomorphic splitting into integrable subbundles of positive ranks . Then there are connected, simply connected complex manifolds with and a biholomorphism with
The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. The theorem proves the two-summand form of Beauville's conjecture with no flatness, compact-leaf or line-bundle assumption: integrability of both summands and a Kähler metric on a compact manifold suffice. Combined with Höring's integrability theorem it gives compatible product decompositions for every split tangent bundle on a non-uniruled projective manifold (Corollary 1.2), and for projective manifolds with nef and big canonical bundle (Corollary 1.3). With the companion preprint on rationally connected manifolds it also covers split tangent bundles there. The factors may be noncompact, and the conclusion concerns the universal cover, not a finite cover.
Formalizing it. The statement involves universal covers, Kähler forms, holomorphic distributions and biholomorphisms of products, all of which must be expressed with Mathlib's manifold library. A machine-checked proof would certify a global continuation argument (Hartogs-type extension, boundary crossing, path rectangles and monodromy) for which no prior formal treatment exists.
Integrability alone gives, by holomorphic Frobenius, local product coordinates. The obvious strategy is to continue these local products along paths and use simple connectivity of . This fails because a path in one foliation need not be transportable along a path in the other: local product charts can break down, and leaves can be noncompact and dense. Compactness makes every metric complete, but does not make the foliations parallel, so the de Rham argument is unavailable. Beauville's example on ( an abelian surface) shows that even when is a product, a non-integrable complementary summand need not be realized by any product structure, so both integrability hypotheses are needed.
ComplexManifold n bundles a Hausdorff, second-countable type with an atlas modeled on Fin n → ℂ that is smooth for 𝓘(ℂ, Fin n → ℂ), i.e. holomorphic transition maps.KahlerMetric X is a real bilinear form on each tangent space that is symmetric, positive definite, invariant under multiplication by Complex.I, smooth in every chart, and whose fundamental form is closed (the cyclic sum of its chart derivatives vanishes).HolomorphicSplitting X r₁ r₂ is a field of idempotent continuous ℂ-linear maps, holomorphic in charts, with range of rank and kernel of rank . Integrable P says that chart-local holomorphic vector fields with values in the range of have bracket in the range of ; both S.projection and the complementary projection are assumed integrable.OrdinaryUniversalCover X Z is a covering map from a connected, simply connected complex manifold that is a local biholomorphism.CompatibleProduct asks for a homeomorphism , holomorphic with holomorphic inverse, whose differential sends the pullback of onto and the pullback of onto .Zariski's cancellation problem asks whether affine space can be recognized from its cylinder: if a variety satisfies , must ? Algebraically, for a finitely generated commutative -algebra and an independent variable ,
where is a polynomial ring in variables and all isomorphisms are -algebra isomorphisms. The problem is one of the central questions of affine algebraic geometry, closely tied to the recognition of affine space, coordinates of polynomial rings, and polynomial fibrations.
The source of this mission is an OpenAI preprint dated September 23, 2026.
Let be independent variables over and . Put
So is the coordinate ring of the hypersurface . For a -algebra , denotes the polynomial ring in one further variable, and the polynomial ring in variables.
The Lean statement OAI.ComplexCancellation.main is open on the platform.
Theorem 1.1 gives a negative answer to Zariski's cancellation problem over in dimension four, with an explicit counterexample of degree small enough to write in one line. The same polynomial yields two further consequences proved in the paper: is a coordinate of but not of , so the Stable Coordinate Conjecture fails in ambient dimension five (Corollary 1.2); and the maps and are smooth -fibrations that are not Zariski-locally trivial, disproving the Dolgachev–Weisfeiler conjecture over these bases (Corollary 7.1). Cancellation in dimension three over is not addressed.
The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists.
The cylinder isomorphism is comparatively explicit: a locally nilpotent derivation sends to , and exponentiating converts into . The hard part is proving . Standard invariants do not help: is smooth, factorial-type obstructions vanish, and topologically is contractible like since its cylinder is . The paper uses additive group actions (locally nilpotent derivations), passing to an associated graded algebra along , lifting actions through a line bundle over a smooth affine quadric, and a rigidity argument based on the Mason–Stothers polynomial abc inequality.
P := MvPolynomial (Fin 5) ℂ with p, s, u, F, J := X 0, …, X 4; x and H are transcribed literally; A := P ⧸ Ideal.span {H}.ringKrullDim A = 4; integrality is IsDomain A; finite generation is Algebra.FiniteType ℂ A.Nonempty (Polynomial A ≃ₐ[ℂ] MvPolynomial (Fin 5) ℂ); the non-polynomiality is ¬ Nonempty (A ≃ₐ[ℂ] MvPolynomial (Fin 4) ℂ). All isomorphisms are -algebra isomorphisms.A complete development needs: explicit polynomial automorphisms (for the cylinder), Krull dimension of hypersurface quotients, locally nilpotent derivations and their kernels, filtrations and associated graded rings, and the Mason–Stothers theorem for polynomials. Contributions formalizing Proposition 2.2, Proposition 3.4 (the graded identification), Propositions 4.1–4.3, Lemma 5.1 (order of a locally nilpotent derivation), Lemma 6.1 (Mason–Stothers) and Proposition 6.3 are welcome.
Let be the -th prime and the -th gap. By the prime number theorem the average gap near is about . A great deal is known about how large individual gaps can be, but much less about how often large gaps occur. A natural question is whether, for each fixed , a positive proportion of all gaps exceed . Erdős and Prachar (1962) asked a closely related question about the sequence : do the indices where it increases have positive lower density?
The source of this mission is an OpenAI preprint dated September 25, 2026.
For every fixed real there are and with
and
The Lean statement OAI.Problem344.large_gaps_and_ratio_density is the conjunction of these two claims and is open on the platform.
Theorem 1.1 says that gaps of size are not rare for any fixed : they occupy a positive proportion of the indices up to every large . This is a statement about the frequency of large gaps, not about the size of the largest one, and it does not follow from the Erdős–Rankin or Ford–Green–Konyagin–Maynard–Tao constructions. Corollary 1.2 answers the Erdős–Prachar question: since is equivalent to , it follows from Theorem 1.1 with . The constants are not made explicit.
The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists.
Counting gaps differs from counting empty intervals: a single very long gap contains many starting points of prime-free intervals, so a positive proportion of empty intervals can come from a sparse set of gaps. Results of the latter kind (Bazzanella–Languasco–Zaccagnini, Tao's empty-interval argument) therefore do not give gap counts. The proof needs a sieve weight that makes a prime in likely while making almost surely prime-free, and then a multiplicity argument (the last prime before the empty interval is selected by at most values of ) to convert weighted interval mass into a count of distinct gaps. Making the second interval nearly empty requires an alternating family of divisor-sum squares whose adjacent dimensions nearly cancel.
prime n = Nat.nth Nat.Prime (n - 1), so prime 1 = 2; largeGapIndices C N filters Finset.Icc 1 N by C * log (prime n) < prime (n+1) - prime n in ℝ.lowerAsymptoticDensity A = sSup {d | ∃ N0, ∀ N ≥ N0, d ≤ initialCount A N / N}, which equals the liminf because the ratios lie in .ratioIncreaseIndices = {n | 1 ≤ n ∧ prime n / n < prime (n+1) / (n+1)} in ℝ.A complete development needs the prime number theorem, the Bombieri–Vinogradov theorem, smooth Goldston–Yıldırım/Maynard divisor-sum correlations, and averages of the Hardy–Littlewood singular series. These are widely reusable. Contributions formalizing Proposition 2.1 (weights for adjacent intervals), Proposition 3.1 (moment identities and a detector bound), Proposition 4.2 (cancellation between high dimensions), Proposition 5.1 (uniform mixed moments) and Lemma 5.4 (singular series in boxes) are welcome.
An integer is -power-free if no prime power divides it (zero is never -power-free). For a fixed integer polynomial one expects to be -power-free for a positive proportion of integers , given by an Euler product of local densities, as soon as no prime th power divides every value of . The heuristic is a sieve: discard the with for each prime . Small primes are handled by the Chinese remainder theorem; the problem lies with primes larger than the range of , where can be divisible by only if it has an unusually large square-full part. The case , where , is the first exponent left open by classical methods. Its best-known instance is the squarefreeness of , singled out by Erdős in 1953 and again in his 1965 survey.
Let be irreducible over , of degree , and let . Define
The local admissibility condition is for every prime : no prime th power divides all values of . The predicted density is
Let be irreducible over with , put , and assume for every prime . Then the Euler product converges,
For this is the paper's new Theorem 1.1; for it follows from Browning's theorem. Already the case (squarefree values of quartics such as and ) is new. The goal statement is published on the platform with status Open.
The result itself. The theorem closes the exponent for every degree, answering Erdős's question about and giving the first unconditional squarefree-density theorem for an arbitrary admissible irreducible quartic. No primitivity or sign condition on is required. The same large-prime estimate also gives densities for separable products and simultaneous power-freeness of several polynomials (Corollary 1.3).
Formalizing it. The statement is elementary, but its proof uses number-field factorization, the unit theorem, determinant methods for counting points on surfaces and curves, and explicit Hilbert-function computations. None of these components is machine-checked. A formal proof would certify a result that the literature had only reached conditionally (on ) or in higher degrees. The finite-prime sieve and the deduction of the density from a large-prime tail bound are reusable for other power-free-value problems.
The sieve over primes is routine. The obstacle is the primes : one must show that very few have for some such (Proposition 1.4, with a power saving ). Counting solutions of as integer points on the surface with determinant methods succeeds only when is large; in the intermediate range the point counts are too weak, and the existing determinant bounds stop exactly at .
Polynomial ℤ whose image in Polynomial ℚ is irreducible, with natDegree ≥ 4; the exponent is f.natDegree - 2 (at least , so the natural-number subtraction is harmless).PowerFree k a says no prime has , so is not power-free, matching the source convention; negative values are allowed.tprod over Nat.Primes; the goal asserts Multipliable explicitly, so the constant is not a junk value, together with and .Let count the prime factors of with multiplicity and let be the Liouville function. Chowla's conjecture (1965) predicts that behaves like a random sign sequence: its correlations along any fixed collection of distinct shifts have average tending to zero. The two-point case asks whether and have the same parity of prime-factor count as often as different parity. It is the multiplicative analogue of the twin prime problem and a central test case for the parity barrier in sieve theory. Elliott's conjecture extends the question to bounded multiplicative functions; Matomäki, Radziwiłł and Tao showed that for complex functions it needs a correction, uniform nonpretentiousness against all twists .
There are two natural averages: the ordinary average and the logarithmic average . Logarithmic averaging blends many scales; an ordinary estimate must control the terminal scale itself.
The source of this mission is an OpenAI preprint dated September 24, 2026, which treats ordinary averages at every cutoff.
There is an absolute such that for all nonproportional affine forms there is with
With , , this is the ordinary two-point Chowla conjecture with a logarithmic saving.
The goal OAI.OrdinaryTwoPointCorrelations.liouville_log_saving is open on the platform.
Theorem 1.1 removes the logarithmic weight and the exceptional scales from earlier two-point results: the bound holds at every cutoff, with an exponent independent of the forms. Theorem 1.2 does the same qualitatively for all one-bounded multiplicative functions satisfying the Matomäki–Radziwiłł–Tao corrected condition, without complete multiplicativity, unimodularity or real values. The implied constants need not be effective, and no uniformity in growing coefficients is claimed.
The results are proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists.
Partial summation turns ordinary cancellation into logarithmic cancellation, but not conversely, so Tao's entropy-decrement method and its descendants do not reach ordinary averages: they need to average over scales. Short-interval estimates give cancellation for most shifts or most scales, not for a fixed shift at every scale. The proof works at the terminal scale through multiplicative dilations, which lead to a divisor graph with edge displacement ; one must bound high traces of the associated operator (closed walks, nonbacktracking moments, prohibited paths, triangular arithmetic savings) with weights matched to ordinary averaging, and in Part I convert this into an explicit logarithmic saving using bounded independence for Boolean circuits.
liouville n is ArithmeticFunction.liouville n cast to ℂ; affineSum f g a₁ a₂ b₁ b₂ N sums over n ∈ Finset.Icc 1 N, and the bound is applied at N = ⌊X⌋₊ for real X ≥ 3, with (Real.log X) ^ c as Real.rpow.Multiplicative asks the identity only for coprime positive arguments; OneBounded only for positive arguments in this source group.UniformlyNonpretentious is stated as: for every q > 0, every χ : DirichletCharacter ℂ q and every K, eventually in N, every t with |t| ≤ N has squared distance at least K. This is equivalent to (1.2).OrdinaryCorrelations) uses the sInf form of (1.2) and is included as a reference item.A complete development needs prime sums and Mertens-type estimates, Dirichlet characters, short-interval mean-value theorems (Matomäki–Radziwiłł–Tao, Theorem 4.3 here), Fourier bounds for rough integers, and the graph-trace machinery. Contributions formalizing Proposition 2.1 (quantitative correlations in every progression), Theorem 5.4 (the nonbacktracking moment), Proposition 10.1 (divisor graph estimate), Lemma 18.5 (uniform nonpretentiousness of Liouville) or the cited Theorem 4.3 are welcome.
Catalan's constant
is the value of the Dirichlet -function of the odd quadratic character of conductor 4. It appears throughout analysis, combinatorics (dimer and spanning-tree constants), and geometry (volumes of hyperbolic 3-manifolds). For odd , is a rational multiple of ; the even values are, like , among the basic special values whose arithmetic nature was unknown. Whether is irrational had long been a well-known question.
The source of this mission is an OpenAI preprint dated September 24, 2026.
is the sum of the alternating series of reciprocals of odd squares displayed above. A real number is irrational if for all integers and . No other definitions are involved.
The Lean statement OAI.InternalCatalan.catalan_irrational is open on the platform.
Theorem 1.1 settles the irrationality of an individual even Dirichlet -value, which family results (Rivoal–Zudilin, Fischler) could not single out. The paper deduces (Section 8) irrationality of the minimal volume of an orientable complete finite-volume hyperbolic 3-manifold with exactly two cusps (Agol 2010 identified this volume as , doi:10.1090/S0002-9939-10-10364-5) and of certain arithmetic hyperbolic volumes. The argument is qualitative: it gives no irrationality measure.
The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists. A formal proof would certify a long argument that combines exact finite certificates (rational matrices, rational trial coefficients) with analytic and -adic estimates.
The standard route needs nonzero integer linear forms . Many constructions give rational approximations quickly, but clearing denominators destroys the decay: this is exactly the obstruction Zudilin identified for his Apéry-like recurrences, and approximation exponents below 1 (Viola–Marcovecchio, Eskandari) do not overcome it. The paper replaces linear forms by growing determinants of size built from moments that are rational combinations of , and ; one must cancel the term exactly, bound denominators prime by prime (including two layers at large odd primes), prove nonvanishing along a sequence of primes via a finite certificate, and obtain a real-place upper bound sharp enough that the normalized limits and are incompatible. The margin between these constants is about .
Irrational and tsum over ℕ. The series is absolutely summable, so tsum agrees with the classical sum.ℝ; there are no partial operations.A complete development needs: Chebyshev polynomial rows and their moments; -adic valuations of the determinant entries and the prime number theorem in the weighted form used (Mathlib's PNT development may be reused); a Frobenius reduction and verified finite certificates for nonvanishing; Andréief's identity, Hardy-space interpolation and Hadamard bounds for the real estimate; and certified rational arithmetic for the final constants. Contributions formalizing Proposition 2.2 (cancellation and rationality), Proposition 3.4 (finite-place bound), Proposition 4.1 (nonvanishing at prime scales), Propositions 5.2–5.3 (interpolation and Hadamard estimates) and Proposition 7.1 (real-place bound) are welcome.
The Riemann zeta function (), continued meromorphically to , encodes the distribution of primes through its zeros. Riemann (1859) conjectured that all nontrivial zeros lie on . Hadamard and de la Vallée Poussin (1896) proved there are no zeros on , which gives the prime number theorem, but all classical zero-free regions shrink toward the line as the height grows. The quasi-Riemann hypothesis asks for a fixed such that for all : one zero-free gap valid at every height. The uniform version for all Dirichlet -functions is a standard formulation in analytic number theory (e.g. Friedlander–Goldston).
This preprint claims a proof with , for , for all Dirichlet -functions, and for all finite-order Hecke -functions over .
For a Dirichlet character modulo (extended by zero on non-units), for , continued meromorphically; the character modulo gives . For with ring of integers , a finite-order Hecke character modulo a nonzero ideal is a character of the ray class group modulo , extended by zero, and . Principal characters have a pole at .
In Lean, is Mathlib's riemannZeta, Dirichlet -functions are Mathlib's DirichletCharacter.LFunction, and the Hecke family is OAI.SevenEighths.HeckeFamily.LFunction: a Character is a multiplicative character of trivial on units (for this class-number-one field these are exactly the ray class characters), and its -function is a lattice sum over divided by the units, continued through a theta-type functional equation pair.
For every Dirichlet character modulo and every with , , except at the pole of a principal character.
For every finite-order Hecke character of and every with , , except at the pole of a principal character.
The three statements are ordered from weakest to strongest; the proof in the preprint goes through the whole Hecke family even for , because Poisson summation introduces Hecke twists of the target.
The result. A fixed zero-free half-plane would give power-saving error terms in the prime number theorem and in prime counts in arithmetic progressions, uniformly in the modulus, and would exclude Siegel zeros beyond . The preprint derives (Corollary 1.2) that the least quadratic nonresidue modulo is , proving Vinogradov's conjecture, and a deterministic polynomial-time square-root algorithm modulo primes.
Formalizing it. This is a claimed resolution of a long-standing question in an unrefereed preprint; a machine-checked proof would be strong independent verification. The goal uses only Mathlib definitions, so it cannot be weakened by a definitional choice. The Hecke milestone uses a custom -function definition that must also be checked against the source.
Classical zero-free regions come from positivity arguments (the inequality) that give regions of width shrinking to the line ; they cannot produce a fixed half-plane. Zero-density estimates bound the number of zeros to the right of a line but do not exclude every zero. The preprint instead continues reciprocals across a uniform distance by comparing two exact representations of a completed cubic-theta sum, with exponent margins independent of the target character.
∀ s : ℂ, 7/8 < s.re → riemannZeta s ≠ 0. Mathlib assigns a finite nonzero value, so no pole exclusion is needed.χ = 1 ∧ s = 1, where Mathlib's value is a junk value at the pole.χ.residue = 1 ∧ s = 1.The goal is not vacuous and cannot be satisfied by a convention: it is a statement about Mathlib's riemannZeta on an open half-plane.
Needed infrastructure: Hecke -functions over imaginary quadratic fields and their functional equations, cubic and sextic residue symbols, Patterson's cubic theta coefficients, large sieve inequalities over , and Mellin inversion. Contributions toward the half-plane (Theorem 3.1) as an intermediate target are welcome.
Risk-averse optimization replaces the expected cost of a random outcome by a risk function that also penalizes dispersion: mean–deviation, mean–semideviation, conditional value-at-risk (CVaR) and their combinations are the standard examples in stochastic programming and portfolio selection. A decision maker who uses should not prefer an outcome that every risk-averse expected-utility maximizer rejects. For costs, the order that expresses this agreement among risk-averse agents is the increasing convex order: is worse than if for every increasing convex disutility . It is the counterpart, for costs, of second-order stochastic dominance.
Whether a given mean–risk model is consistent with stochastic dominance was settled model by model: Ogryczak and Ruszczyński for mean–semideviation models (Eur. J. Oper. Res. 1999, Math. Program. 2001, SIAM J. Optim. 2002) and Pflug for CVaR (2000). Ruszczyński and Shapiro (Math. Oper. Res. 31, 2006) gave a single criterion, Theorem 5.1, which contains these results as special cases: among risk functions that depend only on the distribution of the outcome, consistency with the increasing convex order is equivalent to two structural properties, monotonicity and risk aversion.
Let be a probability space and . The space of outcomes is , the real random variables with . An outcome is a cost: smaller is better. A risk function is a map .
for every version of the conditional expectation.
The paper places one more standing assumption on §5.2: the space is rich enough to carry a uniform random variable, a measurable with for all .
In Lean these are IsUniformRV, cdfOf, cdfInv, DistInvariant, A2, RiskAverse, StLE, ConsistentSt and ConsistentIcx in the namespace ConvexRiskFn.Order; the increasing convex order is the published StochasticOrders.MonotoneConvex.IcxOrder P P X₁ X₂, read as .
Under the standing assumptions, for every distribution-invariant ,
No convexity, translation equivariance or positive homogeneity of is assumed.
Theorem 5.1 reduces a property quantified over all pairs of ordered distributions to two properties that can be checked on the risk function directly. Monotonicity is usually immediate, and risk aversion follows for the main examples from the dual representation of the risk function (the paper verifies it for mean–semideviation and for CVaR-based models in §5.1). The theorem then yields at once the consistency of these models with the increasing convex order, which was previously proved case by case. It also explains the failures: a law-invariant risk function that violates (A2), such as mean–deviation for under the paper's condition , cannot be consistent with any increasing integral stochastic order.
The result has a complete published proof. What the mission adds is a machine-checked version of it on the paper's own space , together with reusable pieces of stochastic-order theory: the cdf characterization of the usual stochastic order, the quantile coupling, conditional Jensen in increasing-convex form, and Strassen's martingale coupling realized on a given space carrying a uniform random variable. Mathlib has conditional Jensen for convex functions (ConvexOn.map_condExp_le_univ) but not the stochastic orders, the quantile coupling or Strassen's theorem. Strassen's theorem for laws on , with a coupling on some probability space, is posed separately on Prove2Me but not proved.
The forward direction is short given milestone 4. The reverse direction is where the work is. Consistency compares and for random variables that are related only through their laws: says nothing about versus , so neither (A2) nor risk aversion applies to the pair as given. The argument has to replace the pair by another pair, with the same laws, on the same space , related by a conditional expectation; only then can monotonicity and risk aversion be chained. Producing that pair is Strassen's theorem, a nonconstructive existence result about martingale couplings, and it has to be realized on the given , not on a product space built for the purpose, because is defined only on . That is the role of the uniform random variable, and transporting the coupling onto through it is a separate measure-theoretic step. The first-order analogue, Lemma 5.1, needs the same kind of transfer, through quantile functions, whose values at and must be handled.
MemLp X p P with 1 ≤ p and p ≠ ⊤, not by almost-everywhere classes. is a function (Ω → ℝ) → ℝ; every definition quantifies only over MemLp arguments, so its values elsewhere play no role. is real valued, as in Definition 5.2.P[X|m].Needed infrastructure: equality in law from equality of cdfs, the quantile transform, conditional Jensen's inequality (in Mathlib) turned into the increasing convex order, and Strassen's theorem in dimension one with the transfer of a coupling to a space carrying a uniform random variable. The last two are reusable well beyond this mission. Proofs of any milestone, and of supporting lemmas such as the cdf characterization of equality in law, are welcome.
Potential games (Monderer and Shapley, 1996) are the finite games whose unilateral payoff differences are all differences of a single function, the potential. They always have a pure Nash equilibrium, and many natural learning dynamics (best response, fictitious play, logit response) converge in them. Most games met in applications are not exactly potential games, so a recurring question is how much of this theory survives for a game that is close to a potential game.
Candogan, Menache, Ozdaglar and Parrilo (arXiv:1005.2405, journal version Math. Oper. Res. 36(3), 2011) decompose the space of finite games into potential, harmonic and nonstrategic components. Section 6 of the paper equips the space of games with a weighted inner product under which this decomposition is orthogonal, computes the closest potential game to any game in closed form, and shows that approximate equilibria of a game and of its closest potential game correspond, with an explicit loss controlled by the distance between them. This mission formalizes that last result together with the statements it rests on.
A finite game has a finite set of players ; each player has a nonempty finite strategy set with elements, and a utility on the set of strategy profiles . For a profile , denotes with player 's strategy replaced by .
A profile is an -equilibrium if for every player and strategy (equation (2) of the paper). A game is a potential game if there is with for all , , , (Definition 2.1).
A game is identified with its tuple of utilities, an element of where . The game graph has the profiles as nodes, with an edge between two profiles that differ in exactly one player's strategy. The operator sends to its differences along the edges where player deviates, , is the gradient of the game graph, , and is the Moore–Penrose pseudoinverse. Definition 4.2 defines the potential, harmonic and nonstrategic subspaces
and a harmonic game is a game in .
Section 6 introduces the weighted inner product and norm
A closest potential game to is a potential game with for every potential game ; a closest harmonic game is defined in the same way.
Let be the closest potential game to and . Then for every , every -equilibrium of is an -equilibrium of , and every -equilibrium of is an -equilibrium of , where
The result. Theorem 6.3 reduces the study of approximate equilibria of an arbitrary finite game to a potential game, where pure equilibria exist and are maximizers of the potential. Section 7 of the paper reports that, in a companion paper, best-response and fictitious-play dynamics are shown to converge to a neighbourhood of equilibria in near-potential games, with the size of the neighbourhood governed by the distance of the game to its closest potential game. Theorems 6.1 and 6.2 make that distance computable: the closest potential game is an orthogonal projection, given by linear operators of the game graph.
Formalizing it. All four statements are proved in the paper; none of them is machine-checked anywhere known to this mission. A formal development produces a verified operator layer for games on the game graph (gradient, pseudoinverses, the projections ), a verified proof that the weighted inner product, and not the unweighted one, makes the decomposition orthogonal, and a reusable perturbation lemma for -equilibria.
Lemma 2.1 and the final step of Theorem 6.3 are elementary inequalities. The obvious way to approximate a game by a potential game, taking the identical-interest part of its zero-sum/identical-interest split, does not give the closest potential game: the paper's Table 7 (p. 35) shows a potential game whose identical-interest part is far from it. The closest potential game has to come from the projection of Section 6. The weight of the mission is in Theorems 5.1, 6.1 and 6.2. They need the decomposition theorem of Section 4 (every game splits uniquely into , , ) and properties of pseudoinverses of the operators and that Mathlib does not provide: Mathlib has no operator pseudoinverse at all. The orthogonality under the weighted product rests on the specific spectral structure of the Laplacian of the graph of a single player's deviations; it is not a general fact, and it fails for the unweighted product when the differ, so the standard orthogonal-complement machinery cannot be applied to with its default inner product.
Players are a finite type ι with decidable equality; strategy sets are finite types E m. Utilities are plain functions u : ι → (∀ m, E m) → ℝ, the shape used by the published MondererShapley.ClosedPath.IsPotentialGame, which is referenced for Definition 2.1. The operator layer works in PiLp 2 (fun _ => EuclideanSpace ℝ (∀ k, E k)) with the unweighted inner product of Section 4; edge flows carry the inner product of (7). The weighted inner product (55) and norm (56) are plain functions, not a second instance on the same type. "Closest" is the minimizing property itself, not an infimum of distances.
Hypotheses made explicit: every strategy set is nonempty (the paper's ), so ; in Theorem 6.3 the set of players is nonempty, which the maximum over players needs. The paper's "an -equilibrium for some " is stated as "a -equilibrium", which is equivalent because (2) is monotone in . Both directions of Lemma 2.1 and Theorem 6.3 are included.
The goal is stated for the closest potential game, as printed. A version for an arbitrary potential game at distance would be a different theorem, and the hypothesis is not vacuous: Theorem 6.2 shows the closest potential game exists. Theorem 6.2 is stated as an "if and only if" characterization, so it gives existence and uniqueness as well as the formula.
Contributions welcome: the Penrose identities for the pseudoinverse, the identities and , and the decomposition theorem of Section 4, all of which are reusable by the other missions of this series.
This mission asks for a formal proof that the matrix multiplication exponent is at most over every field. It is proposed for the Matrix multiplication exponent campaign, using the campaign's existing tensor-rank definition. The target is deliberately non-strict: equality with is allowed.
The starting point is OpenAI's October 2026 matrix-multiplication material, whose original arithmetic-exponent theorem is stated over the complex numbers. An all-fields adaptation has been checked separately in Lean. This mission asks for the corresponding result in the campaign's precise mathematical model; that connection still requires proof.
Let be any field, finite or infinite and in any characteristic. For a positive integer , the square matrix multiplication tensor is the sum of over all indices . Each factor is the vector space of functions from pairs of indices to . Its tensor rank is the least number of pure tensors in an exact decomposition over .
The imported definition MME.matMulExp takes the infimum of the ratios for integer , together with the value at sizes zero and one. The goal refers to this existing definition without modifying it. An upper bound on the infimum need not be attained at any one matrix size.
For every field , prove
The Lean theorem is mme_omega_le_225, with the sole typeclass hypothesis [Field K]. The decimal is interpreted exactly as a real rational, not as a floating-point approximation. There is no restriction to characteristic zero, infinite fields, algebraically closed fields, or the complex numbers.
The campaign template currently uses a strict inequality. This proposal intentionally requests the non-strict bound and should be reviewed on that basis. It does not assert . The proposed numeric campaign value is .
A proof of this goal would place the nine-fourths bound in the same formal tensor-rank model used by other entries in this campaign. Reusing the foundation makes its assumptions and numeric value directly inspectable. Establishing the comparison between the arithmetic and tensor formulations would also produce reusable results for future matrix multiplication missions.
The all-fields quantifier matters: constructions that use interpolation or roots of unity must justify their applicability and any descent back to the original field. A result over the complex numbers alone does not establish this goal.
The available checked adaptation proves the nine-fourths bound for the OAI arithmetic exponent and its exact-rank exponent. A remaining task is to connect that exact-rank representation to the campaign's tensor product and rank definition. This requires checking the coordinate conventions, converting rank decompositions, and transporting the bound through the infimum and logarithms.
The proof must also compile in the campaign's pinned Lean environment. Success in a different Lean or Mathlib version is useful evidence for the source proof, but it does not verify this mission's theorem.
This draft imports the campaign's published mme_omega definition and contains one open goal. It preserves the campaign environment, Mathlib 777aaa6 with Lean 4.29.0-rc3. The separate all-fields OAI adaptation was checked using Lean 4.33.1 and Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; its proof is not yet an accepted Prove2me solution to this goal.
In particular, the bridge to MME.matMulExp and the environment port remain unproved here. The mission should remain open until Prove2me accepts a proof of this exact statement. An independent auditor read the Lean goal and imported definition without seeing the intended wording; that read-back is included verbatim in the goal's natural-language statement for review.
The all-fields adaptation and the proposed connection to the campaign definition are additional formalization work; they are not attributed to the original complex-field statement.
All-pairs shortest paths (APSP) asks for the exact distance between every ordered pair of vertices in an -vertex weighted directed graph. Floyd–Warshall solves it in time, and for decades no algorithm beat for any constant on graphs with polynomially bounded integer weights. In 2026, Alman and Vassilevska Williams (arXiv:2610.06783) gave a deterministic algorithm, the campaign's first entry. Later entries tightened the accounting to and .
This entry records the deterministic exponent . It roughly doubles the saving below compared with , and it matches what was previously only known with randomized hashing.
The model is the campaign's fixed deterministic word RAM (foundation mission: Truly Subcubic APSP on a Word RAM). A finite program uses add, subtract and multiply modulo , indirect load and store, a sign branch, and accept or reject, on words of width . Inputs have integer weights of absolute value at most for a fixed , and there are no negative cycles. The machine has no source of randomness; the algorithm behind this entry is deterministic.
The goal is the campaign template with the value :
which says there is a deterministic word-RAM program that solves APSP in steps.
The algebraic core is the thin-product data structure of Alman and Vassilevska Williams: for an by integer product it answers requested entries in . Two local refinements of that construction sharpen the exponents:
The main new step is a deterministic filtering reduction. Moduli are chosen one small prime factor at a time, using exact thin-product witness counts to certify positive answers and to eliminate whole blocks of unresolved queries. Repeated filtering removes the need to scan individual modular witnesses, which was the bottleneck of earlier deterministic reductions (the prime-by-prime idea is suggested in footnote 9 of the source paper, after Fischer, Kaliciak and Polak). With middle blocks of size this yields all-edges Exact Triangle in , where
and deterministic bit scaling transfers the bound to min-plus product and APSP with polylogarithmic overhead.
The exact rational parameters , and satisfy the thin regime with margin , and give . Hence APSP runs in , and the gap absorbs the subpolynomial factor.
This is the first deterministic entry near . Earlier analyses reached about only by repeating random-prime hashing, which this word-RAM model cannot express. The deterministic filtering closes that gap.
The -model is the simplest exponential random graph model in which every vertex has its own parameter. It was studied by Holland and Leinhardt (1981) in the directed case and by Park and Newman (2004) and Blitzstein and Diaconis (2011) in the undirected case, and it is a close relative of the Bradley–Terry model for paired comparisons. Its sufficient statistic is the degree sequence of the observed graph, so fitting the model to data means solving a system of nonlinear equations in unknowns, one per vertex, where can be in the thousands.
Chatterjee, Diaconis and Sly (arXiv:1005.1136, Ann. Appl. Probab. 21 (2011)) give a simple iteration for this system and prove that it converges geometrically fast whenever a solution exists, at a rate that does not deteriorate with the number of vertices, and that it detects when no solution exists. The same estimate is then used in the paper's consistency theorem for the maximum likelihood estimator (Theorem 1.3) and in its graph-limit theorem (Theorem 1.1). This mission formalizes that algorithmic result, Theorem 1.5, together with the chain of numbered displays in Section 2 that proves it.
Let and label the vertices . For , the -model puts an edge between distinct vertices and independently with probability
Given an observed graph with degrees , the maximum likelihood estimate must satisfy the ML equations
The sup norm of is . For put , and define the map by
Starting from any , the fixed-point iteration is . The fixed points of are exactly the solutions of (3).
For an matrix , the operator norm is . For , the class consists of the matrices with , and for . For , is the matrix with entries .
There are functions and , continuous, independent of and , such that for every and every : if (3) has a solution , then , it is the unique solution of (3), and for all and
and if (3) has no solution, then every orbit is unbounded.
and . 6. (10), p. 13: a single , continuous in its arguments, with and .
The theorem turns an implicit statistical object, the MLE of an -parameter model, into the limit of an explicit iteration with three guarantees: a convergence rate that depends on the size of the parameters but not on ; an a posteriori error bound in terms of the computable step ; and a certificate of non-existence. The uniqueness of the MLE comes out of the same estimate. In the paper, the a priori bound is the device that proves consistency of the MLE (Theorem 1.3, applied with ), and the two-step contraction is reused in the proof of the graph-limit theorem.
The result is proved in the paper; no machine-checked proof of it is known. The work here is to formalize the known proof. The matrix inequality of Lemma 2.1 and the derivative bounds (6)–(7) are self-contained and can be attacked independently of the iteration.
The obvious approach is to show that is a contraction and apply Banach's fixed-point theorem. This fails: every row of the Jacobian of has absolute sum exactly , so is only non-expansive in the sup norm, never strictly contracting. Contraction appears only for the two-step map , through the sign pattern of the Jacobian (positive diagonal, uniformly negative off-diagonal), and only on bounded sets, with a factor that tends to as the norms grow. A second difficulty is uniformity: the factor must be bounded away from independently of , which needs , hence . For the converse, there is no fixed point to anchor the orbit, so boundedness of the orbit has to be converted into convergence before a fixed point exists.
Fin n ; vectors are Fin n → ℝ, whose Mathlib norm is the sup norm . Matrix norms are the explicit maximal absolute row sum.Needed infrastructure: calculus of (derivatives of of a sum of exponentials), the integral form of the mean value theorem for maps , and elementary matrix-norm estimates. The class and Lemma 2.1 are reusable for other diagonally dominant iterations. Proofs of any milestone are welcome, in any order.
A reinforcement-learning agent that does not know its environment has to act and learn at once. Each step spent gathering information about unfamiliar states is a step not spent collecting reward, and an agent that only exploits what it already knows may never find better behaviour. Chapter 8 of Kakade's thesis (Kakade 2003) turns this trade-off into a counting question. Run an algorithm for an arbitrarily long time on one unbroken path of experience, with no resets. At how many timesteps does it fail to act optimally with respect to a fixed planning horizon ? Kakade calls this number the sample complexity of exploration.
The question builds on two algorithms. (Kearns and Singh 2002) gave the first polynomial-time guarantee for near-optimal behaviour in an unknown MDP. (Brafman and Tennenholtz 2002) replaced 's explicit explore-or-exploit switch by optimism: unknown states are treated as maximally rewarding. Kakade's chapter sharpens the analysis of . For deterministic MDPs it shows that the number of non-optimal steps is at most , which matches its own lower bound. The thesis notes that its deterministic results are similar to those of Koenig and Simmons (1993), with the dependence on , and made explicit (pp. 99, 104). The later PAC-MDP literature (for example Strehl, Li and Littman 2009) took this counting notion as its standard measure of exploration efficiency.
An MDP has a finite set of states, a finite nonempty set of actions, a transition model and a deterministic reward . A deterministic MDP has a next-state map , with exactly when .
Online model. An algorithm is a deterministic function that maps the path observed so far, , to the next action . Started at , it produces one path ; is the subpath up to . The -step end time of is the smallest multiple of larger than . The -step value of the algorithm on is the normalized reward it collects until ,
and is the supremum of this quantity over all algorithms continuing from .
-step policies. A -step policy is a sequence of deterministic decision rules . Its -value is , and is the supremum over -step policies. For a set of states , the induced MDP agrees with on and makes every state outside absorbing with reward . The escape probability is the probability that the path of in leaves . A transition model is an -approximation to if for every .
For every , and there is one algorithm such that, for every deterministic MDP with rewards in , every start state and every ,
The result. The bound does not depend on . However long the agent runs, only a fixed number of its steps fail to be -step optimal. The thesis's Theorem 8.3.6 shows that every algorithm has such steps on some deterministic MDP, so for deterministic MDPs the upper and lower bounds coincide. The induced-MDP lemmas carry over unchanged to stochastic MDPs. Together with Lemmas 8.5.4 and 8.5.5, they give the chapter's general bound (Theorem 8.3.1). They are the template for later optimism-based analyses, which compare an optimistic model with the true one and charge the difference to the probability of leaving the known region.
Formalizing it. The results are proved in the thesis; neither Mathlib nor the Prove2Me catalog contains a machine-checked version of any of them. A complete development would contain:
The proof of Lemma 8.5.5 in the thesis uses a Chernoff bound of the form . This form fails for the upper tail when , so the pinned statement needs a different argument.
The algorithm must be fixed before the MDP. It knows nothing about or beyond what its own path reveals, yet the count has to hold for every MDP, every start state and every run length at once. A direct approach could explore each state-action pair once and then plan. That does not bound the count. Exploration is interleaved with exploitation, the agent can only reach unknown pairs through known states, and every step on the way is judged against the full -step optimum of the current cycle. The work lies in charging each non-optimal step to a distinct newly tried state-action pair, with at most steps charged per pair, while the planning policy is recomputed every time the set of known states grows. In the stochastic lemmas, the main issue is that is a supremum over all -step policies, so the comparison has to go through for every competing policy, not only the planner's.
IsTransitionKernel functions .List (S × A × ℝ) → S → A. The run is defined by recursion and is infinite. is the realised normalized sum up to the end time, and is the backward recursion , which is the supremum over algorithms by the Markov property. The count runs over for every .Four formalizations would make the goal trivial or false, and each is excluded:
Reusable beyond this mission are the finite-horizon value layer, the induced-MDP and escape-probability lemmas, and the concentration bound. Contributions to any of these are useful independently of the goal.
Planning in a Markov decision process with a large or infinite state space cannot visit every state. The trajectory tree method of Kearns, Mansour and Ng (2000) finds a near-best policy in a class with a number of generative-model calls independent of the state space, but exponential in the horizon . Chapter 6 of S. M. Kakade's PhD thesis, On the Sample Complexity of Reinforcement Learning (University College London, 2003), trades that exponential factor for a weaker notion of optimality. The weaker notion is tied to a reset distribution that encodes prior knowledge of where good policies spend their time, such as a desired trajectory in robotic control or a known operating regime of a queueing network.
The resulting algorithm, μ-PolicySearch, chooses one decision rule per time step, backward in time, from a hypothesis class , optimizing each against states drawn from . The same idea was later published as Policy Search by Dynamic Programming (Bagnell, Kakade, Ng and Schneider, NeurIPS 2003). Conservative policy iteration (Kakade and Langford, ICML 2002) carries the same reset-distribution idea into the discounted setting.
Timeline:
A T-epoch MDP has a finite state set , a finite nonempty action set , a transition kernel , a deterministic reward and a horizon . Decision epochs are . A non-stationary policy gives a distribution over actions at each state and epoch. A decision rule is a map . A class of decision rules induces the class of deterministic policies that use a rule of at every epoch.
Values are normalized. The -value is times the expected reward collected from epoch to when starting in at epoch , so . The value is . The state-action value is , and the advantage is . The future state-time distribution of from is on .
A μ-reset distribution is a family of distributions on , one per epoch . Its joint law, uniform over epochs, is . For a decision rule the μ-advantage is
and is defined in the same way. The ℓ1 distance of two functions on is .
If a policy satisfies for all and , then for all and all start states ,
Theorem 6.3.1 states what μ-PolicySearch buys. The guarantee holds at every start state, whereas the trajectory tree guarantee holds only at the root it was built for. The policy is guaranteed to compete with each policy of whose future state-time distribution is close to . The penalty makes the role of the reset distribution precise: it is the price of the change from the "training" distribution to the "test" distribution . With Theorem 6.3.2 at , the exact algorithm attains the bound with no slack. The sample-based analysis (Theorem 6.3.3) reduces to controlling the condition.
The results are proved in the thesis, and no machine-checked version is known to exist. The mission produces a Lean development of the normalized T-epoch model (non-stationary policies, -values, advantages, future state-time distributions) together with the undiscounted performance difference lemma. These pieces are the common substrate of Chapters 4–6 of the thesis and of later finite-horizon policy-search analyses.
The performance difference lemma relates two objects defined in opposite directions of time: the state distribution of runs forward from , while the -values of are defined backward from the horizon. A formal statement must keep the epochs of the two aligned, including the boundary epochs and . The change of measure needs the bound , which holds only because values are normalized and rewards lie in . With unnormalized rewards the constant in front of the ℓ1 term is wrong.
A first idea is to read the hypothesis as "the advantages are small under ". That reading is not available. The hypothesis controls averages under only, and the gap between the two distributions is exactly the penalty term.
Fintype S), so expectations and the ℓ1 distance are finite sums. The thesis also allows infinite state spaces in this chapter, with integrals in place of sums.π t s a together with a validity predicate. Deterministic policies enter as indicator policies .The T-epoch layer (policies, state distributions, values, advantages, the future state-time distribution) is shared with the other missions of this series (namespaces SampleComplexityRL.PolicyGrad and SampleComplexityRL.Mismeasure); the μ-reset objects are defined in SampleComplexityRL.MuPolicySearch; IsTransitionKernel and IsPolicy are published definitions. Contributions of the performance difference lemma and of general facts about the T-epoch layer (values in , sums to one) are welcome.
Let be a connected graph and a set of vertices of even cardinality. A -join is a set of edges in which exactly the vertices of have odd degree. A -cut is a cut with odd. Write for the minimum size of a -join and for the maximum number of pairwise disjoint -cuts. Every -cut meets every -join, so . When equality holds is a central question of combinatorial optimization because of its links to integral multiflows. Seymour (1981) proved equality for all in bipartite graphs. Middendorf and Pfeiffer (1998) showed that deciding equality is NP-complete.
Korach and Penn (1992) proved that a minimum -join with connected components satisfies
So a minimum -join with few components certifies a large packing of -cuts, and a connected one certifies . Sebő and Tannier (Math. Oper. Res. 2004) therefore study the problem MTSC: given , and an integer , is there a minimum -join with at most connected components? They show it can be solved in polynomial time for and is NP-complete in general (their Theorem 5). The hardness proof reduces three-dimensional matching (3DM) to MTSC. This mission formalizes the correctness of that reduction.
Three-dimensional matching. An instance consists of three pairwise disjoint sets , , , each of cardinality , and a set of triples . A matching is a subset in which every element of occurs in exactly one triple.
The graph . Take a further set of points and put , so . The graph has as vertices the points of , the triples of , and one new vertex for every unordered pair of distinct points of . Its edges are:
There are no other edges. In Lean, is gadget q H and is gadgetT q H.
-joins and components. For and a vertex , is the number of edges of at . is a -join (IsTJoin) if is odd exactly for . It is a minimum -join (IsMinTJoin) if no -join of is smaller. The connected components of are those of the graph , where is the set of endpoints of edges of . Their number is numComponents F.
This statement is quantified over every and every , and it is the full mathematical content of the reduction.
The result. The Claim shows that minimizing the number of components of a minimum -join is NP-hard. A Korach–Penn certificate for a large packing of -cuts therefore cannot in general be found by optimizing the component count. This sets the case, which Sebő and Tannier solve in polynomial time through isometric embeddings of tree metrics, apart from the general case.
Formalizing it. The Claim is proved in the paper, in one paragraph. No machine-checked version is known, and the platform has no -join library. The mission produces a reusable vocabulary for -joins, minimum -joins and the components of an edge set, together with a checked proof that a concrete gadget is correct. One sentence of the published argument is false as written (see Difficulty); a formal proof settles the conclusion independently of it.
The direction from a matching to a -join is a direct verification. The converse has to control an arbitrary minimum -join: its size, the shape of each of its components, and how the components meet , and . A first reading of the printed proof suggests that every vertex outside that carries edges of is adjacent to at most one vertex of each of , , . This is false for the inner vertex of a path joining two vertices of the same class, and the construction joins every pair of points of , including pairs inside . Such components really occur in minimum -joins, so the count of components has to cover them as well. The stated conclusion (at least components, with equality only in the matching-like configuration) remains true.
On the Lean side, the components of an edge set are not the components of the graph with that edge set on all vertices: there every untouched vertex would be a component, and the Claim would become false.
Fin q), so their disjointness holds by construction. and are finite sets of triples in Fin q × Fin q × Fin q. IsMatching q M requires each element of each class to be the corresponding coordinate of exactly one triple of , and is a separate hypothesis. A covering-only or at-most-one version would be a different problem.Sym2) and is a Finset of edges of . Parity uses . Minimality is " for all -joins ", never an infimum on .Contributions welcome: proofs of the milestones, general lemmas on -joins (a -join in a graph where is independent has at least edges), and lemmas on the components of an edge set, which are reusable well beyond this mission.
UnrelatedSched.ThreeHalves.ThreeDimMatching (Lenstra–Shmoys–Tardos) encodes 3DM with an indexed family of triples and the covering form of a matching, a different encoding from the paper's set with "exactly one".Supply disruptions — fires, quality failures, capacity shortfalls at a supplier — are a first-order risk in manufacturing supply chains. A buying firm has two broad responses. It can dual source, splitting orders between suppliers so that one supplier's shortfall is partly covered by the other, or it can invest in process improvement at a single supplier (kaizen events, supplier development programmes) to make that supplier more reliable. Wang, Gilland and Tomlin, Mitigating Supply Risk: Dual Sourcing or Process Improvement? (M&SOM 12(3):489–510, 2010), build a two-stage newsvendor model that captures both levers and compare them analytically.
This mission formalizes the paper's analysis of the improvement lever on its own: the firm commits early to one supplier, decides how much effort to spend improving it, and then orders. The paper's Theorem 3 shows that, without committed costs, this improvement problem is a concave program with an explicit first-order condition, and its Corollary 2 derives how the optimal effort responds to costs, revenue and the chance that improvement succeeds. These are the facts the paper's later comparisons between improvement and dual sourcing rest on.
A firm sells one product over one season at unit revenue , salvage value and unit penalty for unmet demand. Demand has distribution function and finite mean. The firm orders units from a supplier with design capacity , unit cost and committed cost : the firm pays when units are delivered.
The supplier suffers a random capacity loss and delivers . The law of has a continuous distribution function that depends on the supplier's reliability index ; a larger index means a stochastically smaller loss, for . Demand and losses are independent.
With and , the second-stage expected profit at index is
and is its optimal value.
In the first stage the firm may improve the supplier from its initial index . The paper reparametrizes effort by the target index: reaching index needs effort , where is convex and nondecreasing with . Effort costs per unit and succeeds with probability . The first-stage profit of early commitment is Eq. (7):
Assume and that is concave on for every (decreasing marginal reliability improvement). Then is concave on , and an optimal index , with an optimal order at , satisfies
Theorem 3 turns the firm's improvement decision into a one-dimensional concave program, so that the first-order condition (8) characterizes the optimum and comparative statics are available. Corollary 2 is the managerial content: cheaper or more reliable improvement, a cheaper supplier and a more valuable product all justify more improvement effort. The paper's later results — when late commitment beats early commitment (§4.2.2) and when single sourcing with improvement beats dual sourcing (§5) — compare the optimal values these results describe.
The results are proved in the paper's online appendix; none of them has a machine-checked proof. A complete development provides formal proofs of the layer-cake representation of the random-capacity newsvendor profit, of its critical-fractile solution, and of the concavity and envelope arguments on top of it.
is an optimal value, a supremum over order quantities, and suprema of concave functions are not concave in general. The obvious route — " is concave in for each , hence so is the supremum" — fails, because is not concave in for a fixed beyond the critical fractile. Any argument has to control how the optimal order moves with under random capacity, where the delivered quantity is a minimum of the order and a random effective capacity. The first-order condition then requires differentiating an expectation of a non-smooth function of in the parameter of 's law. Corollary 2 must be argued on the set of maximizers, since is concave but not strictly concave.
The Lean development lives in the namespace MitigateSupplyRisk.Improvement. Model bundles , a demand law and the family of loss laws; and are their cdf. Expectations are Bochner integrals over and over the product . Model.Assumptions collects the standing assumptions of §3: , , (implicit in the paper's division by ), a nonnegative integrable demand, nonnegative atomless losses, and the stochastic order in . Demand needs no density. Effort bundles with , and convex, nondecreasing on , ; taking as primitive assumes every index is reachable. is a real supremum and is built from it, never from the critical fractile. Every statement about carries or , which makes the supremum finite. "Optimal" always means a maximizer over the whole feasible set, and "increasing" is weak throughout, as on p. 492 of the paper.
The paper's proofs are in an online appendix that was not used here. Deviations from the page, each disclosed in the item's Formalization Note:
A trivializing formalization is ruled out: is built from the supremum (not from at a fixed order), the supremum is finite under the stated hypotheses, and every expectation is of an integrable function, so no statement holds through a junk value.
Reusable beyond this mission: the random-capacity newsvendor objects (delivered quantity, expected profit, layer-cake representation) and a Topkis-type monotone comparative statics lemma on a chain. Contributions of either, and proofs of the milestones in any order, are welcome.