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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
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?
Electricity demand response asks consumers to lower their consumption during price events, when generation is expensive or scarce. Field trials such as the Low Carbon London experiment showed that consumers do react to price signals, but that the reaction is erratic: the average consumption falls while its variability stays high, and a producer that has to follow the load curve in real time pays for that variability. Aïd, Possamaï and Touzi (arXiv:1810.09063; Math. Oper. Res. 2022, doi:10.1287/moor.2021.1201) model this as a continuous-time principal–agent problem in which the consumer (the agent) controls both the level and the volatility of consumption, and the producer (the principal) designs a payment that rewards both.
The paper compares two benchmarks. In the second best, the producer observes only the consumption path and the consumer responds optimally to the contract; this is the subject of the companion mission of this series. In the first best, the producer dictates both the contract and the consumer's effort, subject only to the consumer's participation. The first best is the reference point against which the cost of moral hazard, the information rent, is measured. This mission formalizes the first-best value in closed form, Proposition 3.1 (i) of the paper.
The methodology follows the continuous-time principal–agent literature: Holmström and Milgrom (1987) for exponential utilities and linear contracts, Sannikov (2008) for the dynamic-programming view of the agent's continuation value, and Cvitanić, Possamaï and Touzi (2018) for contracts indexed on both the output and its quadratic variation.
Fix integers (usages for the mean effort and for the volatility effort), cost parameters , , nominal volatilities , effort bounds and , risk aversions , a marginal volatility cost , slopes , a horizon , an initial consumption and a reservation utility .
The consumer chooses a mean effort with values in and a responsiveness effort with values in , at cost
The consumption follows with , in the weak sense: is the canonical process on , and an admissible pair is a progressively measurable control with a probability measure under which starts at and solves the associated martingale problem.
The consumer values consumption by and the producer bears the generation cost ; write . For a payment made at time , the consumer's and the producer's criteria are
A contract is an -measurable with uniform exponential moments (2.5). The first-best value is
The consumer's Hamiltonians are and . Finally , , , and .
Assume . Then
The closed form shows how the first-best value depends on each parameter: on the energy value discrepancy through the mean-effort term, on the volatility cost and the effective risk aversion through the volatility Hamiltonian, and on the reservation utility only through the shift by . It is one half of the paper's information rent (Proposition 3.4), the gap between the first- and second-best values, and it is the benchmark against which the calibrated contracts of the paper's Section 4 are judged.
The result is proved in the paper, partly by appeal to standard stochastic control arguments. To our knowledge it has no machine-checked proof. A formal proof requires a verification theorem for an exponential-utility control problem in the weak formulation, and a risk-sharing argument with a pathwise quadratic-variation term in the contract; both are reusable beyond this paper.
The deterministic parts, Proposition 2.1 and the algebra that turns (A.5) and the value of into the goal, are calculus. The difficulty lies in the two stochastic steps. In (A.5), the producer's optimal payment for a given effort depends on ; it must be realised as a measurable function of the path that is a contract in the sense of (2.5), uniformly over all admissible laws, and the participation constraint must be shown to bind. In Proposition A.3 (i), the upper bound on must hold for every progressively measurable, path-dependent control, not only for Markov feedback controls; the paper invokes "standard stochastic control theory", which has to be made precise for controls of the volatility under a martingale-problem formulation, where no Brownian motion is given in advance.
The canonical space is with the coordinate σ-algebra and the canonical filtration; processes are indexed by . Admissible pairs are given by a martingale problem: almost surely, and both and its square minus are martingales. In the criteria, is replaced by its almost-sure value ; a contract remains any -measurable function of the path. Expectations of utilities are negated lower Lebesgue integrals of exponentials in , and every value is an extended-real supremum with . is read as , with indices in Fin N and Fin d.
The Hamiltonians are defined by their infima, never by their closed forms, so that Proposition 2.1 is not true by definition, and the first-best value is a supremum over the model's own objects, not a variable pinned by hypotheses. Three hypotheses are added to the page: (so ), (so is defined), and, for the goal only, , without which the printed exceeds and contradicts the paper's own proof. Misprints corrected and disclosed in the items: the closed form of in Proposition 2.1 is false for and is replaced by with ; the index range of is ; on p. 28, is and "(A.11)" is (A.6).
The parts (ii)–(iii) of Proposition 3.1, the optimal efforts and the optimal contract, are not stated. Contributions welcome: a verification theorem for controlled martingale problems with bounded coefficients, exponential moment bounds uniform over admissible laws, and a pathwise quadratic variation on the canonical space.
The Ising mixed -spin model assigns to each configuration the energy of a random polynomial whose covariance is . Its ground-state energy converges to the value of a variational problem, the zero-temperature Parisi formula (Auffinger–Chen 2017), in which a functional is minimized over non-decreasing order parameters . El Alaoui, Montanari and Sellke (arXiv:2001.00904v1) ask how close a polynomial-time algorithm can get to this maximum. Their answer is an extended variational principle: the best value reachable by incremental approximate message passing is , where the space drops the monotonicity constraint.
The algorithm that reaches this value is built from a minimizer of over , and it runs along the set of times where is positive. Theorem 5 of the paper (p. 30) shows that this set is dense: a minimizer has full support. This mission formalizes that theorem and the first- and second-order optimality conditions it rests on (Section 6.1, pp. 22–31).
Timeline. Parisi proposed the variational formula in 1979. Talagrand (2006) and Panchenko (2013) proved it at positive temperature. Auffinger and Chen (2017) established the zero-temperature version with and proved that a minimizer over the monotone space exists. Jagannath and Tobasco (2016) developed the PDE and SDE tools for the Parisi functional that Section 6.1 of the present paper adapts to non-monotone order parameters. Montanari (2019) gave the first message passing algorithm for the Sherrington–Kirkpatrick case; the present paper (2020) extended it to general mixtures and introduced .
A mixture is with for some ; its derivatives , are the termwise differentiated power series, non-negative and non-decreasing on .
An order parameter is a function . The extended space is
with the weighted distance . The non-negative step functions are the finite sums with and .
For a terminal condition (convex, continuous, even, non-negative, differentiable off with on ) and , the Parisi PDE
has the explicit Cole–Hopf solution : on , with . For , is the limit of along step functions in the weighted distance. The Parisi functional is
Given a Brownian motion , the process solves , . The support of is , and is its closure in .
With , if satisfies , then
The path to the goal, in attack order:
The result. Full support identifies the extended variational principle as one whose minimizers are "nowhere flat". The algorithm of Theorem 3 in the paper follows through incremental steps whose size is set by , and it needs no special treatment of gaps where . The stationarity conditions (Corollaries 6.10–6.11) also characterize minimizers over the way the Auffinger–Chen conditions characterize minimizers over the monotone space. They are the starting point for comparing with the Parisi value.
Formalizing it. The theorem is proved in the paper; nothing here is open mathematics. The paper's proofs rely on cited PDE regularity (Jagannath–Tobasco 2016) and on standard SDE theory, often in one line. The mission produces a machine-checked chain from the explicit Cole–Hopf formula to the support theorem. Along the way it builds the Parisi PDE solution on a non-monotone class, a first-variation formula, and stationarity conditions, none of which have a formal counterpart. No formal statement of the Parisi functional or the Parisi PDE exists on Prove2Me (index search, 2026-10-03).
Two steps resist a direct argument. The first is the first variation (Proposition 6.8): differentiating in requires comparing the SDE for with the SDE for the perturbed parameter and controlling their difference uniformly, which needs bounds on that degenerate as . The second is the exclusion of gaps: on an interval where the PDE is a time-changed heat equation, and the contradiction comes from a strict inequality, which requires the law of to charge every interval (Lemma 6.12). The obvious idea of perturbing upward on a gap only yields the inequality (6.14), which is consistent with a gap; the second-order identity at the gap's endpoints is what closes the argument.
Conventions committed to in Lean:
eVariationOn for the total variation and IntegrableOn for the integral; the latter includes the a.e.-measurability that the paper takes for granted.gaussianReal 0 1. For , is a limit along the filter of step functions converging in the weighted distance; it is never "some solution of the PDE".derivs in . Lemma 6.2's weak-derivative claim is stated as "convex and 1-Lipschitz", its equivalent.EthierKurtz.SolvesBrownianSDE in dimension one, with coefficients extended by zero after time . The driver is assumed to be a standard Brownian motion (IsBrownianReal). Statements about hold for every strong solution, which by Lemma 6.5 is unique.closure (S γ) ∩ Ico 0 1. Right-continuity of , the paper's convention from p. 28, is a hypothesis.A trivializing formalization is excluded: and are the paper's objects, built from the data, so the goal cannot be met by choosing a convenient solution, and minimality over cannot be satisfied by a junk infimum.
Not formalized: the weak formulation (6.4) of Lemma 6.2, printed with a wrong boundary term; the stochastic-integral identity (6.7) of Lemma 6.5; the regularity Lemmas 6.3–6.4; Proposition 6.1(a). The paper's algorithmic Theorems 2–4 are out of scope, because they concern algorithms in an informal model of computation and an AMP state-evolution theory that is not part of this mission.
Useful infrastructure beyond this mission: the Cole–Hopf solution and its Lipschitz dependence on , the Parisi functional on , and the SDE (6.3). Contributions that formalize Itô's formula for these processes or the regularity of are welcome as supporting lemmas.
Demand response asks electricity consumers to lower or smooth their consumption when generation is expensive, in exchange for payments. Field trials such as Low Carbon London showed two effects of such incentives: consumers reduce their average consumption, and the variability of their response depends on how much effort they put into it. A producer who cannot observe the consumer's individual usages, only the aggregate consumption path, faces a moral hazard problem: the payment can depend only on what is observed.
Aïd, Possamaï and Touzi (arXiv:1810.09063v3, 2019; Math. Oper. Res. 2022) cast this as a continuous-time principal–agent problem in which the consumer controls both the drift and the volatility of his consumption, and the producer pays for reductions in both. The volatility channel is what makes the problem new: the classical Holmström–Milgrom model (Econometrica 1987) controls only the drift. The paper uses the general reduction of Cvitanić, Possamaï and Touzi (Finance Stoch. 2018) to optimal contracts with volatility control, and obtains the producer's value in closed form up to a scalar minimisation. This mission formalizes that closed form.
Fix integers , cost parameters and , nominal volatilities , effort bounds and , risk aversions , a marginal cost of volatility , marginal energy value and cost with , a horizon , an initial consumption and a reservation utility . Write and .
Consumption. is the canonical process on with its natural filtration . A control is progressively measurable, with (effort to reduce consumption) and (effort to reduce volatility). Under the consumption follows, in the weak sense,
Effort costs per unit time, with and .
Criteria. For a payment at time , the consumer's criterion is and the producer's is with . Contracts are the -measurable with exponential moments of order uniformly over the consumer's responses (2.5). The consumer's value is , and is the set of his optimal responses.
Second best. The producer offers , the consumer responds optimally, ties are broken in the producer's favour, and participation requires :
Hamiltonians. and .
Assume . With , ,
A companion statement, Corollary 3.1 (i), gives the explicit off-peak payment rates and when .
The closed form reduces an infinite-dimensional contracting problem, a supremum over all path-dependent payments and all consumer responses, to a deterministic one-dimensional minimisation at each time. It is the basis of the paper's comparisons: with the first-best value it measures the cost of moral hazard, and its minimiser gives the price of energy and of responsiveness that the optimal contract charges, which the paper calibrates on Low Carbon London data.
The result is proved on paper. No part of it is machine-checked. A complete formalization would give a checked instance of a continuous-time principal–agent theorem with volatility control. It would also fix, in exact terms, the conventions the paper leaves implicit (weak solutions, the effort cap), and the printed misprints that this mission corrects.
The deterministic milestones are calculus on boxes. The goal is not. The upper bound must hold for every -measurable contract, not only for contracts of a convenient form. The step that fails in a direct attempt is the representation of an arbitrary contract: one needs that every inducing an optimal response can be written as , an integral against and driven by the consumer's continuation certainty equivalent. This is the main theorem of Cvitanić–Possamaï–Touzi (2018) and rests on second-order backward SDEs; it has no counterpart in Mathlib. Restricting the supremum to linear or representable contracts at the outset would assume exactly that theorem. The lower bound needs, for the candidate contract, existence of the consumer's optimal response as a weak solution and a verification argument for the producer's HJB equation.
All objects live in the namespace DemandResponse.SecondBest, and all hypotheses are fields of a structure Params. Conventions:
Fin N, Fin d; , are allowed. when (the paper's ).The goal is an equality of extended reals between , defined from the model, and an explicit real number. A formalization that defines over a restricted class of contracts, or with a real-valued supremum that returns on unbounded sets, would trivialize or change it and is not the goal.
Needed infrastructure: continuous-time martingales on the canonical path space (Mathlib has Martingale and progressive measurability), existence of weak solutions with bounded coefficients, a representation theorem for contracts (Cvitanić–Possamaï–Touzi), and a verification theorem for the producer's HJB equation. The weak-formulation layer and the contract representation are reusable for any continuous-time principal–agent model with drift and volatility control. Contributions of any of these pieces, and proofs of the deterministic milestones, are welcome.
Online decision makers often have to choose an action before seeing the cost assigned to it. A no-regret algorithm performs almost as well, in total, as the best single action that could have been chosen after the costs were known. In a related repeated-game problem, Blackwell approachability asks a player to keep the average of vector payoffs close to a desired set despite an adversary's choices. These two performance criteria look different: one compares scalar costs to a fixed benchmark, while the other measures a geometric distance. Abernethy, Bartlett, and Hazan establish algorithmic reductions between them, with explicit finite-horizon bounds in their COLT 2011 paper. This mission isolates the direction that turns an approachability algorithm into an online linear optimization algorithm.
The bound matters even when the input algorithm has no known rate. It relates the regret of the resulting online algorithm to the actual distance attained on the corresponding sequence. Any subsequent guarantee on that distance then yields a regret guarantee through the same reduction. The paper also gives the reverse reduction and an application to calibrated forecasting; those are separate missions in this series.
Fix a dimension and a nonempty compact convex decision set . On round , an algorithm selects using only the preceding cost vectors . The adversary then reveals in the Euclidean unit ball . The incurred linear cost is . For a horizon , regret compares these costs with the cost of the best single point of evaluated on all rounds:
The minimum exists because is nonempty and compact. No probabilistic model for the cost sequence is assumed. The round index begins at one, and cannot depend on .
The reduction uses , the maximum norm of a decision. Write for Euclidean concatenation of a scalar and a vector, an element of . The generated cone of a set consists of its nonnegative scalar multiples, . For a set , its polar cone is . This negative-sign convention is fixed throughout the mission.
Algorithm 1 of the paper constructs a vector-payoff game. Its player actions are , its adversary actions are , its payoff and target are
A Blackwell approachability algorithm for this game chooses each from the preceding adversary moves. Its finite-horizon approachability rate on a given sequence is , where distance means the Euclidean distance from a point to a set. The online algorithm created by Algorithm 1 uses precisely the same choices .
The goal is Theorem 16 of the paper. For every admissible history-based algorithm, every sequence of unit-ball costs, and every , it asserts
This is a statement about the rate actually obtained on the chosen cost sequence. It assumes no upper bound on and does not require an oracle call in the statement. Thus it also covers algorithms whose behavior is specified directly rather than through an implementation of the oracle.
The milestone targets are the distance formula of Lemma 13, the conic distance identity in display (8) of Theorem 16's proof, and the existence of a valid halfspace oracle in Lemma 15. Lemma 13 says distance to a nonempty convex cone equals the attained maximum of a linear functional over the polar cone's unit ball. Display (8) specializes this geometry to Algorithm 1's lifted target. Lemma 15 says that every halfspace containing that target admits a player action whose payoff remains in the halfspace against every permitted adversary move. Together these statements specify the geometry and the oracle needed by the reduction.
Theorem 16 gives a numerical transfer rule: a bound on approachability distance for Algorithm 1's game immediately bounds average regret for the same sequence. Its factor depends only on the size of the decision set. This permits comparison of algorithms in a common finite-horizon language, without replacing the online cost sequence by a distribution or an asymptotic limit. The source paper uses this direction as one half of its equivalence between approachability and no-regret learning Abernethy, Bartlett, and Hazan, 2011.
The mathematical results are established in that paper; the goal here is a machine-checked Lean development of their statements and eventually their proofs. The mission also supplies reusable definitions of generated and polar cones, a Euclidean lift, a finite-history online algorithm, and regret over a compact decision set. Lemma 13 is useful outside this reduction whenever distance to a cone is compared with linear functionals on its polar. The proposed theorem items currently carry open proofs, while their statements and definition files are checked for elaboration in the pinned Lean environment.
The main obstacle is the change of viewpoint from a scalar regret comparison to distance from a set of lifted vector payoffs. A direct comparison of individual round costs does not describe that distance. The target is a polar cone in one additional Euclidean dimension, so a faithful account must keep the lift's geometry, the cone's sign convention, and the normalization by aligned. The distance formula also asserts that its maximum is attained. An encoding that merely writes an infimum or supremum with default values can silently make an edge case look valid without representing the paper's claim.
The oracle milestone has a separate quantifier demand. One selected action must work against every adversary move for each halfspace containing the target. It cannot be replaced by a possibly different action for each move, or by a claim only about tangent halfspaces. The theorem includes halfspaces with arbitrary offsets and zero normals because the source oracle accepts any containing halfspace.
Vectors live in EuclideanSpace ℝ (Fin d), and lives in EuclideanSpace ℝ (Fin (d+1)) with the Euclidean norm. The generated cone uses exactly one nonnegative multiple of a point of the generating set, as in Definition 11. The polar uses , the opposite sign from a positive dual-cone convention. Distances are Euclidean point-to-set distances. All arithmetic is over exact real numbers, and the regret minimum ranges over the image of the nonempty compact set .
The statements require because the source payoff divides by . This excludes the degenerate case , in which the source instance is undefined. They require wherever an average is formed. Admissible histories consist of unit-ball adversary moves, and each round's decision belongs to . The dimension may be zero syntactically, but the positive- hypothesis excludes that case in results using Algorithm 1. These conditions keep the bound from being satisfied through Lean's default values for division by zero, distance to an empty set, or infima over empty sets.
The paper's display (8) writes and labels its unit ball with dimension ; the formalization uses the cone of in , matching Algorithm 1. Lemma 12's printed bipolar claim omits closedness; this mission does not use that uncorrected sentence as a milestone. The oracle statement covers all containing halfspaces. Contributions are welcome for the distance identity, the oracle existence result, and the final regret inequality, as well as geometric lemmas supporting those proofs.
Learning an unknown quantum state is expensive. Full quantum state tomography of a -dimensional mixed state to accuracy in trace distance needs on the order of copies of (O'Donnell–Wright 2016; Haah et al. 2017), and this is optimal. For a system of qubits, , so full tomography is out of reach beyond a few dozen qubits.
Often one does not need the whole density matrix, only the behaviour of on a fixed list of tests: acceptance probabilities of verification circuits, expectation values of observables, or the answers a piece of quantum advice gives to a set of questions. Aaronson (arXiv:1711.01053, STOC 2018) named this task shadow tomography and asked whether the number of copies can be polylogarithmic in both the dimension and the number of tests. Measuring each test on separate copies costs copies, which is linear in .
Timeline.
A mixed state of dimension is a Hermitian positive semidefinite matrix with . A two-outcome measurement is a Hermitian matrix with all eigenvalues in . Equivalently, . It accepts with probability .
The state consists of independent copies of . A measurement of with classical output is a POVM: a finite family of positive semidefinite matrices on the -register space with . Outcome occurs with probability . An adaptive procedure that measures the copies one after another is described by one such POVM.
Problem 1 (shadow tomography). Given an unknown and known two-outcome measurements , output numbers with for all , with success probability at least . The output must come from a measurement of , with as small as possible. The measurement may depend on the , but not on .
There is a universal constant such that, for and , Problem 1 is solvable with
copies. This is the last display of the proof (p. 19). The goal fixes no constant, so any improvement of remains consistent with it.
The result. Theorem 2 shows that a state of exponential dimension can be learned "for all practical purposes" on exponentially many tests from polynomially many copies. Applications in the paper include a bound on quantum advice and one-way communication, and implications for quantum money and copy-protection. It also shows that the information needed to predict many measurement outcomes is far smaller than the description of .
Formalizing it. The theorem is proved in the paper, and later work improves its exponents. As far as is known it has not been machine-checked. A complete development formalizes the gentle-measurement toolkit (Lemma 12, Lemma 14, Lemma 15), the amplification of two-outcome measurements on tensor powers, and the postselection argument. These are standard tools of quantum learning theory and quantum complexity with no formal counterpart yet. Lemma 14 and Lemma 15 are reusable beyond this mission.
The naive approach measures the directly on shared copies. A measurement that is likely to reject disturbs the state, so later measurements see a damaged state, and separate copies per measurement cost copies.
The proof needs three ingredients:
The potential argument has to hold for the state after postselection, which is correlated or entangled across registers. Independence-based concentration fails there, which is why the Markov claim, not a Chernoff bound, governs that step. Theorem 13 itself rests on a delicate ancilla-based procedure of Harrow, Lin and Montanaro, and the mission cites it as a milestone without its proof.
WildeQIT.IsDensityOperator (positive semidefinite, trace one).IsEffect E: both and are positive semidefinite.Fin k → n.Riemannian optimization algorithms move along a manifold by taking a step in a tangent direction and then coming back to the manifold. The map that does the coming back is a retraction, and the most natural candidate on a submanifold of a Euclidean space is the projective retraction: add the tangent step, then take the nearest point of the manifold. Its practical value depends on whether that nearest point can be computed.
For many manifolds of symmetric matrices the defining property is a property of the eigenvalues: matrices whose largest eigenvalue has multiplicity , matrices with prescribed spectrum, and similar sets that arise in eigenvalue optimization and in alternating projection methods (Lewis and Malick 2008). Daniilidis, Malick and Sendov (reference [8] of the paper) showed that such a spectral set is a smooth manifold when the underlying set of eigenvalue vectors is a smooth, locally symmetric manifold. P.-A. Absil and J. Malick (SIAM J. Optim. 2012; authors' version hal-00651608v2) then showed that, close to such a manifold, the metric projection onto it has a closed form: one eigendecomposition and one projection in . This mission formalizes that result, Theorem 3.9 of the paper.
Write for the real symmetric matrices with the Frobenius norm , for the orthogonal matrices, and for the permutation matrices, which act on (with the Euclidean norm) by permuting coordinates. Let
For , is the vector of its eigenvalues, with multiplicity, in nonincreasing order; every has an eigendecomposition with . For the spectral set of is
For a set and a point , is the set of nearest points of to (it may be empty or contain several points).
Let be a submanifold of : around each of its points it is a coordinate slice of a chart with inverse. Let , let and . The set (open ball) is strongly locally symmetric if for every and every with ,
Assume is a submanifold of , , and (3.15). Then there is such that for every with , the set is a single point , and for every with ,
The goal fixes no constant: is only asserted to exist, as the paper's proof restricts to make the local uniqueness of and Lemma 3.8 apply.
The theorem turns the projective retraction on a spectral manifold, an optimization problem over matrices, into a projection in onto plus one eigendecomposition. For the matrices whose largest eigenvalue has multiplicity , the projection onto is an explicit averaging of the top eigenvalues (Example 3.10 of the paper), which completes a partial result of Oustry (reference [29, Th. 13] of the paper). Together with Theorem 3.5, it is what makes the projective retraction a practical alternative on manifolds where the Riemannian exponential has no known efficient formula.
The result is proved in the paper; to our knowledge none of it is formalized. The mission produces a machine-checked version of the theorem and of the spectral-set toolkit beneath it: the Lipschitz property of sorted eigenvalues, the reduction of projections onto spectral sets to projections onto sets of vectors, and the permutation rearrangement lemma. The formalization also corrects a misstatement: Lemma 3.7 as printed quantifies over all , and its direction "" fails for unsorted (for , , , ). The mission states it for , which is the only case Theorem 3.9 uses.
The obvious argument shows only half of the goal. Lemma 3.7 characterizes the nearest points of that share the eigenvectors of ; it does not exclude a nearest point with other eigenvectors, and the goal asserts that is a single point. Excluding the others needs the equality case of the trace inequality (3.10), which the paper quotes from the literature without proof, and the fact that the projection inherits the ties of , which comes from strong local symmetry and uniqueness of .
The local uniqueness of near a point of a submanifold (Lemma 3.1 of the paper) is itself a tubular-neighbourhood argument through the inverse function theorem. Mathlib has no metric projection onto embedded submanifolds, no von Neumann trace inequality for sorted eigenvalues, and no Hoffman–Wielandt inequality. Finally, the radii interact: the restriction must make Lemma 3.1, Lemma 3.8 and the ball inclusion all hold at once.
EuclideanSpace ℝ (Fin n), with the Euclidean norm (not the sup norm of Fin n → ℝ). Matrices are Matrix (Fin n) (Fin n) ℝ with Mathlib's Frobenius norm (open scoped Matrix.Norms.Frobenius); is IsHermitian (symmetry over ) and is Matrix.orthogonalGroup.eig X, built from Mathlib's sorted IsHermitian.eigenvalues₀; on a non-symmetric matrix it returns , and every statement assumes symmetry. is sortedDesc n, spectral sets are specSet, permutations act by permAct (an isometry), and (3.15) is IsStronglyLocallySymmetric on the open ball.RandomGradFree.Nonsmooth.IsMetricProjection; is {z | IsMetricProjection Q y z}.IsSubmanifold 2 d M. The paper allows or ; covers both. Only the hypotheses of Theorem 3.5 (cited from Daniilidis–Malick–Sendov without proof) are assumed, not its conclusion that is a manifold.Infrastructure that a full development needs and that is reusable beyond this mission: the von Neumann/Fan trace inequality and its equality case for real symmetric matrices, the Hoffman–Wielandt inequality (3.11), the rearrangement inequality over permutations fixing a vector, and the local existence and uniqueness of metric projections onto submanifolds. Useful platform items: RHLinalg.vonNeumann_trace_ineq (the trace inequality for Hermitian matrices), RHLinalg.bilinear_doublyStochastic_le_of_monovary (the rearrangement step), and Bhatia.trace_mul_perm_bounds (trace pairings between permutation pairings of unsorted spectra). Contributions of these lemmas, of alternative proofs of (3.11), and of the equality case of (3.10) are welcome.
The multi-armed bandit is the simplest setting in which a learner must trade off exploiting what it knows against exploring what it does not: one situation, actions, and a reward drawn from an unknown distribution each time an action is taken. Chapter 2 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) uses it to introduce, in the smallest possible setting, ideas that run through the rest of the book: incremental estimation with a step size, the bias introduced by the initial estimate, soft-max policies over learned preferences, and learning by following the gradient of expected reward.
The chapter ends with the gradient bandit algorithm (§2.8), which learns a numerical preference for each action instead of a value estimate. A shaded box on pp. 38–40 shows that its expected update is exactly a gradient-ascent step on the expected reward, so the algorithm is an instance of stochastic gradient ascent. The same argument, a score-function (likelihood-ratio) identity with a baseline, reappears in Chapter 13 as the REINFORCE algorithm and the policy gradient theorem. The bandit case is where the book first carries it out in full.
Actions are . Each action has a reward distribution on with finite mean , the true action value. At each step the learner holds a vector of action preferences and selects action with the soft-max probability
Given , a reward is received. The expected reward is , a smooth function of . With a step size and a baseline , the gradient bandit update (2.12) is
The chapter's estimation sections use a single action's rewards . The sample average after selections is , with an arbitrary initial value . A constant step size updates (2.5). The trace of one , defines the step size (2.8)–(2.9).
For every action , with and ,
that is, the update (2.12) equals the exact gradient-ascent step (2.13) in expected value, for every baseline that does not depend on the selected action.
The result. The identity makes a model-free algorithm, which uses only the sampled action and reward, an unbiased estimator of the gradient of a quantity that depends on the unknown . It therefore places the gradient bandit algorithm within stochastic approximation, where convergence theory for stochastic gradient methods applies. It also explains the role of the baseline: any baseline independent of the action leaves the expected update unchanged, so the choice of baseline can only affect the variance of the update, as Figure 2.5 shows empirically. The estimation milestones make precise two claims the chapter uses repeatedly: sample averages can be maintained incrementally, and constant step sizes produce an exponentially recency-weighted average biased by . Exercise 2.7 removes that bias.
Formalizing it. All of these results are elementary and proved (or left as routine exercises) in the book. None of them is formalized on Prove2Me or, as far as is known, in Mathlib. What this mission adds is a machine-checked version of the book's argument with the reward model and baseline condition stated precisely, and a reusable soft-max layer (definition, partial derivatives, shift invariance) for later missions of this series, in particular the policy gradient theorem of Chapter 13.
The mathematics is beginning calculus, as the book says. The formal difficulty lies elsewhere. The goal is an identity between an expectation over a two-stage random experiment (an action from , then a reward from ) and a partial derivative in one coordinate of a vector-valued parameter. A proof has to justify exchanging the finite sum with the derivative and splitting the reward integral, and it has to use integrability of each . It also needs the fact that the baseline term vanishes because . A scalar-parameter version of the log-sum-exp derivative does not suffice: the book differentiates in one coordinate while all other preferences are held fixed. For Exercise 2.7 the obvious unrolling of (2.6) does not apply directly, because the step size varies with and the book states neither the weights nor the range of .
Fin k. Every statement quantifies over some action, so whenever it has content. Preferences are vectors Fin k → ℝ. The partial derivative in coordinate is the derivative of at . The soft-max derivative milestone is stated with HasDerivAt, so it also asserts differentiability.Integrable identity and mean . The expectation of a function of is . The book's normal-distribution testbed is only an example.In make-to-order production, chemical process industries and other manufacturing settings modelled as projects, activities do not only occupy machines for a while: they also consume intermediate products at their start and deposit products into storage facilities at their completion. Storage is bounded above by a tank or warehouse capacity and below by a safety stock. Resources of this kind are called cumulative resources (or inventory resources, reservoirs in the constraint-programming literature). They were introduced into resource-constrained project scheduling by Neumann and Schwindt (2002), and Chapter 2 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003), develops their theory in §2.12.
A scheduler handling cumulative resources needs a finite combinatorial description of which schedules respect the inventory bounds at every instant, because the time axis is continuous and cannot be checked point by point in a search procedure. Theorem 2.12.4 of the book gives such a description, and it is the basis of the branch-and-bound procedure of Neumann and Schwindt for the problem .
A project consists of activities with , where is the project beginning and the project completion. Activity has an integer duration , with and for the real activities.
For each cumulative resource in a set , every activity has an integer demand . If , activity withdraws units of at its start; if , it deposits units at its completion; means is not used. The demand of the project beginning is the initial stock. Write and . Each resource has a safety stock and a storage capacity .
A schedule is a vector of real start times with and . The active set and the inventory of at time are
The schedule is inventory-feasible if for all and all .
Two standing assumptions of the section are used throughout: (2.12.1) , so the final inventory is admissible; and Remark 2.12.2, .
A nonempty is a -surplus set if , and a -shortage set if . A -surplus set is minimal if no -surplus set arises from by removing a nonempty set of replenishing activities, and none arises by adding a nonempty set of depleting activities. Minimal -shortage sets are defined with the roles of replenishing and depleting activities exchanged. and denote the minimal -surplus and -shortage sets.
A schedule is inventory-feasible if and only if
The theorem turns a constraint over a continuum of time points into finitely many disjunctions, each a choice among precedence relations. An inventory excess caused by a minimal surplus set is removed by a start-to-completion relation (a replenishment is postponed until after a withdrawal starts, equivalently a maximum time lag), and a shortage by a completion-to-start relation . Consequences stated in the book: the feasible region of is a finite union of polyhedra; branching on these relations, organized as pairs of strict orders and reflexive relations, is a complete search scheme; and minimal delaying alternatives for surplus and shortage sets can be enumerated. Because every problem with renewable resources can be rewritten as one with cumulative resources (p. 130), the book also concludes that this union of polyhedra is in general disconnected.
The result is proved in the book (and in Neumann and Schwindt, 2002). To our knowledge it has no machine-checked proof. This mission produces a Lean formalization of the model, of the one-sided minimality notion, and of the two-sided characterization with its supporting lemma.
The combinatorial core is simple to state but easy to state wrongly. The natural first idea, to use inclusion-minimal surplus sets as for renewable resources, gives a different family and a false theorem: the book's minimality allows removing only replenishing activities and adding only depleting ones. The existence lemma needs Remark 2.12.2 to keep at least one replenishing activity in the minimal set, and the sufficiency direction needs (2.12.1) to guarantee a depleting activity outside the minimal set. Both membership conditions of the active set are closed at , so activities that deplete or replenish exactly at the critical instant must be counted on the correct side; a half-open reading changes which schedules are feasible. The initial stock is handled by the same active-set rule as any other demand, which matters for the invariance claim.
Fin (n + 2), activity is Fin.last (n + 1); resources are an arbitrary type K. Demands, safety stocks and capacities are integers (ℤ); start times are reals (ℝ); durations are natural numbers cast to ℝ.TotalDemandWithinBounds, BoundsStraddleZero) wherever the book's proofs use them. Surplus and shortage sets are nonempty by definition, and minimality uses proper inclusions.Reusable parts: the cumulative-resource model and inventory profile, which later missions on continuous cumulative resources (§2.12.2) or on the NP-completeness of (Theorem 2.12.1) can build on. Contributions welcome: proofs of the lemmas, of either half of the theorem, and finite-sum lemmas about Finset.filter that the proofs need.
The smallest enclosing ball problem asks, for finitely many points , for a ball of the smallest radius that contains all of them. It appears in clustering, in collision detection and bounding-volume hierarchies, in facility location (placing one service point so that the farthest client is as close as possible), and in the analysis of geometric algorithms. Sylvester posed the planar version in 1857; Megiddo (1983) gave a linear-time algorithm in fixed dimension, and Welzl (1991) a simple randomized one.
This mission formalizes Section 8.7 of Matoušek and Gärtner, Understanding and Using Linear Programming (Springer, 2007), which uses the problem to introduce convex programming. Unlike the geometric problems of the book's Chapter 2, the smallest ball cannot be written as a linear program. The section shows instead that it is a convex quadratic program, derives the Karush–Kuhn–Tucker (KKT) conditions for convex programs in equational form from the duality theorem of linear programming, and uses them to prove that the smallest enclosing ball exists and is unique. It is the book's bridge from linear to convex optimization.
A function is convex if for all and . A convex program in equational form is
with a real matrix with columns , and convex. A vector is feasible if and componentwise, and optimal if it is feasible and for every feasible . For differentiable , is the row vector of partial derivatives, so is a scalar.
For points , write and let be the matrix whose th column is . The program studied is
A ball is a closed Euclidean ball . The ball is the unique smallest enclosing ball of a set if , , every ball containing has radius at least , and every ball containing of radius at most has center .
For points , the objective of (8.15) is convex, and
The result. Theorem 8.7.4 gives existence and uniqueness of the smallest enclosing ball together with an explicit certificate: the center is a convex combination of the input points, the squared radius is the negated optimum value, and the points with lie on the boundary. It reduces the geometric problem to a convex quadratic program, for which interior-point and simplex-type solvers exist, and it is the basis of the combinatorial characterization "the center lies in the convex hull of the boundary points" used by Welzl-type algorithms. Proposition 8.7.2 is the KKT theorem for equational-form convex programs; it holds without any constraint qualification because the constraints are linear.
Formalizing it. All results here are classical and proved in the book; none is open. The mission produces machine-checked statements and, when solved, proofs of: the first-order optimality criterion for convex functions on convex sets in ; the equational-form KKT theorem derived from LP duality; the boundary characterization of unique smallest enclosing balls; and existence and uniqueness of the smallest enclosing ball in every dimension. Mathlib has first-order necessary conditions at local minima and general convexity theory, but no KKT theorem for linearly constrained convex programs in this form and no smallest-enclosing-ball theory.
Existence of an optimum and convexity of are routine. For the KKT conditions, the necessary direction needs multipliers, which do not come from calculus alone: the obvious Lagrange-multiplier argument handles only equality constraints and says nothing about the sign pattern forced by . For the goal, a solver must connect three layers — the gradient of a quadratic form in matrix notation, the multiplier conditions, and the Euclidean geometry of distances to — and uniqueness of the ball does not follow from uniqueness of the optimizer , which in general is not unique (repeated or cospherical points). The statement quantifies over all optimal and asserts that they all yield the same center.
Fin n → ℝ, so the book's indices become . Points of are EuclideanSpace ℝ (Fin d), so and are Euclidean. The matrix is Matrix (Fin d) (Fin n) ℝ.ContDiff ℝ 1 f. Convexity is ConvexOn ℝ Set.univ f.Fin n → ℝ, LP duality for the pair (maximize , , ) / (minimize , ), compactness of the standard simplex, and elementary Euclidean geometry. The first-order criterion and the KKT theorem are reusable beyond this mission; proofs through any route are welcome.The simplex method, introduced by G. B. Dantzig in 1947, is the standard algorithm for linear programming and remains the core of commercial solvers. It moves from one basic feasible solution to another by pivot steps, and at each step a pivot rule chooses which variable enters and which leaves the basis. For several natural rules, including Dantzig's original largest-coefficient rule, the method can cycle: on a degenerate linear program it can return to a basis it has already visited and repeat forever without improving the objective. Hoffman (1953) and Beale (1955) gave cycling examples.
R. G. Bland (New finite pivoting rules for the simplex method, Mathematics of Operations Research 2(2), 1977) showed that a simple combinatorial rule, choosing the smallest eligible index for both the entering and the leaving variable, never cycles. This makes the simplex method a finite algorithm on every linear program in equational form, and it gives an algorithmic proof of the duality theorem. Chapter 5 of J. Matoušek and B. Gärtner, Understanding and Using Linear Programming (Springer, 2007, DOI 10.1007/978-3-540-30717-4), develops the general theory of simplex tableaus and proves Bland's theorem as Theorem 5.8.1. This mission is the third of a series formalizing that book.
A linear program in equational form is
with a real matrix, , . Following §4.2 of the book, has columns and rank . For an -element set let be its complement, and , the matrices of the columns of indexed by and . is a feasible basis if is nonsingular and ; its basic feasible solution is the unique with and for .
A simplex tableau is a system
in the variables with the same solutions as , . A nonbasic variable , , may enter if ; a basic variable , , may then leave if
The pivot step replaces by . Bland's rule takes the entering variable of smallest index among those with , and the leaving variable of smallest index among those satisfying (5.3).
There is no infinite sequence of bases
in which each is obtained from the feasible basis by a pivot step obeying Bland's rule. Since there are finitely many bases and a Bland step is determined by its starting basis, this is the book's "always finite; i.e., cycling is impossible".
With the optimality criterion and Lemma 5.6.1, Theorem 5.8.1 turns the simplex method into an algorithm: started from any feasible basis, it stops after finitely many pivot steps at an optimal basic feasible solution or with a ray certifying unboundedness. Combined with the auxiliary program of §5.6 for finding a first feasible basis, this yields a constructive proof that every feasible, bounded linear program has an optimal basic feasible solution, and the book remarks that the duality theorem follows easily. Bland's rule is also the model for later combinatorial anticycling rules in oriented matroid programming.
The theorem is classical and fully proved in the book. What the mission adds is a machine-checked version stated in the book's own tableau notation. On Prove2Me the simplex method is formalized in the Bertsimas–Tsitsiklis series (Introduction to Linear Optimization IV), for minimization with reduced costs, with termination proved under nondegeneracy and for the lexicographic rule; Bland's rule is not formalized there.
The obvious termination argument is that the objective value strictly increases at each step, so no basis repeats. That argument fails exactly at degenerate pivot steps, where the minimum in (5.3) is : the basis changes, the basic feasible solution and the objective value do not. Along a degenerate stretch the objective gives no progress measure, and for general pivot rules the method does cycle there. Any proof must therefore use the specific tie-breaking of Bland's rule, which is a statement about indices, not about values, and relate the tableaus of two different bases in the cycle to each other. Counting bases or tracking the objective value alone does not suffice.
Vectors are Fin n → ℝ and the book's indices become . Bases are Finset (Fin n); the sorted enumerations and are Finset.orderEmbOfFin, tableau rows are indexed by Fin m and nonbasic columns by Fin (n - m). Nonsingularity of is IsUnit A_B.det, so the Mathlib inverse is the true inverse wherever it appears. The tableau parameters used by the pivot rules are the explicit formulas of Lemma 5.5.1; the tableau itself is also defined as in the book (same solution set) so that Lemma 5.5.1 is a genuine statement. "Smallest index" compares variable indices, not row positions. Optimality and unboundedness are stated against feasible points, not through a supremum. Every theorem assumes and , the standing assumption of §4.2.
A formalization in which any improving variable may enter proves a different, false statement, since cycling examples exist for such rules; the step relation here fixes both choices by Bland's rule. The step relation is not empty: it holds whenever the current tableau has a positive last-row coefficient and a negative entry in the entering column, so the goal is not vacuous.
The development needs basic linear algebra over Matrix, the uniqueness of basic feasible solutions, and bookkeeping for sorted index enumerations. Lemma 5.5.1 and Lemma 5.6.1 are reusable for any later formalization of the simplex method in this notation. Contributions are welcome for each milestone, for the cycle-form corollary, and for a sorry-free proof of the goal.
Most Markovian queueing models have no closed-form transient solution. The M/M/1 queue already needs modified Bessel functions (Chapter 2 of the book), and a finite-capacity or multi-class model with state-dependent rates has no closed form at all. What an analyst can always write down is the system of forward equations for the state probabilities. Chapter 8 of Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, DOI 10.1002/9781118625651), presents two numerical techniques that turn such models into numbers: the randomization (or uniformization) method for the transient distribution of a finite continuous-time Markov chain, and the Fourier-series method for inverting a Laplace transform, as needed for the M/G/1 waiting-time transform (5.33) and the busy-period transform (5.37).
Uniformization goes back to Jensen (1953) and is the standard transient solver in performance-evaluation and reliability tools. Its appeal is that it replaces a matrix exponential, which is numerically delicate, by powers of a stochastic matrix weighted by Poisson probabilities, with an error bound that can be fixed before the computation starts (Grassmann 1977; Gross and Miller 1984). The Fourier-series method with Euler summation is due to Abate and Whitt (Abate and Whitt 1992; Abate, Choudhury and Whitt 1999).
A continuous-time Markov chain on the states is described by its infinitesimal generator : for , is the rate of jumps from to , and the diagonal entry is with
The transient state-probability vector , , is the solution of the forward equations
started from a given probability vector . Fix a constant with for every (the book takes ) and define the uniformized matrix
It is the transition matrix of a discrete-time chain : the state of after the -th event of a Poisson process of rate that has been thinned. Write for its distribution after steps.
For the second half of the chapter, the Laplace transform of a real function on is , and the Fourier-series approximant with parameter is
with .
The forward equations have a solution, and every solution satisfies, for all ,
and whenever , every component of the sum truncated at is within of .
The mission also contains Eqs. (8.7)–(8.8) as a further theorem, outside the milestone list: the transition probabilities satisfy , and .
The randomization formula reduces the transient analysis of any finite Markovian queue (finite-buffer, multi-server, with balking, reneging or state-dependent rates) to repeated vector–matrix products with a sparse stochastic matrix. The truncation point is chosen from a Poisson tail alone, independently of . Milestone 3 shows that the same matrix gives the stationary equations, so one iteration serves both transient and steady-state computation. The discretization identity (8.27) is what justifies the parameter choice in Algorithm 8.1: the error decays like .
All of these results are classical and proved in the literature. None of them is formalized in Lean or Mathlib as far as a search of the platform and Mathlib shows. Mathlib has the matrix exponential and Poisson summation under decay hypotheses, but no continuous-time Markov chain generators, no uniformization, and no Laplace transform. This mission would add the finite-state link between generators, stochastic matrices and matrix exponentials that later chapters of queueing and reliability theory use, and a verified error formula for a numerical inversion method in wide use.
The book's derivation is probabilistic: it conditions on the number of events of the Poisson() process and thins them. A formal statement cannot rest on that picture, because is defined analytically, by the forward equations. The goal therefore contains a uniqueness statement for a linear ODE on with one-sided derivative at , which the book never mentions. The componentwise bound then needs to be stochastic, so that every lies in . That is exactly where is used; with a smaller the matrix has negative diagonal entries and the bound fails.
For (8.27), the book gives no proof. The identity is an aliasing (Poisson-summation) formula for a periodic function assembled from the values of at all odd multiples of . The convergence of the conditionally summed series (8.24) is the delicate point: continuity of at , the book's only hypothesis, does not guarantee convergence of a Fourier series. Mathlib's Poisson summation theorems require decay of the Fourier transform that the damped, reflected function built from does not have.
Fin (N+1); a row vector is Fin (N+1) → ℝ; is vecMul. A generator is a real matrix with nonnegative off-diagonal entries and diagonal .HasSum, so convergence is part of the claim.Useful infrastructure: the matrix exponential and its derivative (Matrix, NormedSpace.exp), uniqueness for linear ODEs (Grönwall), Fourier series on the circle, and a reusable Laplace transform file. Contributions of general lemmas on generators and stochastic matrices are welcome, as they apply to every finite Markovian model in the series.
The irrationality measure is the supremum of the for which has infinitely many rational solutions . Every irrational number has (Dirichlet), almost every real number has , and it is conjectured that . Known upper bounds:
The campaign's first proved value is Mahler's . This entry records Chudnovsky's bound.
The campaign template with the value filled in: PiIrrationality.UpperBound (19.8899945 : ℝ), i.e. .
Value. The bound is quoted in the literature as (e.g. Hata 1993), a truncation. This entry rounds the last digit up to so that the goal follows from the published constant.
Chudnovsky determined the exact asymptotic behaviour of the Hermite-type contour integrals behind Mahler's approximations, which sharpens the resulting exponent.
Each step down the list replaces Mahler's approximations with a sharper family. Formalizing would build reusable explicit machinery: integral constructions of rational approximations to , bounds on their common denominators via prime-number estimates, and the standard lemma turning a sequence of good approximations into an irrationality-measure bound.
The irrationality measure is the supremum of the for which has infinitely many rational solutions . Every irrational number has (Dirichlet), almost every real number has , and it is conjectured that . Known upper bounds:
The campaign's first proved value is Mahler's . This entry records Mignotte's bound.
The campaign template with the value filled in: PiIrrationality.UpperBound (20.6 : ℝ), i.e. .
Value. The paper's abstract states for all , which gives exactly as stated. The paper also proves for (explicit), so follows from the same source; this entry uses the table value .
Mignotte refined Mahler's method of explicit rational approximations to (Hermite's approximation formulae for the exponential and logarithm) and sharpened the estimates that turn their size and denominators into an irrationality measure.
Each step down the list replaces Mahler's approximations with a sharper family. Formalizing would build reusable explicit machinery: integral constructions of rational approximations to , bounds on their common denominators via prime-number estimates, and the standard lemma turning a sequence of good approximations into an irrationality-measure bound.
This mission formalizes Y. Lodha and J. T. Moore, A nonamenable finitely presented group of piecewise projective homeomorphisms, Groups Geom. Dyn. 10 (2016) 177–200 (doi:10.4171/GGD/347; arXiv:1308.4250v3, whose page numbers are used): the group generated by three explicit piecewise projective homeomorphisms of the line is nonamenable and finitely presented, the first torsion-free finitely presented counterexample to the von Neumann–Day problem.
A discrete group is amenable when it has a finitely additive invariant probability measure on all its subsets. A group containing a nonabelian free subgroup is not amenable, and von Neumann and Day asked whether the converse holds. The counterexamples found before Monod's work are built from torsion groups by elaborate inductive constructions. Monod (2013) found nonamenable groups without free subgroups among piecewise projective homeomorphisms of the line. Lodha and Moore isolate in Monod's group a subgroup with three explicit generators and nine explicit relations.
Timeline.
The generators act on the real line: , and , are the piecewise projective maps of p. 2 (aFun, bFun, cFun). As homeomorphisms of the projective line (a, b, c) they generate (G0), inside the group where the published Monod bundle defines (Monod.Hpp).
Lodha and Moore move to infinite binary sequences through the continued-fraction map (Phi), under which , , become functions , , of sequences (Proposition 3.1). There and are and acting on the sequences that extend . is the group generated by all and , the group generated by the and the with not constant, and the five families of relations (1)–(5) among them. Products are taken left to right, as in the paper.
Section 5 rewrites words in the generators by explicit substitutions into standard forms and sufficiently expanded standard forms, and tracks them through strings in , , , ; these notions form the second definitions bundle.
ConnesFeldmanWeiss.exists_nonsingular_generator_of_isAmenableRel) as two milestones; Theorems 2.1 (Zimmer) and 2.2 (Carrière and Ghys) as printed; the group ; and the identities and orbit comparison of p. 4.The result. settles the finitely presented von Neumann–Day problem with a group that is torsion-free, has explicit generators and relations, and acts by piecewise projective maps, so its elements can be described by labeled tree diagrams much as those of Thompson's group . It shows that shares the combinatorics of without its unresolved amenability question.
Formalizing it. Before this mission none of the paper was formalized. The Monod mission's milestones supply the setting, and the case of Carrière and Ghys that Monod uses is already proved there by an elementary argument (Monod.not_isAmenableRel_mob).
Nonamenability is a short reduction to Theorem 2.2, which in general is deep. Finite presentation is the bulk: one must show that every word that evaluates to the identity can be reduced to an -word by the substitutions of §5, through a well-founded ordering on standard forms (Lemma 5.6) and an analysis of how acts on binary expansions (Lemmas 5.9–5.11).
Lean representation and conventions.
List Bool (finite) and Stream' Bool (infinite). is explicit; and are defined by the recursion of p. 5, digit by digit.Stream' Bool, so that products are left to right as in the paper. Statements about , , take products in the opposite of the homeomorphism group for the same reason.a, b, c are the homeomorphisms that agree with the formulas on , and toSeqGroup turns a bijection of sequences into a group element. Both fall back to the identity for a function that is not a homeomorphism or a bijection. Every generator is in fact one, so the fallback is never reached, and a trivial group would make the goal false.Matrix.ProjectiveSpecialLinearGroup, with the quotient topology), as on p. 4; a class acts on the projective line by the Möbius map of either of its matrices, through the published Monod bundle.What is left out, and deviations.
CountableOrbit.exists_perm_rel_iff_exists_zpow_eq is the underlying fact).LodhaMoorePrinted.printed_relations_four_and_nine_ne); the milestone uses the translations of the relations in , that they come from.LodhaMoorePrinted.eq_of_step_singleton_y_neg_one), and allow commuting and for any exponents, as the proof of Lemma 5.6 does (with commuting only for positive exponents, Lemma 5.6 fails: LodhaMoorePosCommute.not_forall_exists_derives_sufficientlyExpanded).What a development needs. Monod's mission supplies , its lack of free subgroups, the elementary non-amenability argument for with dense, and the passage from an amenable group to an amenable orbit relation. The theorem of Connes, Feldman and Weiss is published and proved (ConnesFeldmanWeiss.exists_nonsingular_generator_of_isAmenableRel); it gives the hard direction of the equivalence. The presentation of Thompson's group is published by the Cannon–Floyd–Parry mission on the two presentations of Thompson's group . Proofs of any milestone are welcome.
This is the second mission of the series on Assumptions of Physics by G. Carcassi and C. A. Aidala (book, v3.0, 2025), formalizing Part II, Chapter 2, "Domain combination and relationships". The chapter asks when the outcome of one experiment can be inferred from another (e.g. temperature from the height of a mercury column), and shows that such inference relationships between verifiable statements correspond to causal relationships between possibilities, which are continuous maps of the natural topologies. It builds on the definitions of the first mission (Assumptions of Physics I), which must be launched first because this mission imports its definition file.
Statements are truth sets over the possible assignments of a fixed logical context; an experimental domain , its possibilities , verifiable sets and natural topology are as in mission I. An inference relationship from to is a map with ; depends on if one exists, and two domains are equivalent if each depends on the other. A causal relationship is a function between possibilities with . The combined domain of a countable family of domains is generated by all their statements under finite conjunction and countable disjunction.
Theorem 2.10 is what justifies describing experimental relationships by functions between possibilities rather than by maps between all finite-precision statements, and Corollary 2.11 identifies equivalence of experimental domains with homeomorphisms that respect the statements. Later chapters use these to transport structure between equivalent domains. The results are proved informally in the book; no machine-checked formalization is known to the drafters.
The forward direction requires showing that each possibility of lies inside exactly one possibility of and that preimages of verifiable sets are verifiable. The converse is subtler: Definition 2.7 does not require continuity, and the book's Corollary 2.8 ("all causal relationships are continuous") does not hold in general. For example, with , and , the identity on possibilities is a causal relationship but . The goal therefore includes continuity of explicitly. That is the hypothesis the book's proof of the converse actually uses.
Domains are ExperimentalDomain Ω on a common type Ω; dependence is ExperimentalDomain.DependsOn (existence of an equivalence-preserving map, which here is the inclusion ), causal relationships are predicates IsCausalRel on functions between the possibility types, and topological notions are Mathlib's (Continuous, ≃ₜ). The combined domain ExperimentalDomain.combined takes a family over an arbitrary countable index type. Theorem 2.12 (transport of structure) is informal in the source and is not formalized here. Propositions 2.15–2.28 are left out: the residual possibility depends on the choice of basis, and Proposition 2.18 appears to need a stronger independence hypothesis than Definition 2.17 provides. They are candidates for a later mission.
We formalize the equivalence between Turing machines and the WordRAM model of computation. Turing machines are the standard model for studying computability, but algorithms are rarely described in terms of tape operations. WordRAM is much closer to assembly, with memory accesses, arithmetic instructions, branches, and loops. The goal is to connect this familiar way of expressing algorithms to the foundations of computability. This will also bring us closer to one day formalizing Fine Grained Complexity.
The formal target is halting equivalence through simulations in both directions, with the stated memory bounds and a family of word widths, each fixed during a run.
A seller who does not know how demand responds to price must learn the demand curve from its own sales while also earning revenue. This is the learn-and-earn problem of dynamic pricing. Every price it charges both earns and informs, and a policy that only earns can stop learning. Keskin and Zeevi (Operations Research 62(5), 2014) study the problem for a linear demand model with unknown parameters. They show that the certainty-equivalent ("greedy") policy can fail, and they give simple conditions on a policy's price path under which its regret is of optimal order.
This mission covers the paper's incumbent price problem (§3.4). Here the seller has charged one price for a long time and knows its expected demand . Only the slope of the demand curve is unknown, and is the single price that reveals nothing about it. A greedy seller whose estimates drift toward stops learning ("incomplete learning"), and its regret can grow linearly. Earlier single-parameter models (Broder and Rusmevichientong 2012) assumed that the intercept is known, which makes the uninformative price , a price no seller would choose. The incumbent price model makes the trade-off real. The paper proves a lower bound on regret for this model (its Theorem 3), and its Theorem 4 gives sufficient conditions for matching that bound. Theorem 4 is the goal of this mission.
Prices lie in with . The incumbent price is . The seller decides the price deviation in each period and observes demand
The unknown slope lies in a known interval with . The shocks are i.i.d., with mean and variance , and they are light-tailed: for , for some . They need not be Gaussian. The expected revenue at deviation is . It is maximized at
and is assumed to lie in the open interval for every .
A pricing policy chooses each price in as a measurable function of past demands and prices only. Its regret over periods is
From the data the seller forms the information metric , the least squares estimate and the truncated estimate . The greedy deviation at the end of period is .
Let with . There is such that for all , and there is a finite with the following property. If a policy satisfies, almost surely for all ,
then for all .
The goal fixes no constants beyond the order . The milestones keep the paper's explicit constants where the paper gives them.
Theorem 4 turns asymptotic optimality into two checkable properties of a price path: enough information (i) and closeness to the greedy price (ii). Any policy meeting them has regret of order . Together with the paper's matching lower bound, this pins down the optimal regret of the incumbent price problem. The same conditions certify whole families of simple policies. One example is the "constrained iterated least squares" rule of p. 1150, which perturbs the greedy price by when it comes too close to . Heavy exploration schemes are not needed. The contrast with the paper's two-parameter Theorem 2, where the corresponding rate is , shows that the known incumbent point is what makes linear information growth free.
The result is proved in the paper. As far as a search of the platform shows, none of it is machine-checked: the platform has no dynamic pricing regret results and no least squares tail bound of this self-normalized, adaptively designed form. A formal proof would give a checked instance of a pattern that recurs throughout learning-and-earning analyses: an exponential tail bound for a self-normalized martingale with an adaptively chosen design, combined with a pathwise information-growth argument.
The deviations are chosen adaptively from past data, so is a martingale with a random, data-dependent quadratic variation . Classical fixed-design least squares bounds do not apply, and a bound that holds on the event uniformly over all policies is needed (Lemma 5). The regret bound then needs a bootstrap. The information grows linearly only if the recent greedy prices are near optimal (the event ). Near-optimal greedy prices are likely only if enough information has already been collected. Closing this loop requires the tail bounds of Lemma 5 to be summable in , and this is where the threshold on enters. A naive argument that bounds the estimation error by using only condition (i) gives , which is far from logarithmic regret.
Everything lives in the namespace KeskinZeevi.IncumbentSufficient. Model bundles with the standing assumptions, and is the closed form above. LightTailedNoise P ε σ states the shock assumptions on a probability space. A Policy is a sequence of measurable history-to-price maps into . The price, deviation and demand processes are defined by recursion from the noise, which realizes the paper's law of the sales process on the noise space. Periods are 1-based. Regret is for a fixed true slope , not the worst case over . Expectations are Bochner integrals of bounded measurable functions, and probabilities are measures of sets.
The goal is a corrected form of the printed Theorem 4. The page says "there exist finite positive constants , and such that if … satisfies (i)–(ii) almost surely for all ". Read literally, that statement is satisfied vacuously by choosing so large that no policy meets (i) (at , ). The Lean statement instead quantifies universally over every above a threshold, every and every start time , which is what the proof establishes, and it implies the printed statement. The sum in (ii) starts at rather than , because is defined only for the greedy policy. This only weakens the hypothesis. When , uses Lean's , a case the hypotheses exclude for . (27) is stated under . The linear-growth milestone is pathwise and is stated for . (A19) has its threshold existential and uniform over policies.
A complete development needs a conditional exponential-moment (supermartingale) argument for under adaptive design, a mean value bound for on , and elementary summation of and terms. The self-normalized tail bound (Lemma 5) and the regret identity are reusable beyond this mission. Proofs of the milestones in any order are welcome, as are sharper constants.
A basic question of combinatorial geometry asks when a family of sets can be pierced (or stabbed) by few points. For intervals on the real line the answer is classical: if every two of finitely many closed intervals intersect, one point meets all of them, namely the rightmost left endpoint. This is the one-dimensional case of Helly's theorem. The situation changes as soon as the sets are allowed to have holes. Unions of two intervals can intersect pairwise without any point being common to three of them, so no single point suffices, and it is not obvious that any bound depending only on the number of holes exists.
This mission formalizes the answer given in Section 8.6 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer, 2007): pairwise intersecting unions of intervals can always be pierced by points. The section uses the result to illustrate a general method of combinatorics, in which a linear programming relaxation of a covering problem is bounded through LP duality and then rounded. The same scheme, a bound on the fractional transversal number followed by a rounding step, appears across discrete geometry and combinatorial optimization.
Timeline.
Fix an integer . A -interval is a union of closed intervals on the real line,
The numbers and are the endpoints of . A finite family of -intervals is pairwise intersecting if for all . A set of real numbers is a transversal of if every contains a point of .
More generally, for a finite set and a system of subsets of : a transversal is a set meeting every member; the transversal number is the smallest size of a transversal; a matching is a subsystem of pairwise disjoint members, and the matching number is the largest size of a matching. The fractional transversal number is the optimal value of the linear program
and the fractional matching number is the optimal value of
This is the book's theorem with its constant .
The result. Theorem 8.6.1 shows that the piercing number of pairwise intersecting -intervals is bounded by a function of alone, and that this function is polynomial. The section also states, without proof, the extension for arbitrary finite families of -intervals. Upper bounds of this kind feed into piercing and hitting-set questions for families with bounded "complexity", and the chain is the standard frame in which such bounds are proved.
Formalizing it. The theorem, both lemmas and the duality chain are proved in the literature and in the book. None of them is on the platform. The work consists of formalizing the book's proof: a double-counting argument, LP duality for the pair of fractional programs together with the rationality of an optimal basic solution, and a rounding step. The general-set-system milestone is reusable for any transversal problem, independent of -intervals.
The obvious generalization of the one-dimensional argument fails: for no point need be common to all members, so there is no single extremal endpoint to choose, and a greedy piercing procedure has no control over how many points it uses. The difficulty is to obtain a bound that does not depend on the size of the family. In the book's route the counting statement of Lemma 8.6.2 holds only for equal weights, while the fractional programs produce arbitrary real weights, and the passage between the two, as well as the passage from a fractional transversal of small total weight to an actual finite set of points, are the steps that need care.
A -interval is stored as data: two functions left, right : Fin d → ℝ with left k ≤ right k, together with the set toSet . Components are indexed . Endpoints are those of the given components, so they depend on the representation, as in the book's proofs. Families are Finsets of such data; Lemma 8.6.2 uses a Fin n-indexed sequence, since the proof of Lemma 8.6.3 applies it to a sequence with repetitions. The hypotheses (the book's definition) and, in Lemma 8.6.2, are explicit. The quantity is real division. Transversal sizes are cardinalities of a Finset ℝ bounded by .
For set systems, is a finite type and a Finset (Finset V) with nonempty members; without this assumption no transversal exists and both fractional programs degenerate. The numbers and are expressed through optimal feasible solutions, not as infima or suprema, so no junk value of an empty or unbounded set is involved. is an sInf over that is attained under the nonemptiness assumption, and is a maximum over the finite family of matchings.
A trivializing formalization is ruled out: the pairwise-intersection hypothesis is satisfiable by nonempty families, the transversal is required to meet the actual sets , not a representation artifact, and the bound and are the book's constants, not weakened ones.
Needed infrastructure: finite sums over Finset ℝ, LP duality for a finite primal–dual pair in inequality form (or a direct proof of the chain), rationality of an optimal vertex, and a left-to-right sweep over a sorted finite set of reals. Contributions of a general LP duality statement for set-system relaxations are welcome and reusable.
A deep-space probe sends a vector encoded as , and up to about 8% of the transmitted numbers may be corrupted arbitrarily. Section 8.5 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer 2007, DOI 10.1007/978-3-540-30717-4) shows that decoding reduces to finding a sparse solution of an underdetermined linear system , and that under suitable conditions this sparse solution is found exactly by a single linear program. The same problem arises in signal processing (sparse representations in redundant wavelet dictionaries) and in computer tomography, and it is the core of what became known as compressed sensing.
Timeline, as recorded in the book's references:
Let be a real matrix with and . The support of is . For an integer , a sparse solution of is an with and . The -norm is .
Basis pursuit is the optimization problem
which is equivalent to the linear program
The matrix is BP-exact for if for every : whenever has a solution with at most nonzero components, is the unique optimal solution of (BP). The crosspolytope is , the kernel of is , and . For with , the cone at is , and is good for if .
For and :
This is the book's geometric characterization of exact recovery, and the statement on which the known probabilistic proofs are built.
With , and an matrix of independent entries, there is a constant such that for every
The book states this without proof. It is included as a separate theorem, not a milestone of the goal.
Lemma 8.5.4 converts an algorithmic property, that an linear program returns a prescribed sparse vector for every right-hand side, into a purely geometric property of the kernel of relative to the low-dimensional faces of the crosspolytope. With milestone 5 it becomes the statement that avoids a finite family of cones, which is where union bounds over faces and estimates for random subspaces enter. Observation 8.5.1 separates what is information-theoretically possible (uniqueness of sparse solutions) from what is computationally achievable by linear programming; finding a sparse solution directly is NP-hard in general. Theorem 8.5.2 is the quantitative payoff: a fixed fraction of arbitrary gross errors can be corrected by solving one linear program.
All of these results are proved in the literature; Lemma 8.5.4, Observation 8.5.1 and the milestones are elementary, and Theorem 8.5.2 rests on Donoho's polytope-neighborliness analysis. The platform has a related formalization of Wainwright's restricted nullspace property (Theorem 7.8 of High-Dimensional Statistics, namespace HighDimStat.SparseLinear), which fixes a support set rather than characterizing exactness for all -sparse vectors through the crosspolytope. A machine-checked proof of Theorem 8.5.2 with the constants and is, to our knowledge, not available anywhere; it would require substantial Gaussian and high-dimensional geometry infrastructure.
For the goal and milestones the difficulty is bookkeeping, not ideas: the scaling between a sparse solution and the boundary point , the case , and the fact that BP-exactness quantifies over all right-hand sides while the geometric side quantifies over boundary points of the crosspolytope.
Theorem 8.5.2 is of a different order. A union bound over the faces of dimension reduces it to bounding the probability that a random -dimensional subspace meets one cone nontrivially, and getting that probability small enough to beat the combinatorial factor with the stated numerical constants is the hard part. Rough asymptotic estimates do not give at .
Vectors are functions Fin n → ℝ (the book's indices become ) and matrices are Matrix (Fin m) (Fin n) ℝ. The -norm is written out as , since Mathlib's norm on Fin n → ℝ is the sup norm. The support is a Finset of indices. Optimality in (BP) and (BP′) is stated against every feasible point; no infimum is taken, so an empty or unbounded feasible set cannot create a spurious optimum. "Every or fewer columns" ranges over finsets of distinct column indices, column being Aᵀ j. The hypotheses and of Lemma 8.5.4 are kept as on the page, although the equivalence does not use them; is also the standing assumption of §8.5 needed for .
In Theorem 8.5.2 the random matrix has the product law of independent gaussianReal 0 1 entries, the constant is quantified before , and measurability of the BP-exact event is part of the conclusion, so the bound concerns a genuine probability rather than an outer measure.
A trivializing formalization is ruled out: BP-exactness requires uniqueness among all minimizers for every right-hand side, not just optimality of , and the crosspolytope condition is an equality of sets, not an inclusion that alone would satisfy.
All definitions live in one module (MatousekLP.SparseRecovery.BasisPursuit); the and support vocabulary is reusable for later sparse-recovery missions. Contributions are welcome on every milestone, on the goal, and on the infrastructure towards Theorem 8.5.2 (Gaussian measures on matrix spaces, measurability of the BP-exact event, the face structure of the crosspolytope).
A binary error-correcting code is a set of -bit words chosen so that the words stay distinguishable after a few bits have been corrupted in transmission. A code can correct any errors exactly when every two of its words differ in at least positions. The more words the code has, the more information each transmitted block carries. So the central quantitative question of coding theory is how large a code of given length and minimum distance can be. Codes are used in every technology that transmits or stores data, from disks and phones to deep-space probes.
In 1973 Philippe Delsarte showed that an upper bound on this maximum size is the optimum value of an explicit linear program (Delsarte, An algebraic approach to the association schemes of coding theory, Philips Res. Repts. Suppl. 10, 1973). The bound was far stronger than the classical volume argument and remains a standard tool. This mission formalizes the self-contained proof of the bound in §8.4 of Matoušek and Gärtner's textbook (Springer 2007). That proof follows Best, Brouwer, MacWilliams, Odlyzko and Sloane (IEEE Trans. Inform. Theory 24, 1978). The mission also covers the step of Delsarte's original argument that the book isolates as a lemma.
Timeline.
A word is , and a code is any set . The Hamming distance is the number of positions with . The weight is the number of ones in . The word is the entrywise sum modulo 2. For , the restricted distance counts only the differing positions that lie in .
A code has distance if for all distinct (Definition 8.4.1). The quantity is the maximum of over all codes with distance .
For the Krawtchouk numbers are
The distance distribution of a code is
The Delsarte linear program has variables . It maximizes subject to:
For Delsarte's original argument, is the matrix whose entry is when and otherwise. The weights are .
The goal is stated against every upper bound of the objective on the feasible set. No particular optimum value is fixed, so the statement covers every and at once.
The Delsarte bound turns an extremal problem over the subsets of the cube into a linear program with variables. For it gives , while the sphere-packing bound gives . Many entries of the standard code tables rest on this bound or its refinements. The positive semidefiniteness in Lemma 8.4.7 is the starting point of the semidefinite programming bounds of Schrijver and of later work. The same framework also underlies the linear programming bounds for spherical codes and sphere packings.
The theorem is classical and fully proved in the literature. Neither Mathlib nor this platform has a formal statement or proof of it. Mathlib has Hamming distance and binomial coefficients, but it has no , no Krawtchouk numbers and no LP bound for codes. This mission would produce the first formal statement and proof. It would also produce reusable identities on Krawtchouk sums and character sums over .
Two of the program's constraints are immediate once is defined: , and for . The difficulty lies in the Krawtchouk constraints. They do not follow from counting pairs at a single distance. They require a sign-weighted count over all words of weight , and the sum must then be regrouped by the distance of each pair. That regrouping identifies a count of words, split by how many ones they share with a fixed word, with the Krawtchouk number. Formally this is an exchange of finite sums together with a binomial counting identity, and the index bookkeeping, including the range , has to be exact.
The obvious attempt proves the inequality one distance class at a time. It fails because the individual terms have no sign. Only the whole sum is nonnegative.
Fin n → Bool, with bit as true. The book's positions become 0, …, n-1. Codes are Finsets of words, and is Mathlib's hammingDist.Finset.sup over the finite family of codes with distance . This family contains the empty code, so the maximum is attained.Fin (n+1) with no index shift. The constraints are imposed for , so they are vacuous for .Matrix.PosSemidef over .No trivialization. The goal is not stated as "" with a real supremum, which Lean would evaluate to on an empty or unbounded set. Its hypothesis ranges over upper bounds of a feasible program: is always feasible, so the hypothesis is never vacuous.
Contributions welcome. Useful lemmas include:
These are reusable for other LP and SDP bounds in coding theory.
Scheduling indivisible jobs on parallel machines to finish all of them as early as possible is a basic problem in operations research and in the theory of algorithms. In the unrelated machines model each job may take a different time on each machine, with no relation between the rows of the time table, as when machines of different types (black-and-white, duplex, colour copiers in the book's example) handle jobs of different kinds. Minimizing the makespan in this model is NP-hard, so the question is how close to the optimum a polynomial-time algorithm can get.
The gap between and for the general unrelated-machines problem has remained open since 1990; it is the standard example of LP rounding driven by the sparsity of basic solutions.
There are machines and jobs ; is the running time of job on machine . A schedule is a map assigning each job to one machine. The load of machine is , the makespan of is the largest load, and is the makespan of an optimal schedule, one whose makespan is at most that of every schedule.
For a real threshold , the linear program in the variables and is
Its optimal value is , with when is infeasible. The constraint matrix has one row per machine, one per job and one per pair with ; the column of carries in the row of machine , in the row of job , and in the row of the constraint if present. Assumption 8.3.1 on a solution is that the columns of belonging to its nonzero variables are linearly independent; basic feasible solutions satisfy it. The support graph of is the bipartite graph with .
Let minimize over all real and let be an optimal solution of satisfying Assumption 8.3.1. Then there is a schedule with for every job and
The theorem gives a polynomial-time 2-approximation for an NP-hard problem, and its proof isolates a reusable principle: a basic solution of an assignment-type LP has a support graph in which every subgraph has at most as many edges as vertices (a pseudoforest), so all but a matching's worth of the fractional assignment is already integral. The same sparsity argument underlies rounding results for the generalized assignment problem and for many later scheduling and allocation relaxations.
The result has been proved since 1990 and is textbook material. It is not formalized on Prove2Me or, to the maintainers' knowledge, in Mathlib. This mission produces a machine-checked version of the rounding theorem together with the counting lemma on basic solutions, the relaxation inequality , and the bound on the chosen threshold, each stated on shared definitions of the scheduling LP.
The obvious approach, rounding every job to the machine carrying the largest fraction of it, can overload a machine by many jobs at once and gives no constant factor. The bound needs two facts that are not visible from the LP value alone: that the support of a basic solution is sparse in the precise sense of Lemma 8.3.2, which has to be read off the linear independence of columns of the constraint matrix after deleting rows; and that the jobs left fractional can be matched injectively to machines, which requires a Hall-type condition derived from that sparsity. Relating linear independence of real column vectors to an edge count in a bipartite graph, and then producing a matching, is where the formal work lies.
A second subtlety is the threshold : the bound holds only because is chosen by minimizing over thresholds, and the relaxation at must be compared with the one at through optimal solutions of different linear programs.
Machines are Fin m, jobs are Fin n (0-based; the book's machines and jobs are disjoint index sets), running times form d : Matrix (Fin m) (Fin n) ℝ, and the standing hypothesis of §8.3 appears in every theorem. A schedule is a function Fin n → Fin m; the makespan is the supremum of the loads over the finite type Fin m, which is the maximum for . The optimum is the makespan of a schedule assumed optimal, never an infimum.
Optimal values of are never written as sInf: statements quantify over optimal solutions, i.e. feasible with for every feasible . The book's convention for infeasible is encoded by letting thresholds without an optimal solution impose no condition in the minimality hypothesis on , which reads for every real and every optimal solution of . The constraint matrix used in Assumption 8.3.1 has rows indexed by Fin m ⊕ Fin n ⊕ {(i, j) // T < d i j} and excludes the column of , as on p. 151.
"Efficiently construct" in Lemma 8.3.3 and "computes" in Theorem 8.3.4 are formalized by the property of the constructed schedule, not by its running time: every job goes to a machine with . This constraint is what rules out the trivializing formalization — "some schedule has makespan at most " is true of the optimal schedule itself and says nothing about the rounding.
A complete development needs: finite linear algebra (a linearly independent family of vectors supported on coordinates has at most members), Hall's marriage theorem (available in Mathlib as Finset.all_card_le_biUnion_card_iff_exists_injective), and the existence of an optimal solution of a feasible, bounded linear program (used to apply the minimality of at ). The counting lemma for basic solutions and the definitions of are reusable for other assignment relaxations. Proofs of any milestone, and alternative proofs of Lemma 8.3.3 by the direct pseudoforest argument of p. 153–154, are welcome.
Airlines, hotels and other capacity-constrained sellers decide, request by request, whether to sell a unit of a perishable resource now or hold it for a more valuable request later. In an airline network an itinerary uses seats on several flight legs at once, so the decision couples the legs. Bid-price controls are a widely used practical answer: each leg carries a threshold price, the bid price, and a request is accepted if and only if its fare covers the sum of the bid prices of the seats it uses. They are simple to store, to explain and to compute from linear programming duals (Simpson 1989 and Williamson 1992, as cited by Talluri and van Ryzin 1998, p. 1581).
Talluri and van Ryzin, An Analysis of Bid-Price Controls for Network Revenue Management, Management Science 44(11), 1998, asked whether this simplicity costs revenue. Their Proposition 1 shows that the optimal policy of the underlying dynamic program already compares each fare with an opportunity cost, which suggests that bid prices might be exactly optimal. Their §3.1 shows they are not: a two-leg, two-period instance in which the best bid-price control earns 10% less than the optimal policy. The same paper then proves (Theorem 1, a separate mission) that fixed bid prices are asymptotically optimal in large networks; the counterexample shows that this asymptotic statement cannot be sharpened to exact optimality.
A network has legs and itineraries; seats of leg are used by itinerary , , and is the -th column. The state is the vector of remaining capacities; selling itinerary moves it to . Time is counted backwards: period has periods to go.
In each period one request vector arrives: is a request for itinerary with revenue , and means no request. Requests lie in , where : at most one component is positive. The requests of different periods are independent, with laws concentrated on and with finite first moments.
A control chooses in each period a decision (reject, or sell one itinerary that fits), measurably in the request . Its expected revenue is
The optimal expected revenue solves the Bellman equations
A bid-price control (Definition 1) is given by real-valued bid prices for every leg, period and capacity, and accepts an arriving request for itinerary if and only if and
The instance of §3.1 has two legs with one seat each, the through itinerary and the local itineraries , , and two periods. In period 2 a $500 through request arrives with probability 0.4 and a $250 request for each local itinerary with probability 0.3; in period 1 a $500 through request arrives with probability 0.8, and nothing with probability 0.2.
In the §3.1 instance, from capacity with two periods to go,
where is the bid-price control with bid prices ; both maxima are attained. The goal fixes the paper's instance and its numbers exactly.
The result shows that the class of bid-price controls, the standard control class of network revenue management practice, does not contain an optimal policy in general, even though the optimal policy of Proposition 1 has a threshold form. The loss in the example is 10% of expected revenue, and it arises because the opportunity cost of a two-leg itinerary is not the sum of the opportunity costs of its legs. This is the negative half of the paper's analysis; the positive half is the asymptotic optimality of fixed bid prices (Theorem 1).
On the formal side, the mission builds a reusable finite-horizon model of network capacity control: request laws on , admissible Markov controls, their expected revenue, the Bellman value, and a proof that the Bellman value is the optimum over admissible controls (Proposition 1). The paper's argument for the counterexample is a few lines of inspection; formalizing it requires the upper bound over all admissible controls and the lower bound over all bid prices, including negative, time- and state-dependent ones. A search of the Prove2Me corpus (2026-09-25) found no network capacity-control model: the existing revenue-management items treat a single resource with discrete fare classes, and the existing finite-horizon dynamic-programming items assume a finite disturbance space, which excludes the request laws used here. As far as known, none of this has a machine-checked proof.
The upper bound ranges over every measurable admissible control, not over a finite menu; it needs Proposition 1, i.e. the verification theorem for a finite-horizon dynamic program with continuous state of the request and integrability under only finite first moments. The bid-price bound ranges over arbitrary real-valued bid-price functions of the period and the capacity, so the argument must show that every realizable pattern of period-2 decisions earns at most 400, not only that one pattern is unrealizable. Equation (5) is an identity between Bochner integrals under only finite first moments, so every integrand involved must be shown integrable rather than assumed so.
Legs are Fin m, itineraries Fin n, A : Fin m → Fin n → ℕ, capacities Fin m → ℕ, requests Fin n → ℝ, laws F : ℕ → Measure (Fin n → ℝ) indexed by time-to-go; expectations are Bochner integrals. A decision is Option (Fin n) (none is reject). Controls are Markov and may depend on the whole request vector; admissibility requires decisions in and measurability in the request. The request laws are probability measures concentrated on with integrable coordinates; the continuity of fare distributions assumed in §1 of the paper is not assumed, because Proposition 1 does not need it and the §3.1 instance has deterministic fares, which the paper itself notes (p. 1581). The paper's remark that a continuous perturbation gives the same counterexample is not formalized. Read literally, (1) and (4) set for every itinerary whose zero fare meets its threshold, which is not a unit vector; both are formalized as accepting only the arriving request (), at most one per period on . In (1), "" is read as , fewer seats on leg . " is finite" is stated as integrability of the Bellman integrands. Probabilities are exact rationals and fares exact reals. The goal cannot be discharged by restricting the bid prices (constant or nonnegative ones only) or the competing controls (a finite list): the Lean statement quantifies over all real-valued bid-price functions and all admissible controls, and it asserts attainment of both maxima, not only the strict inequality .
Reusable parts: the model definitions (bid-price controls, admissible controls, the Bellman value) and Proposition 1 as a verification theorem for finite-horizon capacity control. Contributions are welcome on any milestone; Proposition 1 and equation (5) are general and independent of the instance.
A two-player zero-sum game models any situation in which one party's gain is exactly the other party's loss: a military allocation in the spirit of Colonel Blotto, a sealed-bid contest, rock–paper–scissors. The central question is what each player should do when the opponent is also reasoning about them. John von Neumann answered it in 1928 with the minimax theorem (von Neumann 1928): each player has a strategy guaranteeing the same number, the value of the game, whatever the opponent does. The theorem underlies modern game theory, robust decision making, and the analysis of online learning algorithms, where regret bounds are routinely derived from it.
Section 8.1 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer 2007) presents the theorem as an application of linear programming duality. This mission is the sixth of a series formalizing the capstone results of the book.
Alice has pure strategies and Bob has . A real payoff matrix records Alice's gain, and Bob's loss, when Alice plays her th and Bob his th pure strategy. A mixed strategy of Alice is a probability vector , , ; a mixed strategy of Bob is a probability vector . When the players randomize independently, Alice's expected payoff is
The worst-case payoffs are
over mixed strategies. A mixed strategy of Bob is a best response against if it minimizes ; a mixed strategy of Alice is a best response against if it maximizes it. A pair is a mixed Nash equilibrium (Definition 8.1.1) if each is a best response against the other. Alice's is worst-case optimal if ; Bob's is worst-case optimal if .
The proof in the book passes through three linear programs: the dual of (8.1), which for a fixed maximizes subject to ; program (8.2), the same with as variables subject to , ; and program (8.4), which minimizes subject to , , .
For every payoff matrix with : worst-case optimal mixed strategies exist for both players; for any worst-case optimal of Alice and of Bob, the pair is a mixed Nash equilibrium; and there is a single number , the value of the game, with
for every such pair. The third clause is what distinguishes the theorem from the existence of some saddle point.
The theorem gives a complete prescription for zero-sum play: a worst-case optimal strategy secures at least the value against any opponent, and a worst-case optimal opponent holds the player to at most the value, so both players can announce their strategies in advance without loss. With Lemma 8.1.2(ii) it yields a characterization: a pair of mixed strategies is a Nash equilibrium if and only if both are worst-case optimal. The minimax equality is used downstream in online learning (regret-to-value arguments), in robust optimization, and in Yao's principle for randomized algorithms.
The mathematics is classical and proved; what this mission adds is a machine-checked version in the book's own formulation. The platform already has AGT.zero_sum_minimax (Algorithmic Game Theory I), which proves the existence of a saddle point, and the general FamousTheorems.sion_minimax_theorem. Neither states that every pair of worst-case optimal strategies is an equilibrium with a common value, and neither exhibits the LP route: the dual of (8.1), the programs (8.2) and (8.4), and their duality. The mission records that route statement by statement, so that it can be reused as a worked instance of LP duality.
Lemma 8.1.2 is routine; the entire content is the reverse inequality . The obvious attack, maximizing directly, fails because is a minimum of linear functions and hence not linear, so its maximization is not a linear program as written. The obstacle is removed only by an appeal to LP duality in the proof, together with the facts that the simplices are nonempty and compact, and that the relevant programs are feasible and bounded so that optima exist. None of this is supplied by the pure-strategy structure of the game: pure Nash equilibria need not exist (rock–paper–scissors has none).
Pure strategies are indexed by Fin m and Fin n, with the book's standing assumption carried as hypotheses 1 ≤ m, 1 ≤ n by every theorem; the book's indices become . Mixed strategies are Mathlib's stdSimplex ℝ (Fin m), the payoff is x ⬝ᵥ (M *ᵥ y). is the real sInf and the real sSup of the payoffs over the opponent's simplex; milestone 1 states that these are attained. A mixed Nash equilibrium is defined in the verbal form of Definition 8.1.1 (mutual best responses). Worst-case optimality is defined against all mixed strategies, never as a saddle-point condition, so the goal is not circular with Lemma 8.1.2(iii). LP optimality is stated as "feasible and at least as good as every feasible point", so no supremum over a possibly empty or unbounded feasible set is used.
The book's clause that worst-case optimal strategies "can be efficiently computed by linear programming" is algorithmic and is not part of the formal statement; there is no complexity model. A goal asserting only the existence of worst-case optimal strategies, or only the existence of some equilibrium, would drop the theorem's third clause and is ruled out: the common value is quantified before all pairs of worst-case optimal strategies.
A complete development needs compactness of the standard simplex, continuity of the bilinear payoff, and a strong duality theorem for linear programs in the form of the programs (8.2)/(8.4); the latter is reusable across the whole series. Proofs by other routes (Sion's theorem, a separating hyperplane argument, fixed points) are welcome for the goal; the LP milestones stand on their own as statements about the programs.
Airlines, hotels and rental-car firms sell a fixed, perishable capacity to customers who arrive over time and pay different prices. In an airline network, one ticket for an origin–destination itinerary consumes seats on several flight legs at once, so accepting a cheap connecting passenger today can displace a more valuable request tomorrow on any of those legs. The exact optimal accept/reject rule is a dynamic program whose state is the whole vector of remaining leg capacities, which is intractable at airline scale.
Bid-price control is the standard practical answer. Each leg carries a price , and a request for itinerary is accepted only if its revenue exceeds the sum of the bid prices of the seats it uses. Talluri and van Ryzin (Management Science 44(11), 1998) gave the first rigorous analysis of this scheme. They showed that bid prices are not optimal in general, the subject of a separate mission in this series. They also showed that one fixed vector of bid prices, obtained from a convex upper-bound problem, is asymptotically optimal when capacity and demand are scaled up together. This mission targets that positive result, Theorem 1 of the paper. It is one of the results most often cited to justify the use of bid prices and of deterministic or fluid upper bounds in revenue management; see Talluri and van Ryzin, The Theory and Practice of Revenue Management (Springer, 2004), Ch. 3.
A network has legs and itineraries. Itinerary uses seats of leg ; and is its -th column. The state is the vector of remaining capacities, and time is counted backwards: period has periods to go, and the horizon is .
In each period one request vector arrives. It lies in : at most one component is positive, is a request for itinerary with revenue , and means no request. The are independent with laws concentrated on . Each marginal is continuous on , and each has a finite mean. These are the paper's standing assumptions. For the asymptotic result the revenues are also bounded: almost surely.
The optimal expected revenue solves the Bellman equations
For bid prices write and define the relaxed value
The convex program has an optimal solution .
The fixed-bid-price heuristic uses throughout the horizon. It accepts a request for itinerary with revenue if and only if the remaining capacity suffices () and . The -scaled problem, for an integer , has capacity , horizon and request laws . Each original period is thus split into independent copies. Write for its optimal expected revenue and for the expected revenue of the heuristic with the bid prices of the original problem.
There is a constant , depending on the instance but not on , such that for every integer
This is the paper's , multiplied out.
In the order the paper's argument uses them:
The goal leaves unspecified. The explicit bound (milestone 10), together with (13), identifies one admissible value when .
Theorem 1 says that the whole value of dynamic, state-dependent control over a static price-per-leg rule vanishes relative to revenue as the system grows: the loss is against revenues of order . It justifies computing bid prices once from a convex (or, in later work, linear) upper-bound problem instead of solving the network dynamic program. The same fluid-scaling argument underlies a large later literature on asymptotically optimal policies in network revenue management and online resource allocation. That literature includes re-solving heuristics and the choice-based deterministic linear program (Liu and van Ryzin, M&SOM 2008).
The result has a complete published proof. What this mission adds is a machine-checked version. It includes the network Bellman recursion, the relaxation bound, a coupling argument between a capacitated and an uncapacitated system on the product space of request paths, and a second-moment overflow estimate. Two statements on the printed page are wrong as written and appear here in corrected form (see Formalization scope). A formal proof settles that the theorem survives both corrections. No machine-checked proof of this theorem, or of the fluid upper bound for network revenue management, is known.
The optimal value is defined by a recursion over the full capacity vector and has no closed form; the only access to it is an upper bound. The heuristic's revenue depends on the random time at which each leg runs out, which couples all legs and all periods, so it cannot be computed period by period either. The obvious approach, comparing both values period by period through their recursions, fails for exactly this reason: neither side decomposes over time. The two sides must instead be connected through a third object, the relaxed value , which is explicit but relies on the requests' distributional structure (at most one request per period, and continuous marginals, which make the optimality conditions of the convex program hold). The step from an upper bound on to a lower bound on has to hold path by path, including for group requests that take several seats of one leg. On the probabilistic side, the seat counts of one period are indicators of mutually exclusive events, so their variances do not simply add.
Legs are Fin m, itineraries Fin n, the seat matrix is A : Fin m → Fin n → ℕ and capacities are Fin m → ℕ. A request law is a Measure (Fin n → ℝ), and IsRequestLaw bundles the standing assumptions:
The bound a.s. is a separate hypothesis wherever the paper uses it. Laws are indexed by time-to-go. is defined by the Bellman recursion, with the maximum over the finite control set taken for each realized request; capacity subtraction in ℕ occurs only when . is the closed form (8), which the paper derives from the relaxed control problem (7). An optimal is a hypothesis ( and for all ), not an sInf. The scaled laws use in ℕ. is the integral of the heuristic's pathwise revenue, with strict threshold and capacity check, against Measure.pi over the periods, and is a random variable on the same space. is the closed form .
Corrections to the printed page:
The coupling bound and the mean/variance statement are stated at an optimal of (9), as on the page. The ratio of Theorem 1 is multiplied out because may be , and is quantified before . A formalization that replaced by an easier quantity, or by the uncapacitated system's revenue, would make the goal trivial or different; the definitions here are the Bellman optimum and the capacity-respecting heuristic.
A complete development needs Bochner integrals against product measures, independence of coordinates under Measure.pi, variance of sums, one-sided derivatives of , and first-order optimality for a convex function on the nonnegative orthant. The Bellman-recursion and coupling infrastructure is reusable for other network revenue management results. Proofs of individual milestones are welcome independently.
Every finite algorithm for linear programming rests on one structural fact: if a linear program has an optimum at all, it has one at a point singled out by finitely many linear conditions. The simplex method walks between such points, and exact complexity analyses, sensitivity analysis and integrality arguments all start from them. Chapter 4 of J. Matoušek and B. Gärtner, Understanding and Using Linear Programming (Springer, 2007, DOI 10.1007/978-3-540-30717-4), establishes this fact for linear programs in equational form, in the definitions that the rest of the book (the simplex method of Chapter 5, duality in Chapter 6, the applications in Chapter 8) uses.
This mission is the second of a series formalizing that book. It fixes the book's notion of a basic feasible solution and of a vertex, and targets the theorem that optimal solutions exist whenever the program is feasible and bounded, and can then be chosen basic.
A linear program in equational form is
where is a real matrix, , , and means every coordinate of is nonnegative. A feasible solution is an satisfying both constraints; the set of them is . An optimal solution is a feasible with for every feasible . The objective is bounded from above if some real satisfies for all feasible .
Throughout Section 4.2 the book assumes that has columns and rank (its rows are linearly independent). For , denotes the matrix formed by the columns of with indices in . A basis is an -element set for which is nonsingular, i.e. its columns are linearly independent. A basic feasible solution is a feasible for which some basis has for every .
A point is a vertex of if and some nonzero satisfies for every : is the unique maximizer over of a nonzero linear function.
For of rank with ,
Both parts are one theorem, as in the book. Part (i) says optimal solutions fail to exist only for the two obvious reasons, infeasibility and unboundedness; part (ii) says an optimum can always be found among basic feasible solutions.
Theorem 4.2.3 gives a finite, if impractical, algorithm for linear programming: enumerate the at most sets , solve , and keep the best nonnegative solution. It is the correctness backbone of the simplex method, which visits basic feasible solutions in a smarter order, and it is the source of the book's claim that a feasible and bounded linear program has an optimal solution. Theorem 4.4.1 identifies this algebraic notion with the geometric corners of the feasible polyhedron, which is what makes statements such as "the LP relaxation has an integral vertex" in later chapters meaningful.
All of these results are classical and fully proved in the book. The value of formalizing them here is the definition layer: later missions of this series (Bland's rule, the central path, the scheduling application) state their results about bases and basic feasible solutions in exactly these definitions, and a proved Theorem 4.2.3 in this form lets them import the existence of an optimal basic solution instead of re-deriving it. Related facts are already machine-checked on Prove2Me in the formulation of Bertsimas and Tsitsiklis (Introduction to Linear Optimization I and II: minimization over polyhedra , extreme points, basic solutions as active linearly independent constraints). Those statements concern a different presentation of the program and a different notion of basic solution; connecting them to the equational-form statements here is itself a welcome contribution.
The obvious argument for part (i), "a continuous function on a closed set bounded above attains its supremum", fails: the feasible set is usually unbounded, and a linear function bounded above on an unbounded closed convex set need not obviously attain its supremum without using the polyhedral structure. The existence of an optimum is exactly the nontrivial content of part (i); compactness is not available.
For milestone 1, the delicate direction is the converse: a set of linearly independent columns indexed by must be completed to an -element basis, which requires the rank- assumption. For Theorem 4.4.1, the direction from vertex to basic feasible solution is not local: a vertex is defined by an optimization property, while basicness is a statement about the support of the point.
All items live in the namespace MatousekLP.BFS and share one definition module, MatousekLP.BFS.EquationalForm. Conventions:
Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ; the book's indices are 0, …, n-1;A *ᵥ x = b, is 0 ≤ x (pointwise), is c ⬝ᵥ x;Finset (Fin n); " nonsingular" is linear independence over of the family of columns of indexed by the elements of , together with B.card = m;m ≤ n and A.rank = m on every theorem;Set.extremePoints; the book's remark on p. 55 that the two coincide is not used as a definition;A formalization in which "optimal" were defined through sSup of the objective over the feasible set would make part (ii) trivially true or false on unbounded programs; the definitions here rule that out. Dropping the rank hypothesis would make part (ii) false (no basis exists when the rows are dependent), so it is not optional.
Reusable infrastructure: the column-restriction and basis vocabulary, the support set , and the extension of a linearly independent set of columns to a basis of the column space are needed again in the simplex chapter. Proofs of any milestone, and bridges to Mathlib's Set.extremePoints or to the Bertsimas–Tsitsiklis statements on the platform, are welcome.