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?
Chapter 3 of The Principles of Deep Learning Theory by D. A. Roberts and S. Yaida (arXiv:2106.10165) is the book's first complete example of its effective-theory method. For deep linear networks at initialization, the two- and four-point correlators of the network outputs can be computed exactly at any width and depth. The resulting formulas exhibit, in the simplest setting, the phenomena that organize the rest of the book: criticality of the weight variance , non-Gaussianity that grows with depth, and the depth-to-width ratio as the parameter controlling deviations from the infinite-width limit. This mission formalizes §§3.1–3.3. It is the second mission in a series formalizing the book (namespace DeepLearningTheory).
A deep linear network with widths (all positive) and zero biases maps an input to preactivations
(eqs. 3.1–3.2 with ). At initialization all weights are independent centered Gaussians with (eq. 3.4), with a layer-independent . For inputs let (eq. 3.9).
For every layer , a single input , and neurons ,
The closed forms show that a deep linear network is exactly Gaussian only in the strict infinite-width limit: at criticality the connected four-point correlator (3.29)–(3.30) is for equal widths , the first appearance of the depth-to-width ratio as the book's emergent scale. The same recursive method is reused for nonlinear networks in Chapters 4–5. The results are exact computations in the book; this mission formalizes them.
Each correlator is an expectation of a polynomial in exponentially many Gaussian weights. The book's recursion uses that the layer- weights are independent of the layer- preactivations, followed by Wick contraction of the two or four new weights. In Lean this requires independence of a weight family from a measurable function of the earlier layers, integrability of products of Gaussian polynomials, and careful handling of the Kronecker-delta bookkeeping in the sums (3.23).
n : ℕ → ℕ with n 0 the input dimension; neural indices are . Weights are a random field W : Ω → ℕ → ℕ → ℕ → ℝ on a probability space, only entries with , , are used.IsLinearNetInit P n CW W states mutual independence of all these weights and that each has law gaussianReal 0 (CW / n (ℓ-1)).linearPreact n (W ω) x ℓ i is ; inputKernel (n 0) x₁ x₂ is ; kron and wickDelta4 are the Kronecker delta and the three-term tensor structure.Chapter 4 of The Principles of Deep Learning Theory by D. A. Roberts and S. Yaida (arXiv:2106.10165) begins the analysis of general multilayer perceptrons (MLPs) with a nonlinear activation function at initialization. The first layer is exactly Gaussian; the second layer is the first place where non-Gaussianity appears, as a connected four-point correlator suppressed by and governed by the four-point vertex . This mission formalizes §§4.1–4.2, which are exact at any width. It is the third mission in a series formalizing the book (namespace DeepLearningTheory) and reuses the definitions of Mission II (Deep Linear Networks at Initialization).
An MLP with widths and activation maps inputs to preactivations
(eqs. 4.2, 4.30). At initialization all biases and weights are independent centered Gaussians with and (eqs. 4.3–4.4). The first-layer metric is (eq. 4.8), and denotes the expectation over a centered Gaussian vector with covariance (eq. 4.25), with .
with the four-point vertex (eq. 4.40).
These identities are the base case of the book's recursion (Chapter 4.3 onward) for the kernel and four-point vertex in deeper layers, and they show concretely that a finite-width network is not a Gaussian process: the connected correlator is generically nonzero for nonlinear . The results are exact computations in the book; this mission formalizes them.
The second layer is a Gaussian conditional on the first layer, with a random covariance (the stochastic metric, eq. 4.36). Turning this into unconditional correlators requires conditioning on the first-layer preactivations, independence of different first-layer neurons, and the identification of first-layer activation correlators with Gaussian expectations over the metric , which may be degenerate (e.g. repeated inputs). Integrability of against Gaussians must be controlled.
kron, inputKernel, WeightIndex. New definitions: mlpPreact (), IsMLPInit (independent Gaussian biases and weights with layer-dependent ), firstLayerMetric ( on finitely many inputs), gaussAvg (, via Mathlib's multivariateGaussian, which handles singular positive-semidefinite ), and HasPolyGrowth.Fin D (for the specific statements, or inputs, possibly repeated). is assumed where the formulas divide by .Chapter 13 showed that convex-Lipschitz-bounded and convex-smooth-bounded problems are learnable by regularized loss minimization; Chapter 14 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) shows how to learn them with the simplest possible algorithm. Gradient descent moves against the gradient with a fixed step size and outputs the average of its iterates; its analysis (Lemma 14.1) is a single telescoping identity that bounds for any sequence of directions , and this generality is the whole point. It gives the rate for convex Lipschitz functions (Corollary 14.2), extends to nondifferentiable functions through subgradients (Definition 14.4, Lemmas 14.3 and 14.7), and, because it never used that the directions were gradients, extends to stochastic gradient descent, in which each direction is random with a subgradient as its conditional expectation (Theorem 14.8). Applied to the risk with a fresh example at each step, SGD is a learning algorithm whose sample complexity is the iteration count: examples for convex-Lipschitz-bounded problems (Corollary 14.12) and for convex-smooth-bounded ones (Theorem 14.13, Corollary 14.14). A projected, decreasing-step variant for strongly convex objectives has rate (Theorem 14.11).
Hypotheses are vectors in ; convex, Lipschitz and smooth losses, convex-Lipschitz-bounded and convex-smooth-bounded problems, and strong convexity are those of Mission IX. A vector is a subgradient of at if for all . The iterates of an update rule , are indexed from , and the output after steps is . The randomness of SGD is modelled as the chapter uses it in §14.5: a sample drawn i.i.d. from and an oracle with , where is a stochastic subgradient oracle for if for every . This is the book's condition in the case where the direction depends on the past only through and on fresh randomness, which is what every application in the book does; the expectation is then an integral over . For learning, is a subgradient of at , so that is a subgradient of at (14.13). The projection of onto a convex set is a nearest point of , and the strongly convex variant projects after each step with step size .
For a convex , , a measurable oracle with and , any with , and : ; and for every , gives .
Lemma 14.1. For any directions, ; with , and the average is at most .
Corollary 14.2. Subgradient descent on a convex -Lipschitz with has for every , and gives .
Lemma 14.7. A convex on is -Lipschitz iff all its subgradients have norm at most .
Lemma 14.9. For the projection of onto a convex and , .
Theorem 14.11. For -strongly convex , a closed convex , an oracle with and any , the projected variant with has .
Corollary 14.12. SGD on the risk of a convex-Lipschitz-bounded problem with examples has for every .
Theorem 14.13. For convex, -smooth, nonnegative losses and , SGD with gradient directions has .
Corollary 14.14. For a convex-smooth-bounded problem with and any , SGD with and has for every .
Further items: Lemma 14.3, Claims 14.5, 14.6 and 14.10, and the hinge-loss subgradient of Example 14.2.
SGD is the algorithm behind most of modern machine learning, and Theorem 14.8 is its basic guarantee: dimension-free, independent of the form of beyond convexity, and with a sample complexity matching the regularization bound of Chapter 13 up to a constant. Lemma 14.1 isolates the deterministic identity that makes both gradient descent and its stochastic version work, and Lemma 14.7 is the bridge between the Lipschitz assumption of Chapter 12 and the bounded directions the analysis needs. The learning corollaries make the point that runs through Part II of the book: for convex problems, optimization and learning are the same activity, and one pass over the data suffices.
Nothing here is machine-checked. The chapter's statements are essentially correct, and the formalization records the reading choices rather than corrections: the i.i.d.-oracle model of the randomness, the subgradient form of gradient descent, the bound at every point of the ball rather than at a minimizer, and, in Corollary 14.14, the assumptions and under which the derivation from Theorem 14.13 goes through.
Lemma 14.1 is a completed square and a telescoping sum and is the intended entry point; the clause is the substitution of . Corollary 14.2 is Lemma 14.1 with Jensen's inequality for the average and the subgradient inequality at each iterate, plus Lemma 14.7 to bound the directions. The subgradient facts need convex analysis: Lemma 14.3 in the direction "convex implies subgradients exist" is the supporting hyperplane theorem on , which Mathlib does not offer directly; Claim 14.5 uses the first-order characterization of convexity for differentiable functions; Lemma 14.7's "Lipschitz implies bounded subgradients" is the book's one-line argument along . Theorem 14.8 is Lemma 14.1 plus the conditioning argument of the book, which in the i.i.d.-oracle model is Fubini on the product : the iterate is a measurable function of , and integrating over first gives . Theorem 14.11 adds the projection lemma, the strong-convexity inequality of Claim 14.10, the telescoping of and the harmonic sum ; the second-moment hypothesis makes finite inductively. Corollary 14.12 is Theorem 14.8 for with the oracle of (14.13), which requires exchanging a subgradient inequality with the integral over . Theorem 14.13 replaces the Lipschitz bound by self-boundedness, , and rearranges; Corollary 14.14 is its arithmetic under the added assumptions. In all expectation statements the measurability of the iterates in the sample, from the measurability of the oracle, is a routine but necessary lemma.
Iterates are defined by structural recursion, so no argmin is chosen; the sample-driven SGD stops after updates; the projection onto is a chosen nearest point, unique for closed convex . Bounds are stated for every in the ball (or in ) rather than for a minimizer, which is what the proofs give and is stronger. The oracle bound is required surely (the book: with probability ); the almost-sure version is a routine extension. The second-moment hypothesis of Theorem 14.11 is a lower Lebesgue integral, so that a non-integrable oracle cannot satisfy it vacuously. The learning corollaries assume a measurable loss, nonnegative and bounded at the origin, so that the risks are genuine integrals, and a measurable selector of subgradients. Variable step sizes (§14.4.2), other averaging schemes (§14.4.3), SGD for regularized loss minimization (§14.5.3) and the exercises are not stated.
Trivializing readings are excluded: the expectations are over the product law of the examples with measurable integrands, the subgradient conditions are pointwise inequalities, and the iteration counts are the book's. Welcome contributions: Lemma 14.1 as a reusable telescoping lemma, the measurability of the SGD iterates, and the Fubini step that turns an oracle condition into the inequality (14.10).
Chapters 12 and 13 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) leave binary classification for the general framework in which a hypothesis is a vector and the loss is a convex function of . Convexity makes the ERM problem tractable (Lemma 12.11), but Examples 12.8 and 12.9 show that convexity, even with a bounded class, does not by itself make a problem learnable: one-dimensional linear regression with the squared loss defeats every learner. The chapter therefore isolates two families, the convex-Lipschitz-bounded and the convex-smooth-bounded problems (Definitions 12.12 and 12.13), and Chapter 13 proves that both are learnable, not by ERM but by Regularized Loss Minimization with Tikhonov regularization, . The proof goes through a new idea: stability. Theorem 13.2 expresses the expected overfitting exactly as the expected effect of replacing one training example, strong convexity of the regularized objective bounds that effect (Lemma 13.5, Corollaries 13.6 and 13.7), and balancing the regularization against the fit gives oracle inequalities (Corollaries 13.8 and 13.10) and sample-complexity guarantees (Corollaries 13.9 and 13.11), with ridge regression as the worked example (Theorem 13.1).
Hypotheses are vectors in with the Euclidean norm, as in Mission VI; risk, empirical risk, the product law of a sample and agnostic PAC learnability are those of Mission I. A problem is convex when is convex and every is convex; it is convex-Lipschitz-bounded with parameters when moreover on and every is -Lipschitz on , and convex-smooth-bounded with parameters when every is nonnegative and differentiable with a -Lipschitz gradient. Lipschitzness and smoothness are required on all of because the RLM rule is unconstrained and its outputs need not lie in . The RLM rule is a relation: is an output on if it minimizes over , and a learner implements the rule if all its outputs are minimizers. For the losses of the chapter the minimizer exists and is unique. Given and a further example , is with replaced by ; a learner is on-average-replace-one-stable with rate if for every distribution. Strong convexity is Mathlib's StrongConvexOn, which is Definition 13.4 verbatim.
Expectations over samples are integrals against product laws. For them to be genuine, the theorems about arbitrary learners assume a jointly measurable loss bounded by a constant and a measurable learner, and the theorems about RLM assume a jointly measurable, nonnegative loss bounded at the origin and a measurable learner; for RLM the latter is automatic, since the minimizer is unique.
For a convex-Lipschitz-bounded problem with parameters and the RLM learner with : for every distribution, every and every , ; hence for every and , .
Examples 12.8–12.9. Linear regression on with the squared loss is not agnostic PAC learnable, over or over .
Theorem 13.2. For any measurable learner and , equals the replace-one expectation of (13.6).
Lemma 13.5. is -strongly convex; a strongly convex function plus a convex one is strongly convex; at a minimizer of a -strongly convex , .
Corollary 13.6. For a convex -Lipschitz loss and , RLM satisfies for every , is stable with that rate, and has .
Corollary 13.7. For a convex, nonnegative, -smooth loss and , the replace-one expectation is at most , and at most if .
Corollary 13.8. for every .
Corollary 13.10. .
Corollary 13.11. A convex-smooth-bounded problem with is learned by RLM with once .
Theorem 13.1. Ridge regression on the unit ball with labels in , and has .
Further items: Lemma 12.11, the hinge loss as a convex surrogate of the 0–1 loss, the stability-implies-no-overfitting remark of §13.2, and the ridge regression system (13.4)–(13.5).
Stability is the third route to learnability in the book after uniform convergence and nonuniform learnability, and the only one that applies to convex-Lipschitz-bounded problems in general, for which uniform convergence can fail (the book's Exercise 13.2). The chain from strong convexity through replace-one stability to oracle inequalities is the template for the analysis of every regularized learner, and Theorem 13.2 is an exact identity, not a bound. Ridge regression, support vector machines (Chapter 15) and the regularized algorithms of later chapters are all instances.
Nothing here is machine-checked. The sample sizes of Corollary 13.11 and Theorem 13.1 are the book's . Chaining Corollary 13.10 as printed would need , but the derivation of Corollary 13.7 actually gives the stability rate , with which suffices.
Lemma 12.11 and the hinge surrogate are direct. Lemma 13.5 is elementary but part (3) needs the limit of the strong-convexity inequality at a minimizer. Examples 12.8–12.9 require constructing the two finitely supported distributions of the book and computing the risk of a fixed output on each; the probability that all examples are of the second type is at least under both, and the deterministic learner's output on that sample decides which distribution defeats it. Theorem 13.2 is the exchangeability argument of the book: because swapping and preserves the product law; the formal work is the measure-preserving transposition on and the integrability of the functions involved. Corollaries 13.6 and 13.7 follow the book's pointwise derivation from (13.7) to (13.11) and (13.12) to (13.14), where the smooth case uses the self-boundedness of nonnegative smooth functions and the inequality ; passing to expectations then uses Theorem 13.2 and, for the smooth case, the symmetry . Corollaries 13.8 to 13.11 are the arithmetic of the book once (13.16), , is in hand, with the corrected constant for 13.11. The ridge system is the gradient condition for a strongly convex quadratic, and Theorem 13.1 is Corollary 13.11 applied to , which is -smooth with on the support. In every expectation statement the measurability of for the RLM rule, which the theorems take as a hypothesis, is provable from uniqueness of the minimizer and is worth a lemma.
Losses are real-valued functions of a vector and an example; Lipschitz and smoothness conditions are global on . The RLM rule is a minimizer relation with the regularization parameter as an explicit argument, and Corollary 13.9's learner uses a parameter depending on . Stability quantifies over and averages over the replaced index. Expectation statements carry measurability hypotheses that make every integral genuine, and the theorems about arbitrary learners assume a bounded loss. The minimum over is stated as "for every ", so no minimizer is needed. Definitions 12.1–12.9 and Claims 12.4–12.9 (general convex analysis) are not restated, nor are Examples 12.10–12.11, the discussion of §12.3 beyond the surrogate property, Remark 13.1, and Exercises 12.1–12.4 and 13.1–13.2.
Trivializing readings are excluded: the nonlearnability examples are stated as negations of the framework's learnability, the stability identity is an equality with both sides genuine integrals, and the constants of the oracle inequalities are the book's. Welcome contributions: the transposition invariance of product laws behind Theorem 13.2, the bound for RLM outputs, the measurability of the RLM minimizer, and the self-boundedness inequality (12.6).
The Shape Zero model (Shape Zero LLC, unpublished) aims to obtain all three factors of the Standard Model gauge structure — , and — from a single linear-algebra statement applied at three node sizes. A node carrying oscillator pairs has a -dimensional real state space with a complex structure . Within the model, the couplings that do no net work (passive couplings) are the symmetric matrices, and those that respect are the ones commuting with it. The claim is that the couplings satisfying both conditions form a real vector space of dimension exactly , which is the dimension of the unitary Lie algebra (Unitary group):
| node size | admissible dimension | Lie algebra |
|---|---|---|
| 1 | 1 | |
| 2 | 4 | |
| 3 | 9 |
The dimension count has so far been checked numerically for only, giving . A machine-checked proof covers every , and it is the claim a physicist examining the model would check first.
What this mission does NOT prove. This mission proves the linear algebra: symmetric matrices commuting with form a space of dimension . It does not prove the physics step that passivity forces a coupling to be symmetric. That step is a separate premise of the model, and a completed mission must not be read as establishing it.
Fix a natural number . Consider real matrices, with rows and columns indexed by two copies of , so that each matrix is written in block form with blocks:
Let be the identity matrix and define the standard complex structure
which satisfies . In the Lean development this matrix is PassivityUn.stdJ n, and the index type is PassivityUn.Blk n, the disjoint union of two copies of Fin n.
Two real linear subspaces of the -dimensional space of such matrices are defined:
symm n: the symmetric matrices, ;commJ n: the matrices commuting with , .The admissible coupling class admissible n is their intersection:
This is PassivityUn.admissible_finrank. It asserts the exact dimension for all at once, not for a particular node size.
The result itself. The goal identifies the admissible coupling class with the real form of the Hermitian matrices, the space whose dimension is that of (Hermitian matrix). Applied at it gives the dimensions , and , which the Shape Zero model matches with , and . Without a proof for general , the model rests on a finite numerical check.
Formalizing it. The underlying fact is standard linear algebra, a special case of the correspondence between real matrices commuting with a complex structure and complex-linear maps (Linear complex structure). No machine-checked statement of this exact dimension count was found in the platform library. The mission produces a verified, general- statement whose hypotheses are fully explicit, and it separates the verified linear algebra from the unverified physical premise.
Every step is standard linear algebra, so the difficulty is in the formal bookkeeping rather than the mathematics. The dimension of a subspace defined by equations is not computed by any Mathlib tactic. It has to be obtained by exhibiting an explicit linear equivalence with spaces of known dimension, and that requires moving between the matrix indexed by a disjoint union and its four blocks. Checking small cases numerically, as has already been done, does not extend to a statement about every .
ℝ), not complex. The complex structure enters only through the fixed real matrix .Fin n ⊕ Fin n (PassivityUn.Blk n) rather than Fin (2n), so that block decomposition via Mathlib's Matrix.fromBlocks is direct. The first copy of Fin n indexes the upper/left blocks.Module.finrank ℝ. The ambient space is finite-dimensional, so the convention that finrank of an infinite-dimensional space is never applies.The development needs only Mathlib's block matrices, transpose, linear maps and finrank. The block-characterization lemmas (M2, M3) are reusable for any statement relating real matrices commuting with to complex matrices. Contributions are welcome on the milestones and on the assembling isomorphism.
Mathlib.Data.Matrix.Block (block matrices, Matrix.fromBlocks). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matrix/Block.htmlThe g-factor of a particle, nucleus or atom is the dimensionless number that measures its magnetic moment in units of the moment a classical particle with the same charge and angular momentum would have. Because it is both measured and computed to very high precision, small discrepancies between measured and predicted g-factors are used as tests of the Standard Model; the electron g-factor is known to about two parts in , and the muon g-factor has for two decades shown a several-standard-deviation tension between experiment and theory.
This mission formalizes the mathematical content of the Wikipedia article g-factor (physics): the definitions it gives, the elementary identities it states between them, and the numerical claims it makes about the experimental data.
All vectors live in , written as functions , with component playing the role of the component.
diracMagneticMoment).nuclearMagneton), the moment of a nucleon or nucleus with spin is (nuclearMagneticMoment).bohrMagneton) and electron orbital moment (electronOrbitalMagneticMoment).classicalMagneticMoment) and the angular momentum is (classicalAngularMomentum).The article defines the g-factor as the ratio of a particle's magnetic moment to the one "expected of a classical particle of the same charge and angular momentum", and says "by a quantum-mechanical argument analogous to the derivation of the classical magnetogyric ratio". The goal makes that classical baseline precise: for a system whose charge-to-mass ratio is the same for every particle (, ), with total charge and total mass ,
The goal is the statement that fixes the normalization of every g-factor in the article: it says that a classical body with uniform charge-to-mass ratio has gyromagnetic ratio exactly , i.e. , so any deviation from (such as ) is a genuinely non-classical effect. The milestones pin down the conventions (Dirac versus nuclear magneton, sign conventions for the electron orbital moment) and check the numerical claims the article makes from its data. None of these results is new; the contribution is a machine-checked, convention-explicit record of them.
The mathematics is elementary. The work is in the conventions: division by a mass or by is total in Lean and returns at , so positivity of masses and of must be carried explicitly, and the numerical milestones must be stated with the exact decimal values of the source rather than rounded ones.
Fin 3 → ℝ; the cross product is Mathlib's crossProduct. Component index 2 is the axis.Flow matching models a changing probability distribution using a time-dependent velocity field. A conditional model specifies a density and a velocity separately for each conditioning point. The mathematical question is whether those conditional descriptions determine a velocity for the mixture distribution. This mission concerns the continuity-equation formulation of Theorem 1 of Lipman, Chen, Ben-Hamu, Nickel, and Le, Flow Matching for Generative Modeling (ICLR 2023). The source is arXiv:2210.02747v2, Section 3.1 and Appendix A.
Fix a natural number and let . The conditioning distribution is a Borel probability measure on . At time , position , and conditioning point , write for the conditional density and for the conditional velocity. The variable is integrated against Lebesgue measure; is integrated against . These roles remain distinct even though both variables take values in the same space.
The conditional flux is . The marginal density, marginal flux, and marginal velocity are defined by
These definitions express equations (6) and (8) using a probability measure rather than a data-density function. This representation also allows discrete conditioning distributions. Every conditional density is strictly positive and normalized on , jointly measurable in , and integrable in at each fixed .
The divergence of a differentiable vector field is the sum of the diagonal entries of its derivative. A density and velocity satisfy the classical continuity equation when their flux is spatially differentiable and the density has time derivative equal to minus that divergence.
The goal asserts that is a positive probability density for every and that
The hypotheses require the conditional continuity equation for -almost every conditioning point, at each interior time and spatial point. They also specify a sufficient local domination package for differentiation under the integral. This is an explicit classical interpretation of the regularity qualification in the proof of Theorem 1.
Four supporting targets isolate the mathematical assertions used by this formulation: the probability-density property of equation (6); time differentiation under the conditioning integral; spatial divergence under the conditioning integral; and the velocity/flux identity corresponding to equation (8). The source contains these equations and operations rather than separately numbered supporting lemmas, so the milestone titles identify the relevant equation or proof passage.
The deliverable is a checked interface for passing from a measurable family of conditional continuity equations to the continuity equation of its mixture. It records which variables are differentiated, which measure is used for averaging, where positivity is needed, and which assumptions justify each analytic operation. The time and spatial differentiation lemmas are stated for general measures and integrands, making them reusable outside this particular probability model.
The mathematical result is already proved in the cited paper. The uploaded theorem items are open formalization targets, with explicit proof placeholders. Successful local compilation checks their types and imports; it does not establish their conclusions. The definition module contains no proof placeholders.
Pointwise differentiability of every conditional function does not by itself justify differentiating an integral over the conditioning variable. The regularity predicates therefore require a neighborhood independent of that variable, an integrable bound for the derivative norm throughout that neighborhood, and almost-everywhere measurability of the integrand and derivative. Time and space receive separate predicates because their derivatives take values in different spaces.
There is also a distinction between density normalization in and integrability in at a fixed position. The formal assumptions record both. A probability measure on the conditioning space does not make every measurable function integrable. These conditions prevent the totalized Bochner integral from silently supplying a default value where an intended integral fails to exist.
Space is represented by Fin d → ℝ, with its standard finite-product Borel structure and Lebesgue measure. Its norm is the standard product norm used by mathlib. All finite dimensions, including dimension zero, are included. Time-dependent functions are defined on all real times, while density assumptions apply on the closed unit interval and derivative conclusions apply on its interior. No endpoint time derivative is asserted.
The regularity package is one sufficient realization of the source's Leibniz-rule assumption, not a claim to the weakest possible hypotheses. Conditional continuity equations may hold almost everywhere in the conditioning variable; their exceptional sets may depend on the fixed time and position. Spatial differentiability of the marginal flux is part of the conclusion, so the equation cannot be satisfied merely through the default value of an undefined derivative.
The target is the PDE formulation. It does not assert existence of a global ODE flow, uniqueness of transported measures, or equality with a flow pushforward. Those require a separate transport development. It also asserts no endpoint approximation to a data distribution and no theorem about optimization, neural networks, or Gaussian paths. No marginal continuity equation or differentiation–integration interchange is assumed as an input.
Required infrastructure consists of Bochner integration, finite-dimensional differentiation, finite sums of derivative coordinates, and product-measure integration. Contributions may prove the supporting targets or the goal directly while preserving their statements and the distinction between classical PDE and flow-transport claims.
0df444a360eaa60ab8c11dca51a86af692955474. Differentiation under the integral.Since the 2019 revision of the SI, every unit in the system is fixed by assigning exact numerical values to seven defining constants: the caesium hyperfine transition frequency , the speed of light , the Planck constant , the elementary charge , the Boltzmann constant , the Avogadro constant and the luminous efficacy . Six of the seven base units — every one except the mole — therefore carry in their definition, and the caesium standard is the anchor of the whole system. The first caesium clock was built by Louis Essen and Jack Parry in 1955 (Nature 176, 280); the caesium frequency was tied to the ephemeris second by Markowitz, Hall, Essen and Parry in 1958 (Phys. Rev. Lett. 1, 105); the 13th CGPM adopted the caesium definition of the second in 1967, the CIPM added the "atom at rest at " qualification in 1997, the metre was redefined in terms of and the second in 1983, and the 26th CGPM fixed the present constant-based system in 2018, effective 2019 (Resolution 1 (2018)).
The audience for this mission is anyone who relies on those conversion factors being right: metrology, unit-aware computation, and formal libraries that want a machine-checked statement of what the SI actually fixes, rather than a table copied by hand.
All seven defining constants are exact decimal numbers, hence exact rationals:
each understood as the numerical value of the constant in its SI unit (hertz, metres per second, joule seconds, coulombs, joules per kelvin, reciprocal moles, lumens per watt).
From these one forms the four parameters of the caesium-133 hyperfine transition radiation:
its period, wavelength, photon energy and photon mass equivalent. The optical units bring in one further radiation, of frequency Hz, with period , wavelength , photon energy and luminous energy per photon .
Each line is the assertion that the displayed expression has numerical value exactly .
The radiation parameters ( and the 1967 definition of the second; and the claim that it lies between and cm; J; ); the individual base-unit relations for the kilogram, ampere, kelvin and candela; the derived units of energy, power, force, pressure and absorbed dose; the electromagnetic units, including as an exact multiple of ; the optical units and the parameters of the THz radiation; the katal; and finally the dependence statement: the formulas for the mole and the coulomb return the same value whatever the caesium frequency, while those for the second, metre, kilogram, ampere, kelvin and candela separate distinct positive frequencies.
What the results give is a machine-checked transcription of the exact arithmetic content of the 2019 SI: every coefficient in the table of base and derived units, checked against the defining constants rather than against another table. Downstream, a unit-conversion or dimensional-analysis development can cite these identities instead of re-deriving or re-typing sixteen-digit decimals, where a single transposed digit is a silent error.
What formalizing adds is faithfulness checking, not new mathematics. Every statement in this mission is a true identity between exact rational numbers; none of them is open in the mathematical sense.
This mission is arithmetically easy on purpose, and that should be stated plainly: each target is an equality between explicit rational numbers, and a solver who unfolds the constants and normalizes the arithmetic will close it. There is no analytic content, no limit, no inequality beyond the two decimal bounds on .
The real failure mode is transcription. The coefficients carry up to significant digits (the pascal), they are quotients of two decimals rather than single numbers, and the source displays several of them in a layout where a numerator and a denominator can easily be swapped. A statement that is off in the last digit is false, not approximately true, and is the kind of defect this mission exists to exclude.
Every quantity is modelled as an element of : the numerical value of the physical quantity in the corresponding SI unit. Dimensions are not tracked. A clause such as "" is formalized as the numerical identity , the unit bookkeeping being carried in the prose only; a development that wants dimensional safety must add a dimension layer on top. Decimal literals are exact rationals, not floating-point numbers, and no real-number approximation enters.
The statements are closed identities between explicit rationals, so none of them can be vacuous: each is either true or false, with no hypothesis to satisfy and no quantifier to exploit. The one quantified statement — the dependence of the unit formulas on the caesium frequency — ranges over all positive rationals and asserts non-equality in six cases and equality in two.
The definition layer is a single file of exact rational constants and the caesium radiation parameters; it is reusable by any later unit-related development. Contributions that would extend the mission usefully: a dimension-tracking layer over these constants, and the pre-2019 definitions (the krypton-86 metre, the IPK kilogram, the triple-point kelvin) stated in the same style for comparison.
Boosting answers a question raised by Kearns and Valiant: can a learner that is only slightly better than random guessing be turned into one that is arbitrarily accurate? Chapter 10 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) defines γ-weak learnability (Definition 10.1), the PAC requirement with the accuracy replaced by the fixed value , and presents AdaBoost, the algorithm of Freund and Schapire that, given weak hypotheses, reweights the training set round by round and outputs a weighted majority vote. The chapter's main result (Theorem 10.2) is that the training error of AdaBoost's output decreases as in the number of rounds. Since the output is a halfspace over the predictions of base hypotheses, the chapter then bounds the VC-dimension of that class (Lemma 10.3), so that the number of rounds becomes a knob for the bias–complexity tradeoff. Example 10.1 shows a concrete weak learner, ERM over decision stumps for the class of 3-piece classifiers on the line, and the chapter remarks that, statistically, weak learnability is no easier than strong learnability: a class of infinite VC-dimension is not weakly learnable either.
The framework is that of Missions I and IV: binary classification over a domain with the 0–1 loss, distributions over with a labeling function , learners as functions of the sample, the VC-dimension, and ERM. Labels and hypotheses are Boolean, with values obtained through , , and is true exactly when . A γ-weak learner for with the function returns, for every , every and every measurable realizable by , a hypothesis with with probability at least once ; the failure event is bounded in outer measure as in Definition 3.1.
AdaBoost is formalized as a deterministic function of the sample and of the sequence of weak hypotheses that the weak learner returned. The distributions are defined by recursion: is uniform, , , and ; the output after rounds is . Rounds are indexed from , so is the book's . The class of Equation (10.4) consists of the functions with . Decision stumps over are the threshold functions and their negations ; a 3-piece classifier is outside and inside, with .
If and every round has , then the empirical 0–1 risk of AdaBoost's output after rounds is at most .
§10.1. A class of infinite VC-dimension is not γ-weak-learnable for any (domain with measurable singletons, measurable hypotheses).
Example 10.1. There is one sample-size function with which every ERM learner over the decision stumps is a -weak learner for the 3-piece classifiers.
Exercise 10.3. For a nonempty sample and , the error of under is exactly .
Lemma 10.3. If and , then .
Further item: Exercise 10.4 (1), for .
Theorem 10.2 is the reason AdaBoost works and the template for every analysis of boosting: a potential function, here , bounds the 0–1 training error and contracts by the factor at every round. Lemma 10.3 supplies the other half of the picture, an estimation-error bound growing only like up to logarithms, so that Theorem 6.8 turns the pair into a generalization guarantee for boosting. The remark of §10.1 places weak learning in the statistical landscape of Part I: the VC-dimension characterizes it too, and the gain of boosting is computational.
Nothing here is machine-checked. Two points where the book's text needs care are built into the statements. The weight is undefined when , and the algorithm's normalization then divides by ; in Lean the logarithm of a negative number is , so with the formal algorithm would ignore a perfect weak hypothesis and the bound could fail. The theorems therefore assume , which is the case in which the book's formulas are defined. And the book's derivation of "infinite VC-dimension implies not weakly learnable" from the lower bound of Theorem 6.8 at uses that bound outside the range in which Chapter 28 proves it; the statement itself is true, by the -point form of the No-Free-Lunch argument (Exercise 5.3 of Mission III) and Lemma B.1.
Exercise 10.4 (1) is a one-line embedding of into with the weights and is the entry point. Exercise 10.3 is the computation of the book: after the update, the weight of the mistakes of is and the weight of the correct examples is , and with these are equal. Theorem 10.2 needs, by induction on the round, the closed form of the distribution, the pointwise bound for the sign convention used, the telescoping product (10.2), the identity , the monotonicity of on and . Lemma 10.3 counts dichotomies: Sauer's lemma bounds the restrictions of to a shattered set by , choosing of them gives , the halfspaces of contribute by Theorem 9.2, and the inequality is solved with Lemma A.1; the finite-VC lower bound handles small , and the numeric slack of the book's chain must be checked. Example 10.1 combines a geometric observation, that one of the three regions of a 3-piece classifier has mass at most and a stump agrees with the other two, with the agnostic guarantee for ERM over the stumps from Theorem 6.7, applied with accuracy ; the best stump may only approach error because constant functions are not stumps, and the slack absorbs this. The §10.1 remark is the argument sketched above.
AdaBoost is a function of the sample and of the returned weak hypotheses; the weak learner's randomness and its failure probability (Remark 10.2) are not modelled, and Theorem 10.2 is the deterministic statement the book proves. Rounds are indexed from . The output uses negative, consistently with Mission VI. The class is a set of functions, so Lemma 10.3 is a statement about the VC-dimension of Mission IV, with the bound taken in through the integer part of the real right-hand side and the natural logarithm. Decision stumps are closed under negation, as the book's ; constant functions are not stumps. The efficient ERM for decision stumps (§10.1.1), the face-recognition features (§10.4), Exercises 10.1, 10.2, 10.4 (2)–(3) and 10.5 are not stated. The claims of §10.3 that piecewise-constant classifiers with pieces lie in and that this class shatters points depend on treating as a stump and on the sign convention; with real thresholds, does not shatter three points under either convention, so these claims are not stated.
Trivializing readings are excluded: the weak-error hypotheses are strict where the book's formulas require it, the VC bounds are in , and the weak-learner guarantee quantifies over all distributions and all realizable labelings. Welcome contributions: the closed form of , the contraction identity for , and the dichotomy count behind Lemma 10.3.
Part II of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) turns from the theory of learnability to hypothesis classes that can actually be learned by algorithms, and it starts with the family that almost every practical method is built on: linear predictors. Chapter 9 introduces the affine functions and the three classes obtained by composing them with a link: halfspaces for classification, linear regression for real-valued prediction, and logistic regression in between. For each class it gives an ERM algorithm and the guarantee that goes with it. For halfspaces in the separable case the algorithm is Rosenblatt's Perceptron, and the guarantee is the classical mistake bound (Theorem 9.1): the number of updates is at most , where bounds the data and is the norm of the smallest vector separating it with margin one. The chapter then computes the VC-dimension of halfspaces (Theorems 9.2 and 9.3), which by the fundamental theorem of Mission IV makes them learnable, derives the Least Squares normal equations for regression, and observes that the logistic loss is convex, the property later chapters exploit.
Vectors live in with its Euclidean inner product and norm. The affine functions are , homogenous when ; a halfspace hypothesis is , formalized as a Boolean predictor that is true exactly when (the book leaves unspecified; the VC computations do not depend on the convention). A sample with labels is separable if some has for all ; the constants of Theorem 9.1 are and . The Batch Perceptron starts at and, while some example has , adds ; since the algorithm may pick any mistaken example, a run is any sequence of updates obeying this rule, and the theorem is stated for all runs. For regression the loss is and the Least Squares system is with , written as the linear map , and . The logistic function is and the logistic loss is . The learning-theoretic notions (ERM, PAC and agnostic PAC learnability, VC-dimension) are those of Missions I and IV.
For a separable sample with labels in , every run of the Batch Perceptron of iterations satisfies , and some run of at most iterations ends with for every .
Equation (9.1). A sample is separable if and only if some satisfies for all .
Theorem 9.2. The VC-dimension of the homogenous halfspaces in is .
Theorem 9.3. The VC-dimension of the halfspaces in is .
Least Squares (9.6). The system always has a solution, and solves it if and only if is an ERM hypothesis for the squared loss over the homogenous linear predictors.
Further items: Exercise 9.3, the tightness of Theorem 9.1 (for every a sample with , and a run of exactly updates); the learnability of halfspaces by ERM, a consequence of Theorem 9.3 and the fundamental theorem; Exercise 9.2, is invertible iff the span ; and the convexity of the logistic loss in .
The Perceptron bound is one of the oldest results of learning theory (Novikoff 1962) and the model for every mistake bound in the online-learning chapters: it is independent of the dimension and of the number of examples, depending only on the geometry of the data through and . Theorems 9.2 and 9.3 are the first VC-dimension computations of a class used in practice and give, through Theorem 6.8, the sample complexity of learning halfspaces. The normal equations are the algorithmic content of linear regression, and the convexity of the logistic loss is why logistic regression is tractable in the nonseparable case, where ERM for halfspaces with the 0–1 loss is hard.
Nothing here is machine-checked in this form. Mathlib has the inner-product geometry, the Cauchy–Schwarz inequality, linear algebra of finite-dimensional spaces and convexity of compositions, but neither the Perceptron nor the VC-dimension of halfspaces.
Equation (9.1) is a rescaling and the intended entry point. The convexity of the logistic loss is the composition of the convex function with the linear map . Exercise 9.2 is the identification of the kernel of with the orthogonal complement of the span. The normal equations require showing that a convex quadratic is minimized exactly where its gradient vanishes, and that lies in the range of , which is the span of the . Theorem 9.1 is the book's proof: by induction on the run, and for any feasible , then Cauchy–Schwarz, and finally the passage from a feasible to the infimum ; the existence clause follows because a run can be extended as long as the stopping condition fails and all runs are bounded. Theorem 9.2 is the linear-dependence argument of the book, with a case analysis on the signs of the coefficients and on which side is nonempty, and the shattering of the standard basis; Theorem 9.3 lifts it to by appending a constant coordinate. The learnability of halfspaces is Theorem 6.7 applied to a class that must be shown measurable, nonempty, of finite VC-dimension and pointwise separable; the last needs rational approximations in which the offset moves below more slowly than approaches , so that boundary points keep their label.
Halfspaces are Boolean predictors with negative; the classes are sets of functions, so the VC-dimension is that of Mission IV. The Perceptron is a relation on sequences, not a program: this captures the algorithm's freedom to choose any mistaken example and makes the bound apply to all implementations. is an infimum, which is attained (the feasible set is closed and the norm is coercive), but the theorem does not need attainment. is a real supremum over the finite index set, equal to for the empty sample, where every run has length . The Least Squares statement is about the homogenous class and the sample , with ERM in the sense of Mission I; the bias term is handled by the book's reduction, appending a constant coordinate, and is not formalized separately. The learnability item states qualitative learnability and the ERM guarantee with an unspecified sample-complexity function; the quantitative rate is Theorem 6.8 of Mission IV. Linear programming (§9.1.1), the pseudo-inverse (§9.2.1), polynomial regression (§9.2.2), Exercises 9.1 and 9.4–9.6 are not stated.
Trivializing readings are excluded: labels are constrained to , runs must start at and update only on mistakes, the VC equalities are in , and the ERM equivalence is a biconditional. Welcome contributions: the two Perceptron invariants as separate lemmas, the shattering of the standard basis, and the pointwise separability of halfspaces.
The fundamental theorem of Mission IV says that a class of binary classifiers is PAC learnable exactly when its VC-dimension is finite. That leaves out classes one would like to learn, such as all polynomial classifiers over the line, whose VC-dimension is infinite although each degree separately is learnable. Chapter 7 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) relaxes the definition. In nonuniform learnability (Definition 7.1) the sample size may depend on the hypothesis the learner is competing with: the learner must, for every , eventually do as well as up to , but how soon may depend on . The chapter's main result (Theorem 7.2) characterizes the nonuniformly learnable classes of binary classifiers as the countable unions of agnostic PAC learnable classes. The learning rule behind it is Structural Risk Minimization (SRM): write , weight the pieces, and minimize the empirical risk plus a confidence term that grows with the index (Theorems 7.3–7.5). Applied to a countable class described by a prefix-free code, SRM becomes the Minimum Description Length rule and yields a quantitative form of Occam's razor (Lemma 7.6, Theorem 7.7). The chapter closes the circle with a No-Free-Lunch result for the relaxed notion (Remark 7.2, Exercise 7.5).
The framework is that of Missions I, II and IV: examples in a domain , a hypothesis type with a class , a loss , risk and empirical risk , learners as functions of the sample, the uniform convergence property with an explicit rate , agnostic PAC learnability, and for binary classification the 0–1 loss, the VC-dimension and pointwise separability. The new module adds Definition 7.1 with an explicit rate and, as in Definition 3.4, learners whose outputs lie in ; the same notion for a family of learners indexed by the confidence , since the SRM and MDL rules take as an input; the rate of Equation (7.1), which is meaningful only when that set is nonempty; the index of Equation (7.4); the SRM rule as a minimizer of over the admissible hypotheses, those whose index has positive weight and a defined rate; prefix-free description languages and the MDL rule; and shattering of an infinite set.
For a class of measurable binary classifiers over a domain with measurable singletons, every subclass of which is pointwise separable, is nonuniformly learnable if and only if there are classes with , each agnostic PAC learnable.
Theorem 7.3. If is nonempty and each has the uniform convergence property, then is nonuniformly learnable (general loss).
Theorem 7.4. For weights with partial sums at most , uniformly convergent pieces with rates , , any and any : with probability at least , for every with at which is defined and every , .
Theorem 7.5. With and , every family of learners implementing the SRM rule satisfies the nonuniform guarantee with rate .
Lemma 7.6 (Kraft). For a prefix-free set of binary strings, every finite subfamily satisfies .
Theorem 7.7. For a prefix-free description language on a class with a -valued loss, and : with probability at least , every satisfies .
Further items: nonuniform learnability is implied by agnostic PAC learnability (§7.1); a nonuniformly learnable class of binary classifiers is a countable union of classes of finite VC-dimension (Exercise 7.5 (1)–(2)); a class shattering an infinite set admits no countable cover by classes of finite VC-dimension (Exercise 7.5 (3)) and is not nonuniformly learnable; over an infinite domain the class of all measurable classifiers is not nonuniformly learnable (Remark 7.2).
Theorem 7.2 is the second characterization theorem of the book's Part I and the one that explains why model selection works: any class that can be stratified into learnable pieces is learnable in the nonuniform sense, with the price of not knowing the index paid in sample size rather than in principle. SRM is the abstract form of every penalized learning rule, and the MDL bound of Theorem 7.7 is the cleanest instance, a bound in which the only property of the hypothesis that matters is the length of its description. Remark 7.2 shows the relaxation is not free: even nonuniformly, no learner handles all classifiers over an infinite domain.
Nothing here is machine-checked. The chapter's arguments are short but they combine everything before them: Hoeffding, the union bound with weights, the VC lower bound of Corollary 6.4 and the fundamental theorem. Three places where the book's statements need care are recorded in the formalization: the rate is an infimum that may be undefined for small ; the SRM rule takes as an input and so is a family of learners; and the fundamental theorem's uniform-convergence direction needs a measurability condition, which appears in Theorem 7.2 as hereditary pointwise separability.
The relaxation remark is a direct comparison of two definitions. Kraft's inequality is the coin-tossing argument of the book or an induction on the maximal length: it is the intended entry point. Theorem 7.4 is Theorem 7.3's engine: for each index and each in the set of Equation (7.1), the uniform convergence property bounds the failure by ; the passage from "every in the set" to the infimum uses continuity of the outer measure along an increasing union; the union over uses countable subadditivity and the partial-sum condition. Theorem 7.5 is Theorem 7.4 on the good event together with the two inequalities of the book's proof, using that the target is admissible when and that admissibility of the SRM output gives the bound for it. Theorem 7.3 asks for a single learner: SRM with a confidence schedule chosen so that, for each fixed index, the rate at level eventually falls below any , together with an approximate minimizer within ; the target hypothesis is admissible for large. Theorem 7.7 is Theorem 7.4 with singleton pieces and the weights , a one-sided Hoeffding bound for each , and Kraft's inequality. Exercise 7.5 (3) is the combinatorial construction of the book's hint, disjoint finite subsets of the shattered set with and a labeling that no realizes. The first half of Theorem 7.2 is Corollary 6.4 applied to the nonuniform learner at fixed , with constants chosen so that the two probability bounds actually contradict; the second half is the fundamental theorem on each piece followed by Theorem 7.3.
Learners output hypotheses in , in Definition 7.1 as in Definition 3.4. The rate is an infimum over the set of Equation (7.1), and every statement that uses it is guarded by the nonemptiness of that set; the weight may be , and encodes the book's indices . The SRM rule minimizes over admissible hypotheses, and an SRM family is one that returns an admissible minimizer whenever some hypothesis is admissible, which is the book's assumption that the argmin is attained (automatic for the 0–1 loss). Theorem 7.4's sum condition is on partial sums, and Kraft's inequality is on finite subfamilies, so no divergent series is silently zero. Theorem 7.7 assumes a -valued loss and . The binary-classification results assume measurable singletons and measurable hypotheses; Theorem 7.2 also assumes every subclass pointwise separable, which every class over a countable domain satisfies. Definition 7.8 (consistency) and the Memorize algorithm of §7.4 are not stated.
Trivializing readings are excluded: outputs in keep the risk an honest integral, the rate is never a junk infimum of the empty set, and the failure events are bounded in outer measure. Welcome contributions: a reusable weighted union bound over a countable family of uniform-convergence events, the continuity argument for the infimum rate, and the shattered-set combinatorics of Exercise 7.5.
Two different numbers describe the output of a lamp. Radiant flux is the power it radiates, in watts. Luminous flux is how much of that radiation the standard human eye registers, in lumens — a weighted integral of the radiated power in which each wavelength is counted according to the sensitivity of the eye at that wavelength. Their ratio
is the luminous efficacy of radiation, measured in lumens per watt: it says what fraction of the radiated power is usable for illumination. Photometry is built on this pair of quantities. The lumen and the candela are defined from the watt through exactly such a weighting, with the SI defining constant lm/W fixing the scale at the frequency Hz, and every efficiency figure quoted for a lamp — a tungsten filament at lm/W, a white LED above lm/W — is a statement about this ratio or its wall-plug variant.
The basic structural fact of the subject is that this ratio is bounded. Since the eye's sensitivity curve is normalized to a maximum of , no source, however designed, can exceed the maximum spectral luminous efficacy: lm/W under photopic (daylight, cone) vision, and about lm/W under scotopic (dark-adapted, rod) vision. Those two numbers are the ceilings against which every lighting technology is measured, and they are what this mission formalizes.
Wavelengths are real numbers (nanometres). A spectral radiant flux distribution of a source is modelled as a finite Borel measure on the wavelength axis: is the power, in watts, that the source radiates at wavelengths in . Its radiant flux is the total mass
A luminosity function (luminous efficiency function) with peak at is a measurable with
For photopic vision the CIE 1924 curve peaks at nm; the scotopic curve peaks at nm. The development assumes only the normalization above, never a specific tabulated curve, so every statement holds for the photopic curve, the scotopic curve, and any other normalized weighting.
Given a maximum spectral luminous efficacy — the value lm/W for photopic vision, lm/W for scotopic vision — the spectral luminous efficacy is and the luminous flux is
The luminous efficacy of radiation is , the dimensionless luminous efficiency is , and the luminous efficacy of a source (overall, or wall-plug, efficacy) is , where is the total input power the source consumes — electrical, chemical or other — of which the radiated part is .
Modelling the spectrum as a measure rather than as a density is what makes the two halves of the target statement expressible at once. A spectrum with a spectral radiant flux density is the measure , for which the formulas above reduce to the usual integrals
an ideal monochromatic source at , which has no density with respect to wavelength, is the point mass .
This is a maximum, not a supremum: the assertion is both that no spectral radiant flux distribution exceeds lm/W and that some distribution — the monochromatic source at nm — attains it exactly.
for a scotopic luminosity function with .
; ; ; luminous efficiency in ; the point mass at the peak realizes ; the reduction of to the integral formula for a spectrum with a density; invariance of under rescaling the spectrum; when ; and for a source radiating only where vanishes.
The ceiling is the reference point for the whole of lighting efficiency: quoted luminous efficiencies are efficacies divided by lm/W, so "" for a truncated K black body and "" for a tungsten filament are statements about the distance to this bound. The supporting statements are the facts that make such comparisons well posed — that the efficacy depends only on the shape of the spectrum and not on the wattage, that the wall-plug efficacy of a device is never better than the efficacy of its radiation, and that power radiated outside the response band is pure loss.
Formalizing the material produces a small, reusable measure-theoretic layer for photometric and, more generally, for weighted-average quantities: a bounded weight integrated against a finite measure, normalized by the total mass, with the extreme value attained at a point mass. Nothing here is open mathematics; the value of the mission is a machine-checked model in which the definitions of the International Electrotechnical Vocabulary are stated once and the standard consequences are derived from them, rather than each being asserted in prose.
The mathematical content is elementary — the ceiling is the inequality for — and the work is in the modelling. Three points need care.
First, attainment. On the space of densities the value lm/W is a supremum that is never attained: for the actual CIE curve the set is a single point, hence Lebesgue-null, so a density supported there is zero almost everywhere and has no radiant flux at all. A formalization restricted to densities would either have to weaken the goal to a supremum or state an attainment claim that is vacuously true. Measures avoid this: the monochromatic source is the point mass .
Second, division. Efficacy is a quotient, and the quotient of a real by zero is a junk value; every statement about therefore carries the hypothesis , which is also the physically meaningful one.
Third, integrability. The luminous flux is a Bochner integral, which returns for a non-integrable integrand; the mission's hypotheses ( measurable and bounded, finite) are what rule this degeneracy out.
The wavelength axis is all of , with Lebesgue measure where a density is used; no restriction to positive wavelengths or to a visible band is imposed, since the luminosity function already performs the restriction. A spectral radiant flux distribution is a finite Borel measure; the finiteness hypothesis is carried as a typeclass assumption and the positivity of the radiant flux as an explicit one. The luminosity function is assumed measurable with values in and equal to at its peak, and nothing more: no continuity, no unimodality, no tabulated values. The maximum spectral luminous efficacy appears as an explicit parameter , so that the photopic constant and the scotopic constant are instances of the same statements rather than separate developments. Units are not represented in the types: all quantities are plain real numbers, and lumens per watt appears only in the prose.
The goal is stated as " is the greatest element of the set of achievable efficacies", which rules out the two trivializing readings: a bare upper bound (true of any number above the ceiling) and an attainment claim over a class of spectra that is empty or null.
A complete development needs Mathlib's measure theory and Bochner integration only: finite measures, withDensity, Dirac measures, and monotonicity of the integral. The resulting definitions are reusable for any normalized weighted average of a finite measure, and contributions extending the model — mesopic weighting, black-body spectra and the efficacy figures computed from them, or the CIE curve as tabulated data — are welcome.
The Avogadro constant is the conversion factor between an amount of substance and a number of elementary entities (atoms, molecules, ions, ion pairs). Since the 2019 revision of the SI it is a defining constant with the exact value ; the pure number is called the Avogadro number. Before 2019 the mole was instead defined as the amount of substance in 12 grams of carbon-12, so was a measured quantity: the number of carbon-12 atoms in 12 g, equivalently the number of daltons in a gram, . The two definitions agree to within the experimental uncertainty of the dalton, but no longer by fiat.
The relations that carry this content — , , , , and the crystal/unit-cell count used by the Avogadro Project's X-ray crystal density measurements on silicon-28 spheres — are stated in every chemistry course and used without further comment. They are elementary, but they are also exactly the kind of unit-bookkeeping that is easy to state loosely and easy to get wrong by a factor, and they have no machine-checked formulation.
Fix a common positive scale for masses, volumes and amounts, and record on it three units: a mass unit (gram), a second mass unit (dalton), and an amount unit (mole), each a strictly positive real number. Write
For a sample containing entities, its amount of substance is ; for an entity of mass , the molar mass is ; for an entity occupying volume , the molar volume is ; the elementary amount is . For a crystal of volume whose unit cell has volume and contains entities, the number of entities in the crystal is .
All of these are modelled as real numbers; units appear as positive real parameters rather than as a dimension system, so every statement below is an identity between real numbers that holds for every admissible choice of , , .
Under the pre-2019 definition of the mole, let be the mass of one carbon-12 atom, let satisfy (a mole of carbon-12 weighs 12 grams), and let the dalton be one twelfth of the mass of a carbon-12 atom, . Then
That is: the Avogadro number under the old definition is exactly the number of daltons in a gram. The goal fixes no numerical value — it asserts the shape of the relation, and so survives any revision of the measured value of the dalton.
The six milestone lemmas are the remaining relations the source states: the inversion ; the 2019 statement ; the elementary-amount identity ; the pre-2019 numerical coincidence that a particle of mass has molar mass exactly when ; the worked numerical example that a water molecule occupies about when the molar volume of water is ; and the crystal/unit-cell amount relation.
The result itself is not new mathematics: each identity is one line of algebra once the model is fixed. What the mission produces is the model — a single, audited Lean formulation of amount of substance, molar mass, molar volume, the elementary amount, and the crystal count, in which the pre-2019 and post-2019 definitions of the mole can both be stated and compared, and in which the one place where the two definitions differ (the dalton is measured, the Avogadro number is fixed) is visible rather than hidden in a convention. That layer is reusable by any later formalization that needs to convert between microscopic and molar quantities, including the X-ray crystal density determination of from silicon-28 lattice measurements.
Status honesty: everything stated here is standard, textbook-level content, and all seven statements have been checked to be provable in the model as formalized. The mission's value is the faithful encoding and the audited definition layer, not the difficulty of the proofs.
The proofs are elementary real algebra; the difficulty is entirely in the statements. Two traps recur. First, division in Lean is total, so an identity such as carries no information at and can be satisfied vacuously; every statement here therefore either derives positivity from the unit data or takes the nondegeneracy hypothesis explicitly. Second, it is easy to write a unit relation that is true only for one choice of units — for instance, conflating the numerical value with the dimensional constant — and such a statement still compiles. Readers auditing this proposal should check each statement against both failure modes.
Units are positive real parameters bundled in a structure carrying together with proofs of their positivity; there is no dimension-tracking type system. Amounts, masses, volumes and entity counts are real numbers (the crystal's entities-per-cell count is a natural number). The Avogadro number is the exact rational , so the numerical milestone is a genuine rational-arithmetic bound, not a floating-point approximation. The water example is stated as a strict two-sided bound, , so that it cannot be satisfied by a rounded value.
A trivializing formalization is ruled out as follows: no statement is of the form "some quantity exists", every statement quantifies over an arbitrary admissible unit system, and the goal's hypotheses are simultaneously satisfiable (take , for any ), so the goal is not vacuous.
Contributions welcome: a dimension-typed refinement of the unit layer, and the X-ray crystal density relation for a cubic lattice, which the source describes only qualitatively and which is deliberately not claimed here.
A black body is an idealized body that absorbs all radiation falling on it and, when held at a fixed absolute temperature , re-emits radiation whose spectrum depends on alone. At the end of the nineteenth century two incompatible descriptions of that spectrum were on the table. Wien's distribution law (1896) fitted the measurements at short wavelengths and high temperatures but failed at long wavelengths. The formula Rayleigh obtained from classical equipartition, later the Rayleigh-Jeans law, reproduced the long-wavelength data and grew without bound at short wavelengths - the failure Ehrenfest named the ultraviolet catastrophe in 1911.
Planck's 1900 formula fits at every frequency. He reached it by refusing to treat the vibrational energy of the oscillators as a continuous quantity, writing it instead as an integer multiple of an energy element ; the constant entered physics as the proportionality factor in that hypothesis. Fitting black-body data, Planck obtained , within about of the value that today defines the SI.
What makes Planck's formula the successful one is not only that it fits the data. It contains both classical laws: it degenerates to Rayleigh-Jeans at low frequency and to Wien's law at high frequency, and unlike Rayleigh-Jeans it has a finite total emission. This mission formalizes those four statements - two limits and two integrability claims - about the spectral radiance function itself.
Fix three positive real parameters: the Planck constant , the speed of light , and the Boltzmann constant . They are kept as variables rather than numerical constants, so every statement is a theorem about the functional form, valid in any system of units. Let be an absolute temperature.
Per unit frequency , Planck's law gives the spectral radiance
which is the function planckFreq of the already-published definition bundle
BlackbodyRadiation_planck. That bundle also provides the dimensionless shape function
in terms of which .
Two further functions are introduced by this mission. The Rayleigh-Jeans spectral radiance, the classical equipartition prediction,
and Wien's distribution law, the short-wavelength approximation,
Write for the dimensionless frequency. All three radiances are positive on ; the two comparisons below are stated as ratios, which is the precise form of "agrees with, in this regime".
For all , all four of the following hold simultaneously:
The goal asserts only the shape of the truth - ratios tending to and membership or non-membership in - and fixes no constant, so it is not invalidated by any sharper rate or by the exact value of the total emission.
The four conjuncts are milestones in their own right, together with the two shape-function limits that drive them:
The result itself. The two limits are the sense in which Planck's law reproduces Wien's law for short wavelengths and the empirical long-wavelength formula, which is the criterion Planck was working to when he introduced ; the non-integrability of is the ultraviolet catastrophe, stated exactly rather than as an asymptotic remark; and the integrability of is what makes the total emitted power
CODATA2022.blackbody_exitance_eq_stefanBoltzmann, CODATA2022.bose_einstein_integral_cube),
both of which are Open.Formalizing it. The physics has been settled for over a century; none of it is open
mathematics. What is missing is machine-checked statements: the platform's existing
black-body development (BlackbodyRadiation_planck, and the mission Planck's Law and
Wien's Displacement Law) covers the peak of the spectrum and the exact radiation
constants, but not the two classical regimes, and not integrability. The limit and
integrability lemmas about produced here are reusable for any later work on
Bose-Einstein integrals, the Debye model, or the Stefan-Boltzmann constant.
The obvious argument for each limit is a one-line asymptotic expansion, and the obvious argument for integrability is "the integrand decays exponentially". Neither survives contact with a formal proof as stated. The ratio equals only after cancelling , and , which requires those factors to be nonzero - so the algebraic reduction is valid on a punctured neighbourhood, and must be transported to the limit through a congruence-along-a-filter step rather than by rewriting the function globally. At the ratio is a junk value, which is exactly why the limit is taken within .
For integrability the difficulty is at the two ends at once: near the integrand is but the defining expression is a quotient whose denominator vanishes, and near the exponential decay has to be turned into a dominating integrable function rather than a limit statement. Non-integrability of must be derived from unboundedness of , not asserted from the divergence of the integral, since an unproved-integrability integral in Lean silently evaluates to .
Everything is over with the Lebesgue (volume) measure; membership is
MeasureTheory.IntegrableOn ... (Set.Ioi 0) volume, which includes measurability.
One-sided limits are filters: is the neighbourhood filter of restricted
to , and is Filter.atTop. The three physical parameters and
the temperature are explicit real arguments, each carrying its own strict positivity
hypothesis; no statement is quantified over a possibly empty set of parameters, and every
hypothesis is satisfiable, so nothing here is vacuous.
The radiance functions are total: division by zero yields in Lean, so and the comparison ratios are at . That is harmless for the limits, which are taken strictly inside , and it is why the integrability statements are on rather than on . The comparisons are deliberately stated as ratios tending to rather than as differences tending to : the latter would be a weaker claim, and near it would be satisfied by functions that are not asymptotically equal.
Contributions welcome beyond the milestones: the corresponding statements in the wavelength parameterization, quantitative error bounds on the two approximations, and the integrability of on for general , which would close the remaining gap in the Stefan-Boltzmann chain.
The gravitational constant is the proportionality constant in Newton's law of universal gravitation and, through the Einstein gravitational constant , in the Einstein field equations. It is the least precisely known of the fundamental constants: the CODATA-recommended value is , a relative standard uncertainty of , and published high-precision measurements since the 1980s have at times been mutually exclusive. Everything that is known about is known through a small number of algebraic identities that convert a measurable quantity - a surface acceleration, a mean density, an orbital period - into a value of . Those identities, not the measurements, are what can be formalized, and they are what this mission collects.
The identities themselves are classical: the inverse-square law dates to Newton's Principia (1687), the notation to C. V. Boys in the 1890s, and the first laboratory determination to the Cavendish experiment of 1798, which reported a mean Earth density of - equivalent to in modern units, about above the modern value. The route from "mean density of the Earth" to "value of " is exactly one of the identities below.
All quantities are real numbers; no dimensional type discipline is imposed, and units are handled explicitly where they matter (see Formalization scope).
For a gravitational constant , point masses and a centre-to-centre distance , the Newtonian force is
For a spherically symmetric body of mass and radius , the surface gravity ("small ", as opposed to "big ") is
the ball volume is , and the mean density is .
A circular orbit of radius and period about a mass is the condition that the centripetal acceleration equals the gravitational acceleration:
The Einstein gravitational constant is .
For , and a circular orbit of radius and period about ,
This is the article's statement that is fixed by the period of an orbit and the volume it encloses. It is the weakest stable form of the orbital identity: no numerical value of , no unit system, and no choice of body are hard-coded into it.
The milestone list refines the goal into the chain the source uses: the "big / small " relation, its mean-density form (the Schiehallion-Cavendish route), , Kepler's third law for circular orbits, the grazing-satellite form , the relation to , and the SI cgs conversion of the recommended numerical value.
The result itself. The identities in this mission are the bridge between what an experiment measures and the number reported for : the mean-density form is what turns the Schiehallion and Cavendish results into values of ; the orbital form is what makes the product (the standard gravitational parameter, known far more accurately than either factor) the quantity celestial mechanics actually uses; the relation is what carries the Newtonian constant into general relativity.
Formalizing it. No claim here is open mathematics - each target is a consequence of real-field algebra, and the mission's contribution is a single, faithful, reusable Lean vocabulary for elementary Newtonian gravitation (force, surface gravity, mean density, circular orbits) together with machine-checked statements of the identities the literature quotes informally. The mission is a formalization task, not a research task, and it is presented as such.
The mathematical content is elementary; the difficulty is entirely in faithfulness, and it has two specific sources.
First, division in Lean's real numbers is total: . Several of these identities are therefore true but empty at degenerate arguments unless positivity hypotheses are stated, and conversely it is easy to over-hypothesize and end up proving a weaker claim than the source states. Each statement below fixes a particular choice, and that choice is the thing to audit.
Second, the SI/cgs target is a claim about units, which have no primitive representation here. It is stated in a model where each unit symbol is a real scale factor constrained by the relations between the systems; the honest reading of that target is "the two printed numerical values denote the same quantity given , and ", and nothing stronger.
Everything is over . The definition layer is a single definition item
providing newtonForce, surfaceGravity, ballVolume, meanDensity,
einsteinConstant, the predicate IsCircularOrbit, and the numerical constant
gravitationalConstantSI ; every theorem in the mission is
phrased through those, so the definition layer is the part that must be audited first.
The orbit condition is stated as a predicate on carrying and , rather than as a derived function, so that no target is vacuous: for every , and there is a satisfying it, so the hypotheses of the orbital targets are satisfiable, and the targets are not true merely for want of instances. No target is stated as an existence claim that a witness construction could trivialize.
Units are modelled as real scale factors rather than by a dimensional type system; a solver who wants a genuinely dimension-typed treatment is welcome to contribute it as a separate development, but the target here is the scale-factor statement.
A complete development needs nothing beyond Mathlib's ordered-field and Real.pi API.
The definition layer is intended to be reusable by any later mission on Newtonian
gravitation, orbital mechanics, or unit conversion.
The encyclopedic account of the speed of light makes two claims that look physical but whose content is mathematical. First, invariance: "the speed of light in vacuum is the same for all observers, no matter their relative velocity", so that light travels at "regardless of the motion of the source or the inertial reference frame of the observer". Second, unattainability: "is the upper limit for the speed at which information, matter, or energy can travel through space", and "particles with nonzero rest mass can be accelerated to approach but can never reach it". The supporting apparatus quoted in the same source is likewise mathematical: the Lorentz factor , which "diverges to infinity as approaches "; the Lorentz interval, in which spatial and temporal differences "are combined with a negative sign"; and the kinetic energy , from which the source concludes that "it would take an infinite amount of energy to accelerate an object with mass to the speed of light".
This mission isolates that mathematical core, in one spatial dimension, over the real numbers, and asks for machine-checked proofs of it. Nothing here depends on the numerical value : every statement is proved for an arbitrary parameter , which is the sense in which the source's claims are structural rather than metrological.
Fix a real constant , the invariant speed. Work in one spatial dimension, with a spatial coordinate and a time coordinate ; speeds are real numbers, and a speed is called subluminal when .
Four objects are used throughout, written in the prose exactly as in the mission's Lean development.
Relativistic velocity addition. For speeds ,
Lorentz factor. For a speed ,
Lorentz interval and Lorentz boost. The interval of an event is
and the boost of velocity sends the event to
Relativistic kinetic energy. For rest mass and speed ,
For every and every rest mass , all three of the following hold:
The three conjuncts are, in order, the invariance of light speed under a change of inertial frame, the fact that composing subluminal speeds never reaches , and the unboundedness of the energy required to approach . The goal deliberately asserts only the shape of the claims — no rate of divergence, no numerical constant — so it is not invalidated by any sharper quantitative statement a solver may prove separately.
The milestone list decomposes the goal along the four notions above: interval preservation under a boost, invariance of under composition, closure of the subluminal range under composition, divergence of at , and unboundedness of kinetic energy below .
The three conjuncts of the goal are what make a limit rather than merely a large speed. Closure of under says that no finite chain of subluminal boosts produces a luminal speed; invariance says that the boundary of that range is fixed by every boost; the energy statement says that the boundary is not approached at finite cost. Interval preservation is the geometric statement behind them: a boost is an isometry of the quadratic form , so the light cone is frame-independent.
These results are classical and have been standard since the 1905 formulation of special relativity; nothing in this mission is mathematically open. What the mission produces is the machine-checked version and a small reusable layer of one-dimensional relativistic kinematics: a search for declarations mentioning "Lorentz" in the Mathlib revision used for the drafting check returned none, so the definitions here are contributed rather than reused. The statements are stated for an arbitrary , so they can be reused at (natural units) without restatement.
The algebraic milestones are short once the right nonvanishing facts are in hand, and the obvious first attempt — clear denominators and call a ring normalizer — fails on all of them for the same reason: the denominators , , and must first be shown nonzero, and each of those facts needs the hypothesis , not merely . For velocity addition the usable identities are
whose positivity is where the strict inequality comes from.
The analytic milestone is the one that is not formal manipulation: must be shown to tend to along the punctured left neighbourhood of , which requires the inner expression to be shown positive, not merely convergent to , on a neighbourhood — the one-sided filter is essential, since takes a junk value beyond (see below).
All quantities are real; there is no vector or manifold structure, and spacetime is presented as a pair of coordinates . The invariant speed is a parameter with hypothesis ; the numerical SI value is never used. The definitions are total functions, so two junk-value conventions are fixed and must be respected when reading the statements:
No statement in the mission is vacuous: each hypothesis set is satisfiable, e.g. by , , , and the goal quantifies over all and all .
A complete development needs only Mathlib's real analysis: Real.sqrt, field-simplification and positivity reasoning, and one-sided neighbourhood filters for the divergence milestone. The definition layer (velocity addition, Lorentz factor, interval, boost, kinetic energy) is reusable beyond this mission — natural follow-ups, welcome as contributions, are the associativity and group structure of , the rapidity parametrization , time dilation and length contraction, and the composition law for boosts.
The read-backs attached to the draft items of this proposal are not blind and not independent: they were written by the same agent that drafted the Lean statements, at the explicit instruction of the proposal owner, with full sight of the source material and of the intended meaning. They should be read as an author's restatement, not as independent testimony, and they do not provide the error-catching value of an independent audit.
Missions I and II of this series showed that finite hypothesis classes are learnable, with and without the realizability assumption, by empirical risk minimization. Chapter 5 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) asks the converse question: is prior knowledge, in the form of a restricted hypothesis class, really necessary? Could there be a universal learner, an algorithm that, given enough examples from any distribution, outputs a predictor of low risk? The No-Free-Lunch theorem (Theorem 5.1) answers no: for binary classification with the 0–1 loss over a domain , for every learning algorithm and every training-set size smaller than there is a distribution on which the learner fails with probability at least , even though that distribution is perfectly predictable by some function , so that another learner (ERM over ) succeeds. The consequence for the framework is Corollary 5.2: over an infinite domain, the class of all functions is not PAC learnable. This is the first lower bound of the book and the reason the rest of it is about the complexity of hypothesis classes rather than about universal algorithms.
The framework is the UnderstandingML_Framework module of Mission I, cited as a reference. Binary classification over a domain uses examples in , hypotheses and the 0–1 loss, so the risk of under a distribution over is , computed as the integral of the 0–1 loss. A learner is a function from samples of each size to hypotheses, and a sample of size has the law . PAC learnability of a class (Definition 3.1) requires a sample-complexity function and a learner such that for every , every distribution over and every measurable labeling function realizable by , samples of size yield with probability at least .
Two conventions specific to this mission. The domain is assumed to have measurable singletons (the book's Remark 3.1 assumes away measurability issues); this makes the finitely supported distributions of the proof honest probability measures and makes every under them a genuine integral. And " smaller than " is written in the extended natural numbers, so that an infinite domain satisfies it for every .
Let be any learning algorithm for binary classification with respect to the 0–1 loss over a domain with measurable singletons, and let be a training-set size with . Then there exists a probability distribution over such that
Lemma B.1 (Appendix B). If takes values in and , then for every , , and consequently .
Equation (5.2). Under the hypotheses of Theorem 5.1 there are and a measurable with and .
Corollary 5.2. For an infinite domain with measurable singletons, the class of all functions is not PAC learnable.
Two further items: Exercise 5.1, the passage from an expectation of at least to a probability of at least of exceeding for a -valued variable; and Exercise 5.3, the -fold version of Equation (5.2), with bound when , and is nonempty.
The No-Free-Lunch theorem is the book's first impossibility result and the conceptual pivot of Part I: it shows that learnability is a property of the pair (hypothesis class, learner) and not of the learner alone, and it motivates the bias–complexity tradeoff of §5.2 and the VC-dimension of Chapter 6, whose lower bound (Theorem 6.7, the "only if" direction of the fundamental theorem) is proved by the same symmetrization argument. Corollary 5.2 is the statement that the class of all functions has infinite sample complexity, the negative half of the characterization of learnable classes.
Nothing here is machine-checked. The proof is combinatorial and elementary but has real content for a formalization: a finite subset of the domain, the labelings of , the uniform distribution on labeled by each of them, an exchange of a maximum, an average and a minimum over labelings and sample sequences, and a pairing argument on labelings that differ at exactly one unseen point. Lemma B.1 is a reverse Markov inequality for bounded variables that later chapters also use.
Lemma B.1 is Markov's inequality applied to and is the entry point; Exercise 5.1 is its instance with and , giving , together with the inclusion of in . Theorem 5.1 follows from Equation (5.2) and Exercise 5.1 once one knows that is, under the finitely supported , almost everywhere equal to a measurable function with values in ; the set is the intersection of the event with the finite support of , which is measurable because singletons are. Equation (5.2) is the heart of the mission. One picks of size (available because ), lets be uniform on labeled by the -th function extended by off , and computes as an average over the sequences of instances, which requires identifying as a finitely supported measure on sequences, that is, the product of finitely supported measures. The inequalities (5.4)–(5.6) exchange max, average and min and restrict to the unseen points, and the pairing argument shows that for each unseen point the average over of the indicator that errs on it is exactly . Exercise 5.3 is the same argument with , where at least points are unseen. Corollary 5.2 takes , , and a set of size in the infinite domain, and derives the contradiction from Theorem 5.1 via the identification of for uniform on labeled by with the true error of Definition 3.1, where is uniform on ; the case is handled separately with a single point.
The items are stated in the joint-distribution form of the book's Chapter 5, with over and the risk under the 0–1 loss, rather than in the form of Definition 3.1; Corollary 5.2 is the bridge and is stated with the framework's PACLearnable. Witness labeling functions are required to be measurable, because a non-measurable would make true by Lean's convention for non-integrable functions rather than by content. Clause (2) of Theorem 5.1 is stated in the inner form (a measurable set of probability at least inside the event) rather than as a lower bound on the outer measure of the event, which for a non-measurable event would be the weaker statement. The size condition uses ENat.card, so infinite domains satisfy it. Learners are deterministic functions of the sample; the book's argument goes through for randomized learners by averaging, but the framework does not model them.
Trivializing readings are excluded: the distribution must be a probability measure, the failing set must be measurable with an honest lower bound, and the witness must be measurable. Welcome contributions: the finitely supported product law on sequences, the averaging identity (5.3), and the pairing argument on labelings of .
Mission I of this series set up the statistical learning framework of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) and proved, in the book's Chapters 2 and 3, that finite classes are PAC learnable under the realizability assumption. Chapter 4 removes that assumption. Its idea is the one that organizes the rest of the theory: if the empirical risks of all hypotheses in are simultaneously close to their true risks , then minimizing over is nearly as good as minimizing over , whatever the distribution is. A sample with that property is called -representative (Definition 4.1), and a class for which representative samples are guaranteed at some sample size is said to have the uniform convergence property (Definition 4.3). Lemma 4.2 turns representativeness into a guarantee for ERM, Corollary 4.4 turns uniform convergence into agnostic PAC learnability, Hoeffding's inequality (Lemma 4.5) gives uniform convergence for a single hypothesis, and a union bound gives it for a finite class: Corollary 4.6, the capstone, says every finite class with a loss in is agnostic PAC learnable by ERM with sample complexity .
The framework is the UnderstandingML_Framework module of Mission I, cited here as a reference. A domain is a measurable space, hypotheses form a type with a class , and a loss is given. The risk is , the empirical risk on is , and a sample of size has the product law . A hypothesis is an ERM hypothesis for if it lies in and minimizes over ; a learner is a function from samples of each size to hypotheses, and an ERM learner returns an ERM hypothesis on every sample.
is -representative with respect to , and if for every . has the uniform convergence property with the function if for every and every distribution over , a sample of i.i.d. examples is -representative with probability at least . is agnostic PAC learnable with the function and the learner if returns hypotheses in and, for every , every and every , with probability at least over . As in Mission I, "with probability at least " is an upper bound on the outer measure of the failure event, "" is written as ", ", and sample-complexity functions are carried explicitly rather than as minimal functions.
Let be a finite hypothesis class, a domain and a loss function whose sections are measurable. Then
Lemma 4.2. If is -representative and is an ERM hypothesis for , then for every .
Corollary 4.4. If has the uniform convergence property with , then every ERM learner for is an agnostic PAC learner with the function , and is agnostic PAC learnable as soon as an ERM learner exists.
Lemma 4.5 (Hoeffding's inequality). For a probability measure , a measurable with almost surely and mean , and ,
Chapter 4 is where the book's account of learnability becomes distribution-free in the agnostic sense: nothing is assumed about beyond being a probability distribution, and the guarantee is relative to the best hypothesis in the class. Lemma 4.2 and Corollary 4.4 are the reduction that every later generalization bound in the book (VC dimension, Rademacher complexity, covering numbers, compression) plugs into: prove uniform convergence, get ERM learnability. Corollary 4.6 is the first instance, and its dependence, against the of the realizable case, is the standard illustration of the price of agnosticism. Hoeffding's inequality is stated in the form the book uses everywhere afterward, for the product law of one distribution, with an almost-sure range bound and the mean written as an integral.
Nothing here is machine-checked. Mathlib has no Hoeffding inequality for sums of i.i.d. bounded variables on a product measure in this form, so Lemma 4.5 is a genuine contribution; its proof in the book's Appendix B goes through Hoeffding's lemma on the moment generating function of a bounded centered variable and the Chernoff bounding method, both of which will be needed by the concentration results of later missions.
Lemma 4.2 is three inequalities on real numbers and is the intended entry point. Corollary 4.4 is Lemma 4.2 applied on the complement of the failure event of uniform convergence at : the failure set of the learner is contained in the failure set of representativeness, and outer measure is monotone. Hoeffding's inequality is the substantial item: one needs the moment generating function bound (Lemma B.7 of the book, by convexity of the exponential on ), independence of the coordinates under Measure.pi to factor the expectation of the product, Markov's inequality, and the optimization over ; the two tails are treated separately and added. The degenerate cases are genuine: for the bound is and the claim holds trivially, and for Lean's convention makes the bound again. Corollary 4.6 combines Hoeffding for each with a union bound over the finite class and an arithmetic step showing that gives ; the empty class makes the uniform convergence clause vacuous. The second and third clauses of the goal then follow from Corollary 4.4, the third by exhibiting an ERM learner, which exists for a nonempty finite class by choosing a minimizer of .
The four items live in the general loss framework, not the binary-classification special case, because the chapter is stated for an arbitrary loss; Mission I's IsRepresentative and HasUniformConvergenceWith already carry the chapter's definitions, so no new definition module is introduced. Losses in Corollary 4.6 are real-valued with the range condition for every and measurability of for , which is what the book's "" and Remark 3.1 give. The book's "" is stated as "the guarantee holds with the function ", the same convention as Mission I. In Corollary 4.4 the ERM clause is universal over ERM learners, matching "the ERM paradigm is a successful agnostic PAC learner" for every choice of minimizer; the existence of an ERM learner is a separate hypothesis for the learnability clause because a class with no minimizers on some sample has no ERM rule. Hoeffding's inequality is on i.i.d. coordinates of Measure.pi; the book's "" is the definition of rather than an assumption.
Trivializing readings are excluded: the failure events are bounded in outer measure, so measurability of the events is not a loophole; representativeness is required for every ; the sample-complexity functions are the book's, with ceilings. Welcome contributions: Hoeffding's lemma on bounded centered variables, the factorization of the moment generating function under Measure.pi, and a reusable union bound over a finite class.
Chapters 2 and 3 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (Cambridge University Press, 2014, doi:10.1017/CBO9781107298019), set up the framework in which the whole book asks what learning is. A learner sees a sample drawn independently from an unknown distribution over examples, chooses a hypothesis from a class fixed in advance, and is judged by its risk, the expected loss on a fresh example. The natural rule is Empirical Risk Minimization: pick a hypothesis that does best on the sample. Chapter 2 shows that ERM over an unrestricted class overfits, that restricting the class is what makes learning possible, and that a finite class never overfits once the sample is larger than (Corollary 2.3). Chapter 3 turns this into a definition, Probably Approximately Correct learnability with its sample-complexity function , restates the finite-class result as Corollary 3.2, and then generalizes in two directions that the rest of the book lives in: the agnostic model, in which no hypothesis need be perfect and the learner competes with the best hypothesis in the class, and general loss functions, which cover regression, multiclass prediction and unsupervised tasks. Chapter 4 adds the notion of an ε-representative sample and of uniform convergence, the tool by which the finite-class result extends to the agnostic case; its definitions are included here since they complete the framework.
A domain of examples, a class of hypotheses and a loss . The risk of under a distribution is and its empirical risk on is ; a sample is drawn i.i.d., ; an ERM hypothesis minimizes over ; a learning algorithm maps samples of each size to hypotheses. In binary classification the examples are with over and a labeling function, and the true error is ; the realizability assumption says some has . is PAC learnable if some sample-complexity function and algorithm guarantee, for all , all and all realizable , true error at most with probability at least from examples; agnostic PAC learnability with respect to a loss asks instead for for every distribution over .
Every finite hypothesis class is PAC learnable with sample complexity
by the ERM rule: for a nonempty finite class of measurable hypotheses there is an ERM learner satisfying the PAC guarantee with that sample-complexity function.
Corollary 2.3: under realizability, with examples, every ERM hypothesis has true error at most with probability at least .
Corollaries 2.3 and 3.2 are the first learning theorem of the book and the template for all later sample-complexity bounds: a bad hypothesis is consistent with an i.i.d. sample with probability at most , and a union bound over the class turns this into a guarantee that holds uniformly over all distributions and all realizable labelings. Everything that follows, uniform convergence for finite classes, the fundamental theorem for classes of finite VC dimension, structural risk minimization, replaces the count by a finer measure of the class's complexity but keeps the argument. None of this is machine-checked. The mission fixes on the platform the objects that the rest of the series uses without change: risks, empirical risks, the product law of a sample, the ERM relation, and the four learnability notions of Definitions 3.1, 3.4, 4.1 and 4.3.
The milestone needs that, for a fixed measurable hypothesis whose true error exceeds , the product law gives the event "zero empirical risk" probability at most ; this is the product structure of Measure.pi on the event that each labeled example lies in the measurable set where the hypothesis agrees with , followed by , the union bound over the finite class and the observation that under realizability every ERM hypothesis has zero empirical risk, so a bad ERM hypothesis is a consistent bad hypothesis. The goal packages this as a learner: existence of an ERM hypothesis for every sample (a finite nonempty class has a minimizer), and the arithmetic of the ceiling.
The framework is the book's, with the risk as a Bochner integral, the sample law as a product measure, ERM as a relation and learners as deterministic functions of the sample; failure probabilities are stated as upper bounds on the outer measure of the failure set, the strong form of "with probability at least "; the comparison with is written without an infimum. Sample-complexity functions are carried explicitly: the book's as the minimal such function is not defined, and "" is stated as "the learner satisfies the guarantee with the function ". Hypotheses and labeling functions are assumed measurable (Remark 3.1). The union bound (Lemma 2.2) is Mathlib's measure_union_le and is not an item. Hypotheses: , , finite (and nonempty for the learner to exist).
Trivializing readings are excluded: the milestone's failure event ranges over every ERM hypothesis, and the goal quantifies over all distributions, all realizable labelings and all . Welcome contributions: the product-law bound for a fixed hypothesis and the union bound over a finset, which every later mission of the series reuses.
Chapter 2 of Kearns and Vazirani, An Introduction to Computational Learning Theory (MIT Press, 1994, doi:10.7551/mitpress/3897.001.0001), gives a formal justification of Occam's Razor inside the PAC model. An Occam algorithm is judged not by the predictive power of its hypothesis but by how succinctly the hypothesis explains the sample before it: it must be consistent with the data and short, in the sense that its representation has fewer bits than the data it reproduces. The chapter's theorems say that, when the examples are drawn independently from a fixed distribution, such compression automatically yields prediction: a consistent hypothesis drawn from a small class is, with high probability, accurate on unseen examples. This turns the design of PAC learning algorithms into a combinatorial task, finding a short consistent hypothesis, and the chapter demonstrates the method three times: it shaves a logarithmic factor off the conjunction bound of Chapter 1, it learns conjunctions with few relevant variables through the greedy set-cover heuristic, and it learns Rivest's decision lists, a class strictly more expressive than -CNF and -DNF, by a greedy algorithm whose correctness is a one-line consequence of consistency.
The framework is that of Mission I: a measurable instance space, concepts as boolean functions, a target distribution , the product law of a sample of labeled examples, the error , and consistency of a hypothesis with a sample. Hypotheses may be represented by binary strings through a representation map, with size the bit length; an -Occam algorithm outputs a consistent hypothesis of size at most with . The set cover problem asks for a minimum subcollection of a collection of subsets of a finite universe that covers ; the greedy heuristic repeatedly picks the set covering the most uncovered elements. A -decision list is a sequence of conditions, each a conjunction of at most literals, with a bit attached to each and a default bit; it evaluates to the bit of the first satisfied condition. The greedy decision-list algorithm repeatedly finds a useful condition, one satisfied by some remaining examples all of which carry the same label, appends it with that label and removes those examples.
For a finite hypothesis class , a target , a distribution and , the probability that a sample of examples is consistent with some of error greater than is at most ; hence
makes this probability at most , and any algorithm that outputs a consistent hypothesis from has error greater than with probability at most .
Theorem 2.1 (an -Occam algorithm is a PAC algorithm, with explicit sample-size conditions in place of the constant ); the greedy set-cover bound of §2.3 ( and sets cover); the improved conjunction bound of §2.2; Theorem 2.3 (-decision lists are PAC learnable by the greedy algorithm, which never fails and whose outputs are consistent).
Theorem 2.2 is the single most used tool of the subject: every finite-class sample bound, including the ones for conjunctions, decision lists, -CNF and the discretized geometric classes, is an instance of it, and the Vapnik–Chervonenkis theory of Chapter 3 is its extension to infinite classes with the growth function in place of . Theorem 2.1 is the philosophical statement, that succinct explanation implies prediction, and its converse (Exercise 2.3, and more strongly the boosting theorem of Chapter 4) makes Occam learning equivalent to PAC learning. The greedy set-cover bound is Chvátal's classical approximation guarantee, used in the book for learning with few relevant variables and again in later chapters. Theorem 2.3 is Rivest's result, and its proof exhibits the pattern "consistency by construction plus a counting bound" in its purest form. None of these is machine-checked. Their formalization gives the platform the union-bound-over-a-finite-class argument once and for all, in a form that the later missions of this series reuse verbatim.
Theorem 2.2 requires that, for a fixed measurable hypothesis with error greater than , the product law gives the event "consistent with all examples" probability at most , which is the product structure of Measure.pi applied to the event that each coordinate lies in the set where agrees with ; the union bound over and the elementary inequality finish. Theorem 2.1 adds only the count of binary strings of length at most and arithmetic with real exponents. The set-cover bound is a discrete induction: an optimal cover of restricted to the uncovered elements has at most sets, so one of them, hence the greedy choice, covers a fraction; the covering clause needs the strict inequality . Theorem 2.3 needs that a run of the greedy algorithm never repeats a condition (its satisfied examples are removed), so outputs lie in an explicit finite class, that the first condition of the target list satisfied by a remaining example is useful, and that a complete run is consistent; the bound is then Theorem 2.2.
Everything is in the sample-complexity sense on the Mission I framework; running time is not modelled and "efficient" is dropped from every statement, which is recorded in the natural-language statements. Theorem 2.2's constant is with natural logarithms; Theorem 2.1's constant is replaced by three explicit sufficient conditions. Hypotheses in the finite class are required to be measurable. The greedy heuristic and the greedy decision-list algorithm are relations (any tie-breaking), and the theorems quantify over every run; the decision-list theorem is stated for every with the -conjunctions as conditions, so that its hypothesis is a -decision list rather than the expansion the book sketches for . The conjunction count is , including the empty concept that the elimination algorithm outputs on a sample without positive examples. The few-relevant-variables algorithm of §2.3 is not stated (its bound has an unspecified constant and on both sides). Hypotheses: , (and where must be nonnegative).
Trivializing readings are excluded: the bad-consistent event is over all of , the decision-list failure event ranges over every possible output, and the set-cover bound holds for every greedy run. Welcome contributions: the product-law bound for a fixed hypothesis, the union bound over a finset, the string-counting lemma, and the no-repetition lemma for greedy runs.
Chapter 1 of Kearns and Vazirani, An Introduction to Computational Learning Theory (MIT Press, 1994, doi:10.7551/mitpress/3897.001.0001), introduces Valiant's Probably Approximately Correct model, the framework for the whole book. A learner sees labeled examples of an unknown target concept drawn from an unknown but fixed distribution, and must output a hypothesis that, with probability at least over the sample, misclassifies a fresh example with probability at most ; the model is distribution-free, and the hypothesis is judged on the same distribution it was trained on. The chapter's three positive results are the templates for everything that follows. The rectangle game (Theorem 1.1) shows that an infinite class can be learned from a finite sample by exploiting the geometry of the error region. Conjunctions (Theorem 1.2) are learned by the elimination algorithm, whose analysis, a union bound over "bad" literals, is the prototype of every sample-size bound in the book. And 3-CNF formulae (Theorem 1.4) are learned by a change of variables that reduces them to conjunctions, which, set against the intractability of learning 3-term DNF as 3-term DNF (Theorem 1.3), is the reason the final definition of the model lets the hypothesis class differ from the concept class.
The instance space is a measurable space , a concept is a function , and the target distribution is a probability measure on . The error of a hypothesis is . A sample of examples is with the independent draws from ; a learning algorithm is a function from samples to hypotheses; it has the guarantee on a class if for every and every the probability that its hypothesis has error greater than is at most ; is PAC learnable using if for all some sample size and algorithm with hypotheses in achieve the guarantee. For a literal is a variable or its negation and a conjunction is a finite set of literals; the elimination algorithm starts from all literals and deletes every literal contradicted by a positive example. For the concepts are the closed axis-aligned rectangles and the tightest-fit algorithm returns the smallest rectangle containing the positive examples. A 3-CNF formula is a conjunction of clauses of at most three literals; the expansion records for each triple of literals the value .
Conjunctions of boolean literals are PAC learnable by the elimination algorithm: for every target conjunction, every distribution on and , the elimination hypothesis is consistent with every sample labeled by the target, and with
examples its error exceeds with probability at most ; hence conjunctions are PAC learnable using conjunctions.
Theorem 1.1 (rectangles by the tightest fit, ) and Theorem 1.4 (3-CNF formulae by elimination over the expanded variables, the hypothesis being itself a 3-CNF formula).
Theorem 1.2 is Valiant's original result and the first instance of the two ideas that organize the subject: a hypothesis that is more specific than the target never errs on negative examples, and the error of the hypothesis decomposes as a sum over a polynomial number of "bad" events, each of which is avoided with probability exponentially close to one. Theorem 1.1 is the first learning result for an infinite concept class and the seed of the Vapnik–Chervonenkis theory of Chapter 3. Theorem 1.4 is the first reduction between learning problems and, together with Theorem 1.3, the demonstration that the choice of hypothesis representation can separate tractable from intractable. None of these theorems is machine-checked. Formalizing them fixes, for the rest of the series, the framework in which the error of a hypothesis, the law of a sample and the learnability of a class are stated, so that the Occam, VC-dimension, boosting and noise results of later chapters can be stated on the same objects.
The elimination analysis needs that the hypothesis contains every literal of the target, that its error is at most the sum over its literals of , and that a literal with survives independent examples with probability at most ; the probabilistic content is the independence of the coordinates of the sample law, which is a product measure, and the inequality . The rectangle analysis is the four-strip argument, which for an arbitrary distribution, possibly with atoms, requires choosing the strip with the supremum of the heights at which the strip has weight at least and using the left-continuity of the weight in the height. The 3-CNF result transports the conjunction bound along the injective expansion: the pushforward of the sample law is the sample law of the expanded distribution, and the error of the composed hypothesis equals the error over the expanded variables. The deduction of PACLearnable from the explicit bounds is a choice of sample size.
The model is stated in the sample-complexity sense: algorithms are functions of the sample, and the guarantee bounds the outer measure of the failure set under the product law of the sample, which is the strong form of "with probability at least " and requires no measurability of the failure set. Running time, and hence "efficiently", is not modelled, and the hardness Theorem 1.3 is not stated; each theorem carries instead the explicit algorithm and the explicit sample bound of the book's analysis. Concepts on general instance spaces are required to be measurable in the guarantee. The cube is as functions Fin n → Bool; the expanded variables are indexed by the triples of literals, so is a Fintype.card. Rectangles are closed, possibly empty; the tightest fit of a sample without positive examples is the empty concept. Hypotheses: , ; the sample bounds are as printed, with natural logarithms.
Trivializing readings are excluded: the failure bound is uniform over all distributions and all targets in the class, consistency is asserted for every sample labeled by the target, and the learnability clause quantifies over all . Welcome contributions: the product-law bound , the union bound over literals, and the pushforward identity for the expanded sample.
The Vickrey-Clarke-Groves auction is the textbook mechanism for selling several objects at once: bidders report valuations for bundles, the auctioneer computes the welfare-maximizing allocation, and each winner pays the externality it imposes on the others. Truthful bidding is a dominant strategy and the outcome is efficient. Yet Ausubel and Milgrom (2006) catalogued its practical defects: revenue can be zero when the objects are valuable, revenue can fall when bidders or bids are added, losing bidders can profit by colluding, and a bidder can profit from false identities. Chapter 15 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) reproduces those examples and then gives the cooperative-game answer to when they cannot occur: the VCG payoff vector should lie in the core, the set of outcomes no coalition of auctioneer and bidders can improve upon, and it does so for every set of participants exactly when the coalitional value function is bidder-submodular. This mission formalizes that characterization, Theorem 15.3, together with the lemma and theorem leading to it.
Players are the auctioneer and bidders . A coalitional value function
assigns to each coalition the value it can create by trading among themselves: if the
auctioneer, who owns the objects, is not in , and otherwise the optimal value of the
auctioneer's allocation problem among the bidders of , each bidder receiving at most one
bundle and bundles disjoint (capValue). Two properties of are all the theory uses:
coalitions without the auctioneer are worthless, and adding players never lowers the value
(IsCoalitionalValue).
A payoff vector gives each player a payoff. It lies in the core of the game on a
coalition (InCore V S π) if the payoffs of sum to and no sub-coalition
is paid less than . The VCG payoff vector (vcgPayoff)
pays each bidder its marginal contribution , which is its valuation
minus its VCG payment, and the auctioneer the remainder. A core vector is bidder dominant
(BidderDominant) if every bidder weakly prefers it to every other core vector. is
bidder-submodular (BidderSubmodular) if each bidder's marginal contribution weakly
decreases as the coalition grows.
For a coalitional value function , the following are equivalent: (i) is
bidder-submodular; (ii) for every coalition the core equals
;
(iii) for every coalition , lies in the core of . This is
vcg_core_characterization.
That the combinatorial auction's is a coalitional value function; Lemma 15.1, the core is nonempty and each bidder's VCG payoff is the largest it receives at any core point; Theorem 15.2, the VCG vector is the bidder-dominant core point when it is in the core, and otherwise no bidder-dominant point exists and the auctioneer's VCG payoff is below every core payoff.
The English auction of Sect. 15.2, presented as a primal-dual interpretation of a linear program, and the combinatorial allocation problem of Sect. 15.3 carry no numbered results and are not targets.
Theorem 15.3 is the criterion an auction designer can check before running a VCG auction: when the bidders' valuations make bidder-submodular (for instance when objects are substitutes), the VCG outcome is a competitive outcome, its revenue meets the core benchmark, and none of the defects of Sect. 15.4.2 can arise; when they do not, Theorem 15.2 says the auctioneer's revenue is strictly below every competitive outcome. The result underlies the ascending package auctions proposed as VCG alternatives and the procurement auctions used in supply chains, such as the combinatorial reverse auctions of the chapter's case study.
None of these results has a machine-checked proof. The book proves all three. The formal treatment of the core and of marginal-contribution vectors is reusable for the cooperative-game models of cost allocation in supply chains.
The theorems are combinatorial statements about a function on finite sets, and the difficulty is entirely in the bookkeeping of coalitions. Lemma 15.1 needs the explicit core vector of its proof to be verified against every sub-coalition, which splits into cases on whether the sub-coalition contains the auctioneer and the distinguished bidder. The implication (i) (ii) telescopes marginal contributions along a chain of coalitions between a sub-coalition and , and the chain has to be built and its sum computed. The implication (iii) (i) is the delicate one: a failure of submodularity is a pair of nested coalitions, and the proof needs to extract from it a single-element step at which a bidder's marginal contribution increases, then show the two-bidder sub-coalition blocks the VCG vector. The obvious idea, that submodularity can be checked only on single-element extensions, is correct but must itself be proved.
Coalitions are finite sets of Fin (n+1) and payoff vectors are functions on all players; the
core and constrain only the players of , so vectors differing outside are
interchangeable. The core's budget equation sums over all players of the coalition, including
the auctioneer, which is what the book's proofs use although its displayed definition sums over
the bidders. The theorems take as any function with the two properties, and the auction's
is shown to have them; the VCG vector is defined by the formulas (15.23) and (15.24) rather
than through the payment rule, whose equivalence is the book's derivation. Bidder-submodularity
is stated for rather than proper inclusion, which changes nothing.
The definition module is shared by all five items. The single-item English auction as a primal-dual algorithm and the condition on individual preferences (substitutes) that implies bidder-submodularity are natural extensions on the same definitions.
Revenue management is practised by firms that compete: airlines matching fares while allocating seats, retailers ordering stock and then pricing to clear it, hotels protecting rooms for late high-paying guests. Chapter 8 of Talluri and van Ryzin's The Theory and Practice of Revenue Management (2004) surveys the economics behind these situations: monopoly pricing and mechanism design, the Coase problem, advance-purchase discounts, and oligopoly in quantities (Cournot), in prices (Bertrand, Bertrand–Edgeworth with capacities), in newsvendor capacities and in RM allocations. Most of its numbered results are quoted from the literature; what the book itself establishes is a family of equilibrium arguments built on Talluri's equilibrium graph: when each firm's best response moves monotonically with the rival's action, following best-response arcs must end in an equilibrium pair. This mission formalizes those arguments, with Proposition 8.3, existence of an equilibrium in offer sets under the multinomial-logit choice model, as the goal.
A two-firm game on finite chains of strategies has payoffs , best responses and
pure Nash equilibria (IsBestResponse1, IsNashEquilibrium); its equilibrium graph has
no crossing arcs (NoCrossing1) when best-response arcs , with
always have . The chapter's games are: the RM duopoly of Sect.
8.4.1.3, two firms with capacity and fares whose high-fare demand spills over
to the rival beyond its protection level (spilloverDemand), each firm answering with
Littlewood's protection level (littlewoodResponse); the duopoly newsvendor of Example
8.16 with effective demands (effectiveDemand); linear Cournot
(cournotPayoff); Bertrand–Edgeworth price competition with capacity per firm, linear
demand and efficient rationing (beSales, bePayoff, IsBEEquilibrium); the advance-purchase
model of Sect. 8.3.6 (peakLoadRevenue, advancePurchaseRevenue); and the one-period
offer-set game of Sect. 8.4.3.2, where a firm offering its first products earns
with
(OfferFirm, offerPayoff1, CaseI, CaseII).
If both firms are in Case I () or both in Case II ( on every complete
set), the offer-set game has a pure-strategy equilibrium in complete sets:
mnl_offer_set_equilibrium.
The equilibrium-graph lemma, monotone best responses for both firms give an equilibrium (Sect. 8.4.1.3); Proposition 8.1, Littlewood responses in the RM duopoly are monotone in the rival's protection level, and the resulting equilibrium of the RM duopoly game; Example 8.16, duopoly newsvendor capacities total at least the monopoly capacity; Example 8.15, the symmetric Cournot equilibrium and its price; Theorem 8.5 (i)-(ii), the pure-strategy Bertrand–Edgeworth equilibria; and the advance-purchase comparison of Sect. 8.3.6, and .
Not targets: Theorems 8.1-8.2 (the Coase problem, subgame-perfect equilibria of an infinite-horizon game, proofs in von der Fehr and Kühn), Theorem 8.3 (Harris–Raviv priority pricing, stated with a garbled price formula), Theorem 8.4 (existence via quasiconcavity, cited), Theorem 8.5 (iii), 8.6 and 8.7-8.8 (mixed-strategy and supergame equilibria of Kreps and Scheinkman and Benoit and Krishna), Proposition 8.2 and Proposition 8.4 (the dynamic offer-set game under condition (8.32), proved in Talluri's paper), and the Kreps–Scheinkman derivation of Sect. 8.4.1.6, which rests on Theorem 8.6.
The equilibrium graph is the chapter's own contribution: a bipartite picture of best responses on chains in which monotonicity, the absence of crossing arcs, forces an equilibrium. It is the finite, combinatorial form of the monotone comparative-statics route to Nash equilibrium (Tarski's fixed point on a chain), and it is what makes RM allocation games tractable: the two-class duopoly with Littlewood responses always has an equilibrium, and the offer-set duopoly does whenever the two firms face the same sign of , while Example 8.18 shows a best-response cycle when they do not. The Bertrand–Edgeworth, Cournot and newsvendor results are the benchmarks the book uses to interpret RM competition: capacity constraints soften Bertrand's zero-profit outcome, competing in allocations tends to raise total capacity above the monopoly level, and advance-purchase discounts dominate peak-load pricing as a self-selection mechanism. None of these has a machine-checked proof.
The lemma and the goal are fixed-point arguments on finite chains: the largest best response is a monotone map of the rival's index, the composition of two monotone (or two antitone) maps on a finite chain has a fixed point, and for the offer-set game the monotonicity itself must be extracted from the ratio structure as in the appendix's inequalities (8.A.3)-(8.A.5), separately in the two cases. Proposition 8.1 is a monotonicity of tail probabilities under the pointwise order of effective demands. Example 8.16 is a short probabilistic argument that needs the identity and the strict monotonicity of the tail. Theorem 8.5 requires computing efficient-rationing sales for every unilateral deviation from a symmetric profile, through the recursive definition of residual demand, and a quadratic inequality for upward deviations in part (ii). The advance-purchase item reduces to the identity and the strict decrease of the first-order-condition function.
Products, protection levels and complete sets are natural numbers; the offer-set game's strategies are the complete sets of the book, and its payoff is (8.31) up to the positive factor and the terms independent of both offer sets. Prices decreasing in the product index are a hypothesis, as the nested-by-revenue order of Sect. 8.4.3.2. The RM duopoly is modeled through Littlewood's response, as the book's appendix argues, rather than through expected revenues. Efficient rationing is defined recursively over the firms priced strictly below a given firm, with equal sharing among firms at the same price. Example 8.16 is stated with the equilibrium conditions (8.23) and the strictly increasing distribution of aggregate demand as hypotheses. The advance-purchase item takes the first-order conditions (8.13) and (8.15) and the book's uniqueness assumption as hypotheses, the latter as strictly decreasing in (the page prints "increasing", but its footnote identifies it with the monotone marginal-revenue assumption, which is decreasing in the waiting cost). Theorem 8.5 is stated for its pure-strategy parts (i) and (ii) only.
The vehicle routing problem asks for the cheapest set of delivery routes from a depot to a set of customers when each vehicle can carry only so much. It generalizes the traveling salesman problem, which is the case of a single vehicle of unlimited capacity, and it is the operational problem behind every distribution fleet. Exact methods reach a few hundred customers; the questions that shape fleet design are structural: how does the optimal routing cost compare with the cost of a single grand tour, and how does it grow with the number of customers? Haimovich and Rinnooy Kan (1985) answered both for unit demands by bounding the optimal cost above and below in terms of the optimal TSP tour and the average distance to the depot. Chapter 11 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) presents that result with its full proof as Theorem 11.6, and it is the goal of this mission.
Nodes are the depot and customers , with distances that are symmetric,
nonnegative and satisfy the triangle inequality (VRPMetric). Every customer has demand and
every vehicle capacity , so a route is a sequence of at most distinct customers,
served by one vehicle that leaves the depot, visits them in order and returns; its length is
routeCost c L. A solution is a family of routes visiting every customer exactly once
(IsVRPSolution), with total length solutionCost; the number of routes is free. The
optimal VRP value (vrpOpt c C) is the least total length, the optimal TSP value
(tspOpt c) is the least length of a single route through all customers, and
(avgDepotDist) is the average distance from the depot to a customer.
For every metric instance with customers and capacity ,
This is vrp_tsp_bounds.
The three steps of the book's proof: the radial bound , obtained route by route from the triangle inequality and the capacity; the routing bound ; and the iterated optimal tour partition bound (11.59), that for any tour through all customers some partition of its customer sequence into consecutive routes costs at most .
The chapter's other numbered results are not targets: Proposition 11.1 (state-space relaxation of the routing dynamic program) and Theorem 11.2 (the capacitated comb inequality, proof omitted, which needs the bin-packing function ), and Theorems 11.3, 11.5, 11.7 and Lemma 11.4 (almost-sure asymptotics of random instances and the location-based heuristic), whose proofs the book cites.
Theorem 11.6 is the quantitative link between routing and the two things a planner can estimate without solving anything: the TSP length, which grows like for random customers, and the average depot distance. It says that the VRP cost is the TSP cost plus a radial term per vehicle, and that this decomposition is exact up to a factor bounded by the capacity. The radial term explains Theorem 11.7, that the optimal cost grows linearly in for fixed capacity, and the tour partition heuristic in the proof is a practical route-first-cluster-second method with a provable guarantee. The bounds are the basis of the continuous approximation formulas used in strategic distribution design.
None of these results has a machine-checked proof. The book proves Theorem 11.6 in full. The formal treatment of routes as lists and of the averaging argument over rotations of a tour is reusable for the capacitated heuristics of Sect. 11.3.
The upper bound is an averaging argument that is easy to state and fiddly to formalize: for each of the rotations of the tour's customer sequence, the sequence is cut into blocks of , and one must count, across all rotations, how often each customer is the first or last of a block and how often each tour edge is cut. The counts, each, hold only after the rotations are indexed carefully, and the passage from the average to the best rotation needs the sum of the solution costs computed exactly.
The lower bound has two parts with different flavors. The radial part needs, for each route, that the closed route from the depot is at least twice the largest depot distance among its customers, which is the triangle inequality applied along the route, followed by an averaging step that uses the capacity. The routing part is a shortcutting argument: the routes of a solution concatenate into a closed walk that revisits the depot, and removing the repeated depot visits must not increase the length. The obvious idea, that a VRP solution is itself a tour, is false, and the shortcut has to be constructed.
Routes are lists of customers, solutions are lists of routes, and the feasibility predicate
requires nonempty routes of length at most avoiding the depot, with the concatenation of
all routes a duplicate-free list containing every customer. Costs use the closed walk through
the depot followed by the route. The optimal values are infima of finite nonempty sets of reals,
nonempty because singleton routes are feasible when . The ceiling is
Mathlib's Nat.ceil of the real quotient. The number of vehicles is unrestricted, as the
section assumes; the fixed-fleet version of the problem is not modeled.
The TSP value is defined as the least route cost over all orderings of the customers, so no separate tour model is needed and the mission does not depend on the TSP mission of this series.
The definition module is shared by all five items. Problem 11.18 (tightness of both bounds) and Theorem 11.7 for deterministic instance families are natural extensions on the same definitions.
A salesman must visit cities and return home by the shortest route. The traveling salesman problem is the prototype of combinatorial optimization: easy to state, NP-hard (Karp 1972), and solved to optimality on instances with tens of thousands of nodes by branch-and-cut. In a supply chain it is the core of every vehicle routing model and of the location-routing models of the chapters that follow. Chapter 10 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) covers the symmetric metric TSP, in which distances satisfy the triangle inequality: the cutting planes of branch-and-cut (comb inequalities), the construction heuristics with their worst-case guarantees, culminating in Christofides' (1976) 3/2-approximation, and the lower bounds of Little et al. and of Held and Karp (1970). This mission formalizes those results, with Christofides' theorem as its goal.
Nodes are with distances that are symmetric, nonnegative, zero on
the diagonal and satisfy the triangle inequality (IsMetric). A
tour is a visiting order of all the nodes, of length
with indices mod (tourLength); is the least tour length (optTourLength). A tour has
an edge set (tourEdges), and for a node set the counts of tour edges inside and leaving
(edgesWithin, edgesLeaving) are the sums and
of the integer programming formulation. A comb is a handle with an odd number of
pairwise disjoint teeth, each meeting both and its complement (IsComb); when every tooth
has exactly two nodes the comb is a 2-matching configuration.
The nearest neighbor heuristic always moves to a nearest unvisited node
(IsNearestNeighborTour); the nearest insertion heuristic grows a partial tour by inserting
the unvisited node nearest to it at the cheapest position (IsNearestInsertionRun, with
cycleLength and distToTour). The minimum spanning tree heuristic doubles an MST
(IsMST, graphWeight), takes an Eulerian tour of the doubled tree and shortcuts it,
visiting the nodes in order of first appearance (IsShortcut). Christofides' heuristic
instead adds to the MST a minimum-weight perfect matching on its odd-degree nodes
(oddNodes, IsMinMatchingOn) before taking the Eulerian tour. A 1-tree rooted at is a
spanning tree on the other nodes plus two edges at (Is1Tree); the revised distances
(revisedCost) define the Held-Karp bound.
For every metric instance, every minimum spanning tree , every minimum-weight perfect matching on the odd-degree nodes of , every Eulerian tour of and its shortcut ,
This is christofides_bound.
Theorem 10.1, the reduced-matrix bound ; Theorem 10.2, Proposition 10.3 and Theorem 10.4, the 2-matching and comb inequalities valid for every tour; Theorem 10.6, ; Theorem 10.7, ; Lemma 10.9, ; Theorem 10.10, Euler's theorem; Theorem 10.11, ; Lemma 10.12, the handshaking lemma; Lemma 10.15, the 1-tree bound; Lemma 10.16, the revised distance identities; Theorem 10.17, the Held-Karp bound. Theorem 10.5 (no constant-factor approximation unless P = NP), Theorem 10.8 and the second part of Theorem 10.6 (tightness instances), Lemma 10.14 (Euclidean tours do not cross), Lemma 10.18 (the integrality gap) and Theorem 10.19 (the Beardwood-Halton-Hammersley asymptotics) are not targets.
Christofides' bound was the best approximation guarantee for the metric TSP for over forty years, until the of Karlin, Klein and Oveis Gharan (2021), and it is the reference point against which every heuristic in the chapter is measured: nearest neighbor has no constant bound, nearest insertion and the MST heuristic achieve , Christofides . The comb inequalities are the cuts that make branch-and-cut work, and the Held-Karp bound is the lower bound that tells a practitioner how far a heuristic tour is from optimal. Theorem 10.1 is the historical bounding rule of the first branch-and-bound algorithm.
None of these results has a machine-checked proof. The book proves Theorems 10.2, 10.11, 10.13 and 10.17 and Proposition 10.3 and Lemma 10.9, cites Theorems 10.6, 10.7 and 10.10, and leaves Theorem 10.4 and Lemmas 10.12 and 10.16 as exercises. The formal infrastructure for tours, shortcutting and Eulerian walks is reusable for the vehicle routing chapter.
Christofides' argument has three steps and each has a formal obstacle. The MST bound is a spanning-path argument that needs the removal of an edge from a tour to yield a tree, in Mathlib's terms a connected acyclic subgraph of the complete graph. The matching bound is the subtle one: the optimal tour shortcut to the odd-degree nodes, of length at most by the triangle inequality, is an even cycle whose alternate edges form two perfect matchings on those nodes, the cheaper of which costs at most ; formalizing the decomposition of a cycle on an even node set into two matchings, and the shortcut's length bound, is the bulk of the work. The final step, that shortcutting an Eulerian walk does not lengthen it, is an induction along the walk using the triangle inequality on the skipped stretches, and it needs the first-occurrence order to be handled explicitly.
The obvious approach to the heuristic bounds, comparing the heuristic tour directly with the optimal tour, fails; every proof goes through a spanning tree. For nearest insertion the tree is Prim's, grown in the same order as the insertions, and the bound charges each insertion cost to a tree edge; for nearest neighbor the argument of Rosenkrantz et al. bounds the sum of the largest steps by for each and sums a geometric series, which is where the logarithm comes from.
The comb inequalities are counting arguments on degrees, but the general comb of Theorem 10.4 needs the case analysis of how a tour enters and leaves each tooth. Euler's theorem in the sufficiency direction is Hierholzer's construction, which is not in Mathlib.
Tours are permutations of Fin n, so a tour is an ordering rather than an edge set, and every
tie-breaking of a heuristic is covered by a predicate on its output rather than by an algorithm.
Graphs are Mathlib SimpleGraphs on Fin n; the multigraphs of the two tree heuristics are
represented by closed walks with prescribed edge multisets, and shortcutting is the
first-occurrence order along the walk's node sequence. All degree and edge-set computations use
classical decidability. Theorems on tours assume where a tour must have distinct
edges, otherwise.
Theorem 10.1 is stated for the reduction of the full off-diagonal matrix, because the book's upper-triangular version is false: a random metric instance violates it, since the last row and first column of a triangular matrix are empty and the two edges at a node need not be one row and one column entry. The full-matrix version is the statement of Little et al. It is stated for , because a one-node "tour" is a self-loop that no off-diagonal entry constrains.
Theorem 10.4 is stated with the comb inequality's right-hand side corrected to , the standard form. The book prints , which contradicts its own 2-matching special case (10.15) and is weaker by . The corrected statement implies the printed one.
The -tree root is an explicit node , the book's node . The nearest insertion run is a sequence of lists indexed by iteration, and the theorem compares the -th list's closed length with ; a run always exists, so the hypothesis is satisfiable.
The definition module is shared by all fifteen items. Theorem 10.8 and Problem 10.12 (tightness of the bounds of ), the second part of Theorem 10.6, and Lemma 10.18 on the integrality gap are natural extensions on the same definitions.