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?
Addition and multiplication interact in rigid ways: a finite set of numbers that is highly structured with respect to one operation (an arithmetic progression, say) tends to be unstructured with respect to the other (a geometric progression). The sum–product problem asks for the sharp quantitative form of this principle. It was posed by Erdős and Szemerédi in 1983 (Erdős Problem 52) and has since become a central question of additive combinatorics, with applications in incidence geometry, exponential sum estimates, expanders and randomness extraction.
Timeline.
The conjecture itself remains open.
For a finite set define the sumset and product set
For nonempty both contain at least elements and at most . The quantity of interest is as a function of .
For every there is such that for every finite set ,
The cannot be removed: there is no with for all (take ; the multiplication table is by Erdős).
A proof of the goal would settle the sharp form of the sum–product phenomenon over . Sum–product estimates are an input to incidence bounds, to Bourgain–Katz–Tao-type results over finite fields, and to explicit constructions in theoretical computer science; improvements of the exponent over have come together with new incidence-geometric tools.
Formalization status: the milestones are published theorems (Erdős–Szemerédi, Elekes, Solymosi, Rudnev–Stevens, Erdős's multiplication table bound), but their proofs are not known to be formalized in Lean/Mathlib. The Szemerédi–Trotter theorem, multiplicative energy, and the Elekes and Solymosi arguments are reusable infrastructure. The goal itself is an open problem.
Incidence-geometric methods (Szemerédi–Trotter and its descendants) naturally produce exponents near , and passing beyond has required intricate higher-energy arguments yielding only small gains. None of the existing approaches is known to reach exponents close to ; even over , where arithmetic structure is available, the best general bounds are the real-number ones.
Sets are Finset ℤ; and are Mathlib's pointwise sumset and product set (open scoped Pointwise), and cardinalities are cast to . Powers are real powers (Real.rpow). The empty set is allowed; the hypothesis keeps every exponent positive, so the empty set contributes the trivial inequality rather than a junk value . The constant may depend on but not on . The Solymosi milestone is stated for so that .
The statements are for integer sets only; results proved over specialise to them. Contributions of general-purpose infrastructure (Szemerédi–Trotter over , multiplicative energy, bounds for the multiplication table) are welcome.
A -dimensional complex abelian variety is of Weil type for an imaginary quadratic field if acts on by rational endomorphisms in such a way that each of the two eigenspaces of on meets in an -dimensional subspace. A. Weil observed that such carry a two-dimensional space of rational -classes, the Hodge–Weil classes, that are in general not generated by divisor classes. Whether they are algebraic is one of the main test cases of the Hodge conjecture; by work of Schoen, Moonen–Zarhin and others, algebraicity for abelian fourfolds of Weil type implies the Hodge conjecture for all abelian fourfolds.
E. Markman (arXiv:2502.03415) proves this algebraicity by a new construction. Its starting point, developed in §§1.2 and 2 of the paper, is linear algebra: the even cohomology of an abelian -fold is a half-spin representation of , where , and a rational plane meeting the variety of pure spinors in two conjugate -points (a -secant) equips with the structure of an abelian variety of Weil type. This mission formalizes that construction and its explicit example in §2.4.
Timeline (as summarized in §1.1 of the source).
Let be a complex torus of dimension . Fix a basis of , so that , and write in dual coordinates. The complex structure of is a real matrix with acting on ; its -eigenspace is . A number acts on by and on multiplicatively; a class of type is multiplied by . The Hodge ring is .
For a complex torus of dimension with ample , and a positive integer : are even pure spinors with , and there is a rational acting by on with
That is, is a polarized abelian variety of Weil type.
Equation (2.4.6) (the annihilator of ), Equation (2.4.5) (the plane lies in the Hodge ring), Lemma 2.2.6 (Weil's condition), the rational similarity of (2.2.4)/(2.4.1), the commutation (§2.4, p. 20), and Lemma 2.4.2 (the formula for ).
The result. The construction supplies, for every imaginary quadratic field and every polarized abelian -fold, a polarized abelian variety of Weil type , together with a description of its Weil structure in spin-representation terms. The rest of the paper deforms this structure ( plays the role of the special Mumford–Tate group) and uses Orlov's derived equivalence to obtain the Hodge–Weil classes from sheaves; the final application is the Hodge conjecture for abelian fourfolds.
Formalizing it. The results of this mission are proved in the paper; none of them has a machine-checked proof. The mission produces a reusable Lean model of the spin representation of , of pure spinors and their annihilators, and of Hodge types on , all built on Mathlib's exterior and Clifford algebras.
The algebra in the explicit example is short, but the general milestones rest on facts about pure spinors (their annihilators are maximal isotropic; a conjugate pair with splits ; rationality of by Galois descent) and on Lemma 2.2.6, whose proof in the source uses Chevalley's isomorphism as a morphism of Hodge structures. A coordinate computation settles the example but not the general statements. Sign conventions (the choice of , the complex structure on , and the sign of ampleness) all enter the final negativity claim.
ExteriorAlgebra ℂ (Fin (2n) → ℂ); contraction is Mathlib's CliffordAlgebra.contractLeft; is the truncated exponential .Given a real matrix , consider maximizing the bilinear form over sign vectors , . This discrete optimum, written , is closely tied to the cut norm of a matrix and is NP-hard to compute. Relaxing each sign to a unit vector and each product to an inner product gives the semidefinite value , computable in polynomial time. Grothendieck's inequality (Grothendieck, 1953) states that the relaxation overshoots by at most a universal factor: there is a finite , independent of , of , and of the dimension of the vectors, with for every . The Grothendieck constant is the least such — equivalently, the worst-case integrality gap of the canonical semidefinite relaxation of this bilinear problem.
The constant is not a curiosity of one optimization problem. It originated in functional analysis, where it is central to the geometry of Banach spaces and to harmonic analysis; it governs the approximation ratio available for cut norms; and, in quantum information, it measures the maximal advantage of quantum over classical correlations in Bell-type experiments. Its exact value has been open since 1953.
A timeline of the bounds:
i.e. , which fixes the tenths digit of at .
Fix and .
Here and are unit vectors of a common but arbitrary finite dimension . Since a sign is a unit vector in dimension one, . Call a Grothendieck bound if for every , and , and set .
Upper bounds on come from rounding algorithms. A Krivine scheme of dimension is a pair of partitions of into a region and a region, encoded by measurable odd functions : the algorithm maps each SDP vector to a Gaussian point in , correlated according to the inner products, and reads off the label of the region the point lands in. Taking recovers random hyperplane rounding. The quality of a scheme is carried by its normalized correlation function
where are standard Gaussian vectors in with for every coordinate . For the half-space partition , whose analysis gives Krivine's bound. Writing the odd expansion , the hyperplane scheme sits at .
This is the two-sided bound the source paper states as the outcome of its Theorems 2.1 and 2.2. It is the weakest statement that carries both of the paper's contributions at once; each side is also a milestone in its own right, so partial progress is recorded even if only one direction closes.
The milestone list runs from the classical background to the two new bounds: ; the existence of a finite Grothendieck bound; ; Krivine's ; the affine coefficient constraint valid for every Krivine scheme (Theorem 2.2, equation (1)); the transfer of a member of the affine family into a lower bound on (Appendix A); the lower bound (Theorem 2.2); and the cubic–quintic upper bound (Theorem 2.1).
The two target bounds narrow an interval that had been essentially static for four decades: before 2026 the state of the art was , wide enough that the tenths digit was unknown. The lower bound is also methodologically new. Every previous lower bound was obtained by exhibiting a hard instance; this one instead proves a ceiling on the performance of every rounding scheme in the Krivine family and converts that ceiling, through the Naor–Regev optimality theorem, into a bound on the constant. The affine constraint is the transportable core of that argument: being affine in the coefficients, it survives mixing schemes and passing to limits, which is exactly what the reduction to requires.
On the formalization side, nothing here is machine-checked today. The upper bound (Theorem 2.1) is certified by interval arithmetic in the companion paper, and the lower bound's central one-dimensional inequality likewise rests on a computer-assisted certificate; reproducing either inside Lean means building a rigorous numeric layer on top of the analytic argument. Ahead of that, the mission needs a formal definition of itself and of the Krivine-scheme apparatus, neither of which exists in Mathlib — these are reusable well beyond this mission, since Grothendieck's inequality feeds cut-norm approximation and Bell-inequality bounds. Contributions of intermediate lemmas about , , Gaussian correlation identities, and Hermite expansions are welcome even when the headline bounds stay open.
The obvious route to a lower bound is to write down a matrix and compute. That route is what Davie and Reeds exhausted; improving it has produced gains of order at best, because the hard instances are high-dimensional Gaussian objects whose is itself hard to bound tightly. The route taken here avoids instances entirely, and its difficulty lies elsewhere: a constraint on a single scheme is worthless unless it survives averaging over schemes and passing to limits of schemes of growing dimension, since only then does the Naor–Regev optimality theorem convert it into a statement about . Constraints that are nonlinear in the scheme do not survive that passage, which is why the target inequality is affine in . For the upper bound, the difficulty is that the improvement is genuinely asymptotic: it comes from a limit of schemes of growing dimension rather than any fixed low-dimensional partition, and the final margin of is certified numerically rather than in closed form.
and are defined as suprema of explicitly described sets of reals, over matrices indexed by Fin m and Fin n with real entries; the sign vectors are real-valued functions constrained to take the values and , and the relaxation quantifies over unit vectors of EuclideanSpace ℝ (Fin d) for an existentially quantified , so no dimension bound is built in. The empty-index cases or are included and give value on both sides. is the infimum of the set of Grothendieck bounds; that set is nonempty precisely by Grothendieck's inequality, which is itself a milestone, and it is bounded below, so the infimum is not a junk value.
A Krivine scheme is a structure carrying two measurable -valued functions on Fin k → ℝ, each odd almost everywhere. Almost-everywhere oddness is forced: no -valued function satisfies at the origin, so a pointwise requirement would make the structure empty and every statement about schemes vacuous. With the null-set relaxation the half-space partition is a scheme in every dimension , and the definition file constructs it, pinning down non-vacuity; dimension admits no scheme. The correlation function is the explicit double Gaussian integral against the correlated-pair density, scaled by , and the coefficients are read off as and — where fails to be three times differentiable at these are the ambient junk value , which a solver should keep in mind when reading the coefficient milestones.
No trivializing reading is available for the goal: it pins between two explicit numerical constants, so it can be satisfied neither vacuously nor by a degenerate convention. Solvers should be aware that the source paper states its two theorems in abridged form and refers to its companion paper for the full proofs, and that the further bounds reported there — the stronger lower rungs and , and the upper values and — are explicitly described as system-tested but not author-verified; they are deliberately outside this mission's milestone list.
Erdős Problem 68 asks whether the infinite series 184987\sum_{n=2}^{\infty} rac{1}{n! - 1}184987 is irrational.
Paul Erdős proved in 1948 that \sum_{n=1}^{\infty} rac{1}{2^n - 1} is irrational, but the problem for factorial denominators ! - 1$ remains open.
A sum of independent random increments is a basic model for accumulated noise. A continuous Gaussian process offers a different description of that noise, one that can be studied at every nonnegative time. To compare their individual trajectories, both objects must live on the same probability space. The question is whether their paths can remain close over a whole finite range of observation times, with a quantitative bound on the chance of a large discrepancy. Ethier and Kurtz state such a result for independent sums in Chapter 7, Section 5, Theorem 5.1 of Markov Processes: Characterization and Convergence, printed page 356.
Let be a probability measure on the real line. Assume that it has finite exponential moments in a neighborhood of zero: there is such that
This hypothesis controls both tails of the distribution. In particular, its mean and variance are finite. The distribution need not be centered, symmetric, bounded, or have positive variance. Let denote independent random variables each with distribution , and write for their partial sums.
A Brownian motion with drift and variance rate can be written as , where is standard real Brownian motion and is the nonnegative square root of the variance. When , this expression gives the deterministic path . A coupling specifies a joint probability law for the entire sequence and the Brownian path while preserving their required individual laws. The sequence coordinates are independent of one another; independence between the sequence and the Brownian path is not part of the requirement.
Theorem 5.1 asserts that a coupling and positive constants , depending only on , exist such that
for every integer and every real . Both inequalities displayed here are strict. One joint construction works simultaneously for every horizon and every positive excess ; neither the coupling nor the constants are chosen anew after those parameters are specified. At , the logarithmic term is zero, so the same assertion controls the discrepancy at the first observation time.
The mission consists of this full theorem. The rescaling and Poisson consequences discussed later in the section are outside its target. There are no separate supporting theorem milestones in the accepted grouping.
The estimate controls the largest discrepancy among all partial sums up to a specified horizon. Its deterministic threshold grows logarithmically with that horizon, and its remaining tail decreases exponentially with the excess above the threshold. This makes the theorem a quantitative comparison of trajectories on a common space. The opening of Section 5 identifies strong approximation of independent sums as its subject and introduces approximation of the Poisson process as a subsequent consequence.
The mathematical result is a known theorem stated by Ethier and Kurtz. The present formal target asks for a checked proof of that statement, including the existence of its coupling. The statement is supplied with an unproved theorem body; no proof of the strong approximation estimate is asserted here.
The prescribed marginal laws do not themselves determine the joint relationship that makes the paths close. The construction must preserve independence within the entire increment sequence and the Brownian finite-dimensional laws while also satisfying a maximal estimate for every finite horizon. A comparison of the distributions at one terminal time does not supply these simultaneous path requirements. The exponential tail and the uniform choice of constants are both part of the goal.
The common carrier is a pair consisting of a real sequence indexed by natural numbers and a continuous real path indexed by nonnegative real times. A probability measure on this carrier is the unknown coupling. Its first coordinate at index zero represents , so summing over the first natural indices represents exactly. Its second coordinate is standard Brownian motion; the affine expression supplies the general drift and variance.
The finite maximum event is expressed by the existence of an integer with whose error exceeds the threshold. This avoids any convention for a maximum of an empty set. Exponential integrability supplies the finite moments needed for the mean and variance. The probability bound uses the nonnegative extended-real embedding of the positive finite quantity . The formal statement retains the full exponential-moment class, including point masses. Existing probability-measure, independence, law, Brownian-motion, and variance definitions supply the mathematical vocabulary.
Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986 (held reprint copyright 1986/2005), Chapter 7, Section 5, Theorem 5.1 and equation (5.1), printed page 356; local source PDF page 365. The book title and authors are recorded on local PDF page 2.
Independent sums are a basic model for accumulated random fluctuation. A central limit theorem describes their distribution at one large time, and a functional limit theorem describes weak convergence of a rescaled path. Strong approximation asks for substantially more: construct the sums and a Brownian motion on one probability space so that their paths remain close, with an explicit error bound that holds simultaneously over all earlier integer times. Such a coupling turns Brownian path estimates into quantitative information about random walks and independent sums.
Chapter 7, Section 5 of Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence (Wiley, 1986) states this strong approximation result as Theorem 5.1. Its estimate has logarithmic deterministic error and a strictly exponential tail. The theorem is known as a Komlós–Major–Tusnády type approximation, but the mission follows the exact formulation and hypotheses printed by Ethier and Kurtz.
Let be a probability measure on . The hypothesis requires an such that
Thus the moment-generating integral is finite on a neighborhood of zero. No centering, symmetry, bounded-support, or positive-variance assumption is made.
The conclusion constructs one probability space carrying an iid sequence with common law and a Brownian motion . The Brownian motion has drift and variance chosen to match one summand:
Writing , both and are evaluated on this same space. The theorem does not require the iid sequence to be independent of the Brownian coordinate; their dependence is precisely what permits a close coupling.
There are positive constants , , and , depending only on , such that for every integer and every real ,
Both inequalities are strict: the discrepancy event uses and its probability is . The constants and the entire coupling are chosen before and . The logarithmic term is retained at , where .
The Lean statement uses sequence coordinates indexed from zero, so coordinate represents the source variable and Finset.range k is exactly the sum of the first variables. An existential index with expresses the finite maximum event without replacing either strict inequality.
Weak convergence compares distributions after rescaling and does not place a prelimit sum and its limiting process on the same sample point. This theorem instead supplies a simultaneous pathwise comparison through a common-space construction. The exponential tail quantifies the chance that the uniform error up to time exceeds the logarithmic scale by an additional amount .
The formal statement records the complete coupling rather than only its consequence for normalized terminal sums. It exposes the iid coordinate laws, mutual independence of those coordinates, the Brownian law, the moment-matched affine scaling, the positivity and quantifier order of the constants, and the exact maximal-error event. This is a statement-only formalization: the theorem remains an open Lean goal, and no proof claim is made.
Matching a single sum to a Gaussian random variable is not enough. The construction must coordinate every partial sum with one Brownian path, uniformly over all , while keeping the error logarithmic and the excess probability exponentially small. Independent coupling at each time would destroy consistency across times, while an ordinary invariance principle gives convergence in distribution without the stated finite- tail. The difficulty is therefore the joint construction with all of these quantitative requirements at once.
The common carrier is the product of a real sequence space with the subtype of continuous functions from nonnegative real time to . A probability measure on that carrier is the joint law. iIndepFun asserts mutual independence of all sequence coordinates, and HasLaw gives each coordinate the law . IsBrownianReal specifies the standard Brownian second coordinate.
The Brownian motion appearing in the estimate is defined from that standard coordinate by
This representation covers the zero-variance case: then the scaled Brownian fluctuation vanishes and is deterministic, while the auxiliary standard Brownian coordinate may still be present on the common carrier. The exponential-moment hypothesis supplies the intended finite first and second moments. Probabilities use extended nonnegative reals, and the finite positive real bound is embedded with ENNReal.ofReal.
No local auxiliary definition is expression-essential: all objects in the theorem are provided by Mathlib. The mission intentionally excludes the section's rescaling observations and Poisson corollaries, which do not form separate capstone goals in the accepted grouping. Useful future contributions include the proof of this exact common-space theorem and reusable coupling infrastructure that preserves strict tail estimates.
Ranking is the learning problem behind search engines, recommendation systems and fraud-alert
triage: what matters is not a single classification decision but the relative order the system
assigns to a set of items, because a user or analyst can only act on the very top of a ranked
list. Chapter 10 develops margin-based generalization theory for the score-based ranking
setting, transplanting chunk 05-svm's single-sample Rademacher-complexity machinery to a
genuinely two-sample structure: a ranking example is a pair of points, one drawn from each of
two positions, and the chapter's bound must therefore control two marginal complexities rather
than one. It also introduces RankBoost, the ranking analogue of AdaBoost, with a boosting-style
empirical-error guarantee proved by the same normalization-factor telescoping argument as
chunk 07's AdaBoost bound, adapted to RankBoost's own pairwise per-round quantities.
A ranking example is a pair (x,x') drawn from a distribution D over X×X, labeled by a
preference function f; restricted to {-1,+1} labels (the simplification §10.2 adopts), a
scoring function h:X→ℝ misranks (x,x') when f(x,x')(h(x')-h(x)) ≤ 0 (Eq. 10.1/10.2). The
empirical margin loss R̂_{S,ρ}(h) (Eq. 10.3) uses the same Φ_ρ (Definition 5.5) as chunk
05-svm, restated locally here. Writing S1, S2 for the two coordinate projections of a
pair sample S, and D1, D2 for the corresponding marginals of D, R_m^{D1}(H) and
R_m^{D2}(H) are the Rademacher complexities of H under each marginal (p. 241). Theorem
10.1 bounds R(h) in terms of these two Rademacher-complexity terms, both in their population
form (R_m^{D1}, R_m^{D2}) and their empirical form (R̂_{S1}, R̂_{S2}), via chunk 03's
Theorem 3.3 applied through an auxiliary hypothesis family H̃ = {((x,x'),y) ↦ y[h(x')-h(x)]}.
Corollary 10.2 specializes this to kernel-based linear scoring hypotheses; §10.4 introduces
RankBoost (Figure 10.1), whose per-round weighted pairwise-outcome fractions ε_t^+, ε_t^-
(Eq. 10.11) play the role AdaBoost's single ε_t plays in chunk 07, and Theorem 10.3 bounds
RankBoost's empirical error in terms of them. Corollary 10.4 combines Theorem 10.1 with Lemma
7.4 (the convex hull of H has the same empirical Rademacher complexity as H, restated as a
standing fact of the boosting series) to give RankBoost's own margin-based guarantee.
Theorem 10.1 — the mission's goal. For H a set of real-valued functions, ρ>0, δ>0,
with probability at least 1-δ, for all h∈H:
Corollary 10.2 (milestone). For a PDS kernel K with r an upper bound on K(x,x),
feature map Φ, and H = {x↦w·Φ(x) : ‖w‖≤Λ}, fixed ρ>0: R(h) ≤ R̂_{S,ρ}(h) + 4√(r²Λ²/ρ²/m) + √(log(1/δ)/(2m)).
Theorem 10.3 (milestone). RankBoost's empirical error verifies R̂_S(f) ≤ exp(-2∑_t((ε_t^+-ε_t^-)/2)²), and ≤ exp(-2γ²T) if the edge is uniformly at least γ>0.
Corollary 10.4 (milestone). Theorem 10.1's first bound, applied to h∈conv(H).
Theorem 10.1's proof is the chapter's genuine new technique, not a restatement of chunk 05's
Theorem 5.8: the two-sample decomposition (splitting the supremum over H̃ into a term on x'
alone and a term on x alone, each bounded by the Rademacher complexity under its own
marginal) is what the 2/ρ · (R_m^{D1}+R_m^{D2}) structure expresses, and collapsing it to a
single-sample bound would either be false or silently assume D1=D2 (which only holds for a
symmetric D, an assumption the theorem does not make). Corollary 10.2 is the direct
theoretical basis for the ranking SVM algorithm §10.3 derives. Theorem 10.3 mirrors chunk
07-boosting's Theorem 7.2 almost line for line in its proof technique (the same telescoping
product of normalization factors Z_t), but with genuinely different per-round quantities
(ε_t^+, ε_t^- rather than a single ε_t) that must not be conflated with AdaBoost's own, per
BRIEF.md's pitfall note. Corollary 10.4 is what makes RankBoost's output (a linear, not
convex, combination — normalized by ‖α‖_1) provably generalize independently of the number of
boosting rounds T, the ranking analogue of chunk 07's Corollary 7.5. No prior art exists on
the platform: GET /theorems?q=ranking%20loss returns zero hits.
Theorem 10.1's proof needs the two-sample structure carried through explicitly: H̃'s
Rademacher complexity splits, via the sub-additivity of sup and the fact that y_iσ_i and
σ_i have the same distribution, into a term on S2 alone and a term on S1 alone — treating
a ranking sample as an ordinary single sample (chunk 03's single-hypothesis-set machinery
applied naively) would drop this structure entirely and is exactly the pitfall BRIEF.md
names. Theorem 10.3's proof requires Z_t = ε_t^0 + 2√(ε_t^+ε_t^-) be bounded via the identity
4ε_t^+ε_t^- = (1-ε_t^0)^2 - (ε_t^+-ε_t^-)^2 and the inequality 1-x ≤ e^{-x} — the same
telescoping-normalizer technique as AdaBoost's Theorem 7.2, but RankBoost's own D_t,
ε_t^+, ε_t^- genuinely differ (they are defined via pairwise outcomes y_i(h(x'_i)-h(x_i)) ∈ {-1,0,+1}, not a single-point disagreement h(x_i)≠y_i) and must be modeled as their own
recursively-defined algorithm state, not obtained by substitution into chunk 07's AdaBoost
Lean.
MarginLossFunction restates chunk 05-svm's Definition 5.5; EmpiricalRademacherComplexity/
RademacherComplexity restate chunk 03-rademacher-vc's Definitions 3.1/3.2; IsPDS restates
chunk 06-kernels's PDS-kernel definition; ConvHull restates chunk 07-boosting's convex-hull
definition — all duplicated rather than imported since a draft item cannot import another
chunk's draft module, and none is listed as reusable in missions/README.md's "Published
definitions" table at the time of this session. D1, D2 are computed directly as
Measure.map Prod.fst D/Measure.map Prod.snd D rather than posited via a separate marginal
hypothesis, so the theorem statement itself pins down that they are genuinely the marginals of
the sampling distribution D, not independent parameters. Corollary 10.2's r is an explicit
upper bound on K(x,x) (hrK : ∀ x, K x x ≤ r) rather than a literal sSup, per BRIEF.md's
pitfall note about the possibly-infinite supremum — the theorem's conclusion is monotonic in
r, so this is not a weakening. RankBoost's D_t, ε_t^+, ε_t^-, α_t, Z_t and returned
function f are modeled as their own recursively-defined algorithm state (mirroring chunk
07's AdaBoostDist/AdaBoostEpsilon/AdaBoostEnsemble pattern exactly, but built from
RankBoost's own pairwise-outcome quantities, never by substituting into the AdaBoost Lean, per
BRIEF.md's pitfall note) — RankBoostEpsilonPlus/RankBoostEpsilonMinus are already tied to
RankBoost's own D_t and selected base ranker, so Theorem 10.3 needs no separate hypothesis
connecting them (the same trivialization guard chunk 07's own Theorem 7.2 documents). No
numerical constant is altered from the book in any of the four theorems.
Not formalized: §10.3's ranking-SVM primal/dual optimization problems (an algorithm derived
from Corollary 10.2, not a generalization-theoretic result); §10.4.2 (RankBoost as coordinate
descent, an algorithmic-equivalence argument, not a generalization bound); §10.5 (bipartite
ranking, its own distinct problem formulation with a different generalization error, Eq. 10.20,
explicitly out of scope per BRIEF.md); §10.6-10.7 (preference-based ranking, other criteria),
out of scope per BRIEF.md. The uniform-over-ρ extension mentioned after both Theorem 10.1's
and Corollary 10.2's proofs (referencing Theorem 5.9's technique from a different chapter) is
not drafted, matching chunk 09-multiclass's identical scope decision for the analogous remark.
Regression is usually taught with a fixed parametric model: linear regression fits a -dimensional coefficient vector, and the estimation error is controlled by . Many regression problems in practice have no such finite-dimensional description — the regressor is only known to be, say, convex, monotone, or smooth, and the estimator is a least-squares fit over the (infinite-dimensional) set of functions with that shape. This is nonparametric regression, and the basic question is the same as in the parametric case: how close is the fitted function to the truth, as a function of the sample size ? Answering it requires replacing "dimension" with a genuinely functional notion of complexity, since an infinite- dimensional function class can still be small enough to estimate well (a Sobolev ball) or too large to estimate at all. The theory in this mission, due to van de Geer and developed in Chapter 13 of Wainwright (High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019), gives a single non-asymptotic template — the localized Gaussian complexity — that answers this question for an arbitrary star-shaped function class, and recovers the familiar parametric and Sobolev/RKHS rates as special cases.
Fix design points in an arbitrary covariate space (fixed, not random — this is the fixed-design setting) and observe
where is the unknown regression function, is a known noise level, and are i.i.d. standard Gaussian. Given a class of candidate functions, the nonparametric least-squares estimate is any minimizer
Error is measured in the empirical (design-dependent) seminorm . A class of functions is star-shaped if and together imply — every convex class containing the origin has this property, and it is the minimal structural assumption under which the theory below applies. For a star-shaped class and radius , the local Gaussian complexity
measures how much a mean-zero Gaussian process can be made to look like a member of restricted to the ball of radius . A critical radius is any positive solution of ; by Lemma 13.6, is non-increasing on star-shaped, so this inequality always has a smallest positive solution.
Lemma 13.6. For any star-shaped , is non-increasing on , and consequently has a smallest positive solution for every .
Theorem 13.5 (special case, ).
Theorem 13.13 (goal — general oracle inequality, not assumed in ). With solving the critical inequality for , there are universal constants such that for all ,
with probability at least . The goal is deliberately the statement with unresolved universal constants and an infimum over , rather than any single instantiated bound, so the target survives sharper constant tracking.
Theorem 13.13 is the "master" result behind essentially every concrete rate in the chapter: orthogonal series regression, convex/monotone regression, and (via the KRR specialization of Section 13.4) kernel ridge regression rates for Sobolev and Gaussian-kernel classes are all obtained by bounding for a particular and reading off . Its value is that it isolates exactly the one place where the geometry of enters — the local Gaussian complexity — while the probabilistic argument (a peeling/chaining argument controlling a localized empirical process) is generic. Formalizing it produces, for the first time on the platform, the statement-level infrastructure (star-shaped classes, local Gaussian complexity, critical radius) that any future mission on a concrete nonparametric-regression rate — kernel ridge regression, convex regression, isotonic regression — can specialize, without re-deriving the oracle inequality from scratch. The proof itself (concentration of Gaussian complexity via Borell-TIS/Gaussian comparison plus a peeling argument over dyadic scales) is not attempted here; only the statement is formalized, as a draft goal for future proof contributions.
The naive route to Theorem 13.13 is to bound pointwise via the basic inequality and then bound the right side by for — but is itself random (it depends on the estimate), so this is circular: the bound on the right depends on the very quantity being bounded. The chapter's actual argument resolves this with a peeling device: partition the event space by which dyadic annulus falls into, and apply a uniform (non-circular) bound on each annulus separately via Gaussian concentration, summing a geometric series of tail probabilities. This is the step every first attempt misses, and it is why the local Gaussian complexity — rather than the simpler global complexity of Chapter 4/5 — is the right object: localizing to radius is what makes the per-annulus bound tight enough for the final sum to converge.
Design points are an arbitrary type X (no topology or metric structure is needed for the
statements themselves); the least-squares estimate is represented as a Prop
(IsLeastSquaresEstimate) picking out any function achieving the empirical minimum, matching
the book's "any minimizer" phrasing rather than assuming uniqueness. The local Gaussian
complexity is defined as an expectation over an explicit i.i.d.-standard-Gaussian noise vector
on an abstract probability space, with the inner supremum taken over the subtype of the
radius-restricted slice of the class — this is well-defined (not the junk value 0 of an
unbounded Set ℝ supremum) whenever the slice is nonempty, which holds automatically for any
nonempty star-shaped class (taking exhibits in the class). Since neither X nor
H carries a topology, separability or countability constraint, SatisfiesCriticalInequality
adds an explicit Integrable hypothesis on that same supremum (added in revision), guarding
against Mathlib's Bochner integral silently returning the junk value 0 for a non-measurable
integrand — a value that would otherwise trivially satisfy the critical inequality for every
positive δ, regardless of the function class's actual local complexity. The trivializing
formalization to rule out here is stating Theorem 13.13's universal constants after the
quantification over the function class and sample size, which would let
secretly depend on the instance and make the "universal" claim vacuous; this mission places
the constant quantifiers first, before the class, design and noise data they must not depend
on. A complete downstream development would add: the concentration-of-Gaussian-complexity step
(Borell–TIS or a comparable tail bound), the peeling argument, and the metric-entropy /
Dudley-integral machinery of Section 13.2.1 for bounding explicitly on concrete classes
(Sobolev balls, RKHS balls) — none of which is attempted here.
Many statistical problems — nonparametric regression, density estimation, dimension reduction, testing — are naturally posed as optimization over a space of functions rather than a finite-dimensional parameter vector. Hilbert spaces provide the right generality: they carry an inner product and a norm, so notions of projection, orthogonality and least-squares fitting all make sense, exactly as in ordinary Euclidean space, even though the "vectors" are now functions. Reproducing kernel Hilbert spaces (RKHSs) are the particular class of function-valued Hilbert spaces that make this program computationally tractable: they are generated by a single bivariate kernel function, and every RKHS computation reduces to evaluating that kernel, never to manipulating an infinite-dimensional object directly (the "kernel trick"). Wainwright's High-Dimensional Statistics (2019), Chapter 12, develops the foundational correspondence between kernels and Hilbert spaces that makes this possible, and this mission formalizes its two central theorems.
A Hilbert space is a complete inner product space (Definitions 12.1–12.2); this mission
uses Mathlib's own NormedAddCommGroup/InnerProductSpace ℝ/CompleteSpace typeclasses for
this notion throughout. A linear functional is bounded if
for some and all ; the Riesz representation theorem
(Theorem 12.5) says every such functional is for a unique .
A bivariate function is a positive semidefinite (PSD) kernel (Definition 12.6) if it is symmetric and every finite Gram matrix is positive semidefinite — the natural generalization of a PSD matrix to a (possibly infinite) index set , with no topological structure on required. A reproducing kernel Hilbert space (RKHS) for a kernel is a Hilbert space of functions on such that, for every , the function belongs to and
— the reproducing property. Equivalently (Definition 12.12), is an RKHS exactly when every evaluation functional is bounded on .
Given any PSD kernel function on any set , there is a Hilbert space (embedded into functions on ) in which satisfies the reproducing property (12.3) — and this Hilbert space is unique: any two Hilbert spaces with this property for the same are linearly isometric via an isometry intertwining their embeddings into functions on .
Theorem 12.11 is the theorem that makes the entire RKHS apparatus well-posed: every time a statistician writes down a kernel — linear, polynomial, Gaussian — Theorem 12.11 guarantees that a canonical Hilbert space of functions exists in which that kernel reproduces, so that optimizing over "the RKHS associated with " is a well-defined problem, not merely a suggestive shorthand. Theorem 12.13's converse shows the correspondence is exact — the class of kernel-generated Hilbert spaces is exactly the class of function spaces with bounded evaluation, the class relevant to any statistical application that samples a function at finitely many points. Together, these two results are the foundation the book's own later chapters build directly on: Chapter 13's nonparametric least-squares oracle inequality, and Chapter 14's kernel density estimation, both work by optimizing over an RKHS and are only well-posed because of this correspondence. Mercer's theorem, in turn, is what connects the RKHS viewpoint back to the earlier feature-map viewpoint of Chapter 12.2.2 (Eq. 12.2): the eigenfunctions give an explicit feature map into realizing , and its expansion is what later underlies the book's discussion of kernel PCA and of RKHS balls as ellipsoids in -coordinates.
The formalization difficulty is concentrated in getting the type of the existence-and-
uniqueness claim right, not in any single hypothesis. A Hilbert space is not naturally a
subtype of a fixed ambient space in Lean, so "the Hilbert space " of Theorem 12.11 is
formalized as an abstract type together with its own NormedAddCommGroup/InnerProductSpace ℝ/CompleteSpace instances, connected to "a space of functions on " via an injective
linear embedding into — and uniqueness must then be stated as an isometric
equivalence between any two witnessing Hilbert spaces that respects this embedding, the
faithful rendering of the book's own proof, which literally shows two candidate Hilbert spaces
are equal as sets of functions. A second subtlety is keeping Theorem 12.11's hypotheses
(a bare PSD kernel, no topology on ) cleanly separated from Mercer's theorem's additional
compactness, continuity and measure-theoretic apparatus — the two theorems are frequently
conflated informally, but the book is explicit that Theorem 12.11 needs none of Mercer's
structure.
is an unconstrained Type* for Theorem 12.5, 12.11 and 12.13 — no topology, matching the
book's own generality. Mercer's theorem (Theorem 12.20) additionally requires [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] and a finite measure P, matching its
own compactness/continuity/measure-theoretic hypotheses exactly, never applied outside that
scope. The integral operator of Eq. (12.11a) is presented as an abstract linear map on
Lp ℝ 2 P tied to the defining integral formula via an explicit hypothesis, rather than
constructed as a def, since constructing it as a genuine well-defined operator (needing
integrability and a.e.-measurability arguments) is proof content, not definitional content,
and this mission's definitions file is sorry-free by convention. Mercer's orthonormal-basis
index type is existentially quantified over a countable ι (∃ (ι : Type) (_ : Countable ι), ...) rather than fixed to ℕ, since L²(X;P) can be finite-dimensional for finite X
(Example 12.18/12.21), where no infinite orthonormal basis exists; the uniform-convergence
conjunct is correspondingly quantified over every bijection e : ℕ ≃ ι (vacuous when ι is
finite, a genuine order-independent claim when ι is countably infinite). A trivializing formalization
of this chapter would state only existence in Theorem 12.11 and drop uniqueness (explicitly
warned against by this chapter's own brief), or state Mercer's convergence merely pointwise
or in rather than absolutely and uniformly; this mission avoids both. Out of scope: the
constructive proof detail of Theorem 12.11 (the explicit span-and-complete construction is proof
content, not part of the statement), the chapter's worked kernel examples (linear, polynomial,
Gaussian kernels, Examples 12.7–12.9), and the further consequences of Mercer's theorem
(Corollary 12.26 on RKHS-ball ellipsoids, the feature-map connection of Eq. 12.14) — all natural
follow-on work for a future mission on kernel-based nonparametric regression (Chapter 13,
mission 13-nonparametric-ls), which restates whatever RKHS objects it needs locally rather
than importing this mission's draft, per this book's series-wide convention.
Chapters 2 through 8 of Wainwright's High-Dimensional Statistics build up sharp error bounds for a sequence of specific high-dimensional models — sparse linear regression via the Lasso (Chapter 7), sparse principal components (Chapter 8) — each proved from scratch with techniques tailored to that model's own penalty and loss. Chapter 9 steps back and asks what made all of those arguments work, and isolates the answer into two structural ingredients: a decomposable regularizer, whose triangle inequality is tight across a well-chosen subspace pair, and a restricted curvature condition on the loss, holding only on the cone that decomposability forces the estimation error into. Once these two ingredients are checked for a particular model, a single, already-proved oracle inequality hands back the error bound — no further optimization-theoretic argument is needed. This mission formalizes that oracle inequality itself, together with its two supporting theorems, as the reusable core the book's later chapters (nuclear-norm matrix regression in Chapter 10, graphical model selection in Chapter 11, group-sparse and overlap-group Lassos) each specialize.
Let be a finite-dimensional real inner product space (e.g. , or a matrix space with the Frobenius inner product), and consider the regularized M-estimator
where is a convex empirical cost function, is a norm-based regularizer, and is a user-chosen regularization weight. Write for the true parameter and for the estimation error.
A pair of subspaces of — the model subspace and its (possibly larger) closure — has an associated perturbation subspace , the orthogonal complement of . The regularizer is decomposable with respect to if the triangle inequality is an equality whenever and — the regularizer penalizes deviations away from the model subspace exactly as much as it possibly could. The canonical example is the -norm with the subspace of vectors supported on a fixed index set .
Writing for the dual norm, the good event says the regularization weight dominates the dual norm of the score function at the truth — the non-probabilistic conditioning hypothesis every result in this chapter is stated under. The subspace Lipschitz constant measures the worst-case price of converting between the regularizer and the error norm on a subspace .
Under (A1) convex, satisfying restricted strong convexity (RSC) with curvature , radius and tolerance — for — and (A2) decomposable with respect to : conditioned on , any optimal satisfies
and, whenever and ,
Theorem 9.19 is the book's own claimed unifying result: as it remarks explicitly, the theorem
is a deterministic implication, and every later probabilistic corollary in Parts II and III of
the book is obtained by (i) checking that a specific loss/regularizer pair is decomposable with
respect to a natural subspace pair for the problem at hand, (ii) certifying the RSC condition
with high probability for that loss (via concentration arguments from Chapters 2–6), and (iii)
choosing large enough that the good event holds with high probability — then reading
off the rate directly from . Chapter 7's Lasso
bound (Theorem 7.13, mission 07-sparse-linear) is exactly Corollary 9.20 specialized to
and the subspace of -sparse vectors — but Chapter 9 proves it
once, in a form that Chapter 10's nuclear-norm-regularized low-rank matrix regression (mission
10-matrix-rank), Chapter 11's graphical model selection, and the chapter's own group-Lasso and
overlap-group-Lasso examples all instantiate without re-deriving the optimization argument.
The formalization difficulty here is almost entirely conceptual rather than syntactic: getting
the two-subspace apparatus exactly right. The book explicitly
allows to be a strict superset of (needed for the nuclear norm
in Chapter 10, where the naive choice fails to be decomposable at
all), so every definition and theorem in this mission is parameterized by the pair, not by a
single subspace — and three genuinely different projections appear across the statements: the
error vector's projection onto and onto (both keep
the bar), versus the true parameter's projection onto (the complement of the
small, unbarred subspace). A further subtlety specific to this printed source: several of the
book's own displayed equations for in Theorem 9.19 and Corollary 9.20 lose the
overbar on in PDF text extraction (a rendering artifact, not a mathematical
ambiguity); resolving which subspace is meant required reading the surrounding proof text line
by line, since only — not — is mathematically
consistent with how the constant is derived and used (see MODERATION_NOTES.md).
is [NormedAddCommGroup Ω] [InnerProductSpace ℝ Ω] [FiniteDimensional ℝ Ω], matching
the book's implicit assumption of a finite-dimensional inner-product parameter space throughout
this part of the book. The regularizer's norm axioms (IsRegularizerNorm), the dual norm, and
the subspace Lipschitz constant are all defined via sSup/sInf-free explicit formulas or
sSup over an explicitly-described set (never an unconstrained supremum over all of ),
so no faithfulness trap from an unbounded or empty supremum arises (see
MODERATION_NOTES.md's trap table). κ > 0 and λ_n > 0 are made explicit hypotheses of every
theorem, matching Definition 9.15's own stated positivity of and the chapter's
running convention that is a positive regularization weight — never a narrowing
of the theorem's actual scope. A trivializing formalization of this chapter would either collapse
the two-subspace machinery to a single subspace (which is faithful
only for the /group-Lasso examples, not the general theorem, and not what Chapter 10
needs) or silently drop the second conjunct of Theorem 9.19's conclusion (part (b), the actual
quantitative rate) in favor of only the qualitative part (a); this mission formalizes the full
two-subspace statement and both conjuncts of the goal theorem. Out of scope: the chapter's
worked examples (sparse GLMs, Corollary 9.26; group Lasso; nuclear-norm matrix regression) that
specialize the goal to concrete models — Chapter 10's own mission (10-matrix-rank) restates
the needed instance of this framework locally rather than importing this mission's draft, per
this book's series-wide convention that no draft imports another chunk's draft. Also out of
scope: the RSC-implies-restricted-eigenvalue correspondence (Example 9.16) and the
-based general RSC certification (Theorem 9.36, Section 9.8), both purely
probabilistic results that lie outside this chapter's own deterministic core.
Chapter 2's finite-hypothesis-set learning bound is uninformative the moment is infinite — diverges — yet most hypothesis sets used in practice (linear separators, neural networks, decision trees) are infinite. Chapter 3 answers the question the previous chapter's own worked example (axis-aligned rectangles, Example 2.4) leaves open: is efficient learning from a finite sample still possible for an infinite hypothesis set, and can this be shown in general rather than case by case? The chapter's answer runs through two complementary notions of complexity — Rademacher complexity, a data-dependent measure of how well a function family correlates with random noise, and the VC-dimension, a purely combinatorial measure of the number of distinct labelings a hypothesis set can realize on a finite point set — connected by Massart's lemma and Sauer's lemma, and culminating in a generalization bound that replaces with the VC-dimension .
For a family of functions and a sample , the empirical Rademacher complexity (Definition 3.1) measures how well fits random sign noise on ; the Rademacher complexity (Definition 3.2) averages this over samples. Theorem 3.3 converts a Rademacher-complexity bound directly into a generalization bound via McDiarmid's inequality. For binary hypothesis sets , the growth function (Definition 3.6) counts the maximum number of distinct dichotomies realizes on points, and the VC-dimension (Definition 3.10) is the largest for which (i.e. shatters some set of points). Massart's lemma (Theorem 3.7) is the purely combinatorial tool bounding the expected maximum of a sum of signed vector components by , and Sauer's lemma (Theorem 3.17) bounds the growth function itself, by induction on , whenever the VC-dimension is finite.
Theorem 3.3 (Rademacher generalization bound, milestone). For and any , with probability at least over an i.i.d. sample of size , for all : .
Theorem 3.7 (Massart's lemma, milestone). For a finite with : .
Theorem 3.17 (Sauer's lemma, milestone). For with , for all : .
Corollary 3.19 — the mission's goal. For with and any , with probability at least , for all :
Corollary 3.19 is the chapter's answer to the question chapter 2 leaves open: it is Theorem
2.13's direct infinite-hypothesis-set generalization, replacing (undefined for
infinite ) with the VC-dimension (finite even for many infinite hypothesis sets, such
as halfspaces in , which have VC-dimension ). It is also the template every
later margin bound in the book specializes (Chapters 5, 9, 10's SVM, multi-class and ranking
margin bounds all replace this bound's uniform /VC-dimension term with a
scale-sensitive complexity measure derived from the same Rademacher-complexity machinery), and
Sauer's lemma is independently one of the most cited results in learning theory and extremal
combinatorics. No prior art on the Prove2Me platform is faithful to any of this chapter's
content: RademacherSymmetrization.radS_chernoff (Aether Catalog) proves a different,
Massart-optimized Chernoff bound for the empirical Rademacher complexity of a finite class —
a different object (empirical vs. population) with a different bound form from Theorem 3.3/3.5
— and sauerShelah_full proves only the trivial identity sauerShelahBound k k = 2^k, not
Sauer's lemma itself. A further hit, sauer_shelah (Aether Catalog, Algebra/SauerShelah.lean),
does state the Sauer-Shelah bound itself (F.card ≤ ∑_{i≤d} C(n,i) for a family F of subsets
of Fin n shattering no set larger than d) — checked and not reused: it is a different idiom
from Theorem 3.17 as this chunk needs it, a fixed finite ambient domain Fin n with F a
Finset of its subsets directly, rather than the book's own growth function Π_H(m) (a
supremum over point-tuples drawn from an arbitrary, possibly infinite X, Definition 3.6) that
this chunk's other items and the goal (Corollary 3.19) are built on; reusing it would require
either abandoning GrowthFunction/HasVCDim (needed faithfully by the goal itself) or a
nontrivial reduction lemma this mission's budget does not include, so sauer_lemma is drafted
fresh against this chunk's own GrowthFunction/HasVCDim. All ten items are drafted fresh.
Sauer's lemma's proof is a genuine two-parameter induction (on ) with a real combinatorial
construction: restricting to a sample of size , then splitting the restricted
family into (its restriction to the first points) and (the concepts whose
membership in changes with the addition of the -th point), with and
— a genuinely combinatorial argument, not a
statement that unfolds by simp; a weaker restatement using only the trivial bound
would be true but is explicitly not what Theorem 3.17 states (BRIEF.md's
named trivializing formalization for this chapter). Massart's lemma needs the expectation of a
supremum over a finite set of -many sign patterns kept as an honest average, not silently
replaced by a looser union bound. Corollary 3.19's own term inside the logarithm needs
the side condition carried through explicitly — Corollary 3.18's own domain restricts
to , and the bound is false, not merely unproved, without it (at , can be
smaller than , making the logarithm negative).
GeneralizationError/EmpiricalError are restated locally in this chunk's RademacherVC
namespace (byte-identical in content to chunk 02-pac's own copies), since a draft item cannot
import another chunk's draft module; this duplication is expected and will collapse once
02-pac is moderated, uploaded and listed as reusable in missions/README.md's "Published
definitions" table. EmpiricalRademacherComplexity/Massart's lemma model the Rademacher signs
σ as ranging over the finite type Fin m → Bool rather than a measure-theoretic i.i.d.
process, so the "expectation over σ" in both is the exact finite uniform average over its
2^m outcomes — faithful and simpler than a MeasureTheory construction, since σ's
distribution really is uniform on a finite set of outcomes for every finite m. GrowthFunction
takes a tuple of m points (Fin m → X) rather than a size-m subset of X, a harmless
generalization (repeated points never increase the dichotomy count) documented in the item's own
docstring. HasVCDim is a Prop parametrized by the candidate dimension rather than a total
ℕ/ℕ∞-valued function, so it does not cover the book's VCdim(H)=+\infty case (Examples
3.15-3.16); every theorem using it takes HasVCDim H d as an explicit hypothesis, matching the
book's own "let H... with VCdim(H)=d." Theorem 3.3 adds an explicit measurability
hypothesis on G (hGm) beyond the book's own displayed statement, needed to keep the Bochner
integral ∫ z, g z ∂D from silently evaluating to 0 for a non-measurable g — this is the
book's own standing assumption (footnote 3, p. 30) made an explicit hypothesis rather than an
implicit one. No numerical constant in any of the four theorems is altered from the book's own;
Corollary 3.19's side condition d ≤ m is kept explicit, per BRIEF.md's pitfall note.
Not formalized: Lemma 3.4 and Theorem 3.5 (the binary-classification specialization of Theorem
3.3 via the zero-one-loss identity ), Corollary 3.8 and
Corollary 3.9 (the intermediate Rademacher-to-growth-function and growth-function
generalization bounds), and Corollary 3.18 (the VC-dimension bound on the growth function,
for ) — five intermediate results in the proof chain
Theorem 3.3 → Theorem 3.5 → Corollary 3.8/3.9 → Sauer's lemma → Corollary 3.18 → Corollary 3.19
that are not independently drafted as milestones, per the budget guidance to keep a chunk to a
goal plus its most load-bearing 3-8 milestones rather than every numbered result on the page;
the three drafted milestones (Theorem 3.3, Massart's lemma, Sauer's lemma) are the chain's three
genuinely distinct proof techniques (McDiarmid's inequality, a probabilistic-maximum bound, and
a combinatorial induction), and the goal theorem's own statement is Corollary 3.19 exactly as
displayed, not a restatement of any intermediate corollary. Radon's theorem (Theorem 3.13,
background for the hyperplane VC-dimension example) and the worked VC-dimension examples
(intervals, hyperplanes, rectangles, convex polygons, sine functions) are illustrations, not
general results, and are not formalized — drafting only the example computations (e.g.
VCdim(hyperplanes) = d+1) instead of the general finite-H machinery is exactly the
trivializing formalization this mission avoids.
Every algorithm in Chapters I–V observes the full cost function after playing . Many applications only reveal the scalar cost incurred — routing a network and observing total latency, or placing an ad and observing the click-through revenue, without ever seeing the cost of a path or bid not taken. This is the bandit feedback model, and Chapter 6 asks whether sublinear regret survives it. The chapter's answer is a general two-part reduction — turn a first-order full-information algorithm into a bandit algorithm by feeding it an unbiased gradient estimator built from a single scalar observation — instantiated concretely on online gradient descent to produce the first historical bandit convex optimization algorithm, the FKM algorithm (Flaxman–Kalai–McMahan).
Let be the decision set, containing the unit ball centered at , with diameter at most . At each round the player picks , an adversary has fixed a cost function (Lipschitz constant , bounded by in absolute value on ), and the player observes only the scalar — never itself or its gradient. Regret is , exactly as in the full-information setting, but now the algorithm's plays are themselves random (they depend on the sampled gradient estimates), so the guarantee is on expected regret.
The chapter's construction has two independent parts. Part 1 (Lemma 6.5) is a black-box reduction: given any first order full-information algorithm (Definition 6.4 — one that depends on each cost function only through its gradient at the played point) with a full-information regret bound , feeding an unbiased estimator of in place of the true gradient preserves the regret bound in expectation, up to evaluated at the estimators instead of the true gradients. Part 2 (Lemma 6.7) supplies such an estimator using only one scalar observation per round: sample uniformly from the unit sphere, play for a small radius , and is (for linear ) an unbiased estimator of — more precisely, an unbiased estimator of the gradient of 's -smoothed version , by a Stokes'-theorem identity relating a ball integral to a sphere integral.
for any fixed , any first order algorithm with full-information bound , and any sequence of estimators with .
The FKM algorithm (Algorithm 23: play , form , update on the shrunk set ) with , guarantees
Theorem 6.9's rate is strictly worse than the rate of full-information online gradient descent (Chapter III) — this gap, not a shared rate, is the chapter's real content: bandit feedback provably costs regret, and the FKM algorithm is the historically first algorithm to pin down how much, via the clean two-part reduction that later chapters' improved bandit algorithms (§6.5's self-concordant-barrier method, not formalized here) all refine. Lemma 6.5 is independently reusable: it is a template, quantified over an arbitrary first-order algorithm and an arbitrary unbiased-estimator family, not tied to the sphere-sampling construction that instantiates it for Theorem 6.9. No prior art was found on the platform for bandit convex optimization, gradient-free methods, or Frank–Wolfe-style estimators; this mission's three items formalize the standard textbook account fresh.
Lemma 6.5's proof is a martingale-style argument: it introduces auxiliary deterministic functions (where ) whose gradient at is exactly , applies 's full-information bound to the 's (a genuinely random cost sequence, since is random), and then takes expectations, using unbiasedness () to show and for the fixed comparator . This requires a genuine filtration and conditional expectation, not merely an unconditional expectation, since and are themselves random and adapted to different points in the history. Lemma 6.7's proof invokes Stokes' theorem to relate to , then uses the volume ratio — a calculus fact about Euclidean balls and spheres, not itself re-derived in this mission's Lean (the identity is drafted as the statement Lemma 6.7 asserts, to be proved from Mathlib's own ball/sphere volume and divergence-theorem lemmas).
IsFirstOrderOnlineAlgorithm formalizes only the substitution property of Definition 6.4 (the
book's second bullet); the first bullet, a closure condition on the admissible family of loss
functions, is a precondition on 's domain rather than a checkable mathematical property and is
not formalized — see MODERATION_NOTES.md. SmoothedFunction (Eq. (6.4)) and
IsUniformOnUnitSphere are declared once and shared by both milestones and the goal, rather than
re-derived inline. Lemma 6.5's history is modeled by an explicit filtration 𝓕 (with x t
adapted to 𝓕 t and g t to 𝓕 (t+1)), since Lean's conditional expectation needs a concrete
σ-algebra to condition on; the book's informal "history " is exactly this
filtration once the (deterministic) 's are set aside as carrying no randomness. Kδ, the
shrunk decision set Algorithm 23 actually projects onto, is kept a separate object from K
throughout (a pitfall the chapter brief flags explicitly), and in Theorem 6.9 is
rendered as an infimum, checked non-vacuous since is nonempty and the objective is bounded
below on by the chapter's own assumption.
Not formalized: §6.5's self-concordant-barrier bandit linear optimization algorithm (starred, out of the recommended goal's scope) and Corollary 6.8's ellipsoidal-sampling generalization (a routine corollary of Lemma 6.7 the book itself derives, not independently central).
Write the primes in increasing order, take the absolute differences of consecutive entries, take the absolute differences of the resulting row, and repeat. Every row produced this way appears to begin with :
Gilbreath's conjecture asserts that this never fails. The observation is due to Norman L. Gilbreath (1958), who rediscovered a statement already published by François Proth in 1878 together with an argument that is not accepted as a proof. It is attractive because it is elementary to state and because it is one of the few statements about the primes whose difficulty is not visibly analytic: it concerns the combinatorics of iterated differences rather than the distribution of primes directly.
Timeline.
No proof is known.
Let be the increasing enumeration of the prime numbers, indexed from . Define the rows of the Gilbreath triangle by
Thus is an infinite sequence of natural numbers for every , row is the sequence of primes, row is the sequence of prime gaps , and each later row is the sequence of absolute differences of consecutive entries of the row above it. Only the leading entry of each row is at issue.
More generally, for an arbitrary sequence write and for the -fold iterate, so that .
This is the conjecture in its standard form: every row after the row of primes begins with . It fixes no constants and no ranges, so no computational advance can invalidate it.
The milestone list collects the statements that a proof, or a further computational verification, would be built from: the two low-level structural facts about the triangle (row is the gap sequence; from row on, the leading entry is odd and all later entries are even), a finite verification of the first rows, and the two statements underlying Odlyzko's method — the propagation lemma for an arbitrary sequence beginning and continuing in , and the reduction of the conjecture to the existence, for each row index, of an earlier row with a long enough block of entries in .
The result itself. The conjecture is not known to imply other open statements about the primes, and its interest lies elsewhere: it is a test case for how much of the fine structure of the prime sequence is forced by coarse information. The propagation mechanism shows that the conjecture for a given row index follows from purely local data about an earlier row, and that mechanism is what every verification to date has relied on. A proof would have to show that such blocks of entries in always appear early enough, which is a statement about the density of small prime gaps in disguise.
Formalizing it. Nothing here is currently formalized: Mathlib has the prime
enumeration (Nat.nth Nat.Prime) and the basic facts about it, but
not the iterated-difference triangle nor any of its properties. This mission
contributes the definition of the triangle, the structural facts about its rows, and
a machine-checked version of the reduction step that all computational work on the
problem uses. The goal theorem itself is open — the milestones are known mathematics,
and each is provable with current tools, while the goal is not.
The obvious attack is induction on the row index: to see that it suffices to know that and . But controlling requires controlling and , and so on: the invariant that closes is not "the row begins with " but "the row begins with and its next entries lie in ", and each application of the difference operator consumes one entry of that block. So a finite block of good entries only carries the conclusion a finite number of rows further down, and the conjecture needs such blocks to keep reappearing forever, arbitrarily far down the triangle. Nothing is known that produces them.
A second warning, due to Hallard Croft: the property is not specific to the primes. Sequences that start with , continue with odd numbers, and have gaps that are not too large empirically exhibit the same behaviour, so any proof that uses only such coarse features would prove a much more general statement — and conversely, an argument exploiting deep properties of primes is likely to be proving the wrong thing.
Rows are total functions , defined for every index, and the
whole triangle is a single family indexed by the row number. Differences are taken as
Int.natAbs of a difference computed in , so truncated natural
subtraction never occurs; the one place where -subtraction does appear is
the milestone identifying row with the gap sequence, where the subtraction is
justified by monotonicity of .
Primes are indexed from via Mathlib's Nat.nth Nat.Prime, so ; rows are
indexed with row the primes, and the goal quantifies over all in the
form d (k + 1) 0 = 1, with no upper bound and no extra hypothesis, so no vacuous or
finitely-truncated reading of the goal is available. The general difference operator
is stated for arbitrary sequences , which is what makes the
propagation lemma usable as a black box, and reusable beyond this mission.
A complete development needs no analytic input for the milestones: Mathlib's
Nat.nth, Nat.prime_nth_prime, Nat.nth_prime_zero_eq_two and the strict
monotonicity of the prime enumeration suffice. Contributions that would extend the
mission beyond its current list: a formal version of a concrete computational
verification (checking that the leading entries of the first rows are for an
well beyond the hand-checkable range), and formalizations of the general
statement for non-prime sequences of the Croft type.
Mirror symmetry was discovered in string theory as a duality between families of Calabi–Yau manifolds, and it entered mathematics as a prediction: the generating function counting rational curves on one manifold equals a period integral of a mirror manifold. In his 1994 ICM address, Homological algebra of mirror symmetry (alg-geom/9411018), M. Kontsevich proposed that these numerical coincidences are shadows of an equivalence of categories: the symplectic geometry of should be encoded by Fukaya's -category , whose objects are Lagrangian submanifolds and whose products count pseudo-holomorphic discs, and the complex geometry of the mirror by the derived category of coherent sheaves. His Homological Mirror Conjecture asserts that the derived category built from embeds as a full triangulated subcategory of .
Kontsevich states the conjecture "in slightly vague form", because Fukaya's construction was not, and still is not, available in the generality the statement needs. He therefore closes the paper with the one instance he can compute by hand, in the section Two-dimensional tori: a return: for the flat torus , the objects are closed geodesics with unitary local systems, the products are sums over triangles in the universal cover weighted by , and their structure constants are values of the classical theta-function. He predicts an equivalence with for an elliptic curve . This instance was proved by A. Polishchuk and E. Zaslow, Categorical mirror symmetry: the elliptic curve (math/9801119). Later instances include the four-torus (Abouzaid–Smith, arXiv:0903.3065) and Calabi–Yau hypersurfaces (Sheridan, arXiv:1111.0632). None of this has been formalized.
Fix a real number , and let be the torus carrying the translation-invariant symplectic form of total area ; a region of Euclidean area in coordinates has symplectic area .
A brane consists of: a primitive vector and a point , which together determine the closed geodesic ; a grading , a real lift of the direction angle normalized so that is parallel to ; and a real constant describing a flat unitary line bundle on , whose parallel transport along a path of parameter length is . Two branes are transverse when ; their geodesics then meet in the finite set , which indexes a basis of the Floer space . All of this space sits in a single degree, the Maslov index
For three pairwise transverse branes and intersection points , , , a triangle is a triple of lifts of with parallel to , parallel to , parallel to , and positively oriented. Kontsevich's structure constant is
the coefficient of in . On the complex side, denotes the complexes of -modules with bounded, coherent cohomology.
For every there exist a smooth proper curve over , an assignment of an object of to each brane, and isomorphisms
with for , carrying the products to composition in whenever .
Existence of the Fukaya -category of the torus; finiteness of with points; the Maslov relation ; together with associativity of up to coboundary; the degeneration of an -category with to a differential graded category; the theta-function shape of the structure constants; and their associativity equation.
The conjecture reorganizes mirror symmetry: the numerical predictions compare two elements of an uncountable set of power series, whereas the homological statement compares two objects in a countable set of triangulated categories, and the numerical statements are meant to follow from it. The torus case is the smallest instance in which every ingredient — Lagrangian branes, Maslov grading, disc counts, theta functions, and coherent sheaves on an elliptic curve — is present and computable, so it is the natural first target.
What this mission adds beyond the literature is machine-checked mathematics where none exists. Mathlib currently has no symplectic manifolds, no Lagrangian Floer theory, no Fukaya categories, and no -categories; it does have schemes, sheaves of modules, and derived categories of abelian categories. The mission supplies the missing layer and the torus model, and asks for the comparison theorem. The definitions, the derived category with coherent cohomology, and the theta-function estimates are reusable outside this mission.
The obvious route — "transport the Polishchuk–Zaslow proof" — stalls at the point where the two sides are compared. Establishing that the triangle sums converge and equal theta-function values is analysis that Mathlib supports; producing an elliptic curve as a scheme with prescribed parameter, computing -groups between the mirror sheaves, and matching all products simultaneously is not currently supported by any library. A second difficulty is bookkeeping: gradings, Maslov indices and shifts must line up, since the product of two morphisms is nonzero only when , and the same numerical condition controls which triples of branes bound triangles at all.
Conventions committed to in Lean. An -category is encoded as a single graded module with morphism components and products given by a map on lists, of degree , with , and Stasheff signs in the bar-construction normalization; is " then ". Triangles are normalized by requiring the first vertex to lie in , which picks exactly one representative in each -orbit; only positively oriented triangles are counted; sums are tsums, so convergence is part of the work. The hom-space isomorphisms in the goal are required to be additive, not a priori -linear, because the derived category of -modules is not equipped with a -linear structure in Mathlib; the required compatibility with the structure constants pins down the algebra anyway. The goal asks only for the existence of a smooth proper curve over ; the paper's further prediction that has parameter is deliberately left out of the statement.
The goal is not trivially satisfiable: the intersection set of two transverse branes is nonempty, so the required isomorphisms force the corresponding -groups to be nonzero of the right size, in the right degree, with the prescribed products.
The general conjecture, for an arbitrary symplectic manifold with , is not stated here, and deliberately so: without symplectic manifolds and Floer theory in Mathlib, any general statement would have to take the Fukaya category as an unconstrained parameter, which would make it either vacuous or false. Building that infrastructure — symplectic manifolds, graded Lagrangian branes, Floer cohomology, twisted complexes over an -category and their triangulated structure — is the natural way to extend this mission, and such contributions are welcome.
Many approximation problems resist the standard PCP toolkit: the best known NP-hardness factors for Max-Cut, Vertex-Cover and approximate graph colouring are far from the best known polynomial-time algorithms. To explain this gap, Khot (CCC 2002) proposed the Unique-Games Conjecture and the family of -to-1 Games Conjectures. The -to-1 conjectures assert perfect completeness: the hard instances are either fully satisfiable, or satisfiable only to a vanishing extent. Perfect completeness is what makes these conjectures usable for colouring problems, where a "yes" instance must be genuinely -colourable rather than almost so.
A line of work culminating in Khot–Minzer–Safra and Dinur–Khot–Kindler–Minzer–Safra established the almost-perfect completeness version for -to-1 games: for every there is an alphabet bound such that distinguishing value from value is NP-hard. Their route goes through Håstad's hardness for linear equations, which cannot have perfect completeness, so the loss is intrinsic to the technique. The source paper of this mission removes that loss for .
A label-cover instance (Definition 1.1 of the source) consists of a bipartite graph , two finite alphabets , and for each edge a constraint . The constraint is a projection constraint if there is with , and a -to-1 constraint if in addition for every . Given assignments and , the fraction of satisfied edges is , and
An instance all of whose constraints are -to-1 is a -to-1 game.
For , is the promise problem: given a -to-1 game with both alphabets of size at most , distinguish from . Writing for the same promise problem over all projection instances, the PCP theorem together with the parallel repetition theorem gives that is NP-hard for a suitable (Theorem 1.2 of the source); this mission takes that statement as an external input.
In Lean this is stated as a polynomial-time gap-preserving reduction: for every there is a soundness threshold such that for every source alphabet bound there is a target alphabet bound and a polynomial-time computable map sending projection label-cover instances with alphabets of size at most and value to -to-1 games with alphabets of size at most and value , and instances of value at most to -to-1 games of value at most . Combined with the NP-hardness of , this is exactly Theorem 1.6.
The milestone list follows the source's own numbering: the hardness of approximate colouring of -uniform hypergraphs that starts the construction (Theorem 3.1), the two Grassmann decoding theorems the inner PCP rests on (Theorems 3.2 and 3.3), the sunflower bound on zoom-outs (Lemma 3.8), and the linear-algebraic layer connecting NAE-satisfying bilinear forms with their tensor decompositions (Propositions 4.13, 4.14 and Corollary 4.15).
Theorem 1.6 confirms the -to-1 Games Conjecture, the first of Khot's -to-1 conjectures to be settled with perfect completeness. Via known reductions it yields: for every , it is NP-hard to -colour a -colourable graph (previously known for ); for every , it is NP-hard to find an independent set of relative size in a -colourable -uniform hypergraph; and hardness results for low-rank matrix completion.
None of this material is formalized today. Mathlib has no label cover, no PCP machinery, no Grassmann graph and no complexity classes beyond the computability layer. A complete development therefore contributes reusable infrastructure — finite two-prover games and their value, gap-preserving reductions, the Grassmann graph over and its agreement tests — well beyond this single theorem.
The obvious attempt is to redo the -to-1 construction with a perfectly complete outer PCP, namely hardness of systems of quadratic equations over in place of linear ones. This fails at composition: the Grassmann agreement test, the only known device that produces -to-1 constraints, is a test for linear functions and cannot certify quadratic constraints. Linearizing the quadratic equations by a low-rank test destroys the covering property of the outer PCP, which is what makes the composed soundness analysis work. The source paper's answer is a three-layer construction (outer, middle and inner PCP) with a lazy parallel repetition in the middle layer and an inner PCP based on a tensor of the standard Grassmann encoding with Golowich's low-rank variant.
All objects are finite and explicit. A label-cover instance carries left vertices , right vertices , alphabets and , a finite edge set, and a projection map for every pair of vertices; only projection instances are representable, as in Definition 1.1. The value is the supremum over all pairs of assignments of the fraction of satisfied edges, taken in ; when there are no edges, or no assignments at all, the convention gives value . A tripled set (Definition 4.1) is modelled as , with the triple indexed by being . The Grassmann objects live in modelled as , and all probabilities are ratios of cardinalities of finite sets of subspaces, with the convention that an empty denominator gives .
Hardness is not stated as "NP-hard" — no notion of NP is available — but as the existence
of a reduction. This matters: a reduction required only to preserve the gap, with no
computability condition, would be trivially satisfiable by a map that inspects the value of
its input and returns one of two fixed instances. The formalization therefore requires the
reduction map to be computed by a Turing machine within a polynomial time bound, using
Mathlib's Turing.TM2ComputableInPolyTime together with an explicit binary encoding of
instances. The NP-hardness of the source problem (Theorem 1.2,
i.e. the PCP theorem plus parallel repetition) is an external input and is not part of this
mission.
Contributions of intermediate infrastructure are welcome: the games of Sections 4–6 (Game1a, Game1b, Game2a, Game2b, Game2c, Game3) and their completeness and soundness lemmas are the natural next layer of milestones, as are the covering properties of Appendix C and the list-decoding bounds of Appendix E.
In 1935 Werner Burau attached to every braid on strands a matrix over the ring of Laurent polynomials . The resulting homomorphism is the oldest and most studied linear representation of the braid group, and whether it is faithful — whether a nontrivial braid can act as the identity matrix — became one of the best known questions about braid groups.
The history is short and sharp:
Let . The braid group is taken here in Artin's presentation: generators subject to
Let . The unreduced Burau representation is the homomorphism
i.e. the identity matrix altered only in the two rows and columns , . That these matrices satisfy the two families of braid relations — so that is well defined — is proved in the mission's definition file, together with the invertibility of each generator matrix (its inverse is the identity altered by the block ).
Equivalently, is the action of the mapping class group of the -punctured disk on the relative homology of the infinite cyclic cover determined by total winding number; this is the description used throughout the source paper.
A representation is faithful when it is injective.
The goal of the mission is the Main Theorem of the paper:
The milestones are three supporting results, each of which can be attacked independently:
Faithfulness of closes the classification of the faithful Burau representations: is faithful exactly for . It immediately gives faithfulness of the Jones representation of (Corollary 1.1 of the paper), since the Jones representation contains the reduced Burau representation as a summand. Beyond the statement itself, the kernel and the image of for remain poorly understood, and the paper's disk-sequence and parity technology is proposed by its authors as a tool for that problem.
For formalization, essentially nothing of this is machine-checked today: Mathlib has neither braid groups nor the Burau representation. This mission puts in place a checked definition of over (including well-definedness and invertibility), and then asks for the mathematics. Even the three-strand case — Magnus–Peluso, known since 1969 — is not formalized anywhere, and it is the natural first target.
The obvious approach fails in both directions. One cannot simply compute: a braid in the kernel would have to be found or excluded among infinitely many words, and no normal form for turns injectivity of into a finite check. Nor can one argue by a free-subgroup / ping-pong pattern, which is how non-faithfulness is proved for .
The source argument is topological. To a braid one associates the arc and the sequence of punctured disks cut out by its intersections with a fixed arc ; the Moody polynomial then obstructs membership in the kernel provided no cancellation occurs among its monomials. Three-strand braids always satisfy the relevant parity condition; four-strand braids do not, and the paper repairs this by pushing a point-pushing braid into and applying Moody's theorem there. A complete formalization therefore needs curves on punctured disks, minimal position, and the Birman exact sequence — none of which exist in Mathlib. Contributions that build any of that infrastructure are as welcome as contributions to the statements themselves.
Conventions fixed by the Lean development:
A complete development will additionally need: point-pushing subgroups and the Brunnian group , the Moody polynomial of a pair of arcs, and winding-number sequences. These are not yet formalized and are deliberately not part of the current statements; proposals for faithful formalizations of them are welcome in the mission discussion.
Galois theory attaches to every finite Galois extension a finite group , the group of field automorphisms of fixing pointwise, and the fundamental theorem of Galois theory turns the subfield structure of into the subgroup structure of that group. The inverse Galois problem asks whether this correspondence is surjective over the rationals: given an arbitrary finite group , is there a Galois extension with ? The question was posed in the early nineteenth century and is unsolved.
What makes it a live research question rather than a curiosity is that the known positive results come from genuinely different sources, and none of them covers all finite groups.
Fix a field and a group . A Galois realization of over is a field equipped with a -algebra structure such that the extension is Galois — normal and separable — together with a group isomorphism
where denotes the group of -algebra automorphisms of under composition. The group is realizable over , written IsRealizable K G, when at least one Galois realization of over exists. No finiteness of is imposed in the definition; it is automatic once is finite, because an infinite Galois extension has infinite automorphism group.
Two base fields beyond appear throughout. denotes the field of rational functions in one variable over , written RatFunc K; and for the statement that a group is realizable over some number field, the base field ranges over the intermediate fields of .
The goal fixes no degree, no polynomial and no construction: it asserts only the shape of the truth, so no later refinement of the known constructions can invalidate it.
The last milestone is the Hilbert-irreducibility descent step; together with the geometric milestones it makes precise which half of the classical programme is missing.
The result itself would settle a two-century-old question and, with it, the surjectivity of the Galois correspondence over : every abstract finite group would be known to arise from an explicit arithmetic object, a polynomial with rational coefficients. Its absence is felt in practice — constructing a single new Galois group over is publishable work, as the recent additions of the degree- group (van Bommel–Costa–Elkies–Keller–Schiavone–Voight, 2024) and of the Mathieu group show.
Formalizing it produces something available today independently of the goal: a machine-checked library of the known realizability results. Mathlib has the fundamental theorem of Galois theory, cyclotomic extensions, the Kronecker–Weber theorem, solvability of groups and symmetric/alternating group theory, but it does not have a predicate for " is a Galois group over ", nor any of the milestones above. Every milestone here is a proved theorem of classical number theory and an unformalized one; the cyclic and abelian cases are within reach of current Mathlib, while the Shafarevich and Riemann-existence milestones are substantial formalization projects in their own right.
The obvious strategy fails at a well-understood point. Over the problem is solved: by the Riemann existence theorem every finite group occurs as the deck-transformation group of a branched cover of the projective line. Hilbert's irreducibility theorem then descends realizability from to . What is missing is the step in between: producing the cover over rather than over , i.e. showing that the geometric solution can be chosen with rational field of constants. The rigidity method makes this work for many groups, but there is no known argument covering all of them; an approach that only produces realizability over some number field is not enough, and that weaker statement is included as a milestone precisely to mark the line.
A second, purely formal difficulty: the milestones are classical but their published proofs are long. Shafarevich's theorem rests on a delicate analysis of embedding problems, and the Riemann existence theorem is analytic input that Mathlib does not currently have in the required form.
The mission fixes one definition file, published first, carrying the structure GaloisRealization and the one-field class IsRealizable. Conventions it commits to:
IsGalois K L is Mathlib's Galois condition (normal and separable); finiteness of the extension is not assumed.Equiv.Perm S for a finite type , and is alternatingGroup (Fin n); degenerate small cases are included rather than excluded.Group.IsSolvable.The statements cannot be satisfied vacuously: IsRealizable K G asserts the existence of data, so a solver must exhibit an extension; and the hypotheses of the milestones (cyclic, abelian, solvable, or none at all) are all satisfiable, so no milestone is empty. The one conditional milestone, Hilbert descent, is stated with realizability over as an explicit hypothesis.
Infrastructure a complete development needs, most of it reusable well beyond this mission: transport of a Galois realization along an isomorphism of groups and along an isomorphism of base fields; the fixed-field construction and the fundamental theorem in the form ""; Galois groups of cyclotomic fields; Dirichlet's theorem on primes in arithmetic progressions (already in Mathlib); Hilbert's irreducibility theorem (not in Mathlib). Contributions of any of these as reusable platform definitions or lemmas are welcome, as are decompositions of the harder milestones into sketches.
The Riemann hypothesis concerns the zeros of a complex analytic function, yet it admits an equivalent formulation involving only positive integers, finite sums, the real exponential, and the natural logarithm. Jeffrey C. Lagarias established this formulation in An Elementary Problem Equivalent to the Riemann Hypothesis (Theorem 1.1). It connects the distribution of divisors of an integer with the analytic behavior of the zeta function. For number theorists and formalizers, the interest lies in making that connection precise without confusing an elementary statement with an elementary proof.
The objective is the known equivalence selected by LeanEval v1, not a resolution of RH. Lagarias's paper builds on results of Guy Robin concerning large values of the divisor-sum function; those results remain substantial parts of the formalization workload (Lagarias, §3).
For a positive integer , its divisor sum is
where the sum runs over positive divisors, including and . Its harmonic number is
All inequalities below are inequalities of real numbers. The symbols and denote the real exponential and natural logarithm. The Euler–Mascheroni constant is .
The Riemann zeta function is obtained by analytic continuation of from . RH asserts that its nontrivial zeros have real part . The Lagarias elementary criterion in this mission is the assertion that for every positive integer . These conventions agree with the arithmetic quantities in Lagarias, Problem E, with the precise equality-clause distinction stated below.
There are no hypotheses on the goal theorem. The quantifier ranges over all positive integers, not a bounded test set or an unspecified tail. The benchmark uses a non-strict inequality and does not include an equality characterization. Lagarias's Problem E additionally requires equality only at ; the proof of the reverse implication in Theorem 1.1, p. 8 uses the non-strict inequality alone. The stronger source formulation is therefore not silently substituted for the benchmark.
The milestone list records the following source statements, with their thresholds unchanged:
for arbitrarily large integers .
All five are taken from Lagarias, §3, pp. 6–8; the finite check is explicitly an unnumbered step, not a newly attributed lemma.
The result identifies an exact arithmetic reformulation of RH. It does not make either side unconditional. A proof of the equivalence gives a bridge between statements in different mathematical languages; it does not certify the universal inequality merely because many instances can be checked. This distinction is central to the interpretation of Lagarias's theorem.
The formalization would connect existing Mathlib definitions of the zeta function, divisor sums, harmonic numbers, and Euler's constant through a machine-checked argument. Reusable outputs include explicit harmonic/exponential comparisons, certified finite real inequalities, and formal versions of Robin's conditional and oscillation results. The mathematical results are known; this proposal supplies open formalization targets, not completed proofs. No accepted LeanEval result is claimed by creating or launching the mission.
The elementary appearance of the criterion hides its main analytic requirements. Bounding the divisor sum crudely, or checking any finite number of integers, cannot establish the universal equivalence. The conditional upper bound and especially the quantitative oscillation theorem connect zeta zeros with unusually large divisor sums. They must be proved, not packaged as definitions or presumed available because the paper cites them (Lagarias, Propositions 3.1–3.2).
The oscillation statement requires uniform positive constants and arbitrarily large indices. Replacing it with one counterexample loses essential information. The bounded computation also requires rigorous control of exponential and logarithmic values: an ordinary floating-point loop is not a Lean proof. Beyond the listed milestones, completion still requires standard growth comparisons, threshold bookkeeping, and assembly of the two implications. The short length of the source's final argument should not be read as an estimate of total formalization effort.
The goal is LeanEval.NumberTheory.riemann_hypothesis_iff_lagarias_elementary_criterion, with type RiemannHypothesis ↔ LagariasElementaryCriterion. The criterion definition is copied from the benchmark. σ 1 n is natural-valued and cast to the reals; harmonic n is rational-valued and cast to the reals. RH remains Mathlib's predicate on riemannZeta, excluding negative even trivial zeros and the point . No replacement axiom, hidden RH assumption, altered zeta function, or circular child restatement is permitted.
The goal excludes and includes . Thresholds ensure positive logarithm arguments in the analytic milestones. The oscillation milestone expresses an infinite subset of the naturals as an unbounded set, retaining ; deletion of the finitely many smaller indices does not change the source's infinitude claim. Its real exponent is represented by Real.rpow, not natural exponentiation. Constants are chosen before the arbitrary cutoff.
The benchmark pins Lean 4.33.0 and Mathlib 6f1ef4e5dd604a435bddba4747b13970cd65d2a1. The proposal targets Prove2me's supported Lean 4.33.1 environment, Mathlib 0df444a360eaa60ab8c11dca51a86af692955474. These environments are distinct; eventual benchmark credit requires the benchmark's own validation. Contributions to analytic infrastructure, source-faithful supporting results, and certified finite inequalities are welcome. The five milestones are an initial source-backed structure, not a claim that all required infrastructure is already present.
In the last of the twenty-four questions that closed his 1982 survey Three-dimensional manifolds, Kleinian groups and hyperbolic geometry (Bull. Amer. Math. Soc. 6 (1982), 357–381), Thurston asked to "show that volumes of hyperbolic -manifolds are not all rationally related" (p. 380). Twenty-two of the twenty-four have since been answered — geometrization by Perelman, tameness by Agol and by Calegari–Gabai, the ending lamination conjecture by Brock–Canary–Minsky, virtual fibering by Agol — and this one is among the two that remain open.
Some rational relations are forced, and for a trivial reason: a degree cover of a hyperbolic -manifold has times its volume, so any two commensurable manifolds have rationally related volumes. The question, which remains open, is whether every rational relation arises that way — equivalently, whether some two hyperbolic -manifolds have irrational volume ratio. Remarkably, not a single such pair is known.
The bundle fixes the meaning of every term. Hyperbolic -space is the upper half-space . Its volume is Lebesgue measure with density — the Riemannian volume of the metric written out, so that no Riemannian machinery is required. The hyperbolic distance is given by its closed formula
A Kleinian action is a free, properly discontinuous action by hyperbolic
isometries; the quotient is a complete hyperbolic -manifold, discreteness and
torsion freeness being consequences rather than hypotheses. The volume of the
quotient is the measure of a fundamental domain, in the sense of Mathlib's
MeasureTheory.IsFundamentalDomain, and the set of volumes collects those that
are finite and positive.
Two conventions are stated rather than derived, and are worth flagging. Isometries are not required to preserve orientation, so the set of volumes also contains those of non-orientable quotients; this enlarges the set but not its -span, so neither goal is affected. And preservation of the hyperbolic volume is a field of the structure rather than a consequence of preserving the distance: it holds for every hyperbolic isometry, but deriving it amounts to classifying , which is not the subject of this mission.
The goal is that the volumes are not all rationally related: there are two of them, and , with for every rational .
Two milestones support it. The first is that passing to a subgroup of index multiplies the volume by , a fundamental domain for the subgroup being the union of translates of one for the whole group; this is the source of every known rational relation, and it is why the question is phrased as it is. The second is that the set of volumes is nonempty — that some finite-volume hyperbolic -manifold exists at all — without which the goal would be vacuously false rather than open.
A stronger form of the question, that the -span of the set of volumes is infinite dimensional, is also stated.
The question is a geometric statement whose difficulty is arithmetic. For the Bianchi groups of an imaginary quadratic field , Humbert's formula gives the covolume as , so the ratio of two such volumes is, up to explicit algebraic factors, a ratio of Dedekind zeta values at ; and Neumann and Yang showed that the Bloch invariant of a hyperbolic -manifold lies in a subgroup of finite -rank determined by its invariant trace field, so that manifolds sharing an invariant trace field with a single complex place, such as an imaginary quadratic one, have rationally related volumes. Producing one irrational ratio therefore means separating two such transcendentals — a statement of the same order of difficulty as the irrationality of . The value of formalizing the question is not that it will be closed, but that its statement, and the elementary relations that make its naive form false, are pinned down exactly.
Submission hold — source-fidelity repair (2026-09-04). The public goal restricts answers to elementary expression trees and is only a stronger subquestion. It does not formalize the source's broader special-function closed-form question. The existing published target is preserved, with this scope warning. Do not confirm or submit this version as a faithful formalization of the full source. The legacy mathematical target below is retained for traceability while the replacement is prepared.
A standard Brownian motion starts below the exponentially decaying boundary b(t)=b0 exp(-ct). The first time it crosses the boundary has a continuous density characterized by a generalized Abel--Volterra integral equation. The source asks for an explicit distribution, motivated in part by neuronal threshold models with a decaying refractory boundary.
This mission turns CUHK-Shenzhen AI Math Problem 13, First-passage time of Brownian motion to an exponentially decaying boundary, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.
Construct one expression in a fixed elementary language whose evaluation is a continuous nonnegative density on positive times, solves the Abel equation, and integrates to one. The language contains real constants, rational constants, arithmetic, exp, log, square root, trigonometric functions, and the normal density. The first milestone drops elementary representability and normalization and asks for a continuous nonnegative Abel solution.
Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in Brownian motion, first-passage times, stochastic processes, Volterra integral equations. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.
Moving-boundary first-passage laws rarely have elementary closed forms. The Abel kernel is singular at the upper endpoint, and showing that a candidate equation solution is the actual passage density requires uniqueness and probability normalization. The capstone may be false under the selected expression language; a non-elementarity theorem would be a legitimate disproof of this precise formal target.
Formalize existence and uniqueness for the Volterra equation using weakly singular kernels, then connect it to Brownian first passage. Explore transformations suggested by the exponential boundary, Laplace transforms, and iterative resolvent kernels. Symbolic or numerical calculations may reveal special-function rather than elementary structure. If so, characterize the required extension of the expression language and prove why the current language is insufficient.
The already-published goal uses finite elementary-expression trees with arithmetic, exp/log/sqrt, sin/cos and normal density. The source explicitly permits standard special functions beyond this language. Accordingly the published declaration is a stronger elementary-only subquestion, not a faithful replacement for the full closed-form question. It is preserved as an existing result; its proof or disproof must not be reported as settling every special-function formula. The Abel-solution milestone asserts only existence of a continuous nonnegative solution; uniqueness, normalization, and identification with the first-passage density remain separate obligations. A complete source-faithful replacement needs an agreed formula class or a concrete proposed formula, not an unrestricted function renamed a closed form.
For each positive boundary height and decay parameter, there exists a continuous nonnegative solution of the stated Abel equation on positive times. This node asserts existence only, not uniqueness, unit mass, or an elementary closed form.
The CUHK-Shenzhen AI Math Problems page added this problem on June 23, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.
A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no sorry, and expose a top-level theorem solution when submitted to Prove2Me.
The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.
The files were built locally with Lean 4.30.0 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.
A Hadamard matrix is a square array of +1s and −1s whose rows are mutually orthogonal — equivalently, one whose determinant attains the absolute maximum that Jacques Hadamard proved in 1893 any ±1 matrix can reach. The story opens earlier, with James Joseph Sylvester's 1867 doubling construction producing such matrices in every power-of-two order; Hadamard himself added orders 12 and 20. The conjecture bearing his name asserts that a Hadamard matrix exists for every order divisible by four. Raymond Paley's 1933 construction from finite fields settled vast new families, and computer searches filled stubborn gaps — beginning with order 92 at JPL in 1962 and reaching order 428 only in 2005, after which 668 became the smallest order whose existence is still unknown. Far from a curiosity, these matrices are workhorses of applied mathematics, underpinning error-correcting codes (the Reed–Muller code that sharpened Mariner spacecraft imagery), spread-spectrum and CDMA signal design, optimal statistical designs of experiments, and coded-aperture spectroscopy. Settling the conjecture would close a 130-year-old gap where combinatorics, number theory, and design theory meet.
A reinforcement-learning agent that learns a Markov decision process (MDP) from data ends up with point estimates of the Q-values: the long-run discounted reward of taking an action in a state and acting optimally afterwards. Point estimates say nothing about their own reliability. Choosing between two actions whose estimated values differ by a small margin, deciding how much more data to collect, or allocating exploration effort all need the sampling distribution of the estimate. Finite-sample bounds (Kearns and Singh 1998) give rates with loose constants. Asymptotic normality gives exact limiting constants.
Zhu, Dong and Lam establish a central limit theorem for the plug-in Q-value estimate of a finite MDP whose data are collected by an exploration policy, with an explicit covariance matrix. For a fixed policy, the analogous result for the value function was obtained by Mannor, Simester, Sun and Tsitsiklis (2007). The new step is the optimal Q-values, which depend on the data through a maximum over actions. The paper uses the covariance to design a pure-exploration policy (Q-OCBA) that allocates samples to maximize the probability of selecting the optimal policy.
Let and be finite nonempty sets of states and actions. A pair has a random reward with law on , mean and variance , and moves to state with probability . The discount factor is . The Bellman operator is
and the Q-values are its fixed point , with .
Data are collected by an exploration policy . Starting from some state, the agent repeatedly takes , observes , and moves to . The state-action pairs then form a Markov chain with transition matrix . From observations, the plug-in estimates are the sample mean reward and the empirical transition frequencies at each pair, with fixed initial values at unvisited pairs. The estimate is the fixed point of .
The standing assumptions are:
Under Assumptions 1–3, almost surely, and
Here , and , , are diagonal with entries , and . The matrix is the multinomial covariance of . The covariance is part of the statement: the paper's subsequent results (Corollary 1, Q-OCBA) use it.
The result. Theorem 1 gives asymptotically exact simultaneous confidence regions for all Q-values from one trajectory of exploration data. The closed form of shows how each source of noise contributes: reward noise through , transition noise through , the amount of data at each pair through , and propagation through the dynamics of the optimal policy through . This decomposition is what makes usable as an objective for allocating exploration effort, which the paper's Q-OCBA policy does. Corollary 1 (CLT for the optimal value ) is derived from it.
Formalizing it. The result is proved in the paper, but the proof cites its probabilistic core: a joint central limit theorem for empirical transition frequencies of an irreducible finite Markov chain (Trevezas and Limnios 2009, Proposition 3), together with the multivariate delta method. A machine-checked proof would also certify that the covariance formula, with its transposes and weights, is correct as printed. No Q-value CLT or Markov-chain CLT for empirical transition matrices is currently formalized on the platform. The existing Markov-chain CLTs there are scalar and assume uniform ergodicity.
The deterministic half (milestones 4, 5, 7) is linear algebra plus an implicit-function argument. The obstacle is that depends on through a maximum, which is not differentiable at ties. Assumption 2 removes ties at , and differentiability holds only on a neighbourhood where the argmax stays the same.
The probabilistic half is harder. A natural first idea is to treat the visits to each pair as i.i.d. samples and apply the classical multivariate CLT. This fails because the number of visits is random and depends on the whole trajectory, and the samples at different pairs are dependent through the chain. The CLT (23) needs a martingale or regeneration argument for the Markov chain on state-action pairs. The chain is only assumed irreducible, so it may be periodic, and uniformly ergodic CLTs do not apply directly.
S × A with Fintype, DecidableEq and Nonempty; the paper's flattening is notation only. , and the initial state law are PMFs, and rewards are probability measures on with MemLp id 2 (Assumption 1).MarkovChainCLT.chainMeasure. Every initial state law is allowed. Time is 0-based.bellmanFix). It is the unique fixed point whenever the Bellman operator is a contraction, which covers every stochastic and a neighbourhood of .multivariateGaussian on EuclideanSpace, and convergence in distribution is TendstoInDistribution.Trivializations ruled out.
Matrix.inv returns on singular matrices, but is invertible under the pins, so is not a junk zero.multivariateGaussian returns a point mass for a non-positive-semidefinite matrix, but and are positive semidefinite.Infrastructure. A complete development needs:
TendstoInDistribution form;Contributions of any of these as standalone lemmas are welcome.
Not posed. Corollaries 1–2 and Theorems 2–6 of the paper (optimal-value and fixed-policy CLTs, non-unique optimal policies, constrained MDPs, Q-OCBA consistency, approximate value iteration, kernel representations) are not part of this mission.
Many selection problems in machine learning and operations research ask for a set of items that maximizes a utility with diminishing returns, subject to a combinatorial feasibility constraint: summarizing a collection of images or documents, placing sensors, recommending a diverse set of products, or choosing a set of edges that forms a matching. Diminishing returns is submodularity; the feasibility constraints in these examples (matroids, intersections of matroids, matchings, knapsack-type systems) are instances of -extendible systems, a class introduced by Mestre (ESA 2006). Many useful objectives, such as graph cuts and diversity-regularized utilities, are non-monotone: adding an item can lower the value.
The greedy algorithm has a long history for this problem class. Fisher, Nemhauser and Wolsey (1978, doi:10.1007/BFb0121195) showed that greedy gives a -approximation for monotone submodular objectives over -systems, a class that contains -extendible systems. For non-monotone objectives, the known greedy-based algorithms ran the greedy algorithm repeatedly. Gupta, Roth, Schoenebeck and Talwar (WINE 2010) obtained roughly , Mirzasoleiman et al. (2016) roughly , and Feldman, Harshaw and Karbasi (COLT 2017) , each with or oracle queries. Harshaw, Kazemi, Feldman and Karbasi (arXiv:2104.02772; Mathematics of Operations Research, 2022) showed that a single random subsampling of the ground set, followed by one run of the plain greedy algorithm, gives a -approximation for non-negative submodular objectives with expected oracle calls. This mission formalizes that guarantee.
Let be a finite ground set of size , with a fixed linear order that is used only to break ties. A set function is a map . The marginal gain of at is .
The problem is for non-negative submodular ; OPT denotes a maximizer.
SampleGreedy with sampling probability keeps each element independently with probability , giving a sample . It then starts from and repeatedly adds the element of largest marginal gain among those with and , ties broken by the fixed order, until no such element is left. Its expected value is
For the analysis the paper introduces Algorithm 2, which runs greedy over the whole ground set, flips a -coin for each chosen element, and maintains a set (initially OPT), removal sets , snapshots and indicators (" was considered") and .
For non-negative submodular , a -extendible system with , and every : SampleGreedy's output is always independent, and $$f(T) \le \frac{(p+1)^2}{p},\mathbb E_{1/(p+1)}[f(S)], \qquad f(T) \le (p+1),\mathbb E_{1/(p+1)}[f(S)] \ \text{if is monotone},
f(T) \le p,\mathbb E_{1/p}[f(S)] \ \text{if is linear}.$$
In attack order: Lemma 3 (p. 8, already Proved on the platform: a random set whose elements each appear with probability at most keeps a fraction of in expectation); Lemma 4 (p. 10, SampleGreedy and Algorithm 2 have the same output law); Lemma 5 (p. 11, invariants of Algorithm 2); Lemma 6 (p. 12, ); Lemma 7 (p. 13, inequality (5)); Lemma 8 (p. 14); the display of §4.1.1 (p. 14); Lemma 9 (p. 15, linear objectives); Lemma 10 (p. 16, inequality (7)).
The result shows that one random subsample plus one greedy pass beats the repeated-greedy algorithms for non-monotone objectives over -extendible systems, both in ratio and in query count, and matches the classical for monotone objectives. Since no polynomial-query algorithm achieves a ratio better than for this problem (Feldman, Harshaw and Karbasi 2017, Theorem 4), the ratio is nearly tight. The proof technique, which couples the subsampled algorithm with an auxiliary algorithm that flips coins only for the elements it considers, is reused in the paper's streaming algorithm and in later subsampling-based algorithms.
The result is proved on paper; no machine-checked version is known. A formalization would give a checked analysis of a randomized greedy algorithm over an abstract independence system, including the coupling of two random processes, which is the step that informal proofs usually treat most briefly. It would also give reusable definitions of -extendible systems and of greedy runs with explicit tie-breaking. The mission also records a defect of the printed text: Lemma 9 as printed is false for linear functions with , so it is stated here with .
The obvious argument would analyze SampleGreedy directly, but there the sample and the greedy path are entangled: which element is chosen next depends on the whole sample. The analysis instead goes through Algorithm 2, and the hard step is Lemma 4, an exact equality of output laws. Its proof needs both algorithms to break ties identically and the coins to be fixed in advance. After that, the expectation bounds of Lemmas 7, 8 and 10 condition on the history up to the iteration in which a given element is considered, and the coin of that element is independent of that history. In the finite-sum encoding this conditioning becomes a combinatorial regrouping of the coin outcomes, which has to be carried out explicitly. Lemma 6 requires a disjointness argument for the sets across the whole run.
The ground set is a Fintype α with a LinearOrder α, which is the paper's tie-breaking order (p. 10). Set functions are Finset α → ℝ, and is a predicate Finset α → Prop. The parameter is a natural number with . Submodularity is the published lattice form NonmonotoneSubmod.Shared.Submodular (), equivalent on finite ground sets to the paper's (1). The while loops run for exactly iterations, which is enough because each effective iteration adds or considers a new element. Expectations are exact finite sums over the samples or coin outcomes. Algorithm 2's coins are a fixed bit set, and its line 6 is one fixed minimum-cardinality choice. "-approximation" for a randomized algorithm is read, as in the paper's proof, as , stated against every independent . Linear means (1) with equality and allows , except in Lemma 9, which adds . The oracle-count clause of Theorem 1 is not formalized.
Trivializing encodings are excluded. The expected value is a sum over the greedy runs on each sample, with the sample as the greedy pool (not the whole ground set followed by a filter). The weights sum to 1. The comparison set is always assumed independent. The ratio is real division. A sanity file checks that the output on a sample differs from the output on the whole ground set.
A complete development needs the greedy run's invariants, the coupling of Lemma 4, and the regrouping of finite sums over coin outcomes by the history before a given element is considered. The last of these is reusable for any analysis of an algorithm that flips independent coins. Proofs of any milestone, and alternative proofs of Lemma 4, are welcome.
A portfolio loss often depends on several risk factors whose individual distributions can be estimated well but whose joint distribution cannot. Regulators and risk managers then ask for the worst-case risk: the largest value a risk measure can take over all joint laws compatible with the known marginals. For Value-at-Risk and Expected Shortfall of sums this question has a long literature on risk aggregation (Embrechts, Puccetti, Rüschendorf, Wang and others). Ghossoub, Hall and Saunders (arXiv:2010.14673v1, published in Mathematics of Operations Research, 2023) treat a general loss of two Polish-space-valued risk factors and the whole class of spectral risk measures, which contains Expected Shortfall and, for constant weight, the expectation. Their main result is a duality theorem in the style of Kantorovich duality for optimal transport.
Let and be Polish spaces with their Borel -algebras, and probability measures on them, and the set of couplings: probability measures on with marginals and . A loss is a function .
For a coupling , the generalized inverse of is for . A spectral function is a bounded, increasing, right-continuous with , and the spectral risk measure is
Expected Shortfall is the case . Two measures on carry : , with distribution function (so may be positive), and , the probability measure with .
The Maximum Spectral Measure is the primal value
For a threshold function define the cost , and let be the pairs with for -a.e. and -a.e. . The dual value is
The assumptions are: (A.1) is upper semicontinuous; (A.2) with lower semicontinuous integrable ; (A.3) with upper semicontinuous integrable , both bounds for -a.e. and -a.e. ; (A.4) is bounded and right-continuous.
The goal asserts only the equality of values. It does not assert attainment in the primal or the dual; the paper does not claim dual attainment (Remark 3).
The theorem gives a computable upper bound mechanism: every dual feasible triple certifies an upper bound on the worst-case spectral risk, and the bounds are tight. For it is Kantorovich duality for the cost ; for Expected Shortfall the infimum over collapses to one real threshold, which the paper exploits in §5 for stability and asymptotic results. The ingredients (the ES-mixture representation of spectral risk measures, the Rockafellar–Uryasev formula, interchange of infimum and integral for normal integrands) are standard tools of risk measure theory that are reusable well beyond this paper.
The result is proved in the paper, not formalized anywhere known. A complete development adds a machine-checked version of Kantorovich duality for upper semicontinuous costs with integrable bounds and almost-everywhere constraints, which the platform currently has only for continuous nonnegative costs with bounded continuous potentials (MongeKantorovichYao.monge_kantorovich_duality). Related platform work includes the Open goal RiskFunctionals.Distortion.choquet_representation, a lower-tail analogue of milestone 3 for distortion acceptability functionals, and RUCVaR.MinFormula.theorem_10, the Rockafellar–Uryasev formula on a finite-dimensional carrier.
The informal derivation on p. 7 exchanges a supremum over couplings with an infimum over threshold functions, an infimum with an integral, and two integrals, and then applies Kantorovich duality to a cost that depends on . Each exchange needs a reason. The supremum–infimum exchange needs a minimax theorem over the weakly compact set against an infinite-dimensional convex set of 's, with upper semicontinuity in that holds only for , not on the larger natural domain . The infimum–integral exchange must cope with the atom of at , where the pointwise infimum need not be attained, and with the factor , which is unbounded near . Applying Kantorovich duality to needs the cost to be upper semicontinuous with integrable bounds, which is Lemma 1. Lemma 3 of the paper () is false in general and is not part of the mission; Lemma 4 holds without it.
The development is in the namespace MaxSpectralRisk.Duality over Mathlib. Couplings are the published MongeKantorovichYao.transferencePlans μ ν. A spectral function is a StieltjesFunction ℝ that vanishes on and integrates to over ; this builds in A.4, since monotonicity bounds it on and values on are never used. is its Stieltjes measure restricted to and has density against ; milestone 1 checks the paper's distribution-function description. , and the auxiliary , take values in EReal; and are when their integrand is not integrable, matching the paper's . Integrals over against are Lebesgue interval integrals. Weak convergence of couplings is convergence in Mathlib's ProbabilityMeasure topology. "For -a.e. and -a.e. " in A.2, A.3 and means "off with ".
That reading is essential: a -almost-everywhere dual constraint can be violated on the support of a coupling (the diagonal of under Lebesgue marginals), which breaks weak duality. Equally, a dual over constant only, over bounded only, or values computed as real sSup/sInf (which return on unbounded sets) would not be the paper's problem.
Contributions are welcome at every level: the Stieltjes and integration-by-parts facts behind milestones 1 and 3, the convex analysis of milestone 2 and Lemma 2, a general Kantorovich duality for semicontinuous costs (reusable for any optimal transport mission), and the minimax theorem behind Proposition 3.
Products with positive network effects (messaging apps, online games, social platforms) are known to support higher profits: a buyer's utility grows with the number of other buyers, and a seller can monetize that complementarity (Katz and Shapiro 1986; Candogan, Bimpikis and Ozdaglar 2012). Ajorlou and Jadbabaie ask whether a seller of a product without such an effect can create one artificially, by announcing a sales-based rebate: every buyer pays the market price and later receives a reward that depends on the realized sales volume (arXiv:1902.09646v4, Management Science, 2023).
Because consumers are uncertain about a common quality component and about each other's valuations, the purchase decision becomes a global game with correlated private valuations, in the sense of Carlsson and van Damme (1993) and Morris and Shin (1998). A natural first guess is that a rebate increasing in sales volume, which imitates a positive network effect, should help the seller. The paper's Theorem 2 says the opposite: when the price is already optimal, no increasing sales-based reward program is profitable. This mission formalizes that result and the identities on which it rests.
A firm sells one product at a market price to a unit mass of consumers. Consumer values the product at , where the common quality has the Gaussian prior and the taste is idiosyncratic. Write
A consumer who observes holds the posterior . Valuations are ex ante , with density , where and are the standard normal density and distribution function.
If consumers buy exactly when (a threshold strategy with cutoff ), the sales volume at quality is . A reward program is a function of the sales volume; at cutoff it induces the reward as a function of the quality. The cutoff is an equilibrium for when
The firm's expected profit is
With no reward the cutoff is and the profit is . Assumption 1 says that maximizes the no-reward profit . A reward program is profitable at an equilibrium cutoff if (2) strictly exceeds the no-reward profit at .
Under Assumption 1, for every weakly increasing reward program and every equilibrium cutoff of (1) for ,
The result. Theorem 2 separates two effects that are easy to conflate: an inherent network effect raises profit, but an induced one, paid for through a rebate increasing in sales, lowers the expected net price exactly at high valuations and so cannot beat the optimal plain price. It is the negative half of the paper's design question; the positive half (optimal programs are decreasing in sales volume, "full refund or nothing", §III–§IV) is built on the same representation (9) of the profit by valuations, which is a milestone here. Lemma 1 is the paper's general criterion for when any reward program beats the equivalent plain price, and applies beyond monotone programs.
Formalizing it. The results are proved in the paper (body p. 16, appendix p. 29); no machine-checked version is known. The formal work consists of the Gaussian conditioning identity behind (9), the Gaussian integral of on p. 7, the shift argument for Lemma 5, and the assembly into Theorem 2 with every hypothesis made explicit. The model layer (Gaussian prior, posterior, threshold equilibria) is reusable for the paper's other results and for related global-game pricing models.
The paper treats (9) as a change of conditioning, but it is where the posterior formula of p. 9 must be shown to be the actual conditional law of the quality given a valuation, inside an integral restricted to valuations above the cutoff: the profit (2) integrates over qualities, the right side of (9) over valuations, and connecting them requires Fubini over the joint Gaussian law of together with the factorization of the joint density into times the posterior density. The strict part of Lemma 5 needs more than "a shift of an increasing function is larger": the increase must happen on a set of positive Gaussian measure, which uses that a monotone non-constant function differs between two shifted Gaussian laws. Theorem 2 also uses that the equilibrium cutoff lies in , which is where the bound and Assumption 1 interact.
The model is a structure with fields and a validity predicate , , which every statement assumes (implicit on the page). Laws are Mathlib's gaussianReal, with variances passed through Real.toNNReal; expectations are Bochner integrals of bounded measurable integrands. and are the published BlackScholesModel.stdNormalCDF and stdNormalPDF. The reward program is a function ℝ → ℝ constrained to on , "increasing" means weakly increasing on , and is defined from and the same cutoff used in (1) and (2). In milestones 2–5 the reward is a general measurable function with values in , the paper's . Lemma 5 is posed on with " non-constant": non-constancy of on does not survive composition with , whose range is . Assumption 1 enters only through its maximization clause over prices ; its first-order characterization is not posed. Integrals are over the open half-line.
Three formalizations would trivialize or alter the goal and are excluded: restricting to strictly increasing programs (which drops constant rebates), decoupling from the equilibrium cutoff, and comparing the profit with the price- profit instead of the no-reward profit at the market price .
Contributions welcome: proofs of the milestones in any order, in particular the Gaussian identities (milestones 1 and 2), which are of independent use for Gaussian signal models, and general lemmas on Gaussian shifts of monotone functions.