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?
Moment-angle complexes are central objects in toric topology. They convert the combinatorics of a simplicial complex into a topological space assembled from disks and circles, allowing face structure to influence homotopy and homology. When the simplicial complex triangulates a sphere, the resulting space is a moment-angle manifold. Torsion in the integral homology of these manifolds is difficult to realize in low simplicial dimension, and torsion in the homology of their based loop spaces is even more constrained. Yang Han and Keke Li's Theorem 1.7 asserts that dimension four is already universal: every finitely generated abelian group can occur as a subgroup of both homology theories for one and the same simplicial -sphere.
This mission formalizes that headline existence statement. It is not restricted to a chosen finite list of groups or primes, and it requires a common simplicial sphere rather than permitting separate witnesses for ordinary and loop homology.
Let be an abstract simplicial complex on a finite vertex set . Its geometric realization is formed from probability vectors whose supports are faces of . The condition that is a simplicial -sphere means that this realization is homeomorphic to the unit sphere .
For each face , assign a copy of the closed disk at vertices in and the boundary circle at vertices outside . The associated moment-angle complex is
The all-ones point is a canonical basepoint. Write for the based loop space with the compact-open topology. For a space , the mission uses total integral singular homology
as an additive abelian group. Saying that an abelian group is a subgroup means that there is an injective additive homomorphism .
For every finitely generated abelian group , prove that there are an integer and a simplicial complex on Fin m such that and there are injective homomorphisms
The quantifier order matters: the same and the same must support both embeddings. The target concerns additive subgroups of total graded homology; it does not require the two embeddings to land in the same degree or to preserve multiplicative structures.
The theorem gives a universality statement for moment-angle manifolds over simplicial -spheres. It says that no classification by a bounded list of torsion primes or exponents can describe all such homology and loop-homology groups. Requiring both embeddings for a single connects the ordinary topology of the manifold to its based-loop topology rather than proving two unrelated existence results.
Formalizing the theorem requires reusable foundations in several areas: finite abstract simplicial complexes, geometric realization, polyhedral products, based loop spaces, integral singular homology, graded direct sums, and additive embeddings. The published article presents a human proof; this mission records its intended main theorem as an open Lean target. The definitions do not assume the existence of the required sphere or embeddings, so a solver must supply the mathematical construction and all homological consequences.
The assertion ranges over arbitrary finitely generated abelian groups, including free parts and prime-power torsion of unbounded exponent. A finite check of selected groups cannot establish the target. The same finite simplicial object must simultaneously control two different homology theories, one of which is applied to an infinite-dimensional function space. Standard library support is strongest for singular homology as a functor, while concrete calculations for moment-angle spaces and loop spaces require additional bridges.
There is also a substantial representation boundary between combinatorics and topology. The face data of , the union of disk-circle products, the homeomorphism , and the induced maps on homology must all refer to compatible spaces and basepoints. A formal solution cannot replace “simplicial sphere” by a mere Boolean flag or replace homology by an arbitrary group-valued field.
Lean represents using AbstractSimplicialComplex (Fin m). Because Mathlib's structure includes singleton faces automatically, the auxiliary face predicate explicitly restores the conventional empty face where the moment-angle union needs it. The geometric realization is the standard support-restricted probability simplex, and the sphere condition is an actual homeomorphism to the Euclidean unit -sphere.
The moment-angle space is a subtype of (Fin m → ℂ) defined by the literal disk/circle coordinate condition. The loop space consists of based continuous paths with matching endpoints and carries the compact-open topology inherited from Mathlib's path construction. Homology is singularHomologyFunctor with coefficients in , and total homology is a direct sum over all natural degrees.
The statement permits the two embeddings to occupy different degrees and makes no ring-embedding claim; these choices match the source phrase “contain as a subgroup.” It rules out vacuity by requiring an actual simplicial complex, an actual sphere homeomorphism, and injective additive maps. Contributions that isolate degree-specific refinements, compute homology of standard polyhedral products, or formalize reusable loop-space equivalences are welcome, provided they reconnect to the stated root theorem.
For many natural chains, convergence to stationarity is not gradual: the distance stays near its maximum for a long time and then collapses to zero in a comparatively negligible window. A deck of cards under riffle shuffles is "not at all mixed" for six shuffles and "essentially mixed" after eight. This abrupt transition is the cutoff phenomenon, discovered by Aldous and Diaconis in the 1980s, and Chapter 18 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) develops its theory: precise definitions of cutoff and cutoff windows, the product criterion necessary for cutoff, and complete proofs for two model families — the biased walk on a segment and the lazy hypercube walk, the latter with the sharp location and window , in both total variation and separation. Chapter 19 complements this with lamplighter walks: chains on the wreath-product state space of lamp configurations over a moving lamplighter, whose relaxation, mixing, and separation times are governed — beautifully — by the hitting and cover times of Missions VI. Both chapters are formalized in this mission.
A family of chains is a sequence on state spaces with stationary distributions ; all single-chain quantities acquire an index . As before, , , , and . The family has a cutoff when for every
and a cutoff at with window when and the distance at time tends (in the appropriate limsup/liminf sense) to as and to as . The separation distance from is (Mission III), , and a separation cutoff is defined by the same window template with in place of . From Mission VII, is the relaxation time; from Mission VI, and are the maximal hitting and cover times, and the pairwise distance is from Mission II.
The concrete chains: the lazy biased walk on holds with probability and otherwise steps up with probability , down with probability (reflecting at the endpoints); the lazy hypercube walk is the walk of Mission IV on . The lamplighter chain over a graph has states (lamp configuration in , lamplighter position in ); one step randomizes the current lamp, moves the lamplighter one step of the lazy walk on , and randomizes the new lamp. Its stationary distribution is uniform lamps times the walk's stationary distribution.
Theorem 18.3: the lazy hypercube walk has a cutoff at with window — the family's total variation distance undergoes its full collapse in a window of size around .
The results. Cutoff is the deepest phenomenon in the quantitative theory of Markov chains: it says mixing is a phase transition in time. The hypercube is the fundamental example where everything can be computed — the eigenvalue structure of Mission VII delivers the upper bound and a refined distinguishing-statistic argument (Mission IV) the lower — and the location with window is the sharpest statement of the coupon-collector heuristic. The product condition 18.4 is the basic sanity criterion in the ongoing research program of characterizing cutoff. The lamplighter theorems tie together the entire series: hitting times (Mission VI), cover times (Mission VI), relaxation times (Mission VII), and separation (Missions III, XI) all meet in one family of chains that furnishes counterexamples — for instance, families with total-variation cutoff but no separation cutoff.
Formalizing them. Nothing about cutoff exists in any proof assistant. The definitions themselves (families of chains, windows, limsup/liminf in a real parameter) are a formalization contribution: they force precision about quantifier order that informal texts elide. The hypercube cutoff is a landmark target — a sharp two-sided asymptotic statement, not an inequality.
The upper half of the hypercube cutoff needs the full eigenvalue decomposition of the walk ( with multiplicity , via Mission VII's spectral representation) and the bound summed over binomial coefficients; the lower half needs the Hamming-weight distinguishing statistic pushed to second-order precision (mean and variance at time ). Proposition 18.4 converts an eigenfunction with eigenvalue near into a quantitative anti-concentration statement — the formal content of "a bounded ratio forbids abrupt collapse". Theorem 18.2 rests on a central-limit-flavoured estimate for the biased walk's position, done with fourth-moment bounds rather than the CLT. The lamplighter theorems are the heaviest: the upper bounds couple lamp refreshment with the cover-time of the base walk, the lower bounds run separation-distance and eigenfunction arguments, and all four inequalities must hold with universal constants over an arbitrary growing graph family — the statements quantify over the family, so the proofs must too. The asymptotic language throughout (liminf/limsup over , limits in the window parameter ) exercises the filter library in earnest.
Families are dependent functions ∀ n, Matrix (V n) (V n) ℝ over a sequence of finite state-space types. Cutoff and windows are rendered exactly by the book's Eq. (18.3) and §18.1: the window definition uses Filter.liminf/limsup over composed with limits in the real parameter (through ⌊t n + α w n⌋₊, with the natural-floor convention on negative reals). The mixing-time ratio in the cutoff definition uses real division of the natural-valued mixing times (total division: the hypotheses keep denominators eventually positive). The biased walk's stationary distribution is passed as a hypothesis rather than a closed form. In the lamplighter theorems the comparability constants and the threshold are existentially quantified, with the graph family and its connectivity as hypotheses; the lamplighter matrix and its product stationary distribution are explicit definitions. Lemma 19.3 is stated for a single reversible chain at all times .
Every mixing bound in Missions II–IX ultimately leaned on either coupling or the spectrum, and the spectral route demanded reversibility. Chapter 17 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) opens a third route: martingales — processes whose conditional expected increment vanishes — and the beautiful evolving-set process of Morris and Peres built from them. The payoff theorem of the chapter bounds the mixing time of any lazy irreducible chain by its bottleneck constant, with no reversibility hypothesis anywhere — an honest strengthening of the spectral route through the Cheeger inequality, whose proof is a martingale analysis of a random sequence of sets growing and shrinking under the chain's flow. The same chapter proves the optional stopping theorem in the exact discrete form the rest of the series consumes, and applies the machinery to sharp return-probability estimates for lazy walks.
Throughout, is a chain on a finite state space with stationary distribution ; , , and as in the earlier missions; . The chain is lazy when at every state.
A martingale adapted to the chain is a family of functions of the trajectory up to time such that the conditional expectation of , given the trajectory so far, equals — for a finite chain, a pointwise finite-sum identity. A stopping time is a -valued stopping rule in the sense of Mission III: whether to stop at time depends only on the trajectory up to .
From Mission IV: the edge measure is , with , and the bottleneck constant is the minimum over sets with of . The evolving-set process is the Markov chain on subsets of in which, from the current set , one draws uniform on and passes to the superlevel set
— states currently receiving a large share of the flow out of are likely to join, states receiving little are likely to leave.
Theorem 17.10 (Morris–Peres), the capstone of Chapter 17: for any lazy irreducible chain — reversibility not assumed —
The results. The optional stopping theorem is the workhorse identity of discrete probability — the earlier missions' gambler's-ruin and hitting-time computations are all instances, and Missions XI–XII cite it again. The Morris–Peres theorem is the strongest known elementary relation between geometry and mixing: for reversible chains it recovers the Cheeger-based bound of Mission VII, but it needs no reversibility, and its proof technique — controlling the root as a supermartingale — introduced evolving sets as a tool that has since produced heat-kernel decay, isoperimetric mixing profiles, and bounds for non-reversible and time-inhomogeneous chains well beyond the book.
Formalizing them. Mathlib's martingale library lives in measure-theoretic generality; this mission's chain-adapted martingales are self-contained finite objects (families of functions on trajectory spaces), so the optional stopping theorem here is independent of, and complementary to, the measure-theoretic one. Evolving sets exist in no proof assistant; the process is a genuinely novel formalization target — a Markov chain whose states are Finsets, defined through interval lengths of a uniform variable.
The optional stopping theorem needs the dominated-convergence step (bounded martingale, a.s. finite time) rendered as an elementary tail estimate — the series must be shown summable and equal to by an exchange of finite sums with a limit. The evolving-set transition probabilities are interval lengths: the probability of passing from to is the length of the set of whose superlevel set is exactly , which the formalization encodes by explicit upper and lower thresholds (a min over and a max over of the clipped ratios ); establishing that these lengths sum to one over , and that the process has the two martingale properties, is delicate finite-order-statistics reasoning. The goal theorem then runs a supermartingale argument on : laziness keeps the thresholds in , an expansion estimate converts the bottleneck constant into a per-step multiplicative decay of , and Lemma 17.12 converts that decay into a total-variation bound. Theorem 17.17 composes the same machinery with a Cauchy–Schwarz step. None of this exists in any library; the auxiliary supermartingale lemmas are welcome as separate contributions.
Martingales, stopping times, and stopped expectations are the trajectory-calculus objects of Missions I and III: finite sums over paths weighted by , with expectations over the stopping time as tsums in (non-summable families sum to ; the a.s.-finiteness hypothesis is the statement that the stopping mass sums to ). The evolving-set matrix is defined by the clipped-threshold formula described above — an explicit real matrix on Finset V — and the goal and lemmas assume positive and lazy exactly where the book does. Theorem 17.17 is stated for the lazy walk on a connected graph with positive degrees, with written out. Real-valued bounds on the natural-valued are direct inequalities on the cast, with no hidden rounding.
The Ising model is statistical mechanics' fruit fly: spins on the vertices of a graph, neighbours preferring to agree, a single parameter — the inverse temperature — tuning the strength of that preference. Chapter 15 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) studies the Glauber dynamics for this model and exhibits, on concrete graphs, the phenomenon that made mixing times a subject: a dynamical phase transition. At high temperature (small ) the dynamics mixes in steps on any bounded-degree graph; on the complete graph the same dynamics passes, as crosses an explicit threshold, from mixing to exponentially slow mixing. The chapter also introduces two comparison tools of independent value — the sensitivity of the spectral gap to edge removal, and the block dynamics comparison — and the Kenyon–Mossel–Peres bound for trees, all formalized in this mission.
Spin configurations on a finite graph with vertex set of size and maximum degree are functions assigning to each vertex (encoded over Booleans, ). The Ising model at inverse temperature is the Gibbs distribution
each edge counted once, the normalizing partition function. The Glauber dynamics for picks a uniform vertex and re-samples its spin from conditioned on all other spins — concretely, the new spin at is with probability where is the sum of the neighbouring spins.
The yardsticks are as in the earlier missions: is the total variation distance, , and . From Mission VII: an eigenvalue of a chain is a real with for some nonzero ; is the largest eigenvalue , the spectral gap is , the largest over eigenvalues , and the relaxation time is .
Theorem 15.1, the high-temperature fast-mixing theorem: if then the Glauber dynamics on any graph satisfies
together with its refinement for graphs with all degrees even, where the condition relaxes to .
The results. Theorem 15.1 is the standard fast-mixing criterion for Glauber dynamics, and the model application of the path-coupling technique of Mission VIII. Theorem 15.3 exhibits, in the cleanest possible setting, the correspondence between the static phase transition of the mean-field Ising model and the dynamical transition of its Glauber dynamics — the phenomenon at the heart of Markov-chain approaches to statistical physics. The tree bound of Kenyon–Mossel–Peres and the block-dynamics comparison are the standard tools for spatially structured spin systems; block dynamics in particular is the engine of recursive gap bounds on trees and lattices.
Formalizing them. Nothing about the Ising model, Gibbs distributions, or Glauber dynamics exists in Mathlib. The Gibbs-distribution layer (weights, partition functions, conditional single-site laws with their closed forms) is foundational for any future formalization of statistical mechanics; the phase-transition theorem 15.3(ii) would be, to our knowledge, the first formalized instance of exponentially slow mixing driven by an energy barrier.
The high-temperature theorem is path coupling (Mission VIII) plus the tanh lemma: the one-site coupling of two adjacent configurations contracts the Hamming metric at rate , and every analytic input is in Lemma 15.2 — which is why that elementary lemma is a milestone of its own. The slow-mixing half of Theorem 15.3 runs through the bottleneck bound of Mission IV: the magnetization performs a one-dimensional walk in a double-well free-energy landscape, and the bottleneck at zero magnetization has exponentially small stationary mass — a large-deviations estimate carried out with binomial coefficients. The cycle's lower bound needs Wilson's method (Mission VII) with an explicit eigenfunction. The tree and block theorems are exercises in the comparison technology of Mission VII (Dirichlet forms, canonical paths through block updates); their constants are crude but the inductive structure is delicate. Everything sits on the subtlety that the state space has size , so all "polynomial" bounds are polynomial in , not in the size of the state space.
The Gibbs distribution is defined by explicit finite sums (weight over partition function, total division); no positivity side conditions are needed since the weights are exponentials. The Glauber dynamics is the generic single-site heat bath of Mission II applied to the Ising distribution, so the closed form is a provable lemma, not a definition. Asymptotic statements (, "for sufficiently large ") are rendered with explicit quantifiers and a free precision parameter ; the phase-transition constants are existentially quantified. The tree is encoded as words of length over an alphabet of size ; the block dynamics re-samples a uniformly chosen block from the conditional Gibbs distribution, with the convention that a conditioning of zero mass yields a zero row (total division), which the theorems' hypotheses exclude on the support. The even-degree refinement of the goal is stated as a second conjunct with its own hypothesis.
How many shuffles does a deck of cards need? The question created the modern theory of mixing times: Diaconis and Shahshahani's analysis of random transpositions (1981) and the Bayer–Diaconis "seven shuffles suffice" analysis of the riffle shuffle (1992) are its founding results. Chapters 8 and 16 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) treat the four standard shuffles: random transpositions (pick two cards, swap them), the riffle shuffle (cut and interleave, the Gilbert–Shannon–Reeds model), random adjacent transpositions, and the -reversal chain of segment reversals — the last motivated by genome rearrangement, where a chromosome evolves by reversing segments and the mixing time measures evolutionary distance ("from shuffling cards to shuffling genes").
All four chains are random walks on a symmetric group; decks are encoded as in Mission III, an arrangement being a permutation with position on top. Random transpositions have increment distribution , . The lazy adjacent-transposition walk puts mass on the identity and on each . One inverse riffle shuffle assigns each card an independent uniform bit and moves the cards labeled to the top, preserving relative order; the (forward) riffle shuffle is its time reversal, given by transposing the inverse-shuffle matrix (the stationary distribution being uniform). The -reversal chain on circular arrangements indexed by picks a position and a length uniformly and reverses the segment .
for random transpositions on cards (Corollary 8.10), formalized as: for every there is with for all .
Proposition 8.11 (random transpositions lower bound , via fixed points); Proposition 8.13 (riffle shuffle: ); Proposition 8.14 (riffle shuffle: for large , by the counting bound of Mission IV); the random adjacent transpositions upper bound for large (§16.1.2, display (16.4)) and lower bound (§16.1.3, by following a single card); and Proposition 16.2 (the -reversal chain with satisfies , via conserved adjacencies).
The results. Random transpositions at (the constant here is not sharp; the sharp constant is part of the celebrated Diaconis–Shahshahani cutoff) and riffle at are the emblematic mixing results outside of spin systems; the riffle bound is the mathematical content of "seven shuffles suffice" for . The adjacent-transposition walk at order is the basic example where geometry (diameter ) forces polynomial mixing. The -reversal lower bound is the quantitative starting point of the biological application.
Formalizing them. Random walks on symmetric groups and their mixing are entirely absent from Mathlib; so are the combinatorial devices these proofs run on — the Broder stopping time, rising sequences and the Eulerian-number analysis of riffle shuffles, single-card projections, conserved adjacencies. The riffle shuffle formalization via bit strings and the stable-sort permutation Tuple.sort gives a clean combinatorial model reusable for the cutoff analysis of Mission XI.
Corollary 8.10's route is the Broder strong stationary time: mark cards under a card-and-position scheme and prove that, conditioned on the marked set and its positions, the marked cards are uniformly ordered — an exchangeability induction on top of Mission III's stopping-rule framework; then the coupon-collector-style tail with an extra factor. Proposition 8.11 requires the fixed-point statistic: the expected number of untouched cards after transpositions and a second-moment bound, fed into Proposition 7.8. The riffle upper bound runs through inverse shuffles: after inverse shuffles the deck is a uniform stable sort of -bit labels, and mixing reduces to the birthday problem for labels; formalizing "distinct labels imply uniform order" is the crux. The -reversal lower bound needs a second-moment argument for the number of conserved adjacencies with the exact variance bookkeeping of the book. Throughout, the walk-on-group conventions (left vs right increments, forward vs inverse shuffle) are the classic source of silent errors; the formal statements pin them.
All chains are explicit matrices on Equiv.Perm (Fin n) (or Equiv.Perm (ZMod n) for the circular -reversal chain); increments act on the left, matching Mission I's group-walk convention. The riffle shuffle is defined as the transpose-reversal of the explicit inverse-riffle matrix — the two have equal distance to uniformity by Lemma 4.13 (Mission II), which a solver may use rather than re-derive. Asymptotic statements (, "for sufficiently large ") are spelled out with explicit quantifiers; upper bounds carry a where integer rounding requires it. The -reversal family takes the length function as a hypothesis-carrying parameter with , and its lower bound is a genuine limit statement (Tendsto, distance to stationarity tending to ).
Welcome contributions: exchangeability and projection lemmas for deck chains; Eulerian/rising-sequence counting; the single-card chain projection (reused for Mission XI's cutoff examples).
Why do interior-point methods solve convex programs in Newton steps? Nesterov and Nemirovskii's answer is self-concordance: a convex function whose third derivative is controlled by its second, along every line, admits a Newton analysis with absolute constants and no condition number — and the logarithmic barrier is self-concordant. This mission formalizes §9.6 and Chapter 11 of Boyd & Vandenberghe: the self-concordance calculus, the Newton-decrement analysis, the duality gap along the central path, the per-centering work bound , and the crown result — with the aggressive schedule the barrier method reaches duality gap after
centering steps, each of uniformly bounded Newton cost.
Determine the exact second-order term in the least possible largest factor in a factorization of into distinct integers exceeding , with the proposed rational constant .
The final step from bandits to reinforcement learning: actions now change the state of the world. Chapter 38 of Lattimore–Szepesvári studies online learning in an unknown Markov decision process with states, actions and rewards in . The optimism principle of Mission II scales up: UCRL2 maintains confidence sets over transition kernels, solves an extended MDP by extended value iteration, and recomputes only when a state-action count doubles. The goal theorem: with probability , , where is the diameter of the MDP — sublinear regret with no prior knowledge of the dynamics. The matching lower bound brackets the true complexity of tabular reinforcement learning up to .
Randomness appears to enlarge efficient computation, but the Sipser–Gács–Lautemann theorem places every bounded-error probabilistic polynomial-time language at the second level of the polynomial hierarchy, giving one of complexity theory’s foundational limits on the power of randomization.
How well can any algorithm possibly do? Chapters 13–17 of Lattimore–Szepesvári answer with three matching impossibility results. The divergence decomposition identifies the information a policy collects: . Feeding it into the Bretagnolle–Huber inequality of Mission VI yields the goal theorem — the minimax lower bound over Gaussian bandits, showing MOSS (Mission III) is optimal up to a constant. The same machinery gives the instance-dependent bound of Lai–Robbins type: every consistent policy suffers , certifying the asymptotic optimality of the UCB of Mission III and KL-UCB of Mission IV, and a high-probability lower bound showing the Exp3-IX guarantees of Mission V cannot be improved.
Graph theory began with a unicursal problem: Euler's question whether the bridges of Königsberg can be crossed in one closed walk using each bridge exactly once. For graphs whose arcs are all undirected, or all directed, the answer has been known since the nineteenth century: a connected graph has such a closed walk exactly when every node has even degree, respectively when every node has as many incoming as outgoing arcs. Street networks mix one-way and two-way streets, so routing problems such as the Chinese postman problem live on mixed graphs, where neither criterion applies.
Chapter II, §7 of Ford and Fulkerson's Flows in Networks (RAND Report R-375-PR, 1962; Princeton University Press, 1962) settles the mixed case with a necessary and sufficient condition read off from network flows. The same chapter treats, in §4 and §8, the other classical min–max theorems of combinatorics that flow theory reproves in a few lines: the König–Egerváry theorem on bipartite graphs, Menger's theorem on disjoint chains, and Dilworth's chain decomposition theorem for partially ordered sets.
A mixed graph has a finite set of nodes and a set of arcs. An arc is either directed, an ordered pair leading from to , or undirected, an unordered pair . No arc joins a node to itself, and there is at most one arc leading from one node to another: at most one directed arc , at most one undirected arc , and never both an undirected and a directed arc on the same pair. Directed arcs and may both be present.
A closed route is a sequence of nodes and arcs in which each leads from to : a directed arc is traversed with its direction, an undirected arc in either direction. Nodes may repeat, and a single node () is a closed route. The graph is unicursal if some closed route contains every arc of exactly once and every node of at least once.
is connected if is nonempty and any two nodes are joined by a path, arcs being allowed against their direction. The degree of a node counts the arcs incident with it, directed and undirected together. For with complement , write and for the numbers of directed arcs from to and from to , and for the number of undirected arcs joining and .
For §4, a chain in a directed graph is a sequence of at least two distinct nodes with consecutive pairs arcs, and an disconnecting set of nodes meets every chain from to . For §8, is partially ordered by , a decomposition partitions into chains , and the bipartite graph of has an arc whenever ; independent arcs are pairwise node disjoint, and a proper cover is a node set meeting every arc with no proper subset doing so.
The mixed graph is unicursal if and only if
MatousekLP.Integrality.konig.AppliedComb.Posets.dilworth.Theorem 7.1 contains both classical Euler criteria: for an undirected graph condition 3 is vacuous, and for a directed graph, applied to single nodes and their complements, it forces equal in- and out-degrees. In the mixed case, condition 3 is a cut condition over all node subsets, which is what makes unicursality decidable by one feasible-circulation computation. That computation is the first step of the Edmonds–Johnson treatment of the mixed Chinese postman problem (Edmonds & Johnson, 1973). Lemmas 8.1 and 8.2 are the bridge by which König's theorem gives Dilworth's theorem, and through it minimal chain decompositions that a bipartite matching algorithm can compute.
All results here are classical and proved; none of the book's statements has been formalized in this form. The platform has Proved formalizations of König's theorem and of Dilworth's theorem, used here as references. It also has an undirected set-to-set Menger theorem (Menger.menger_set), Euler's criterion for undirected multigraphs (AppliedComb.Graphs.eulerian_iff), and the existence of an Euler tour in a connected, even, symmetric mixed graph (ChinesePostman.Mixed.mixed_euler_tour). That last result is one step of the sufficiency direction of Theorem 7.1, not the theorem itself. The directed, node-disjoint, set-to-set Menger theorem and the mixed-graph criterion are new.
Necessity in Theorem 7.1 is a counting argument. Sufficiency is not: conditions 2 and 3 do not by themselves say which way to orient each undirected arc. A wrong local choice can leave a node unbalanced with no way to repair it, so a greedy orientation does not work. The global information is the cut condition over all subsets, and turning it into an orientation needs a feasibility theorem for circulations with integral solutions. Only then does the classical Euler argument apply, and that argument also needs an induction that splits off closed routes and reassembles connected pieces. For Lemma 8.2 it is showing that a proper cover never contains both copies and of an element; this uses transitivity, and finding F2 shows it fails without it.
Nodes are a Fintype with decidable equality. A mixed graph has directed arcs in a Finset (N × N) and undirected arcs in a Finset (Sym2 N); an arc is an element of (N × N) ⊕ Sym2 N. A closed route with arcs is a pair of maps Fin (m+1) → N and Fin m → MixedArc N, and "each arc exactly once" is injectivity plus surjectivity onto the arcs of . Unicursality is defined by the existence of such a route, never by conditions 1–3, and condition 3 is quantified over every subset with the difference taken in . These two choices rule out the trivializing formalization in which "unicursal" is defined by the theorem's own conditions or condition 3 is checked only at single nodes. Connectedness includes nonemptiness of , so the empty graph is neither unicursal nor connected.
For §4, chains are lists of distinct nodes, and Theorem 4.2 states the maximum and the minimum as attained (IsGreatest, IsLeast) with a common value. For §8, is Fin n with a relation carrying IsStrictOrder; the bipartite graph's nodes are Fin n ⊕ Fin n, and a decomposition is a Finpartition of Fin n into chains.
Beyond the paper. Two variant items stand beside the faithful statements. [Strengthened] Lemma 8.1 replaces the partial order by any relation without directed cycles. The book asserts this on p. 47, and the proof uses only that an independent arc set gives each element at most one successor and one predecessor (finding F1). [Sharpness probe] Lemma 8.2 makes the same weakening for Lemma 8.2 and is expected to be false: on five elements with , , , , , and no other relations, is a proper cover of size (finding F2).
A complete development needs Euler-tour infrastructure for mixed graphs, Hoffman's circulation theorem with integrality, and integral max-flow for Menger. Of these, the circulation theorem is the subject of a sibling mission (Flows in Networks III). Proofs of any item by any method are welcome, including direct combinatorial proofs that avoid flows.
John Conway asked whether a graph on 99 vertices can have every edge in exactly one triangle and every nonedge in exactly one quadrilateral. He included this question among his five $1,000 problems and explicitly accepted either a construction or a proof of impossibility (Conway, 2017). This mission organizes structural constraints and graph reconstruction around the existing public formal statement, which remains open. It complements the existing Conway mission: both point to the same mathematical question, while this mission curates additional published intermediate theorems and the precise bridges still needed to use them.
The historical restriction most relevant here is Wilbrink's 1984 theorem that a hypothetical graph cannot be vertex-transitive (Wilbrink's paper). That result is already formalized on Prove2Me. The consolidated local Conway99 development also contains graph-owned point, finite-field, and rooted constraints. Its written and finite-check results have different verification levels; the platform-accepted lemmas cited below are the machine-checked part of that work.
A strongly regular graph with parameters is a finite simple graph on vertices in which each vertex has neighbours, adjacent vertices have exactly common neighbours, and distinct nonadjacent vertices have exactly common neighbours. Write for a candidate graph and for its integer adjacency matrix, whose entry is when and are adjacent and otherwise. Let be the identity matrix and the all-ones matrix. In this mission, the parameter tuple is .
The condition makes each edge part of a unique triangle. Each vertex's 14 neighbours split into seven paired edges. The condition makes each nonadjacent pair have exactly two common neighbours. These facts lead to triangles and the matrix equation , both already proved on the platform (triangle count, matrix identity). Choosing one vertex as a root splits the remaining vertices into its 14 neighbours and 84 nonneighbours; the graph's actual adjacency blocks then satisfy further identities (rooted theorem). The word actual matters: arbitrary matrices satisfying some of these identities have not thereby been shown to arise from one graph.
This is the already published Conway99.conway_99 theorem, reused as the goal. A graph satisfying it proves existence; a proof of the negation of this full existential settles nonexistence. Neither outcome has been established in the archive.
The first layer collects necessary facts about every hypothetical : rooted block equations, point-Gram identities, and finite-field identities. The accepted theorems are rooted blocks, point Gram, and finite fields. An independent binary cut-response rank theorem supplies reusable seven-vertex algebra; its statement does not assume a Conway graph. A selected twelve-owner contact theorem gives a further conclusion only when its chosen triangle, owner set, and regularity premises hold.
The reconstruction layer asks whether compatible local data can be obtained from, or assembled into, one graph satisfying all four strongly regular parameters. The public adjacency-matrix formulation and triangle line-system formulation are still open. A future coclique-completion equivalence concerns graphs with a specified independent 22-set; it cannot replace the unrestricted goal unless that set is shown to exist in every candidate. No unpublished or pending statement is presented as a completed milestone.
An accepted admitted-coclique spike theorem supplies a precise lattice membership identity when a 22-point set and its point-vector average are already admitted to one lattice. It does not produce that coclique, establish the needed lattice for every graph, or close the reconstruction gap. An accepted printed-census correction is retained as a reference to prevent the known erroneous expressions from being reused as graph counts; it is an audit of formulas, not a structural exclusion.
A construction would settle Conway's existence question with a checkable 99-vertex object. A nonexistence proof would explain why the local triangle and common-neighbour conditions cannot coexist globally, despite the standard parameter equations being consistent. Either result must address the whole graph, not one selected root, lattice, shell, or completion packet (Conway's question; formal goal).
The formalization already gives reusable graph-owned interfaces: block identities from an actual root, a point Gram representation, and modular restrictions. Those are machine-checked necessary conditions, while deeper rank, lattice, triangle-transport, and finite-support exclusions in the consolidated local development remain written or locally checked mathematics. This mission makes their status visible and provides a place to connect faithful formal versions as they are published. A conditional theorem remains useful, but its hypotheses must be derived from the candidate graph before it can narrow the unrestricted goal.
The adjacency equation and its eigenvalue multiplicities constrain every candidate but do not determine the binary off-diagonal entries of . Local equations can have feasible matrix or incidence data even when those data have not been embedded in a common simple graph. Conversely, excluding a fixed support, one lattice choice, or a branch with an ordinary point leaves other configurations untouched. The consolidated local frontier records those coverage gaps, including exceptional-only configurations and unexcluded incidence systems. The central task is to close a graph-wide bridge or exhibit a graph, while retaining every hypothesis on narrower results.
The goal uses Mathlib's SimpleGraph.IsSRGWith and quantifies over a finite vertex type, a graph, and decidable adjacency exactly as in the published statement. Supporting statements may use Fin 99 after an explicit relabelling, integer adjacency matrices, finite triangle sets, real Gram matrices, and finite-field reductions. They must derive data from one G, or mark any independent packet as an additional hypothesis. A theorem about selected owners, a prescribed coclique, a particular determinant or rank, or a saved finite support must keep that restriction visible; none may silently assert that every candidate supplies it.
Existing published definitions and theorems should be imported by their platform IDs. Contributions are welcome for exact bridges between graph, matrix, triangle, and coclique representations; proofs that a conditional packet follows from every candidate; faithful formalizations of written universal constraints; and a construction or unconditional contradiction. The mission's published milestones record actual theorem statements. Prospective bridge descriptions remain research targets until they have separately audited and published platform IDs.
Certify by specializing OpenAI's general seed theorem to and .
The construction gives
Here is block sensitivity at the all-zero input. The ratio is approximately . Prove the exact inequality , then reuse the foundation's finite-certificate theorem.
The goal uses the campaign's shared definitions and requires arbitrarily large sensitivity. This is a stronger specialization of the existing construction, not a claim of a new construction or global parameter optimality.
Value iteration and its policy-evaluation special case, value computation, are the basic algorithms of dynamic programming for Markov decision processes (MDPs). Both are fixed-point iterations of a -contraction, so they converge at the geometric rate , the discount factor. When is close to , which is the regime of long effective horizons in reinforcement learning ( or ) and in healthcare and operations applications, the number of iterations grows like .
Goyal and Grand-Clément (arXiv:1905.09963, Operations Research 2023) observe that behaves like the gradient of a function with smoothness constant and strong-convexity constant . This suggests importing the accelerated schemes of convex optimization: Nesterov's acceleration and Polyak's momentum (heavy-ball) method (Polyak 1964; Ghadimi, Feyzmahdavian, Johansson 2015). For the affine operator of a fixed policy, they prove that both schemes converge at a rate governed by rather than , with , provided the Markov chain of the policy is irreducible and reversible. This mission poses the momentum result, Theorem 5.5.
A finite MDP has a state set with , a finite action set , transition probabilities (from state to state under action ; each is a probability vector), rewards , and a discount factor . A policy is a matrix with nonnegative rows summing to ; it induces
The value function of is , the expected discounted reward from each starting state; it is the unique fixed point of .
Reversibility (Definition 2.1): the chain with transition matrix is irreducible, and it has a stationary probability distribution with for all .
Momentum Value Computation (M-VC) starts from arbitrary and iterates
with the constant step sizes (4.2)
The analysis runs through the matrix
which propagates the error of the pair , and its spectral radius , the largest modulus of a complex eigenvalue.
For a valid MDP and a policy whose chain is irreducible and reversible, the M-VC iterates with step sizes (4.2) converge to , and for every
The goal states the paper's three clauses as printed: convergence, the little-o rate for every , and the comparison with .
The rate is the optimal rate of the heavy-ball method on strongly convex quadratics with condition number . Theorem 5.5 shows that policy evaluation for reversible chains enjoys the same improvement over , so that an -approximation of needs a number of iterations scaling like rather than . The paper also shows that the reversibility assumption cannot simply be dropped: on a cyclic chain both accelerated schemes may diverge. Lemma B.2 is an exact spectral computation for a structured block matrix that reappears in any heavy-ball analysis driven by a matrix with real spectrum in .
The paper is a sibling series of four missions. This one poses Theorem 5.5; the others pose Theorem 5.1 (Accelerated Value Computation), Theorem 6.3 (a lower bound for first-order methods on a chain MDP) and Theorem 7.1 (Safe Accelerated Value Iteration). The results are proved on paper; none of them has a machine-checked proof. The work here is to formalize the known argument: the linear-recursion representation, the spectrum of , and the passage from spectral radius to a little-o rate.
The obvious argument bounds in some norm and iterates. No such bound by the rate holds in general: is not normal, and for eigenvalues of the two roots of (B.1) coincide, producing Jordan blocks. The rate must come from the spectral radius, and the gap between and is exactly what the absorbs. Computing needs two separate facts: the eigenvalues of are tied to those of through the quadratic (B.1), which needs a determinant identity for block matrices with commuting blocks; and the eigenvalues of are real and lie in , which needs reversibility together with irreducibility, used to make the stationary distribution positive. For non-real the modulus computation fails, which is why the hypothesis cannot be dropped.
States and actions are finite types. The MDP data is a plain structure, with validity (stochastic , ) a separate hypothesis; the paper's initial distribution plays no role and is omitted. The value function is the Neumann series . The norm on is the sup norm, and is with respect to it as . Spectra and spectral radii are those of the complexified matrices, so that the non-real eigenvalues of are seen. Reversibility uses the published mm_basic notions: irreducibility, a stationary probability distribution, and detailed balance with respect to it; detailed balance alone would be trivially satisfied by and is not used.
Three printed slips are corrected, and each milestone keeps the printed text verbatim. Lemma B.1 is printed with , but is undefined; the statement uses . Lemma B.2 prints , a negative number; its proof computes , the rate of Theorem 5.5, which is stated. On p. 22 the constant is printed as . The second step size, printed in (4.2), is the of (M-VC) and App. B.
A statement that holds only vacuously, for example one in which reversibility is replaced by detailed balance with an arbitrary vector or in which is unconstrained, is ruled out by the hypotheses above. Lemma B.2 is an equality and must not be weakened to an upper bound.
A complete development needs the determinant of a block matrix with commuting blocks, the reality of the spectrum of a reversible chain (implied by the published MarkovMixing.spectral_representation once the stationary distribution is shown positive), Gelfand's formula for matrices, and the convergence of the Neumann series. The spectral facts about reversible chains and the block-matrix spectrum are reusable beyond this mission. Proofs of any milestone are welcome independently.
Value iteration is the standard method for solving a discounted Markov decision process (MDP), and its policy-evaluation variant, value computation (VC), computes the value of a fixed policy by iterating an affine contraction. Both converge geometrically at rate , the discount factor. When is close to one, as in long-horizon reinforcement-learning benchmarks ( or ), the number of iterations grows like , and each iteration costs a full sweep over states and actions.
In convex optimization, gradient descent on a -strongly convex, -smooth function has the same kind of rate, and Nesterov's acceleration improves the dependence on the condition number from to . Goyal and Grand-Clément (arXiv:1905.09963, Operations Research 2023) read as a gradient with "strong convexity" and "smoothness" , transfer Nesterov's and Polyak's step sizes to value iteration, and ask when the transferred methods are actually faster. This mission covers the first answer they give: for policy evaluation on a reversible chain, the accelerated scheme converges at a rate of order instead of .
An MDP has a finite set of states with , a finite set of actions , transition probabilities (from state to state under action ; each is a probability distribution), real rewards , and a discount factor . A policy assigns to every state a probability distribution over actions. It induces the reward vector , the transition matrix , the policy operator , and the value function
the expected discounted reward when actions are drawn from . VC iterates .
Accelerated Value Computation (A-VC) starts from arbitrary and sets, for ,
with the constant step sizes and . Write .
A transition matrix is reversible if it is irreducible (every state reaches every other with positive probability in some number of steps) and has a stationary probability distribution satisfying detailed balance, for all .
The analysis runs through the matrix
whose powers propagate the stacked error , where and . Its spectral radius is the largest modulus of a complex eigenvalue.
If is irreducible and reversible, then , and for every
The goal is stated with the slack because the iteration matrix has a defective leading eigenvalue: the error is of exact order in general, so a clean bound is false.
The result. Since , A-VC reaches an -approximation of in iterations against for VC, at the same per-iteration cost. This matches the rate of Nesterov's method for strongly convex functions with the paper's identification of the constants. The same paper shows that this improvement does not extend to arbitrary MDPs: Theorem 6.3 gives a lower bound for every first-order method on a chain MDP, which is why reversibility (or a real spectrum, Remark 5.4) is needed here.
Formalizing it. The result is proved in the paper; no machine-checked proof exists. A formal proof needs the reality of the spectrum of reversible chains, the localization of the spectrum of a structured block matrix, and the passage from the spectral radius to a little-o rate for a matrix with a nontrivial Jordan block. The paper's printed statement puts under the square root, . That rate is faster than and is false (a one-state chain is a counterexample). The mission poses the rate that the paper's own proof concludes on p. 9. This is one of four missions from this paper; the other three pose Theorem 5.5 (momentum value computation), Theorem 6.3 (the first-order lower bound) and Theorem 7.1 (safe accelerated value iteration).
The obvious argument says ", so at rate ". That argument breaks twice. First, computing requires knowing where the eigenvalues of lie. For a general stochastic matrix they fill the unit disk, and then the roots of (5.3) can exceed in modulus. Reversibility is what confines them to , and the reality of the spectrum of a reversible chain is not in Mathlib. Second, the eigenvalue of (coming from ) is a double root of (5.3) with a single eigenvector, so is not ; only the -relaxed little-o holds. The eigenvalues of are non-real for , so the whole computation must be done over .
FoundationsML.ReinforcementLearning definitions; irreducibility, stationarity and detailed balance are the published mm_basic. is the discounted reward series, not an arbitrary fixed point of .Ruling out trivial readings: the hypotheses are satisfiable (a two-state chain with is valid, reversible and has a policy), the rate is stated with rather than for some , and is a fixed object rather than a variable constrained by hypotheses.
Needed infrastructure, reusable beyond this mission: the reality and location of the spectrum of reversible stochastic matrices (also used by the sibling mission on momentum value computation); spectra of block matrices with commuting blocks; and the bound from Gelfand's formula. Contributions of any of these as stand-alone lemmas are welcome.
Quantum communication and computation often require a receiver to infer which preparation was sent after it has passed through a noisy quantum process. When possible preparations are mixed states, their overlap makes exact identification impossible. A measurement is then judged by its average probability of a correct label. The pretty good measurement gives a concrete measurement from the ensemble itself, without first solving the optimization over all measurements. Barnum and Knill related it to a general reversal operation for noisy dynamics and bounded its error through pairwise state fidelities in their preprint, §V–VI. The bound is useful when the overlaps are easier to estimate than the measurement's success probability.
The present mission addresses the preprint's second main result. The source is arXiv:quant-ph/0004088v2, not the later journal pagination. The preprint also strengthens its Theorem 3 relative to the published text, as its acknowledgment explains; this mission concerns Theorem 5 and the calculation around it.
An ensemble is a finite family of output density matrices with probabilities satisfying . A density matrix is a positive semidefinite complex matrix with trace one. For each label , fix an orthonormal eigenbasis and nonnegative eigenvalues such that
The eigenpair index runs over a finite output basis ; zero eigenvalues are allowed. The input labels form a finite basis . A label distribution is represented by .
The paper's classicizing channel has Kraus operators . Acting on an input matrix , its value is . In particular, its output on is . The paper assumes has full support when it writes its reversal operation. For a general Kraus family , that operation has operators
The inverse square root is spectral: invert nonzero eigenvalues and leave zero eigenvalues at zero. With full support, it is the usual inverse square root.
For an input label , classical fidelity is the chance that the composite operation returns the same label. Averaging gives
The Bures–Uhlmann fidelity used here is the unsquared quantity . For the classicizing channel, the reversal operation realizes the pretty good measurement, as shown by equation (36) and the discussion after equation (37) in the preprint, p. 10.
The goal, in the reading established by the paper's proof, is
The sum is over ordered pairs; each unordered pair of distinct labels is counted twice. The coefficient is exactly one. The goal applies to every finite ensemble with the spectral data above and a full-support output. It does not fix the number of labels or the dimension of the output.
The milestones are the reversal formula (36), the classical-fidelity identities in (38), the unit squared Frobenius norm (40), the diagonal-block expression (41), the off-diagonal trace-norm identity following (42), and the two-block estimate of Lemma 6. They record the paper's mathematical statements and keep the attack path tied to the authors' displayed results.
The result bounds a measurement's probability of error using only pairwise similarities of the possible output states and their prior probabilities. For nearly distinguishable states, the weighted fidelity sum is small, so this particular measurement succeeds with high probability. The theorem therefore gives a usable guarantee for a specified recovery procedure, rather than only asserting that some procedure exists. In the preprint, §VII, Barnum and Knill describe quantum-information applications of such recovery bounds.
The mathematical result is already proved in the paper, subject to the correction explained below. The formalization work is to make the mixed-state channel, its recovery, the finite-dimensional spectral conventions, and the block-matrix norm estimate precise in Lean. The published Prove2Me definitions for Kraus updates and trace norm supply reusable starting points. A complete proof of this mission would add a checked mixed-state pretty-good-measurement bound; the local statements here compile as open theorems, and no proof is claimed.
The obvious pairwise-overlap estimate does not by itself express the error of the recovery channel. The recovery's classical fidelity is initially a channel evaluation on basis states, while the bound uses trace norms of blocks of a Gram matrix. The key obstacle is controlling the off-diagonal Frobenius mass of the positive square root of that Gram matrix by the trace norms of the corresponding blocks of the Gram matrix itself. Lemma 6 states the needed two-block comparison, including rectangular blocks. The matrix dimension and block labels must remain consistent when it is applied across a larger array.
All systems and index sets are finite, with matrices over and real probabilities. A general completely positive map is represented by an unbundled finite family of Kraus matrices. The classicizing family has rectangular matrices from the input-label space to the output space; the reversal has matrices in the opposite direction. Composite Kraus families are indexed by pairs. The classical fidelity is defined from the channel action in equation (10); the goal does not define it using the desired overlap bound. The reversal is defined by equation (12) for a general family, so its specialized formula remains a theorem.
The spectral hypotheses include nonnegative probabilities and eigenvalues, unit sums, and orthonormal eigenvectors. Full support of is an explicit hypothesis wherever the reversal appears, following page 7. Empty input or output types cannot satisfy the normalized data together with these hypotheses. The Bures–Uhlmann expression is the unsquared trace of a positive square root; using the squared fidelity would change the constant and is outside this mission. Lemma 6 is independent of the ensemble and can be reused for finite block-matrix estimates. Contributions to the spectral identities, the array equalities, and the block-norm argument are welcome.
Equation (39) prints the square of the optimal success probability on its left. The first line of (38) compares that quantity with the recovery fidelity in the opposite direction to Corollary 4. The proof on pages 12–13 concludes the displayed bound for . This mission states that proved conclusion and records the printed discrepancy in its item and audit notes.
Banks lend to one another, and the shape of the resulting network decides how a loss at one bank reaches the others. A long line of work, starting with Allen and Gale (2000) and continued by Acemoglu, Ozdaglar and Tahbaz-Salehi (2015), compares the ring network, where each bank is owed money by one neighbour, with the complete network, where every bank holds an equal share of every other bank's debt. That literature studies contagion after shocks hit and finds that the complete network spreads losses thinly and can absorb small shocks better.
Shu's paper (Management Science, doi:10.1287/mnsc.2022.01519) asks the ex-ante question: when banks choose how much risk to take, knowing the network they sit in, which network makes them take more? A successful bank subsidizes its failed counterparties through the clearing of interbank debt, and anticipating that subsidy pushes it toward riskier projects. Proposition 4 of the paper says that this effect is stronger in the complete network. This mission formalizes that proposition and the computation behind it.
There are banks. In a regular network with share matrix , bank owes bank the face value , every bank has total interbank liability , and every bank also owes a senior deposit . The two networks of Definition 3 are
Each bank chooses a project in a common interval . The project pays with probability and otherwise, independently across banks. Assumption 1 requires , decreasing, and concave. The standing assumption says a successful bank never defaults.
After the state is realized, interbank payments clear. A payment equilibrium is a vector with
where if bank succeeds and if it fails. Bank 's profit is . A risk-taking equilibrium is a profile in which each maximizes bank 's expected profit given . Equilibria need not be unique, and the paper selects the least one.
The key quantity is the network risk-taking distortion
which is bank 's expected net interbank payment to the other banks when its own project succeeds. In a regular network, expected profit equals , so acts like extra debt that the bank repays only when it succeeds. Superscripts and mark the complete and ring networks.
With the least equilibrium of the complete network and the least equilibrium of the ring,
The result. Proposition 4 reverses the conventional reading of the complete network as the safer structure. The co-insurance that makes it resilient after a shock is the same cross-subsidy that weakens incentives before the shock. Two networks with the same face-value liabilities therefore induce different equilibrium risk-taking. Liabilities alone are not a sufficient statistic for risk incentives, and the network topology matters in its own right. The same comparison is the template for the paper's later results on the number of banks and on central clearing.
Formalizing it. The proposition is proved in the paper, not open, and none of it is machine-checked yet. A formal proof must establish the two clearing vectors, the counting identity behind (I.15), and the two closed forms of the distortion. The printed argument also leaves a step to be supplied: its final appeal to "the monotone selection theorem" needs the distortion comparison at every profile of the other banks. It is proved only when they all choose the same project, and it is false in general. The goal is nevertheless stated for least equilibria exactly as in the paper, and its formal proof has to bridge that gap. The milestones are true as stated.
The distortion of the ring is not a function of the number of failures alone. What a successful bank receives depends on the length of the run of failed banks immediately upstream of it, so the closed form needs an exact count of the binary strings with a given number of failures and a given initial run length. The comparison of the two distortions is not termwise either: the positive part sits inside a sum on the ring side and outside it on the complete side.
The obvious final step is to say that the distortion is larger in the complete network, and that a larger distortion raises the optimal risk exposure. That step does not go through as stated. The equilibrium comparison needs control of the best-response maps at every profile, while the distortion comparison holds only on the diagonal, where all other banks choose the same project. Some further structure of the two games is needed to restrict attention to that diagonal.
Banks are Fin N with , and states are Fin N → Bool with true meaning success. The paper's general model is specialized to a regular network given by , which covers both networks of Definition 3. Every expectation is a finite sum over the states, so no measure theory is involved. The payment equilibrium is the greatest solution of the clearing system, because the paper asserts only generic uniqueness. Every bank's project lies in , and is a hypothesis of every statement.
The distortion milestones (2, 5 and 8) are stated at the constant profile in which every bank chooses the same , which is how the page's single reads. At , where every other bank fails, the printed ring binomial has lower index , and the weight is fixed explicitly to at . Proposition 4 is stated for least equilibria and weak inequality. It adds one hypothesis the page does not state, continuity of on , so that best responses and least equilibria exist. Without it the IsLeast hypotheses could be unsatisfiable and the goal vacuous.
Trivializing encodings are ruled out: is an actual solution of the clearing system, not a junk supremum, and the run length is only used in states where some bank succeeds.
A complete development needs Knaster–Tarski on the box , the clearing computations for the two networks, binomial identities, and a monotone comparative statics argument for the equilibria. Published Topkis results on supermodular games (existence of least equilibria, and monotonicity of least fixed points in a parameter) are included by reference as tools. The clearing and counting lemmas are reusable for the paper's other results on ring and complete networks. Proofs of any milestone, and of the goal, are welcome.
Not posed here: Proposition 1 (strategic complementarity in any network, a separate mission), Proposition 2 (existence), and the later comparative statics in the number of banks, central clearing and bailouts.
When every participant in a repeated game runs a no-regret learning algorithm, the time-averaged play converges to a coarse correlated equilibrium, and in smooth games the average welfare approaches the price-of-anarchy guarantee. These facts are a standard justification for equilibrium predictions in auctions, routing and markets, where agents learn rather than solve for equilibria. Against an adversary, the regret of any learning algorithm can grow like , which gives average regret of order . Syrgkanis, Agarwal, Luo and Schapire (arXiv:1507.00407, NIPS 2015) asked whether learning is faster when the opponents are themselves learning, and so their play changes slowly.
Timeline. Daskalakis, Deckelbaum and Kim (2011) gave a decentralized algorithm with regret in two-player zero-sum games. Rakhlin and Sridharan (2013) obtained the same rate in zero-sum games with optimistic mirror descent, which uses the last observed utility as a prediction of the next one. Syrgkanis et al. (2015) extended recency-biased learning to general multi-player normal-form games. They isolated the RVU property, proved that it gives constant total regret (Theorem 4, Corollary 8), and proved that each individual player's regret is (Theorem 11, Corollary 12). This mission formalizes the second result. Later work by Chen and Peng (2020) and by Daskalakis, Fishelson and Golowich (2021) improved the individual rate to polylogarithmic in .
A static game has players. Each player has a finite strategy set with , and a utility function . A mixed strategy is a point of the probability simplex , and the players randomize independently. The game is played at times . At time each player picks and then observes its utility vector
so its expected utility is . The regret of player after steps is
Strategies are measured in the norm . Utilities are measured in its dual, . A regularizer is 1-strongly convex if . The range is .
Optimistic follow the regularized leader (OFTRL) with step size and predictor sequence plays and
With one-step recency bias, . An algorithm has the RVU property (Regret bounded by Variation in Utilities) with parameters if its regret against every is at most . It has the stability property with constant if .
If , every player runs OFTRL with and , then for every player and every ,
The result. Corollary 12 shows that recency-biased regularized learning in a game guarantees each player average regret . The adversarial optimum is . The bound covers every player separately and needs no coordination beyond a common step size. Corollary 8, by contrast, bounds only the sum of the regrets. Theorem 11 isolates the two algorithmic properties responsible, RVU and stability. Any algorithm with both, including optimistic mirror descent and the other recency biases of the paper, inherits the bound.
Formalizing it. The result is proved in the paper, with the proofs of Proposition 7 and Lemma 20 in its supplementary material. No machine-checked version of optimistic FTRL, of the RVU property or of fast rates in games appears to exist. A formalization makes the following explicit: the strong-convexity form the proofs actually use, the convention for the first utility vector , and the exact range of times on which stability is needed. A later mission of this series formalizes the companion bound on total regret (Corollary 8) on the same objects.
The game-theoretic part is short. Once Proposition 7 and the stability bound are available, Theorem 11 is a summation and Corollary 12 is arithmetic with real powers. The weight lies in the single-player analysis of optimistic FTRL. The first idea, to compare consecutive argmax points through first-order optimality conditions, fails because the regularizer need not be differentiable and the maximizers can lie on the boundary of the simplex. The arguments must work with the optimality of argmax points over and with a quadratic-growth consequence of strong convexity. That consequence is not immediate from the midpoint condition in footnote 3. It needs continuity of the regularizer to pass from midpoints to the whole segment. Bounding the variation of utility vectors by the movement of the other players needs a total-variation estimate for product distributions.
Players are Fin n and strategies Fin d, both indexed from . Time keeps the paper's indices: is the initial play and sums run over . The vector is the utility vector against ; the paper never defines it. Mixed profiles and expectations use the published agt_games definitions. is and is Mathlib's sup norm. Optimistic FTRL and the leader sequence are predicates on trajectories, so every maximizer is a valid run. The goal quantifies over every run of the dynamics.
Standing assumptions and disclosed additions:
Trivializations are ruled out. The regularizer class is nonempty: satisfies it. Removing the bound on utilities would make the stability claim false. The goal fixes the paper's step size and constant, so it is not a statement about a chosen run, an unbounded supremum or a vacuous parameter range.
A complete development needs the following:
These are reusable well beyond this mission, for online learning and for learning in games, and contributions of each are welcome.
Ring learning with errors (ring-LWE) is the algebraic variant of the learning-with-errors problem on which most practical lattice-based cryptography is built, including the key-encapsulation scheme ML-KEM standardized by NIST in 2024. Its hardness rests on the paper of Lyubashevsky, Peikert and Regev, On ideal lattices and learning with errors over rings (J. ACM 60(6), 2013, doi:10.1145/2535925; conference version at EUROCRYPT 2010). The paper's main theorem (Theorem 3.6, p. 19) is a polynomial-time quantum reduction from worst-case approximate shortest-vector problems on ideal lattices to the ring-LWE decision problem. Statements about reductions, running times and negligible probabilities are outside the scope of this mission.
What this mission formalizes is the algebraic tool both of the paper's reductions rest on, which the authors list among their main technical contributions (p. 7): a Chinese-remainder technique for clearing an ideal. An arbitrary ideal of the ring of integers need not be principal, so a reduction that receives samples from a lattice cannot simply divide by a generator. Lemmas 2.14 and 2.15 show that, modulo an ideal such as , multiplication by a well-chosen identifies with , and more generally with for every fractional ideal . Steps 1–3 of the BDD-to-LWE reduction of §4.2 consist of exactly these identifications. The authors note that the lemmas are "probably standard for experts in computational number theory" (p. 16); the formulation used in lattice cryptography is theirs, and it is reused throughout the later literature on algebraic lattices.
Let be a number field of degree and its ring of integers. An integral ideal is a nonzero ideal (the paper excludes , footnote 2, p. 13). A fractional ideal is a set such that is an integral ideal for some nonzero ; the nonzero fractional ideals form a group under multiplication, and denotes the inverse. Two integral ideals are coprime when .
For the cleared ideal is . When it is an integral ideal, and " is coprime to " means
For a fractional ideal and , the map sends into , and therefore induces an -linear map
The dual of a fractional ideal is ; is the codifferent, and . For the cyclotomic field , a primitive -th root of unity, () is the automorphism with , and for a prime with a primitive -th root of unity the primes above are , . Calligraphic of the paper are written I, J, M in the milestone texts.
For nonzero ideals , with coprime to , and a nonzero fractional ideal ,
as -modules, via .
The isomorphism of Lemma 2.15 is what makes ideal lattices usable in worst-case to average-case reductions: it turns a discrete Gaussian sample from an arbitrary ideal into a uniform element of the fixed ring , and turns the ring-LWE secret in back into a coset of . Lemma 2.16 is the corresponding tool for the search-to-decision reductions of §5, which move between the CRT components of a completely split . Lemma 2.9 gives the scale of the lattices involved.
On the formal side, none of Lemmas 2.14–2.16 is stated on the platform or in Mathlib in this form. Mathlib has the Chinese remainder theorem for ideals, inverses of fractional ideals in Dedekind domains, trace duals with , and the isomorphism ; the mission connects these to the quotient modules and explicit primes that lattice cryptography works with. All statements are proved in the paper; what remains is the formal proof.
The obvious argument for Lemma 2.15 — both quotients have cardinality , so an injective map is bijective — needs the multiplicativity of the norm on fractional ideals and finiteness of the quotients, and still needs the kernel computation, which uses unique factorization: from one has to cancel and inside the group of fractional ideals and then use coprimality of and . Lemma 2.14 needs the factorization of along the primes of and a CRT choice of ; for it would assert that is principal, which is why the nonzero convention matters. In Lemma 2.16 the delicate point is the direction of the action: sends to , not .
NumberField, is 𝓞 K, fractional ideals are FractionalIdeal (𝓞 K)⁰ K, and integral ideals are coerced into them. Ideals are nonzero, per footnote 2: every statement carries I ≠ ⊥ (and J ≠ ⊥, M ≠ 0 where the paper's convention applies); I ≠ ⊥ is essential because Lean defines . Two kernel/surjectivity milestones drop the nonzero hypotheses on and , which only strengthens them.ClearedCoprime: and in the semiring of fractional ideals.FractionalIdeal.dual ℤ ℚ. is the inverse image of under IsCyclotomicExtension.Rat.galEquivZMod, acting on ideals by images; uses the representative of in . norms sum over all complex embeddings; bounds are phrased through nonzero elements of .When independent players repeatedly choose actions, a low-regret guarantee controls each player's performance against a fixed alternative. It does not directly control the social cost, the sum of all players' costs. For a class of games satisfying smoothness, however, the individual comparisons can imply a bound on the cost of the joint play. This connection makes learning guarantees useful for studying decentralized systems in which nobody selects the entire outcome. The paper uses the smooth-game framework for this purpose.
Syrgkanis, Agarwal, Luo, and Schapire study regularized learning in games and, in Appendix H, show a separate consequence for first-order regret in cost-minimization games. A first-order bound scales with the comparator's cumulative cost, rather than only with the number of rounds. Their Theorem 23 turns that guarantee into an average-cost estimate whose additive term falls as . The result is proved in the paper's supplementary material. This mission targets a machine-checked statement and proof of that known result.
There are players. Each player has pure strategies; a pure profile chooses one for each player. Player incurs a cost . The total cost is , and is the minimum over pure profiles. A mixed profile gives each player a probability distribution over its strategies. Players randomize independently, and is the expected total cost.
In round , player uses and sees a vector . Its coordinate is the expected cost of playing pure strategy against the other players' round- mixed strategies. Thus is that player's actual expected cost. Equation (21) assumes that, for every fixed pure strategy ,
The constants are the constants of the learning guarantee. The logarithm is natural.
A game is -smooth when one pure profile works against every pure profile :
Here replaces only player 's strategy in . This is the paper's cost-game smoothness condition (20). It concerns a single witness , rather than a different witness chosen for each .
The goal is Appendix H's Theorem 23. For and , if the game is -smooth and every player's realized play obeys (21), then
The constants are exactly those printed in the paper. The milestone list follows the displayed statements in its proof: the identity expressing social cost through cost-vector inner products, the aggregate first-order inequality (22), the expected smoothness inequality, the quadratic inequality for the auxiliary quantity , and the final root bound. Together they describe the intermediate claims available to solvers without changing the theorem's target.
The theorem says that the joint play of agents with individual first-order regret guarantees approaches an explicit benchmark in average social cost. The term separates the learning transient from the benchmark determined by , , and . It is a statement about arbitrary realized trajectories that meet the regret condition; the players need not coordinate on a common learning rule.
The paper already proves Theorem 23. The remaining work here is to formalize its cost model, the product-distribution expectations, the first-order bound, the smoothness transfer, and the real inequality behind the exact constants. A proof of this mission would give reusable finite-game definitions and a checked route from player-level cost comparisons to a social-cost statement. Its intermediate claims may also be useful when an alternative algorithm supplies the same first-order guarantee.
Summing the individual regret bounds leaves a sum of square roots of comparator costs. The cost benchmark in the conclusion is a single quantity, so the player-level terms cannot simply be replaced one at a time by . The cost-vector identity and smoothness condition must also agree on the same independent product distribution: changing only one player's pure action while keeping the opponents mixed is easy to encode with a different, unintended distribution. After those choices, the exact coefficient depends on the signs and domains in a quadratic bound. In particular, the intermediate Cauchy–Schwarz inequality uses , while the final theorem has no sign restriction on .
Players are Fin n, and each player's strategies are Fin d. The condition makes the pure optimum a minimum over a nonempty finite set. Mixed profiles are probability weights on each strategy set, with the players' choices independent. The published agt_games definition supplies product-profile probabilities and finite expectations; its expectedPayoff operation is used as an expectation of costs. The paper-specific layer defines pure and expected social cost, the pure optimum, cost vectors, smoothness, and the realized first-order regret condition.
Time has the paper's indices: every round sum runs from through , without shifting the sequence. The goal uses and so its divisions represent the paper's formula. Every cost is in ; every played profile is mixed; (21) is required for every player and every fixed pure comparator. The formulation does not restrict the game to a chosen example, assume the goal inequality, replace with a default-valued infimum, or allow an empty strategy set. The first-order condition is stated on the realized sequence, which follows from any algorithm that guarantees (21) for all sequences.
The intermediate inequality (22) and the quadratic milestone explicitly require , the sign used in their Cauchy–Schwarz step. Theorem 23 itself allows any real , as the paper's stated formula does. The source prints in (22); the Lean statement uses the intended round index . The source also switches between and ; both denote the natural logarithm. Contributions on finite product expectations, the mixed smoothness consequence, and the final real inequalities are all within scope.
Lower bounds on the regret of stochastic multi-armed bandit strategies say how often any reasonable strategy must sample an arm that is not the best one. They are the benchmark against which upper bounds for UCB, KL-UCB and Thompson sampling are judged optimal. The classical bounds of Lai and Robbins (1985) and Burnetas and Katehakis (1996) were proved by changes of measure on carefully chosen events, combined with Markov–Chernoff estimates of their probabilities.
Garivier, Ménard and Stoltz (arXiv:1602.07182v3), published in Mathematics of Operations Research in 2019, replace those arguments with one inequality, which they call the fundamental inequality of their article, inequality (6), p. 6. Every lower bound in the paper follows from it: the asymptotic Lai–Robbins / Burnetas–Katehakis bound for an arbitrary model (Theorem 1), the non-asymptotic bounds for small horizons (Theorems 2–4), and the non-asymptotic logarithmic bound for large horizons (Theorem 5). The same inequality, in the form of Lemma 1 of Kaufmann, Cappé and Garivier (2016), underlies lower bounds for best-arm identification. This mission formalizes the inequality and the lemma that carries its proof.
A bandit problem with arms is a family of probability distributions on , each with a finite expectation. A strategy plays for rounds. In round it picks an arm as a measurable function of , where the are independent uniforms on . It then observes a reward drawn from and a fresh independent uniform . The strategy together with the problem determines the law of ; is its expectation. The number of draws of arm is
is the Kullback–Leibler divergence between two probability measures: when is absolutely continuous with respect to and the integral exists, and otherwise. The binary divergence , for , is the Kullback–Leibler divergence between the Bernoulli distributions of parameters and . For it is given by (5):
It equals for and .
The Lean development builds on the published StochasticBandit K, which holds the arm laws ν.P a. The local FullStrategy K implements the paper's measurable strategy on ; fullHistoryMeasure ν ψ T is the law of , fullPullCount ψ a is , and fullExpPulls ν ψ T a is its expectation. The published BanditPolicy K describes the observed-history kernel model used by the two referenced chain-rule results. The shared definitions supply the Bernoulli law and klBer p q for .
For every strategy , every pair of bandit problems , every horizon , and every -measurable statistic with values in :
in , with . The arm laws have the finite expectations required in §1.1; their divergences may be infinite.
The result. Inequality (6) turns a lower bound on the number of draws into a choice of an alternative problem and a statistic , usually . The binary divergence then contains expected numbers of draws directly, and no event or concentration estimate is needed. In the paper this gives a few-line proof of the Lai–Robbins / Burnetas–Katehakis bound for any model. It also gives the non-asymptotic bounds showing that the regret grows almost linearly while is below a divergence-determined threshold. Each of these is a separate mission of this series, and each applies (6) once.
The formalization. The paper calls the equality in (8) standard and re-proves it for completeness; the inequality half, Lemma 1, is its own contribution. Observed-history kernel versions of the equality in (8) and the one-round step (9) are already formalized on the platform, under the hypothesis that every arm divergence is finite. Lemma 1 and the full-information inequality (6) itself are proved in the paper but not formalized. A machine-checked (6), stated with no divergence-finiteness hypothesis, would make every downstream lower bound in the series a matter of calculus with the binary divergence.
Two points need care. First, Lemma 1 is stated for an arbitrary -valued . The data-processing inequality only gives it directly for indicators of events, and pushing forward by gives a law on , not a Bernoulli law. The paper's route enlarges the space by an independent uniform variable, which needs the product with Lebesgue measure, the invariance of the divergence under that product, and Tonelli's theorem. Second, the goal has no finiteness hypothesis on the arm divergences, while the published chain-rule results assume it. When for an arm that is drawn with positive probability, the left side is and there is nothing to prove. When such an arm is never drawn, its term is . The divergence between the history laws must then be shown to be finite and equal to the remaining sum, which the published decomposition does not cover.
Fin K, indexed from . The horizon is a natural number; at both sides are . For no policy exists, so needs no hypothesis.FullStrategy K, measurable functions of the paper's . The same strategy runs under and . The local history law includes every auxiliary uniform, so may depend on any of them.Integrable id for each arm, expressing §1.1's finite-expectation condition. The published StochasticBandit structure supplies only the probability-law condition.klBer, never a real formula. A real formula would return a finite junk value at , where (5) is , and would make the goal trivially true there. A version with a finiteness hypothesis on the arm divergences, or with a real-valued binary divergence restricted to , would be a weaker theorem and is not the target.unitInterval. is real-valued and measurable, with values in .StochasticBandit and BanditPolicy and on Mathlib's InformationTheory.klDiv. The goal uses a local explicit auxiliary-uniform strategy; the published chain-rule references use observed-history kernel policies and are related proof tools. Other tools are data processing (klDiv_map_le), the chain rule for klDiv and composition products, and Tonelli. The tensorization identity for products of probability measures is Proved on the platform as Tensorization.klDiv_prod_eq_add. Lemma 1 is reusable well beyond bandits, wherever a divergence must be compared with the means of a bounded statistic. Proofs of the milestones, and an extension of the chain rule to infinite arm divergences, are welcome.Many stochastic optimization models contain an expected-value constraint
where is a random object with unknown law , is a decision and is a known loss. When is known only through an i.i.d. sample , data-driven distributionally robust optimization (DRO) replaces by the worst case over a ball of distributions around the data. H. Lam, Recovering Best Statistical Guarantees via the Empirical Divergence-Based Distributionally Robust Optimization (arXiv:1605.09349v1, 2016; Operations Research 67(4), 2019), studies a ball of reweightings of the sample itself, measured by the Burg entropy, and links its radius to empirical likelihood (Owen 2001).
Lam's Theorem 2 shows that, for a fixed decision , the minimum and maximum of over this ball bracket with probability tending to when the radius is . Theorem 3, the goal of this mission, complements it: the two bounds also converge almost surely to . A confidence statement says the robust bounds are rarely wrong; consistency says they are eventually tight, so that the robust constraint does not stay conservative as data accumulate.
This mission is the second of a three-mission series on the pointwise theory of the paper (1: coverage, Theorem 2; 3: reduction to a Burg ball on a finite support, Proposition 1).
Let be i.i.d. random elements of a measurable space with law . Fix a decision and write .
The Burg generator is for and for . The empirical Burg-entropy divergence ball of radius is the set of weight vectors
On the simplex, , the -divergence of from the uniform weights.
Let and let be the -quantile of the distribution. The lower and upper empirical DRO values are
The proof works with the centred observations .
Under the conditions of Theorem 2 (, finite),
with the printed conventions at and for arguments outside the domain of the logarithm. 3. The elementary inequality (p. 34): for . 4. (77) (p. 34): if with , then
Milestones 2, 4 and 5 are deterministic statements about an arbitrary data vector; only Lemma 3 and the goal are probabilistic.
The result. Theorem 3 shows that the empirical DRO with the calibration is a consistent estimator of the constraint function at every fixed decision, not only a confidence bound. Together with Theorem 2 it places the empirical Burg-ball DRO on the same footing as the classical normal-approximation confidence interval: correct asymptotic coverage and shrinkage to the truth. The deterministic bounds (76)–(77) are also reusable on their own: they control the worst-case reweighting of any finite sample by its first two empirical moments.
Formalizing it. The theorem is proved in the paper; no machine-checked proof is known. The mission asks for a formal proof of the printed argument, specialized to one decision. A closely related open target exists on the platform: GenEmpLik.Expansion.lemma_1 (Duchi, Glynn and Namkoong) states the expansion of the robust mean, sample mean plus , for a smooth generator class under stationary ergodic data. Combined with the strong law it would give the upper half of Theorem 3, but it is a different statement with different hypotheses and is itself unproved, so it is not used as a milestone here.
The tempting argument, "the ball shrinks to the empirical distribution and the empirical mean converges", does not close by itself: is only square integrable, not bounded, and the maximizing weight shifts mass towards the largest observations, so the gap has to be controlled against the extremes of the sample rather than by the size of the ball alone. The printed proof routes this through the convex dual (76). That step needs a constraint qualification, the conjugate of the Burg generator with its boundary conventions (an infinite value outside the domain of the logarithm, and the degenerate multiplier ), and a choice of multiplier that dominates every centred observation while still letting all three terms of (77) vanish. The almost-sure statement then combines Lemma 3 with two strong laws on one event of full probability.
ξ 0, …, ξ (n-1): a sequence of measurable maps that is independent (iIndepFun) and identically distributed (IdentDistrib with ξ 0). is the Bochner integral of h x ∘ ξ 0, and the moment conditions are MemLp (h x ∘ ξ 0) 2 (finite mean and variance) together with positive variance, which makes the integral the true mean.EuclideanSpace ℝ (Fin m); plays no role in a pointwise statement and is dropped.GenEmpLik.Expansion.robustMean, whose ball has radius .robustMean burg (q/2); is robustLower burg (q/2) from the frozen shared EmpiricalDRO.Coverage.Setting module, a real infimum over the same published ball (PhiDivRobust.Counterpart.probUncertaintySet). For the value sets are nonempty and bounded, so the real sSup/sInf are the attained maximum and minimum.burg is valued in EReal with for , so a zero weight is excluded from the ball by an infinite divergence and never by a junk value of Real.log. The dual summand dualTerm is EReal-valued with the printed conventions: for ; or at .sSup/sInf of an empty value set, a free radius detached from the quantile, and a dropped variance condition are all excluded by the encoding above. The paper's printed (75) writes where its radius makes it ; at a single decision the two coincide.NumStochOpt.ListScheduling.lemma_8_1_i_max_over_sqrt_ae, included as a reference. Mathlib's ProbabilityTheory.strong_law_ae supplies the laws of large numbers. Contributions welcome: the duality (76) for general -divergence balls, and the deterministic bound (77).Newton's law of universal gravitation states that any two point masses attract each other with a force proportional to the product of their masses and inversely proportional to the square of their distance. It is the first quantitative law of gravity (Newton, Principia, 1687) and it remains the working model of gravity in celestial mechanics, geophysics and engineering whenever relativistic effects are negligible.
The law is stated for point masses, while planets, moons and apples are extended bodies. Newton delayed publication for about twenty years because he could not prove that the Earth attracts external bodies as if all its mass were concentrated at its centre. The result that closes this gap is the shell theorem: a spherically symmetric distribution of mass exerts, on every external point, the same gravitational attraction as a point mass at its centre carrying the total mass; and mass located at radii larger than that of the test point exerts no net force at all.
Timeline (as described in the source):
Space is with the Euclidean norm. The gravitational constant is .
If is a finite, spherically symmetric mass distribution carried by the closed ball , then for every with ,
The shell theorem is what licenses treating the Sun, planets and moons as point masses in the -body problem and in Kepler orbit computations, and it gives the linear growth of the gravitational field inside a uniform planet. The interior statement ("no net force inside a hollow shell") has an exact analogue in electrostatics (Coulomb's law is also inverse-square).
The results are classical and fully proved on paper. This mission asks for machine-checked proofs, together with the reusable infrastructure they require: vector-valued integrals against rotation-invariant measures, the surface measure of the sphere, and the Newtonian kernel .
Newton's argument (or the modern one via Gauss's law) is geometric: slice the shell into rings, or apply the divergence theorem to a sphere. Neither is directly available: Mathlib has no divergence theorem on spheres in the required form, and the ring-slicing computation requires explicit spherical coordinates for a surface measure that is defined abstractly. Using symmetry alone shows the field is radial, but its magnitude requires an actual computation of a singular integral (for the interior of a solid ball the integrand is unbounded).
EuclideanSpace ℝ (Fin 3). Mass distributions are Measures; the field is a Bochner integral. Because a non-integrable Bochner integral is defined to be , statements where integrability is not automatic either carry an explicit integrability hypothesis or are placed where the integrand is bounded (test point strictly outside the support).Space ≃ₗᵢ[ℝ] Space), centred at the origin.NNReal); radii are assumed strictly positive.Measure.toSphere (surface measure on the unit sphere) pushed forward by scaling.Contributions welcome: a general "radial field" lemma from spherical symmetry, the computation of the field of a uniform shell, and the disintegration of a spherically symmetric measure into shells.
Comparing histograms is a basic operation in statistics, computer vision and machine learning: a bag of image descriptors, a word-frequency vector, a discretized density. When the bins carry a geometry (colors that are close to one another, words with related meanings), a comparison that ignores the geometry, such as an norm between the histogram vectors, treats a small shift of mass to a neighboring bin as severely as a shift to a distant bin. Optimal transport compares two histograms by the cheapest way to move one onto the other, with costs read off a ground distance between bins. Rubner, Tomasi and Guibas introduced it to image retrieval as the earth mover's distance (Rubner et al. 2000), and it has since been used for document classification (Kusner et al. 2015) and as a training loss (Frogner et al. 2015).
These uses rely on the transport cost being a distance, so that nearest-neighbor search, clustering and the geometry of the space of histograms behave as expected. This mission formalizes the statement that it is one: Proposition 2.2 of Peyré and Cuturi, Computational Optimal Transport (2019), the discrete form of the classical fact that the -Wasserstein distance is a metric (Villani 2003, Theorem 7.3).
Fix and write . The probability simplex is
its elements are histograms. For the set of couplings (2.10) is
the nonnegative matrices with row sums and column sums ; is the mass sent from bin to bin . For a cost matrix , the Kantorovich problem (2.11) is
A matrix is a distance on if it is symmetric, exactly when , and for all . For , write for the entrywise power. The -Wasserstein distance (2.17) is
In the Lean development these are couplings a b, frob C P, otCost C a b, powCost D p and W D p a b in the namespace CompOT.Metric.
For a distance matrix and , for all ,
The case of the goal's attainment and triangle inequality is already proved on the platform, in another encoding (couplings as functions on for a finite metric space ): MarkovMixing.transport_metric, included here as a reference item. The goal for general is new.
The result. Proposition 2.2 makes a metric space whose metric depends on the ground distance . This is what entitles later chapters of the book to speak of Wasserstein barycenters, geodesics and Lipschitz properties of the transport cost, and it underlies the use of as a loss or a retrieval distance. Remark 2.15 of the same page records that for it is , not , that is a distance, so the restriction is substantive.
Formalizing it. The result is classical and fully proved in the book; it has not been machine-checked for general in this discrete matrix form. The platform's result uses a different encoding of couplings, so this mission supplies the matrix-form transportation polytope , the cost and shared with the other missions of this series, plus a discrete gluing lemma and a Minkowski step stated for arbitrary couplings, which are reusable in any finite transport argument.
Symmetry and definiteness are short once the minimum in is known to be attained, which needs compactness of ; strict positivity for fails for an infimum that is not attained. The triangle inequality is the substantial part. The direct idea of composing the two transport plans as does not give a coupling: the composition must be renormalized by the middle histogram , and may have zero entries, on which a naive is undefined. The renormalized matrix must then be shown to have the right marginals, which uses that wherever . The final step needs Minkowski's inequality for weighted sums together with the triangle inequality of and the monotonicity of ; for it fails.
Indices are Fin n (0-based). Histograms are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, and is Mathlib's stdSimplex ℝ (Fin n); histograms may have zero entries. is a real infimum over the subtype , and every theorem assumes the histograms lie in , where is nonempty (it contains ) and compact. That attainment is part of what a solver proves; it is not a hypothesis. The exponent is a real number with , and all powers are real powers. The book's "positive" is read as ; strict positivity is the clause . The hypotheses of the goal are exactly those of the page: , (i)–(iii), and . The milestones carry the same setting, and milestones 5 and 6 are stated for all couplings instead of only optimal ones, since the proof does not use optimality there.
A trivializing formalization is ruled out: without the simplex hypotheses can be empty and the real infimum would be , making "" true for unrelated histograms; and the four claims are stated about itself, not about the glued coupling or about a minimum over a set assumed nonempty.
Needed infrastructure: compactness and nonemptiness of and attainment of ; transposition of couplings; the gluing construction; Minkowski's inequality for finite weighted sums (Mathlib has Real.Lp_add_le and its weighted variants). Proofs of any milestone are welcome, as are reusable lemmas on .
Optimal transport between two histograms is a linear program: move mass out of each source bin and deliver mass to each target bin at unit cost , as cheaply as possible. Its dual replaces the transport plan by a pair of price vectors and is the basis of most of the computational methods in G. Peyré and M. Cuturi's Computational Optimal Transport (Foundations and Trends in Machine Learning, 2019, doi:10.1561/2200000073): the dual ascent and Hungarian methods, the auction algorithm, the semi-discrete solvers of Chapter 5, and the dual reading of Sinkhorn's algorithm in Chapter 4. The book states the duality as Proposition 2.4 and derives it from linear programming strong duality (Bertsimas and Tsitsiklis, Introduction to Linear Optimization, 1997, Theorem 4.4). Remark 2.21 gives it an economic reading: a vendor sets a collection price at each warehouse and a delivery price at each factory, and the best price the vendor can charge while staying below every shipping cost equals the optimal transport cost.
This is the third mission in a series on the book. It covers §2.5 (Dual Problem, pp. 382–385) and §3.1–3.3 (Kantorovich Linear Programs, C-Transforms, Complementary Slackness, pp. 400–405).
Indices run over and . A histogram is a vector in the probability simplex . Fix , and a cost matrix ; no sign or metric condition is imposed on .
In Lean these are couplings, frob, IsOptimalCoupling, dualFeasible, dualObj, IsDualOptimal, cTransform, cbarTransform and Complementary in the namespace CompOT.Duality.
Stated with both extrema attained: there are an optimal coupling and a dual optimal pair with .
Milestones 6 and 7 are consequences of the goal; milestones 1 and 5 do not need it.
Proposition 2.4 is the finite-dimensional form of Kantorovich duality. It turns the optimal cost into a maximum over price vectors, so that any admissible pair of prices certifies a lower bound on and an optimal pair certifies optimality of a plan through complementary slackness (Propositions 3.2 and 3.3). The -transform reduces the dual to a concave maximization in one vector (3.5), which is the form used for semi-discrete transport and for stochastic dual methods; Proposition 3.1 shows that alternating - and -transforms stalls after one round.
All of these results are classical and proved in the book or by direct reference to linear programming. General-form LP strong duality, weak duality and complementary slackness are already machine-checked on the platform (LinearOptimization.lp_strong_duality and its siblings, from the Bertsimas–Tsitsiklis series); measure-theoretic weak Kantorovich duality is also on the platform with integrability hypotheses. What this mission adds is the book's own discrete statements in the book's notation, as a base that later missions of the series (dual ascent, auction, entropic duality) can cite, with the -transform calculus of §3.2 formalized for real-valued finite costs.
Weak duality, the -transform facts and Proposition 3.3 are finite computations with sums and minima. The content of the mission is the equality in Proposition 2.4 together with attainment of both the minimum and the maximum. Attainment of the minimum needs compactness and nonemptiness of ; attainment of the maximum is not a compactness argument, since is unbounded (it is invariant under ). Reducing Proposition 2.4 to the general LP statement requires an explicit translation of and into the general-form primal–dual pair, including the sign conventions of equality-constrained primal variables and free dual variables. The Lagrangian argument on p. 382–383 exchanges a min and a max without justification beyond "always possible for linear programs", so it does not yield a proof by itself.
Indices are 0-based (Fin n, Fin m); matrices are Matrix (Fin n) (Fin m) ℝ; all quantities are real. Histograms are encoded as a ∈ stdSimplex ℝ (Fin n), the book's standing convention for , and every statement involving or carries it; this also forces . Zero entries in and are allowed. Optimality of a plan and of a dual pair are predicates quantifying over the whole feasible set, never real ⨅/⨆, so no junk value from an empty or unbounded set can enter. The -transforms are real infima over a finite index set; statements that use them without histograms assume (and where the -transform appears), because Lean's infimum over an empty index is .
The goal cannot be satisfied trivially: it asserts existence of a plan that is optimal against every coupling and a pair that is optimal against every admissible pair, with equal values; dropping either optimality clause, or the equal-mass hypotheses, changes the theorem.
Two printed slips are corrected and disclosed in the item notes: Proposition 3.2 prints where its proof uses , and Propositions 3.2 and 3.3 refer to the primal and dual as "(2.24)" and "(2.11)", meaning the discrete primal (2.11) and dual (2.20).
Useful infrastructure: the platform's general-form LP strong duality (included as a reference item), Mathlib's stdSimplex and finite infima. Contributions welcome: proofs of each milestone, a direct proof of Proposition 2.4 by reduction to the LP theorem, and alternative proofs of the goal.