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?
A polytope may be described by its vertices or by its facets. These descriptions can differ sharply in size even when every vertex has only binary coordinates. Grünbaum's account of 0/1-polytopes in §4.9 records a result of Bárány and Pór: the maximal number of facets grows superexponentially with dimension. The result is an existence statement about the geometry of binary coordinate sets. The source describes random polytopes as witnesses, without specifying a probability distribution as part of the theorem.
Fix a dimension . A -polytope here is a nonempty convex hull of finitely many points in with full affine span. A 0/1-polytope is the convex hull of a subset of . Both properties are required of the witness. A facet is a nonempty exposed face of affine dimension . The count uses the book's convention that the empty face has dimension and is excluded from natural-indexed face counts. This representation follows Grünbaum §§2.4 and 3.1 for faces and full-dimensional polytopes, and §4.9 for the binary coordinate family.
The single source obligation is the unnumbered Bárány–Pór assertion quoted by Grünbaum in §4.9, printed p. 69a (PDF p. 94). In mathematical notation, the statement is
The constant and threshold are chosen before ; the witness may depend on . The logarithm in Lean is natural logarithm. Changing a fixed logarithm base rescales the existential constant. The result is asymptotic: it does not assert the inequality in every small dimension. The threshold also keeps the natural-number expression in the facet dimension away from underflow.
The goal item Grunbaum2003.barany_por_binary_facet_growth carries this entire obligation. Its body is sorry, so the package presents a compiled statement, not a machine-checked proof. There are no separate source lemmas in this mission and no milestones to assert beyond the goal.
The theorem shows that binary vertex coordinates do not impose a merely exponential ceiling on the number of facets. It gives a family of full-dimensional binary polytopes whose facet counts eventually exceed an expression of the form for one fixed . A formal proof would establish that family in the chosen polytope and face-count representation. The present statement makes the quantifier order, full-dimensionality, binary-coordinate restriction, and strict facet inequality explicit for such a proof.
The existence of many binary vertices alone does not certify many facets: one must establish distinct supporting faces of codimension one. The source attributes the strong lower bound to a random construction. A proof must connect that construction to the geometric facet count while keeping one constant valid for every sufficiently large dimension. The mission statement leaves the construction method to the proof, as the quoted book assertion supplies no probability-space parameters or probability bound.
Lean represents a point of by Fin d → ℝ and a polytope by a set of such points. IsDPolytope requires a finite nonempty convex-hull presentation and full affine span. IsZeroOnePolytope requires a convex-hull presentation whose generators have every coordinate equal to zero or one. faceCount P k uses the finite cardinality of nonempty exposed faces of affine dimension ; for the full-dimensional witness, faceCount P (d - 1) is the facet count. No face-finiteness, simplicity, or probabilistic assumption is added to the theorem.
The package uses these three expression-essential definitions and the Mathlib real-power and logarithm notation. IsDPolytope and faceCount match the definitions already staged for other missions in this textbook series. A proof may reuse geometric lemmas or supply a new formal version of the Bárány–Pór construction, provided it proves the stated inequality for the original full-dimensional binary family.
source.pdf, PDF pp. 35, 51, 94).A polytope can be given by a list of vertices, a list of inequalities, or much less explicit access. The last case arises when geometric information is available through queries to a physical or computational object but a full description is unavailable. Grünbaum's account of a result by Gritzmann, Klee, and Westwater asks how much of a polytope can be recovered when each query shoots a ray from a known interior point and reports where it meets the boundary. The target is the complete face lattice, including incidence among faces of every dimension, and the cost is the number of oracle calls. The result appears in Convex Polytopes, §3.6, printed pp. 52b–52c (PDF pp. 74–75 of the supplied source).
Fix a positive integer . A -polytope is a nonempty finite convex hull in real coordinate space whose affine span is the whole space. The origin is known to lie in the interior of . A ray query supplies a nonzero direction ; the oracle returns the intersection of the positive ray with the boundary of . The theorem requires this boundary-point property for every nonzero direction. It does not give the reconstruction program the vertices, inequalities, face counts, or coordinates of .
A face is represented by an exposed subset of , ordered by inclusion. The resulting face lattice includes the empty and whole faces. For , counts nonempty faces of affine dimension ; hence is the vertex count and is the facet count. The empty face has dimension in the book's convention and is excluded from these natural-indexed counts. These conventions follow Grünbaum §§2.4 and 3.1 (printed pp. 17 and 31; PDF pp. 35 and 51).
The single source obligation is the unnumbered Gritzmann–Klee–Westwater theorem of Grünbaum §3.6. For each , one finite exact-real ray-query program works for every eligible and every correct ray oracle for . It halts with an encoding of the entire face lattice after at most
queries. The square on the facet count, both coefficients, and the continuation of “queries” across the page break are part of the printed statement. The program is selected before the unknown polytope and its oracle. The finite running time and output may depend on the instance. No common output, fixed runtime bound, or bit-complexity bound is asserted.
The Lean declaration is Grunbaum2003.ray_oracle_face_lattice_reconstruction. It asserts existence of the program, universal correctness, finite termination in a halt instruction, the displayed query inequality, and a concrete encoding of the whole face lattice. Its body is sorry: this package is a compiled statement and does not claim a machine-checked proof.
The conclusion recovers all face incidences from boundary samples on rays from one interior point. It is stronger than recovering only a vertex or facet list because the output explicitly determines the ordering of all faces. The bound measures the information requested from the oracle; the source does not constrain the number of internal arithmetic steps. A formal proof would connect the geometric reconstruction argument to a precise query machine and establish that its output matrix has exactly the claimed faces and inclusions.
Ray answers are geometric points, while the desired output is a global combinatorial structure. Sampling one direction per visible feature gives no direct certificate that all faces and incidences have been found. In particular, a proposed reconstruction must use only the permitted oracle answers and still know when its finite description is complete. The theorem also needs a uniform program for every polytope in a fixed dimension, with the instance dependent query count above. The present statement makes these quantifier and resource requirements explicit.
The machine has a finite instruction list for rational constants, exact real arithmetic, sign branches, tape movement, oracle queries, and halt. Its tape begins at zero. A query reads a nonzero direction from the tape and writes back the oracle's boundary answer; only this instruction increments the query counter. A zero direction, invalid label, or division by zero fails instead of creating a successful execution. Thus an unrestricted oracle value at zero cannot certify the theorem. Arithmetic and sign tests are exact real operations, matching the source's query model rather than imposing a bit model.
The output is a self-delimiting Boolean inclusion matrix indexed by a finite type. A bijection connects its indices to all exposed faces of , and each matrix entry is one precisely when the associated faces are ordered by inclusion. This rules out an output consisting merely of face counts, vertices, or facets. IsDPolytope, faceCount, PolytopeFace, the ray-oracle predicate, machine syntax and execution, and the output predicate are the expression dependencies of the goal. The exposed-face subtype and full-dimensional polytope predicate are shared unchanged with this book's other staged missions. Contributions needed for a proof may include geometric face finiteness and reconstruction lemmas, but those are not added as unreviewed mission items here.
source.pdf, PDF pp. 74–75).Every consistency guarantee for an empirical-risk-minimization procedure — the Lasso, kernel ridge regression, maximum likelihood — ultimately rests on relating an empirical average to its population expectation, uniformly over the class of candidate functions or parameters being searched. Chapter 4 established the classical form of this connection: a uniform law of large numbers, bounding by an absolute quantity governed by the (unlocalized) complexity of . Such a bound is often wasteful: it treats a function with small population norm the same as one with large population norm, when intuitively the empirical and population norms of a small function should already agree closely. This mission formalizes the sharper, localized form of this uniform law — the same localization principle Chapter 13 used for nonparametric least squares, now applied directly to the empirical-versus-population norm comparison itself, giving relative rather than absolute control and recovering optimal convergence rates that the unlocalized theory misses.
Fix a probability distribution over a covariate space and i.i.d. samples . For , the population norm is and the empirical norm is ; by linearity of expectation, , so the question is how tightly concentrates around , uniformly over a function class . A class is star-shaped around the origin if , and -uniformly bounded if for every . The relevant complexity measure is the population localized Rademacher complexity
where are i.i.d. Rademacher signs independent of the samples — note that, unlike Chapter 13's Gaussian complexity for fixed design points, this expectation integrates out the randomness of the samples themselves, since this chapter treats as genuinely random throughout. A critical radius is any positive solution of .
Theorem 14.1 (goal). Given star-shaped and -uniformly bounded, and solving the critical inequality, for any ,
with probability at least ; and if additionally ,
with probability at least .
Theorem 14.1 is the technical engine behind two of the book's other sharp results: Example 14.2's derivation of the optimal rate for bounded quadratic function classes (where the unlocalized analogue of this theorem only achieves the slower rate), and, more broadly, every later argument in the book that needs to translate an empirical-norm guarantee (as produced directly by an M-estimator's optimality, e.g. Chapter 13's nonparametric least-squares bounds) into a population-norm guarantee, or vice versa. The gap between the "absolute" uniform law of Chapter 4 and the "relative" one here is exactly the difference between a bound that is only informative for functions of order-one population norm, and one that remains sharp arbitrarily close to the origin — which is precisely where a consistent estimator's error eventually lives. Formalizing the statement produces, for the first time on the platform, the localized-Rademacher-complexity vocabulary at the population level (as opposed to Chapter 13's fixed-design Gaussian-complexity version), reusable by any future mission needing to pass between empirical and population norms.
The naive approach — apply Hoeffding's inequality to for a fixed , then union-bound (or apply the unlocalized Rademacher-complexity uniform law of Chapter 4) over — gives a bound whose complexity term does not shrink as , since it uses the complexity of all of regardless of a given function's own size. This is exactly the sub-optimality Example 14.2 exhibits concretely: the naive bound gives rate where the truth is . The fix is not merely technical bookkeeping — it requires a genuine peeling argument over dyadic norm-scales (exactly as in Chapter 13's proof of Theorem 13.13), applying the localized complexity at the scale appropriate to each individual , and controlling the resulting geometric sum of tail probabilities across scales. A reader's first instinct — bound in terms of and substitute — is circular, since is itself the random quantity being controlled.
The covariate space X carries an arbitrary MeasurableSpace structure (no topology
needed for the statement); the sample sequence and the Rademacher signs are both represented
as families of measurable functions on a shared probability space Ω, with their joint
independence stated as a single IndepFun between the two vector-valued sequences (rather
than building a combined-index iIndepFun), since it is the two sequences — not each pair
of individual variables — whose independence the book invokes. The two conclusions of Theorem
14.1 are stated as a conjunction with the second gated behind its own extra hypothesis, never
collapsed into a single implication, since the book's own statement keeps them syntactically
and logically distinct (the second requires a strictly stronger and additional condition on
top of the first's). The universal constants (c1,c2,c0,c1',c2') are quantified before every
instance object, so they cannot secretly depend on the function class, sample size, or radius.
Every f ∈ F is required measurable (hF_meas, added in revision): the book's own framing
implicitly restricts to measurable, square-integrable f throughout (p. 454), and without this
hypothesis the population norm popNormSq, which appears directly in the goal's conclusion,
could silently take Mathlib's Bochner-integral junk value 0 for a non-measurable,
pointwise-bounded member of a star-shaped, uniformly-bounded F.
The trivializing formalization ruled out here is stating the localization constraint at the
empirical rather than population norm in popRademacherComplexity — this chapter's whole
point (contrast Chapter 13's Gn, correctly localized at the empirical norm since there the
design is fixed) is that 's localization is a population-level object,
precisely because the samples are random here. Welcome future contributions: Corollary 14.3's
covering-number sufficient condition for the empirical version of the critical inequality,
and Theorem 14.20's Lipschitz/strongly-convex cost-function uniform law, both deferred from
this mission (see STATUS.md) as they need substantial additional apparatus (metric entropy
integrals; cost functions and strong convexity) beyond what Theorem 14.1 itself requires.
Many high-dimensional data sets — gene-expression profiles, sensor networks, social interactions — come with no natural ordering of variables, only pairwise dependencies whose structure is itself the object of interest. A graphical model encodes these dependencies as an undirected graph: vertices are variables, and edges mark direct (conditional) dependence. Recovering the graph from samples — graphical model selection — is a combinatorial problem masquerading as a statistical one: there are candidate graphs on vertices, far too many to search directly. For Gaussian data, however, graph structure is exactly the sparsity pattern of the inverse covariance (precision) matrix, which turns graph selection into coupled sparse-regression problems — one per vertex — each of which the Lasso theory of Chapter 7 already knows how to solve. This mission formalizes the theorem, due to Meinshausen and Bühlmann (2006), that shows this reduction actually works: solving independent Lasso problems and combining the results recovers the exact graph with high probability, at a sample complexity governed by the same kind of incoherence condition that governs Lasso support recovery itself.
An undirected graphical model on a finite vertex set pairs a graph with a random vector . Two equivalent structural properties connect to (Theorem 11.8, Hammersley-Clifford): factorizes according to if its density is a product of nonnegative functions, one per clique of , each depending only on the variables in that clique (Definition 11.1); is Markov with respect to if, for every vertex cutset separating into disjoint pieces and , the sub-vectors and are conditionally independent given (Definition 11.5). For a strictly positive density, these are the same condition.
For a zero-mean -dimensional Gaussian vector with covariance and precision matrix , the graph structure is exactly the support of : . The neighborhood of each vertex is itself a vertex cutset (separating from everything else), so the conditional independence holds, and — by standard Gaussian conditioning — decomposes as a linear function of plus independent Gaussian noise, with regression coefficients supported exactly on . Neighborhood regression exploits this directly: for each vertex , solve the Lasso
read off , and combine the per-vertex estimates into a single edge set via the OR rule ( iff or ) or the more conservative AND rule (iff both hold). The relevant incoherence condition, analogous to Chapter 7's, is stated for a positive definite matrix and subset : is -incoherent with respect to if .
Theorem 11.8 (Hammersley-Clifford). Factorizes G p ↔ IsMarkov G X P for any strictly
positive density .
Theorem 11.12 (goal — graph selection consistency). Suppose for every , is -incoherent with respect to , and . With , the neighborhood-Lasso estimate combined via either rule satisfies, with probability at least :
Theorem 11.12 is the statistical justification for one of the two standard approaches to Gaussian graphical model selection (the other being the penalized-likelihood "graphical Lasso" of §11.2.1). Its significance is computational as much as statistical: rather than solving one -dimensional penalized-likelihood problem, neighborhood regression solves independent, embarrassingly parallel Lasso problems, each of dimension — a substantial practical advantage at scale, with (as this theorem shows) no loss in statistical guarantee. Formalizing it produces, for the first time on the platform, statement-level infrastructure for undirected graphical models (Hammersley-Clifford, the Markov property via vertex cutsets, neighborhood structure) together with the random-design analogue of the Lasso support-recovery machinery — a genuinely different technical regime from Chapter 7's fixed-design Lasso theory, since here the "design matrix" is itself Gaussian and statistically coupled to the response through the very covariance structure being estimated. As with the other missions in this series, only the statements are formalized here; the proofs (an extension of the primal-dual witness technique to random design, per the book's own proof sketch) are left as the draft goal for future proof contributions.
The proof of Theorem 7.21 (Chapter 7's Lasso support-recovery guarantee) is for a deterministic design matrix, with all randomness confined to the additive noise. Here the "design" is itself random and Gaussian, and — critically — it is statistically dependent on the very quantity (, encoded in 's support) the Lasso is trying to recover, since 's own covariance structure is exactly what the incoherence condition constrains. The naive approach of just conditioning on the realized design matrix and invoking Theorem 7.21 fails, because the deterministic-design incoherence condition would then need to hold for the sample covariance , not the population covariance that is actually assumed — and controlling the gap between sample and population incoherence under the joint (not fixed) randomness of predictors and response is exactly the extra step the book's proof needs, handled via an extension of the primal-dual witness technique that tracks both sources of randomness together.
The vertex set V is an arbitrary finite type; the covariate space for X is ℝ
throughout (all variables jointly Gaussian). The Gaussian design is characterized via its
one-dimensional projections (every linear combination is univariate Gaussian with the matching
variance) rather than via Mathlib's multivariate-Gaussian machinery directly, to keep the
definition self-contained. IsAlphaIncoherent's ambient index set is realized as a subset of
the full vertex type rather than as a literal submatrix, since the book's condition never
references an entry outside it. The theorem states the conclusion jointly for both the
OR-rule and AND-rule estimated edge sets on one shared high-probability event, matching "based
on either rule" literally rather than picking one. The trivializing formalization ruled out
here is treating the neighborhood-Lasso estimate as a fixed-design Lasso problem (silently
dropping the joint randomness of predictors and response) — every design realization in this
formalization is the actual random vector Xdes i ω, not a deterministic parameter, and the
Gaussian design hypothesis (IsIIDGaussianDesign) is stated over the same probability space
Ω as the least-squares residual. Theorem 11.8 (Hammersley–Clifford) is formalized only for the
continuous case — a random vector with a density with respect to Lebesgue measure — matching
what the Gaussian goal (Theorem 11.12) actually needs; the book's own Definition 11.1 also
permits a discrete (counting-measure) density, with the Ising model (Example 11.4) as a worked
instance, which this mission does not cover. Contributions welcome: the graphical Lasso's own
guarantees (Propositions 11.9, 11.10, deferred from this mission — see STATUS.md), and the
proof of Theorem 11.12 itself via the primal-dual witness extension the book sketches.
A striking fact discovered by Dvoretzky in the 1960s (conjectured by Grothendieck, and sharpened into its modern quantitative form by Milman in 1971) is that every high-dimensional convex body, however irregular, contains a round slice: a random low-dimensional section (or projection) of any bounded convex set in is, with high probability, close to a Euclidean ball — provided the dimension of the slice is small enough relative to a single geometric parameter of the body. This is remarkable because it holds for every bounded set, arbitrarily irregular; no special structure is assumed beyond boundedness. This chapter proves the theorem in its Gaussian form, as a culmination of every geometric and probabilistic tool the book develops: chaining and Dudley's inequality (Chapter 8), the matrix deviation inequality (Chapter 9), and Gaussian width and the stable dimension (Chapter 7) all combine into a single closing argument.
Fix a subset . For a standard Gaussian vector , the Gaussian width of is (Chapter 7), and the stable dimension of a bounded is up to an absolute constant factor (Definition 7.6.2) — a robust substitute for the ordinary linear-algebraic dimension of , which can jump discontinuously under a small perturbation of , unlike .
An Gaussian random matrix with i.i.d. entries is a random matrix each of whose entries is an independent standard normal random variable.
for every Gaussian random matrix with i.i.d. entries, every bounded containing the origin, and every , where is the Euclidean ball of radius centered at the origin. The probability is the book's own literal numeral, not a free parameter — this is the theorem the book actually states, not a family of theorems indexed by a confidence level.
Dvoretzky-Milman's theorem is one of the foundational results of the local theory of Banach spaces (asymptotic geometric analysis): it says every -dimensional normed space contains an almost-Euclidean subspace of dimension proportional to (a geometric invariant closely related to) in the worst case, and much larger for spaces whose unit ball is already well-behaved (the stable dimension of the cube , for instance, is proportional to itself — Example 11.3.6). This underlies results throughout convex geometry, compressed sensing, and high-dimensional statistics wherever a random low-dimensional projection needs to be shown to preserve geometric structure. The book's own framing makes clear why this chapter is placed last: the theorem's proof is a genuine capstone, invoking Chevet's inequality (itself built from the matrix deviation inequality of Chapter 9, which is built from chaining, Chapter 8) as its main technical tool.
The theorem and its proof are classical (Milman 1971; this book's specific route via Chevet's inequality is a standard modern exposition). This mission formalizes the goal theorem's statement — including its two supporting geometric quantities, Gaussian width and stable dimension, and the notion of a Gaussian random matrix — as a complete, faithful target for a solver, in the book's own sub-namespace built for this chapter (no dependency here is reusable from an earlier chunk, since none of this book series' Chapter 7 or Chapter 9 definitions has yet been published).
The natural first idea — bound directly using concentration of for each fixed — runs into exactly the uniform-supremum obstacle the whole book has been building tools to overcome: a bound that holds for one at a time, even with a union bound over a net of , does not obviously extend to the full convex hull without first controlling uniformly over both and on the unit sphere of the target space — a two-parameter supremum. The book's actual route goes through Chevet's inequality, itself proved using the matrix deviation inequality's own chaining-based argument, to control this two-sided supremum, and then converts the resulting inequality into the containment via a support- function duality argument (a convex body is pinned down by its support function, so bounding uniformly over on the sphere is exactly what is needed).
A is Ω → Matrix (Fin m) (Fin n) ℝ with an explicit IsGaussianMatrix hypothesis (entries i.i.d.
, formalized entrywise with joint independence). conv(AT) is convexHull ℝ of the image
of T under A's mulVec, round-tripped through EuclideanSpace's continuous linear equivalence
with the underlying function type. w(T) reuses this mission series' ExpSup/GaussianWidth
convention (redefined locally, per the drafts-cannot-import-drafts rule, following the same
ProbabilityTheory.stdGaussian-based realization of a standard Gaussian vector as
08-matrix-deviation). The stable dimension is formalized directly as rather than via the book's literal (but only asymptotically equivalent, per
Exercise 7.6.1) definition through a squared Gaussian width — the goal theorem's own
proof uses only the inequality direction of that equivalence, and the goal's hypothesis already
carries an unpinned absolute constant that absorbs the equivalence constant, so this substitution
preserves the theorem's exact truth content (see StableDimension's own doc-comment and
MODERATION_NOTES.md for the full argument) rather than approximating it.
Ball-center deviation, disclosed. The book's printed theorem statement carries no hypothesis that contains the origin; its proof opens by translating so that it does ("Translating if necessary, we can assume that contains the origin"), and Remark 11.3.4 then confirms the ball is centered at the origin in that case. This mission states the WLOG-reduced case directly — adding as an explicit hypothesis — rather than also formalizing the translation argument that recovers the fully general (untranslated) statement. This is disclosed as a genuine narrowing of the literal printed statement, though not of what the book's own proof actually establishes.
This mission covers Theorem 11.3.3 only, with no milestones: BRIEF.md explicitly instructs that
if the chapter's full proof chain (general matrix deviation inequality, Chevet's inequality, random
projections of sets — Theorems 11.1.5, 11.2.4, 11.3.1) proves too heavy for the session, milestones
should be cut rather than the goal substituted. All three are left out, not approximated, given
this chapter's five from-scratch definitions already needed for the goal's own statement. ExpSup,
GaussianWidth, StableDimension and IsGaussianMatrix are reusable by any later development
needing Gaussian width, the stable dimension, or a Gaussian random matrix. Solvers' contributions
are welcome on the goal theorem itself and, beyond this mission's current scope, on the three
named milestones.
The central limit theorem says that converges to a normal random variable. Donsker's theorem says something much stronger: the whole rescaled path of the random walk converges to the whole path of a Brownian motion, as a random element of .
The payoff is a machine. Once in , every functional of the path that is continuous — or merely continuous at almost every Brownian path — transfers automatically. The maximum of the walk converges to the maximum of Brownian motion; the fraction of time the walk spends above a level converges to the corresponding occupation time; the last zero before time converges to the last Brownian zero before time , which is how the arcsine law escapes the simple random walk it was proved for. This is the invariance principle of Erdős and Kac: the asymptotic behaviour of a functional of should not depend on the step distribution, as long as the central limit theorem applies.
Chapter 8 of Rick Durrett's Probability: Theory and Examples (Version 5, 2019) proves this by embedding rather than by the usual tightness argument. Skorokhod's representation theorem puts a mean-zero, finite-variance random variable inside a Brownian motion as the value at a stopping time; iterating puts the whole walk inside one Brownian motion at a sequence of stopping times whose gaps are i.i.d.; and the law of large numbers then forces the embedded walk to be uniformly close to the Brownian path.
Let be i.i.d. with mean and variance , and . Define to be at integer and linear in between, and set
a random element of , the continuous functions on the unit interval with the uniform norm and its Borel -algebra.
On the Brownian side, let be a Brownian motion, and write for its restriction to , again a random element of .
that is, the laws of on converge weakly to the law of Brownian motion. This is a statement about measures on a function space, not about finite-dimensional marginals: it is exactly the extra content over the central limit theorem.
Theorem 8.1.1, Skorokhod's representation theorem: a mean-zero, square-integrable law is the law of for a stopping time with ; Theorem 8.1.2, the embedding of the whole walk, giving stopping times with distributed as the walk and with i.i.d. gaps; Theorem 8.1.5, the continuous mapping theorem for almost surely continuous functionals; and its two workhorse instances, Example 8.1.6 on maxima and Example 8.1.8 on occupation times of half-lines.
The results themselves. Donsker's theorem is the reason the arcsine law, the distribution of the maximum, and the occupation-time law are universal rather than artefacts of the simple random walk for which they were first computed. It is also the prototype for every later functional limit theorem — for martingales in Durrett's section 8.2, for stationary sequences in 8.3, for the empirical process converging to a Brownian bridge in 8.4.
Skorokhod's embedding deserves separate billing. It says any centred law with finite variance sits inside Brownian motion, which is what makes the path-space comparison possible at all, and it is the tool behind the law of the iterated logarithm in Durrett's section 8.5. The construction is a two-point mixture: write the law as a mixture of two-point laws with mean zero, use the exit time of for each, and the exit-time identity integrates to .
Formalizing them. Mathlib has the i.i.d. central limit theorem, convergence in distribution for
random elements of an arbitrary topological space (TendstoInDistribution, with the continuous
mapping theorem and Slutsky), Brownian motion as a process with its invariances, and the machinery
of stopping times for filtered spaces. It has no functional limit theorem of any kind, no Wiener
measure on , no Skorokhod embedding, and no continuous-time optional stopping. Nothing in
the library relates a random walk to a Brownian path.
The goal is the hardest item in this series, and the embedding route is the reason the mission is stated the way it is. Durrett's proof: with and stopping times realizing as , Lemma 8.1.9 says that if in probability for each , then in probability. The hypothesis is the weak law applied to the i.i.d. gaps of Theorem 8.1.2 after Brownian scaling; the conclusion plus the converging-together lemma gives the theorem. The work is uniform control of the Brownian path over shrinking time windows — the modulus of continuity — together with the bookkeeping of the polygonal interpolation.
Skorokhod's theorem needs the two exit-time facts for Brownian motion, Durrett's Theorems 7.5.3 and 7.5.5: takes the values and with probabilities and , and . Both come from optional stopping applied to and , and continuous-time optional stopping is itself not in the library. The mixture identity,
is elementary but needs Fubini and the two expressions for .
Theorem 8.1.5 is the Mann–Wald theorem in the form that allows a discontinuous : Mathlib's
TendstoInDistribution.continuous_comp handles genuinely continuous maps, and the extension to maps
continuous almost everywhere with respect to the limit law is the milestone. Given it, the two
examples are short — the maximum is continuous outright, and the occupation-time functional is
continuous at every path spending no time at the level , which Fubini shows is almost every
Brownian path.
is C(Set.Icc (0:ℝ) 1, ℝ), whose compact-open topology is the uniform one because the
domain is compact, with the Borel -algebra — Mathlib has no measurable-space instance on a
space of continuous maps, so the mission supplies it, and a BorelSpace instance with it.
The polygonal interpolation is written as a finite sum,
which agrees with at integer and is linear in between, and is manifestly continuous,
so walkPath is a genuine element of with no side condition. Both properties were proved
in Lean before publishing rather than assumed. Indexing is from zero, so .
The Brownian limit is brownianPath B, the restriction of the path to . Restriction is a
total function: it returns the zero path for a discontinuous argument. That junk branch is never
reached, because every statement assumes every path of is continuous, not merely almost
every one — one may always modify a Brownian motion on a null set to achieve this, and Durrett's
canonical construction on has it by definition. Without it there would be no
-valued random variable to speak of.
Weak convergence is Mathlib's TendstoInDistribution, the same predicate mission II used for the
Lindeberg–Feller theorem, instantiated at rather than at .
Skorokhod's theorem and the embedding of the walk are stated as existence of a probability space
carrying the Brownian motion, a filtration and the stopping times. This is how Durrett states them
— the construction needs an independent pair alongside the Brownian motion, and he notes
himself that is a stopping time only for the enlarged filtration. The filtration is
therefore an explicit family that is increasing, sits inside the ambient -field, and
contains — the pastSigma of mission V, which this mission imports as a
reference. The stopping-time property is {T ≤ t} ∈ F_t, stated directly rather than through a
bundled filtration structure.
Theorem 8.1.2's conclusion "" is read as equality of the laws of the whole processes: the push-forward of equals the law of the partial-sum process of an i.i.d. sequence with step law , taken on the infinite product measure. The gaps are required to be independent and identically distributed, as the book says.
The counting in Example 8.1.8 is a sum of indicators rather than a filtered cardinality, to keep a decidability side condition out of the statement, and the limit is the Lebesgue measure of as a real number. Example 8.1.6 takes the maximum over , which includes , and the limit is the supremum of over , attained because the path is continuous on a compact interval.
Existence of a Brownian motion is a hypothesis, not a claim, exactly as in mission V, except in Theorems 8.1.1 and 8.1.2 where the existence of a suitable space is the content of the statement and a Brownian motion must be produced; that is Durrett's Theorem 7.1.1, which the library does not yet have, so those two items subsume it.
Contributions welcome beyond the listed items: Lemma 8.1.9 on its own; Theorem 8.1.3, the CLT derived from the embedding; Example 8.1.7, the last zero before time and the arcsine law; continuous-time optional stopping and the exit identities 7.5.3 and 7.5.5 that Skorokhod's theorem rests on; the extension to ; and the martingale, stationary-sequence and empirical-process versions of sections 8.2 to 8.4.
Central values of twists of elliptic-curve and modular-form -functions govern arithmetic questions ranging from Mordell--Weil ranks to the distribution of nonvanishing twists. Classical Iwasawa theory organizes twists whose conductors grow vertically through powers of one prime. Kriz and Nordentoft introduce a horizontal analogue in which the order of the character is fixed while its conductor acquires new prime factors. Their paper Horizontal p-adic L-functions constructs measures encoding these twists and proves a structure theorem that forces quantitative nonvanishing.
The mission formalizes the paper's common mechanism behind its nonvanishing theorems: Fourier theory of horizontal measures, norm-compatible modular-symbol theta elements, interpolation of central values, and propagation from nonzero measures to logarithmic-power lower bounds. The elliptic-curve statements in Theorems 1.1 and 1.2 are obtained in the paper by specializing this mechanism to weight-two newforms and adding the stated Galois-representation hypotheses.
Fix a prime . The digit group is the compact product
A continuous character of has finite image and factors through a finite product. For a complete algebraically closed nonarchimedean field of residue characteristic , a horizontal measure is represented in Lean by a continuous -linear functional on the Banach space . Its Fourier transform is
The integral measures arising from the digit Iwasawa algebra have Fourier norms in a discrete geometric lattice. This is recorded explicitly by HasDiscreteFourierNorm; it is the norm-language counterpart of the discrete valuation hypothesis used in Corollary 2.9.
On the arithmetic side, modular symbols produce theta elements at finite squarefree conductors. Their projection maps do not initially form a compatible inverse system: an Euler factor appears each time a prime is removed. At an orderly prime this factor is a unit, so normalization produces a compatible system and hence a horizontal -adic -function. Evaluation at a character gives the modified central -value of the corresponding twist.
For every nonzero integral horizontal measure , there is a finite set of characters and a constant such that
for some , for every continuous character . If interpolates modified central values, these corrected values are nonzero and have optimal -adic size. This is Theorem 1.6, equivalently the digit-algebra case of Corollary 2.9, combined with Corollary 5.4.
For a modular elliptic curve over , the normalized theta system is assembled into the horizontal -adic -function of Definition 5.3 and shown to satisfy Corollary 5.4. The final milestones then specialize the structure and propagation theorems to prove Theorems 1.1 and 1.2 (assuming modularity), retaining the three alternative hypotheses of Theorem 1.1 and the jointly-good hypothesis for simultaneous nonvanishing in Theorem 1.2.
If a fixed-order family has counting function bounded below by and every character is related to a nonvanishing one by one of finitely many conductor-bounded corrections, the same lower bound holds for the nonvanishing subfamily. This isolates the formal content of Theorem 5.9 used in the applications of Section 5.4.
The structure theorem replaces one-variable Weierstrass preparation in an infinite-dimensional, non-noetherian Iwasawa algebra. It shows that the zero set of a nonzero horizontal measure is rigid enough that finitely many translations detect an optimal Fourier value everywhere. Through interpolation, this converts a single nonzero horizontal -adic -function into infinitely many nonzero complex central values with a quantitative lower bound.
A formal proof will add reusable infrastructure for nonarchimedean Fourier analysis on profinite products, finite group rings, inverse systems of theta elements, and character-counting asymptotics. None of these results currently has a machine-checked proof in Mathlib. The development is arranged so the analytic structure theorem and the modular-symbol construction can be attacked independently.
The central obstacle is that the horizontal Iwasawa algebra is neither noetherian nor reduced. A direct compactness or finite-generation argument on its spectrum is unavailable. At finite level, Fourier inversion introduces the group order into the valuation estimates; globally, one must control compatible finite quotients while keeping the exceptional correcting set finite. The arithmetic half has a separate normalization problem: raw theta elements satisfy norm relations only up to Euler factors, and interpolation must track imprimitive characters and the removed Euler factors exactly.
The first version works with the exponent- digit group , which is the setting of Theorem 1.6. Characters take values in the unit group of a complete algebraically closed ultrametric field . Measures are continuous linear functionals on , and discreteness of integral Fourier values is an explicit hypothesis. The definition does not assume the finite-correction conclusion.
The modular-form layer is exposed through RawThetaSystem, ThetaSystem, and InterpolationDatum. Milestones must construct these data from genuine modular symbols and prove their norm and interpolation fields; merely postulating the desired nonvanishing values does not satisfy the goal. The quantitative statement uses an explicit eventual lower bound rather than asymptotic notation hidden behind an uninterpreted predicate.
The new definition node isolates the horizontal Iwasawa algebra and the interpolation interface. The first new milestone constructs a nonzero horizontal -adic -function . The second milestone assumes such a pair and combines the horizontal-measure structure theorem, the Friedberg--Hoffstein quadratic seed, Corollary 5.10, and fixed-order character counting to obtain the lower bound in Theorem 1.1(1). The mission goal then follows immediately by applying the existence milestone and passing its witness to the implication milestone.
A unit fraction is the reciprocal of a positive integer. The number can be written as a sum of distinct unit fractions in infinitely many ways — , , and so on — and the combinatorics of such representations is one of the oldest recurring themes in Erdős's problem lists. Most questions in the area concern size: how many terms are needed, how small the largest denominator can be, how large the smallest one must be. Erdős Problem 287 asks instead about the shape of a representation: how tightly can the denominators be packed?
Order the denominators increasingly and look at their consecutive differences. For the differences are and . The question is whether a difference of at least must always occur, in every representation of , no matter how many terms it has. The problem is recorded in Erdős and Graham's 1980 problem book (ErGr80, p. 33) and was selected for the booklet of favourite problems prepared for the 1999 Budapest conference on Erdős's mathematics ([Va99, 1.15]). It remains open.
Timeline. The weaker statement that some difference must be at least — equivalently, that is never the sum of the reciprocals of a block of consecutive integers — is classical. Theisinger (1915) proved that the harmonic number is not an integer for , using Bertrand's postulate. Kürschák (1918) introduced the -adic argument that proves the general block statement: for , the difference is not an integer. Erdős's 1932 paper [Er32], whose title translates as "A generalisation of an elementary number-theoretic theorem of Kürschák", extends the result from blocks of consecutive integers to arithmetic progressions; the erdosproblems.com entry for Problem 287 cites it for the difference- bound. Nothing stronger appears to be known: the passage from to is the open part, and no partial result is recorded in the entry beyond a conditional one, namely that the conjecture would follow for all but finitely many exceptions if it were known that for every large there is a prime with also prime.
Fix an integer and integers
with
the sum taken in . Call such a tuple a representation of length . The denominators are strictly increasing, hence distinct, and all exceed : the value is excluded because already exhausts the total. The gaps of the representation are the consecutive differences for , and its maximal gap is .
Representations exist for every , and for only the excluded ; no representation of length exists. Examples: with gaps ; with gaps ; with gaps .
This is the open conjecture, stated with no bound on and no restriction on the denominators beyond those in Setting. It is the weakest form that captures the question: asserting a bound for one particular , or for denominators in some range, would be a different and strictly easier statement.
Equivalently: no block of two or more consecutive integers has reciprocals summing to . This is closed mathematics and the natural first target.
The gap-two bound is an immediate consequence, since a representation all of whose gaps equal is exactly a block of consecutive integers.
So the constant in the goal is optimal and cannot be replaced by .
The result itself. A positive answer would say that a representation of by unit fractions can never have all its denominators within distance of each other — a structural constraint of a kind that the size-based results in this area do not provide. The conditional route recorded on the problem page is instructive about where the difficulty sits: it reduces the conjecture, up to finitely many exceptions, to the existence of primes in with prime, a statement of Bertrand-with-extra-structure type that is itself out of reach of current technology. A direct proof would therefore either bypass that route or resolve the conjecture for the remaining cases by different means.
Formalizing it. The gap-two bound and the block theorem behind it are closed mathematics, so the honest description of that part of this mission is formalization, not research. It is nevertheless not already available: Mathlib proves Theisinger's case harmonic_not_int, that for , but not Kürschák's block version , which is the form Problem 287 needs. Supplying it is a genuine strengthening of the library's existing development and is reusable for any question about reciprocal sums over intervals. The goal itself is open, and this mission does not claim otherwise: it is registered with an open proof, and the milestones are what a solver can realistically close today.
The obvious first idea — bound the number of terms, then check finitely many cases — fails immediately, because is unbounded: representations of exist with arbitrarily many terms, so no finite computation can settle the conjecture. The second idea, extending the -adic argument that gives the gap-two bound, also fails, and instructively. That argument works because a block of consecutive integers contains exactly one element of maximal -adic valuation, which leaves the total with negative valuation. Once gaps of size are permitted the denominators may be chosen to avoid that configuration — for instance all even, as in — and the valuation obstruction disappears. There is no evident replacement prime or weighting that rules out all gap- configurations simultaneously, and the conditional result quoted above suggests why: the known routes pass through the distribution of primes in short intervals with a multiplicative side condition, rather than through a congruence obstruction.
A representation is encoded as a function together with the hypotheses ∀ i < k, 1 < f i and ∀ i j, i < j → j < k → f i < f j, and the requirement ∑ i ∈ Finset.range k, (1 : ℚ) / f i = 1. Only the values of below are constrained; the function is not required to be monotone or bounded elsewhere, and nothing outside the window is used. The conclusion is ∃ i, i + 1 < k ∧ 3 ≤ f (i + 1) - f i, the existential form of "the maximal gap is at least "; the subtraction is natural-number subtraction, which is harmless because is increasing on the window, so no truncation can occur. The sum is a rational equality, not an approximation.
The statement admits no trivializing reading. The hypothesis 1 < f i is essential and is not vacuous — dropping it would admit , ; the strict monotonicity is what makes the gaps well defined and the denominators distinct; and k ≥ 2 guarantees that at least one gap exists, so the conclusion is not an empty existential. Asserting exactly rather than at least would be false, as has a gap of .
Infrastructure: the block theorem is proved from Mathlib's padicNorm and padicValNat API — padicNorm.add_eq_max_of_ne, padicNorm.sum_lt', padicNorm.not_int_of_not_padic_int, pow_padicValNat_dvd and pow_succ_padicValNat_not_dvd — and needs no new definitions. That development is reusable beyond this mission and is a candidate for upstreaming to Mathlib alongside harmonic_not_int. Contributions are welcome on any milestone independently; a formalization of the conditional reduction to primes with prime would also be a valuable addition, and is not included as a milestone here only because the problem page states it too briefly to formalize faithfully without consulting a primary source.
Edge-colored tournaments combine a complete orientation with a finite palette. They are a natural setting for comparing local multicolor obstructions with global directed reachability. The question attributed to Sands, Sauer, and Woodrow asks whether three colors force one of two outcomes: a directed triangle whose three arcs all have different colors, or a single vertex that can reach every target along a monochromatic directed path.
The problem was recorded by the Open Problem Garden in 2008. A minimum-counterexample reduction was later restated by Georgakopoulos and Sprüssel in their study of three-colored tournaments. The available project computation excludes counterexamples through eleven vertices, but that package is explicitly candidate_only: it is bounded search evidence, not a proof of the unrestricted theorem.
A tournament is an orientation of a finite complete simple graph. For each pair of distinct vertices , exactly one of and is present. Every directed arc receives one of three labeled colors.
A rainbow directed triangle is a cyclically oriented triangle
whose three arc colors are pairwise distinct. A transitive three-vertex subtournament is not a directed triangle and is therefore not forbidden merely because its three arcs have different colors.
A vertex is a monochromatic source when, for every vertex , there is some color and a directed -to- path all of whose arcs have color . The chosen color may depend on ; the theorem does not demand one common color for all targets. Length-zero reachability handles .
The formal domain is nonempty finite tournaments. This nonemptiness convention is stated explicitly because an empty vertex type has neither a rainbow triangle nor a candidate source and would trivialize the negation of the intended question.
For every nonempty finite tournament with a three-coloring of its arcs,
No compatibility is required between the colors of paths to different targets, and unused palette colors are permitted.
The first milestone freezes the exact bounded claim supported by the replay package:
The statement includes all tournaments and all three-color arc assignments at those orders, not only one symmetry representative. The repository's observations report exhaustive search after a minimum-counterexample reduction, but the Lean theorem remains open until it has an accepted proof.
The root theorem would turn a local forbidden configuration into a global reachability certificate. Such a result clarifies how orientation and edge color interact: ordinary Gallai decompositions for undirected colored complete graphs cannot be imported unchanged, because the hypothesis forbids only rainbow cyclic triangles and allows rainbow transitive triples.
The formal development creates reusable definitions for colored directed reachability and exposes the direction of every relation. This matters in minimum-counterexample arguments, where an auxiliary arc may encode that cannot reach ; reversing that convention invalidates the cycle reduction. A verified finite milestone would also provide a regression target for SAT, SMT, or exhaustive encodings without elevating their raw output to a universal theorem.
The classical Gallai theorem is not directly applicable. It assumes an undirected complete graph with no rainbow triangle of any orientation, whereas this problem permits a transitive triple with three distinct colors. A proposed partition must therefore control both arc colors and directions between parts.
The minimum-counterexample route yields a useful spanning cycle in an auxiliary nonreachability digraph. It does not itself bound the size of a counterexample. The order-eleven computation terminates because its domain is finite, but no induction from eleven to arbitrary order follows. A proof must add a structural theorem that survives all orientations and allows monochromatic paths of arbitrary length rather than treating reachability bits as independent physical arcs.
Lean represents the tournament as a binary relation D with looplessness and exactly one orientation on each unordered pair. The coloring is a total function on ordered pairs, but only values on actual arcs are semantically used. Monochromatic reachability is the reflexive transitive closure of arcs of one fixed color. The root and finite theorem quantify over every nonempty finite vertex type.
The finite replay, its solver versions, hashes, and no-witness observations remain external candidate evidence. They do not close the milestone without a checkable certificate or a proof accepted by the platform. Contributions may formalize the minimum-counterexample cycle lemma, build an independently checked finite certificate, isolate a directed decomposition theorem, or prove the root. No contribution may replace a directed rainbow triangle by an undirected one, require the same path color for every target, or assume heredity of failure for arbitrary induced subtournaments.
Diophantine equations ask for integer solutions to arithmetic equations. One family of questions starts with a set of positive integers and imposes the same condition on every pair: their product, increased by one, must be a square. The question is how many distinct integers can satisfy all those conditions together. It connects a simple definition with a global restriction on simultaneous integer solutions.
The paper There is no Diophantine quintuple, by Bo He, Alain Togbé, and Volker Ziegler, resolves the nonexistence question for sets of five elements. This mission targets its headline result, Theorem 1 in Section 1. The mathematical theorem is proved in the paper; the remaining goal is a complete Lean proof of that result.
A perfect square is an integer of the form for a natural number . A Diophantine -tuple is a set of distinct positive integers such that the product of any two different members, plus one, is a perfect square. Here records the number of elements, not a bound on their sizes. A Diophantine quintuple would have exactly five members (definition in Section 1).
Write those five integers as . Positivity means for every index. Distinctness means whenever . The square condition requires a possibly different square root for each pair. There is no requirement that the ten square roots coincide, be distinct, or satisfy an additional ordering condition.
The theorem concerns positive integers. Replacing them by rational numbers changes the question. Likewise, allowing zero changes the admissible objects, and allowing repeated entries ceases to represent a five-element set. These domain choices are explicit in the formal target.
The single goal is the following nonexistence statement:
This is Theorem 1 of the paper. The mission's goal is the existing declaration no_diophantine_quintuple.
The integers are unrestricted in size. The target does not fix the smallest entry, require a particular triple among the entries, or assume that an entry falls below a numerical search threshold. A proof must cover every quintuple satisfying the stated domain conditions.
The result rules out an entire class of simultaneous square equations. As an immediate consequence, any set of distinct positive integers satisfying the same pairwise condition has at most four elements: a larger set would contain five distinct members that inherit the condition. This consequence explains why the five-element statement also constrains larger configurations.
A completed formalization would supply a reusable theorem that can be invoked whenever five distinct positive integers and their pairwise square witnesses arise. It would turn the informal nonexistence claim into a checked contradiction from precisely those hypotheses. The published statement is currently open for a Lean proof; its successful compilation verifies that the statement is well formed, not that the theorem has been proved.
Testing examples cannot establish this target by itself. Any computation with a fixed search limit addresses only a bounded collection, while the statement quantifies over all positive integers. A formal proof that uses a finite computation must also establish why the computation covers every possible case.
The conditions are simultaneous: each entry participates in four pairwise equations. Solving or excluding one isolated pair does not by itself settle whether all ten equations can hold together. The paper's proof overview in Section 2 describes the arithmetic estimates and computational components behind its result. Formalizing those components entails checking their hypotheses and connecting their conclusions to the unrestricted goal.
The Lean declaration represents the entries by a function a : Fin 5 → Nat. It places the existence of that function under a negation and includes three conditions: every value is positive, different indices have different values, and every pair of different indices has a natural-number square witness.
The square condition is written for all unequal indices. This is equivalent to the usual condition for increasing pairs because multiplication is commutative. No increasing ordering of the five values is imposed. A development using sorted entries must justify its connection to this unrestricted indexed representation.
The root statement needs only Lean's core natural numbers, finite index type, arithmetic, and logic. It introduces no custom predicate whose meaning could hide additional assumptions. A complete proof may use Mathlib and reusable supporting results about integer arithmetic, squares, and the arithmetic tools required by the chosen argument. Supporting declarations should state their hypotheses explicitly and ultimately connect to this exact root theorem. Contributions establishing the known result, including an alternative rigorous proof, are within scope.
For every integer
, there exists a prime p such that
An almost complex structure gives every tangent space of a smooth manifold the linear algebra of a complex vector space, but it need not come from complex-valued coordinate charts. The gap between these two notions is a global differential-geometric question, not a change of terminology. Granja and Milivojević describe the following as “a major open problem in differential geometry”: whether every closed almost complex manifold of dimension at least six admits an integrable complex structure (Introduction, p. 1). This mission records that question as an open conjecture, not as an established theorem.
Fix an integer . Let be a connected, compact, Hausdorff, second-countable smooth manifold without boundary and of real dimension . An almost complex structure on is a smooth field
of real-linear maps satisfying for every and . This condition forces even real dimension, but by itself supplies no complex coordinate charts.
A complex structure of complex dimension is an atlas with values in whose transition maps are complex differentiable. Such an atlas induces an integrable almost complex structure. The target concerns existence on the underlying smooth manifold: the complex structure obtained may induce a different almost complex structure from the supplied . It does not claim that every chosen almost complex structure is integrable.
Here “closed” means compact and without boundary. Connectedness is explicit because it is part of the standing manifold convention in the cited 2022 source. The lower bound is on real dimension: , equivalently .
For every and every closed connected smooth real -manifold ,
“Compatible” means that the underlying real smooth structure of the complex atlas is smoothly equivalent to the given smooth structure on the same topological space. No claim of uniqueness, equality with the original atlas, or integrability of the supplied is made.
The real six-dimensional case is essential. Since carries an almost complex structure, the conjecture would imply that its underlying smooth manifold carries some complex structure. That special case remains unresolved; restricted nonexistence results, such as results imposing compatibility with a particular metric, do not decide the unrestricted existence question.
A positive solution would replace a pointwise tangent-bundle reduction by genuine holomorphic coordinates for every manifold in the stated class. It would in particular settle the existence question for . A negative solution would identify additional global obstructions to complex atlases that are invisible to the existence of an almost complex structure.
The formalization isolates a reusable smooth almost complex structure on top of Mathlib’s tangent-bundle and manifold APIs, while making the desired complex atlas explicit. This prevents the central distinction from being hidden inside an unconstrained predicate named “integrable.” It also exposes the compatibility between the original real smooth atlas and the real atlas underlying the complex charts, which future work on characteristic classes, Nijenhuis tensors, and concrete six-manifolds can reuse.
The equation is fiberwise algebra. Integrability requires local complex coordinates whose overlaps are holomorphic, equivalently the vanishing condition identified by Newlander and Nirenberg. Smooth variation of does not make that differential condition automatic. Thus simply viewing each tangent space as a complex vector space does not construct a complex manifold.
The six-sphere shows why the dimension threshold cannot be treated as a routine stable-range simplification. Its known almost complex structure supplies the hypothesis in real dimension six, while no arbitrary complex atlas is known. Likewise, replacing the conclusion by a complex vector-space structure on each tangent fiber would merely repeat the hypothesis and would not address the open problem.
The namespace AlmostComplexToComplex uses Mathlib’s boundaryless Euclidean manifold model. AlmostComplexStructure n M contains a continuous real-linear map on every tangent space, the pointwise identity , and smoothness of the induced self-map of the total tangent bundle. It contains no integrability field.
The main theorem assumes the real atlas is modeled on and concludes the existence of charts modeled on . Mathlib’s IsManifold condition over at order one states complex differentiability of chart transitions. Two conditions on the identity map compare the original real atlas and the real manifold structure underlying the complex charts in both directions; an unrelated smooth structure therefore cannot satisfy the conclusion merely by being placed on the same carrier type.
This is a chart-level interface, not yet a development of analytic integrability theory. Mathlib at the pinned revision has no ready-made almost-complex/Nijenhuis package connecting the structure above to the Newlander–Nirenberg criterion. The target does not assert that the supplied is integrable or homotopic to the one induced by the resulting atlas. A dedicated milestone is also outside this minimal draft because faithfully constructing the standard sphere and its known almost complex structure would require additional sourced infrastructure; no surrogate special case is inserted.
The traveling salesman problem — visit cities by the cheapest round trip — is the most widely known problem in combinatorial optimization, and its central open question concerns a linear program. The subtour-elimination relaxation (the Held–Karp bound) replaces tours by fractional edge weights, and both in theory and in practice (it powers the lower bounds inside the Concorde solver) it is remarkably close to the true optimum. How close, in the worst case, is the integrality gap of the relaxation: the supremum of over metric instances. Explicit instance families push the gap up to ; the best proven upper bound sits just barely below . The 4/3 conjecture — the gap is exactly — has been the benchmark question of approximation algorithms for four decades.
An instance on cities is a cost function assigning to each ordered pair of cities a real cost , required to be a metric cost: symmetric (), zero on the diagonal (), and satisfying the triangle inequality . Nonnegativity follows; distinct cities at distance zero are allowed, as usual for metric TSP.
A tour visits every city exactly once and returns to its start. Formally a tour is given by an ordering: a permutation of the cities, traversed as and back to ; its cost is the sum of the costs of consecutive steps, and — written tspOpt c — is the minimum over all orderings.
The subtour-elimination (Held–Karp) relaxation replaces the tour by a fractional edge weight for each pair of cities. A weight vector is feasible (IsHeldKarp x) when it is symmetric with zero diagonal, has entries in , gives every city fractional degree two (), and crosses every nontrivial cut at least twice: for every set of cities other than and all cities, . The Held–Karp bound hkValue c is the infimum of over feasible (the double sum counts each edge twice, hence the ). The incidence vector of any tour is feasible, so always.
Together with the known lower-bound families this says the integrality gap is exactly . The goal carries no algorithm and no constant to improve: it is the terminal statement of the ladder, open in both directions (a proof or a counterexample instance would each settle it).
Five results over the same definitions: the relaxation is valid (); instance families force the gap arbitrarily close to ; tree doubling gives ; Wolsey's theorem gives , the classical upper bound; and the Karlin–Klein–Oveis Gharan record for some (FOCS 2022). The last milestone is a statement-level target: its known proof (max-entropy sampling, strongly Rayleigh polynomials) is far beyond current formalization practice, so the mission's usable proving frontier remains Wolsey — the milestone records the state of the art as a formal statement.
The 4/3 conjecture is the reference open problem of approximation algorithms: the quality of the subtour LP calibrates every algorithmic advance on TSP, and the conjectured extremal instances guide the search for better rounding schemes. The bound is also what practical solvers actually compute — branch-and-cut on this LP solves instances with tens of thousands of cities — so the conjecture is a statement about the observed tightness of the world's most-used combinatorial lower bound.
Nothing in this circle exists in any proof assistant: Mathlib has no TSP, no LP relaxations, no polyhedral combinatorics of tours. The mission's milestones force the base layer into existence — tours over Equiv.Perm, cut constraints over Finset, and, for the upper bounds, the parity and tree arguments (spanning trees against the LP, T-joins for the bound) whose infrastructure is reusable for matching theory and network design far beyond TSP.
The naive plan — round the LP solution to a tour — has no known analysis losing less than in general, and the half-integral extremal instances show the hard cases are structured and simple-looking at once. Christofides' matching argument is provably stuck at against the LP; forty years of work moved the constant by , and that advance needed an entirely new probabilistic toolkit. On the other side, no instance family with ratio above has ever been found despite extensive computational search over small instances (Benoit–Boyd and successors). Both directions of the goal are genuinely open territory.
The Lean model commits to: cities Fin n; costs c : Fin n → Fin n → ℝ with IsMetricCost (symmetry, zero diagonal, triangle inequality — nonnegativity is derived, and semimetrics are included as in the standard statement of the conjecture); tours as orderings π : Equiv.Perm (Fin n) traversed cyclically via finRotate, so every permutation denotes a Hamiltonian cycle and every Hamiltonian cycle is denoted; both optimal values as sInf over nonempty, bounded-below sets of reals, so they are genuine minima for n ≥ 3. The hypothesis 3 ≤ n is load-bearing: for n ≤ 2 the degree-2 constraints are infeasible, sInf ∅ = 0 by convention, and the bounds would be false — every theorem therefore carries it.
Welcome contributions: the milestones in any order — held_karp_le_opt is the natural entry point (the tour's incidence vector crosses every cut at least twice); integrality_gap_lower_bound needs the three-path instance family and a case analysis on its tours; tree_doubling_bound needs spanning trees against the LP; wolsey_bound adds the T-join/parity argument and is the summit. Reusable infrastructure — spanning tree polytopes, T-joins, Eulerian traversals, cut lemmas — is welcome as platform theorems. Graph-TSP (), path TSP, and asymmetric TSP are deliberately left to future missions; the Karlin–Klein–Oveis Gharan bound is stated as a milestone, but its sampling machinery is expected to arrive, if ever, as shared infrastructure built over many contributions.
Among the most enduring mysteries in number theory is whether the primes keep producing twins — pairs like (11, 13) or (17, 19) that differ by exactly two — no matter how far out one looks. The general form was set down by Alphonse de Polignac in 1849, and the first deep theorem came from Viggo Brun in 1915, who proved that the reciprocals of the twin primes converge to a finite value, now called Brun's constant; in doing so he invented modern sieve theory and showed that twins must thin out even if there are infinitely many. Hardy and Littlewood went further, conjecturing a precise density of about 2C₂·x/(ln x)² for the count of twins below x. For nearly a century the infinitude itself stood untouched, until Yitang Zhang's stunning announcement on 17 April 2013 that some gap below 70 million recurs infinitely often — the first finite bound ever proved. A Polymath collaboration led by Terence Tao, together with James Maynard's independent multidimensional sieve, soon drove that bound down to 246, where it still stands. Closing the gap all the way to 2 — the twin prime conjecture itself — remains open. This mission states it cleanly: the set of primes p for which p + 2 is also prime is infinite.
Formulated in 1985 by Joseph Oesterlé and David Masser as an arithmetic distillation of Szpiro's conjecture on elliptic curves, the abc conjecture makes a deceptively simple claim about coprime triples with a + b = c: the three numbers cannot all be built from many repeated small primes at once, so c can only rarely exceed rad(abc)^(1+ε). Dorian Goldfeld called it 'the most important unsolved problem in Diophantine analysis,' and for good reason — a single proof would cascade through number theory, delivering Fermat's Last Theorem for all large exponents almost for free, along with Roth's theorem, the Mordell–Faltings theorem, the Fermat–Catalan conjecture, infinitely many non-Wieferich primes, and all but finitely many counterexamples to Beal's conjecture. Since 2012 Shinichi Mochizuki has claimed a proof via inter-universal Teichmüller theory, published in 2021, but the community has not accepted it: in 2018 Peter Scholze and Jakob Stix identified a gap they regarded as fatal. A precise formal statement gives everyone a shared, machine-checkable target around which to organize verified progress.
The first Prove2Me Itô's lemma mission established the time-dependent scalar stochastic chain rule under explicit regularity and integrability assumptions. Itô calculus II develops its structural consequences: products of correlated Itô processes, quadratic covariation, Brownian squares, integration by parts, stochastic exponentials and geometric Brownian motion. These are indispensable tools for stochastic differential equations, martingales and mathematical finance. The classical identities are discussed in standard stochastic-calculus texts and in the Itô's lemma overview.
This is a genuinely separate follow-on mission. It reuses the accepted first-mission scalar Itô formula and the independently proved LevyStochCalc vector Itô formula, together with previously published smooth cutoffs, progressive-measurability, derivative-control and mixed-Hessian lemmas. It will not republish those results. The published foundation includes a two-coordinate smooth bump, compactly supported truncated coordinate product, finite-sum cross-variation contraction and controlled stochastic integrands, subject to the exact accepted catalogue status of each theorem.
Work on a filtered probability space with a finite-dimensional Brownian driver . Consider two continuous adapted Itô processes sharing that driver. At an initial deterministic horizon , write their dynamics in integral form:
Initially use the exact IsVectorItoVersion interface of the accepted finite-dimensional vector Itô theorem, with bounded measurable/progressive coefficients, the required square-energy hypotheses and a deterministic path bound on the state up to . Distinguish identities holding almost surely at each fixed time from identities holding simultaneously for all times. The cross-variation density is .
The principal goal is the continuous Itô product formula, as an equality of explicitly defined stochastic and ordinary integrals, not just an informal differential calculation:
All integrals must exist under the formal theorem hypotheses. For the first version, use a compactly supported smooth approximation of which agrees with the product on a bounded state region. This is necessary because the accepted vector formula globally bounds the first and second Fréchet derivatives of its test function, whereas itself has unbounded first derivatives.
Prove the truncated-product smoothness, support, derivative identities, Hessian entries, uniform-continuity and energy bounds as separate compact helpers. Use the already proved vector Itô theorem and simplify using the accepted cross-variation finite-sum theorem. Next, remove deterministic state bounds by a genuine stopping-time/localisation theorem, with explicit stopped-integral identities and almost-sure convergence. A zero-horizon case and continuity-based all-time formulation are separate careful endpoint steps.
Reference the first mission's accepted scalar time-dependent chain rule, proved vector Itô formula, scalar-to-one-dimensional Brownian embedding, square-energy domination, continuous adapted composition progressive measurability and the accepted cutoff/product calculus. Audit exact theorem IDs and pinned imports before attaching each reference. Do not use the earlier analyticity-level ContDiff ℝ ⊤ plateau theorems: compactly supported nonzero smooth cutoffs require the level ↑(⊤ : ℕ∞). The corrected C∞ targets and remote-accepted proofs are the intended foundations.
Establish is smooth with compact support and matches on the interior plateau. Identify its first Fréchet derivative, Hessian mixed coefficients , zero diagonal coefficients, and norm bounds. Use equality in a neighbourhood to transport derivatives; derivative equality on a closed-ball boundary cannot be assumed. Preserve explicit dimensional types for Fin 2.
Specialise the accepted vector Itô theorem to the truncated test function. Verify its measurability, progressive measurability, boundedness, uniform Hessian continuity and integrability requirements. Reduce the Hessian double sum to the covariance term, identify ordinary integrals and the Brownian stochastic integrals, and prove the displayed product formula for bounded paths.
Localise the two coordinates with increasing exit radii. Prove the stopped-process representation, stochastic-integral stopping and localisation identities and the vanishing probability of finite-horizon exit as the radius tends to infinity. Remove deterministic state bounds for the genuine continuous Itô class under explicit local integrability. Prove the continuous-process all-time version on one probability-one event where justified. The unrestricted result must not assume the desired product equality or quadratic covariation.
Specialise the product formula to to obtain . For -coordinate Brownian motion, derive the diagonal quadratic-variation and off-diagonal covariance identities, specifying whether the chosen definition uses convergence in probability, or brackets of continuous local martingales. Show the finite-variation cross term vanishes under suitable hypotheses.
Rearrange the product formula as stochastic integration by parts for continuous semimartingales. Specialise to deterministic finite-variation factors and prove product martingale statements only with suitable integrability, not merely from a local-martingale equality.
Prove, for constant real and ,
solves , in the exact integral sense. Establish positivity, the logarithmic Itô correction, the Doléans stochastic exponential for Brownian integrals under specified integrability assumptions, and optional expectation/martingale claims with their requisite hypotheses. Use localisation or an independently proved growth-controlled Itô formula when exponential derivatives are unbounded.
The mission turns the first scalar chain rule into reusable stochastic algebra for correlated drivers and finance. The covariance term matters in multidimensional hedging, insurance risk models and diffusion-generator calculations. The product formula will also support Feynman–Kac discounting and stochastic verification for dividend-control problems, subject to those missions' own filtration and jump assumptions.
The nontrivial work is bridging the accepted vector formula's global derivative hypotheses to unbounded products, identifying Fréchet Hessian entries with coordinate derivatives, proving progressive measurability and energy of stochastic integrands, and correctly stopping the processes and their integrals. A formula for general càdlàg jump semimartingales needs left limits and jump-remainder sums; that is a later separate mission, not a hidden assumption here. Likewise, exponentials require integrability or localisation beyond a naïve bounded-derivative substitution.
All declarations use Prove2Me's pinned Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474 (Lean 4.33.1), targeted imports and remote proof validation only. No local Lean/Lake/LSP. First reuse existing Proved theorems by immutable IDs. New proof obligations must be published as precise theorem declarations, compile remotely and receive accepted proofs before being described as Proved. Avoid vacuous deterministic-only or zero-volatility substitutes for the general product result. Existing original Itô mission remains unchanged. This is initially a private, unconfirmed captain proposal, not a launched mission; review and publication are separate authorised steps.
The Feynman–Kac formula links solutions of parabolic partial differential equations to expectations of functionals of diffusion processes. It provides the probabilistic meaning of a differential equation containing drift, diffusion, discounting and a source term. The Feynman–Kac article presents the one-dimensional terminal-value formula and a martingale derivation. James Nolen's Stanford lecture notes, Section 4.1, give a rigorous treatment of classical-solution representations and explain localisation when growth conditions replace boundedness.
This mission formalises the classical-solution representation of the one-dimensional backward Feynman–Kac formula in Lean 4 and its uniqueness consequence. Its central result has time- and state-dependent drift and volatility, nonnegative killing or discount rates, a running source, and a terminal payoff. Earlier special cases build useful reusable results. It is closely related to the separately developed Prove2Me mission on Itô's lemma, which supplies stochastic-calculus prerequisites.
Fix a probability space with a filtration and an adapted real Brownian motion, a deterministic finite horizon , and a starting state . Let be an adapted continuous diffusion starting at at time , with integral-form dynamics
Let and denote drift and diffusion coefficients, a state- and time-dependent discount or killing rate, a continuous running payment rate, and a terminal payoff. A classical solution satisfies
Use a solution with continuous derivatives and explicit growth or boundedness assumptions, and a genuine diffusion whose stochastic integral is independently defined. Initially assume bounded measurable coefficients, bounded , and sufficiently bounded to make the relevant Itô integral square-integrable. Stronger Lipschitz hypotheses may be used for separate SDE existence and uniqueness statements. These assumptions will be stated in formal theorem binders and made internally consistent.
Establish measurable and integrable trajectories, pathwise time integrals, exponential-discount positivity, the unit initial discount, the multiplicative discount identity and the derivative or integral equation for . The process is started at a deterministic state, thereby avoiding informal conditioning on a continuous random variable taking an event of probability zero.
Reuse verified Brownian, stochastic-integral and time-dependent Itô results from Prove2Me where their exact pinned definitions match. Establish the required diffusion composition, finite-variation discount product identity and running-payment fundamental-theorem-of-calculus bridge. The key process is
For a classical PDE solution, its finite-variation drift vanishes and its stochastic differential is the discounted spatial-gradient term. This must follow from genuine Itô calculus and the PDE hypothesis rather than be inserted as an assumed martingale.
Prove boundedness and measurability of terminal and running rewards, progressive or predictable measurability of the stochastic integrand, and the square-integrability estimate that upgrades the stochastic integral to a true centred martingale. Distinguish the almost-sure stochastic identity, the martingale property and the expectation identity. A bare local-martingale statement is insufficient to conclude equality of expectations without localisation or another integrability argument.
The principal capstone proves, for every permitted , the terminal-value representation
The same diffusion and coefficients must be used on both sides. A uniqueness theorem follows for two classical solutions in the designated bounded or growth-controlled class, since their right-hand sides coincide. Special cases include the heat equation, constant discount, zero running source and deterministic terminal data. These are genuine specialisations of the representation, with their own useful analytic identities.
Subsequent milestones can allow polynomially growing terminal payoffs using stopping-time localisation and moment estimates, generalise to multiple Brownian coordinates and multidimensional generators, and address domains with boundary exit. The converse theorem, that an expectation has the differentiability needed to solve the PDE, is a separate analytic regularity objective. It must be given its own hypotheses and must not be claimed as an immediate consequence of the representation theorem.
Feynman–Kac creates a reusable bridge between stochastic processes and deterministic differential equations. For financial mathematics, the running term represents discounted intermediate cashflows and the terminal term represents a contingent payoff. Under appropriate modelling assumptions, the same ideas underlie Black–Scholes valuation and more general diffusion pricing models. Nolen's lecture notes explain the backward and forward formulations.
There is existing Lean work to compare. The MarkovProcess library reports a bounded-potential Feynman–Kac semigroup and resolvent perturbation theorem, without a diffusion PDE. The MathFin library proves a heat-kernel route to the Black–Scholes PDE, while recording the general variable-coefficient diffusion problem as an additional task. Those external builds are research references, not automatic Prove2Me imports. Within Prove2Me, Brownian and Itô results have already been accepted at the pinned environment. This mission should reuse the precise applicable forms and provide downstream generator and stochastic-verification tools for derivative-pricing and dividend-control missions.
The challenging interfaces are filtration consistency, deterministic initial conditions, time-dependent Itô calculus, measurability of path-dependent discount factors, Fubini or time-integration steps, and the distinction between local and true martingales. The endpoint must be handled without a spurious time derivative outside the solution's domain. Differentiability of a solution at the spatial boundary of an open domain or near terminal time requires additional treatment in extensions.
The root must be nontrivial. It cannot assume the terminal representation, the vanishing stochastic-integral expectation, or the desired martingale property as opaque unproved model fields. Constant solutions, a deterministic process, or a zero payoff may serve as examples, but cannot replace the universally quantified stochastic diffusion statement. Each theorem should have accurate source provenance and a checked dependency relation.
Use the Prove2Me pinned Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474 with targeted imports. Any necessary process structures, discount definitions or helper theorems must be published and verified in that environment. The externally reported MarkovProcess pin is newer and requires a compatibility audit before adapting any code. Reuse the already proved Prove2Me stochastic-integral and vector Itô statements where their exact assumptions apply. The independent Itô's lemma mission supplies ongoing time-dependent diffusion foundations.
The main deliverable is a formal theorem of representation and a classical uniqueness corollary for bounded sufficiently regular solutions. Existence of a classical PDE solution, full generality for unbounded data, semigroup generation, multi-dimensional regularity, and stopping-domain formulas remain explicit extensions rather than silently presumed properties. Draft definitions and theorem statements must be remotely elaborated and checked before confirmation, with their meaning preserved when syntax is repaired.