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.
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?
Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) is the standard introductory text of the field. Its Chapter 3 sets up the model that the rest of Part I works in: the finite Markov decision process (MDP), the value functions of a policy, and the Bellman equations that relate the value of a state to the values of its successors. Section 3.6 then states the fact every planning and control method of the book relies on: in a finite MDP there is an optimal policy, its value is the unique solution of a system of nonlinear equations, and a policy that acts greedily with respect to that solution is optimal. Dynamic programming (Chapter 4), Monte Carlo control (Chapter 5), Sarsa and Q-learning (Chapter 6) are all methods for solving the Bellman optimality equation; their correctness statements presuppose that it has exactly one solution and that it identifies optimal behaviour.
The book is deliberately informal ("we chose not to produce a rigorous formal treatment", p. xiii): §3.6 asserts these facts without proof. The results themselves are classical, going back to Bellman (1957), Howard (1960) and Blackwell (1965); a textbook proof for discounted finite MDPs is in Puterman, Markov Decision Processes (Wiley, 1994), Chapter 6.
A finite MDP has a finite set of states , a finite nonempty set of actions , a finite set of rewards , and dynamics
Eqs. (3.2)–(3.3). From one derives and , Eqs. (3.4)–(3.5).
A policy gives a probability of each action in each state. Fix a discount rate . The return of a reward sequence is (3.8). The state-value function and action-value function of are the expected returns
In the Lean development these are stateValue M γ π s and actionValue M γ π s a, computed as from the transition matrix and the expected reward of the Markov chain the policy induces. A policy is optimal (IsOptimalPolicy) if for every policy and every state . The optimal value functions are
optimalValue and optimalActionValue, with the maximum over all stochastic policies.
For every finite MDP and :
The goal is what turns "find a good policy" into "solve a system of equations". Parts 3 and 4 identify with the unique solution of (3.19), so any procedure that finds a solution of (3.19) has found ; part 5 converts into an optimal policy by a one-step search. Parts 1 and 2 say that the book's definition (3.15) makes sense: a single policy is simultaneously best at every state, so "the optimal value function" is well defined and shared by all optimal policies. Chapter 4's policy iteration and value iteration, and the fixed points of Q-learning, are statements about this equation. Exercises 3.18 and 3.19 are used, by number, in the proof of the policy gradient theorem (p. 325).
The mathematics is classical and proved in many texts; what is missing is a machine-checked version in the book's own model. Platform relatives exist in different models: FoundationsML.ReinforcementLearning.bellman_equations_unique_solution (uniqueness for a fixed policy, with an expected-reward kernel instead of ), BertsekasDP.discounted_main_theorem (cost minimization over deterministic stationary policies), BanditAlgorithm.mdp_discounted_bellman_solution (existence of a solution with a greedy deterministic policy, rewards in ) and FoundationsRL.RLBasics.bellman_optimality (finite horizon). None of them states the book's result: the four-argument dynamics, stochastic policies, the maximum over all of them, uniqueness of the solution of (3.19), and optimality of every policy supported on greedy actions. This mission produces that statement and, with it, a vocabulary of finite-MDP definitions that the later missions of the series reuse.
The book's derivation of (3.19) (p. 63) starts from with a policy that is optimal at every state at once. The existence of such a policy is the substance of the goal, and it does not follow from the definition: (3.15) takes a separate maximum at each state, and a priori the maximizing policy could depend on the state. Uniqueness for (3.19) is likewise not a consequence of linear algebra, as it is for (3.14): the equation is nonlinear because of the maximum. The fixed point must be related to the value of an actual policy, and every policy's value must be bounded above by it.
S and A are finite types with A nonempty (without an action, is undefined). One action set serves every state, as the book's footnote 3 (p. 48) allows. Rewards form a finite set M.R : Finset ℝ and the dynamics are the four-argument M.p s a s' r with the normalization (3.3).MDP, Policy, trans, expReward, policyTrans, policyReward, stateValue, actionValue, optimalValue, optimalActionValue, IsOptimalPolicy) follow the conventions shared by the whole series and are meant to be merged with the finite-MDP layers of the later chapters. Lemmas on summability of the value series, the Bellman operator as a -contraction in the sup norm, and the Markov-chain identities for are welcome as separate contributions.Thompson Sampling (TS) is the oldest heuristic for the stochastic multi-armed bandit problem: it was proposed by Thompson in 1933 (Biometrika 25) and is used in practice for online advertising and recommendation, where it often performs as well as or better than upper-confidence-bound methods (Chapelle and Li, NIPS 2011; Scott 2010). Until 2012 its theoretical guarantees for the frequentist regret were weak: earlier analyses gave only regret in time (Granmo 2010; May, Korda, Lee and Leslie 2011).
Agrawal and Goyal, Analysis of Thompson Sampling for the Multi-armed Bandit Problem (arXiv:1111.1797v3, COLT 2012), gave the first logarithmic finite-time bound on the expected regret of TS. This mission formalizes their two-armed result, Theorem 1. A companion mission covers the -armed bound, Theorem 2.
Timeline. Lai and Robbins (1985) proved that every consistent algorithm has regret at least . Auer, Cesa-Bianchi and Fischer (2002) gave UCB1 with an finite-time bound. Agrawal and Goyal (2012) proved for two-armed TS. Kaufmann, Korda and Munos (ALT 2012) and Agrawal and Goyal (AISTATS 2013) later proved asymptotically optimal bounds for Bernoulli TS.
There are two arms. Arm has a fixed, unknown reward distribution supported in , with mean . Plays of an arm give i.i.d. rewards, independent of the other arm. Arm 1 is the unique optimal arm, , and is the gap.
Thompson Sampling for general stochastic bandits (Algorithm 2 of the paper) keeps, for each arm , a success count and a failure count , both starting at . In each round it
is the number of plays of arm before round . The expected regret in time is
the expectation being over the rewards and the algorithm's randomness.
The analysis uses the Beta cdf , the binomial cdf , and the random variable : the number of independent draws made before one exceeds .
There is an absolute constant such that for every two-armed instance with rewards in and , and every ,
The constant is not fixed numerically: the paper states the theorem in form (footnote 1), and the explicit display it reports on p. 8, , is not the formal claim.
The result. Theorem 1 shows that TS, a randomized Bayesian heuristic with no explicit confidence bonus, has regret logarithmic in on every two-armed instance, matching the order in of the Lai–Robbins lower bound. The proof introduced a way to control the optimal arm's waiting time between plays through the Beta–Binomial duality, and later analyses of TS reuse that device.
Formalizing it. The result is proved on paper and has no machine-checked proof that we know of. The platform's existing TS results concern Gaussian TS (Lattimore and Szepesvári, Ch. 36) and Bayesian regret, which are different algorithms or regret notions. A formalization adds a reusable Lean model of Algorithm 2 on -valued rewards, Beta–Binomial facts (Fact 1, Lemma 1), a binomial-median theorem, and binomial Hoeffding bounds. It also produces a proof with a constant that has been checked, since the printed constants contain an arithmetic slip.
The standard UCB argument does not transfer to TS. For UCB, the optimal arm's index exceeds its mean with high probability however often the arm has been played, because the exploration bonus is deterministic; the analysis then only has to count plays of the suboptimal arm until its own index concentrates, after plays. Under TS the optimal arm's sample is random and, if the arm has been played rarely or its early rewards were poor, it falls below with constant probability. The optimal arm may then wait a long, random time between plays, and the length of that wait depends on the arm's posterior, which in turn depends on how long it has waited. Counting plays of the suboptimal arm with a union bound over rounds, under the assumption that the optimal arm is already concentrated, therefore does not work; controlling these waiting times is the central difficulty and is where the dependence enters.
StochasticBandit 2 (a probability measure on per arm, mean banditArmMean), with the hypothesis that each reward law gives mass to . Lean arm 0 is the paper's arm 1 and Lean arm 1 the paper's arm 2. Lean rounds are indexed from .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.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.
Many stochastic and nondifferentiable optimization problems are not solved by minimizing their true objective directly: may be nonsmooth, an expectation that cannot be evaluated, or only approximately known. A standard remedy replaces by a sequence of "good" approximations (smoothed versions, sample averages, perturbations) that converge to , and runs one step of a descent method on the current approximation at every iteration. Approximation and optimization then proceed simultaneously. More generally, in nonstationary optimization the objective and the feasible set change with the iteration number , and the iterates are required to follow the time path of the optimal solutions,
Such procedures are essentially nonmonotone: a step on gives no guarantee of decrease of for , nor of . Their convergence therefore cannot be proved by the usual monotone Lyapunov argument. Section 6.4 of Yu. Ermoliev's chapter "Stochastic Quasigradient Methods" in Ermoliev & Wets (eds.), Numerical Techniques for Stochastic Optimization (Springer 1988), gives the basic deterministic convergence theorem for this setting (Theorem 6.3) and the convergence criterion for nonmonotone sequences on which its proof rests (Theorem 6.4, taken from Ermoliev's 1976 monograph; the chapter compares its conditions with Zangwill's necessary and sufficient convergence conditions).
Timeline, as recorded in the chapter's bibliography (pp. 180–181): Ermoliev and Nurminski introduced limit extremal problems, in which and both converge ("Limit extremal problems", Kibernetika 1973, [14]); Nurminski gave convergence conditions for stochastic programming algorithms (Kibernetika 1973, [11]); Gupal treated time-varying functions (Kibernetika 1974, [15]); Ermoliev's monograph Stochastic Programming Methods (Nauka, 1976, [5]) contains the criterion stated here as Theorem 6.4 (p. 181); Nurminski formulated the general problem of nonstationary optimization (Kibernetika 1977, [16]); and Gaivoronski proved convergence of stochastic nonstationary procedures (Kibernetika 1978, [19]), the source of the chapter's Theorem 6.5.
Throughout, points are vectors of with the Euclidean norm and inner product .
with step sizes .
Let and be convex continuous on , a nonempty convex compact set, uniformly on , , , and . Then the iterates of (6.41) satisfy
The statement fixes no rate and no constant: only the qualitative limit, which is what the book proves.
Theorem 6.3 is the prototype of the convergence results for simultaneous optimization and approximation. It covers smoothing schemes in which is replaced by with a vanishing perturbation (the chapter's (6.39)–(6.40)), penalty and regularization sequences, and the deterministic skeleton of stochastic nonstationary methods such as Theorem 6.5. Theorem 6.4 is reusable well beyond this mission: it is a general tool for proving that accumulation points of a nonmonotone algorithm are solutions; the chapter introduces it as the tool for "essentially nonmonotonic solution procedures" in general.
Both results are classical and proved (Theorem 6.3 in the chapter itself, Theorem 6.4 in Ermoliev's 1976 monograph, whose proof the chapter cites but does not reproduce). No machine-checked proof of either is known to the platform's catalogue (searches for nonstationary optimization, Zangwill-type criteria and nonmonotone convergence return no match). The formalization adds a Lean statement and proof of a nonmonotone convergence criterion, a Lean proof of convergence for projected subgradient steps on a changing objective, and reusable facts about Euclidean projection onto a convex compact set.
The obvious argument for projected subgradient methods tracks and shows that it decreases whenever is far from . Here that argument fails at two points. First, the subgradient is taken on , not on , so the decrease of holds only up to an error controlled by , and only while the iterate stays away from ; near , may increase. Second, a decrease of over each excursion does not by itself exclude "cycling": the sequence may visit every neighbourhood of a point infinitely often. Theorem 6.4 is formulated in terms of exit times and subsequences rather than single steps for this reason, and its hypothesis that takes only countably many values on is what separates it from a monotone-descent statement.
EuclideanSpace ℝ (Fin n); sequences are indexed by ℕ from as in the book. The iteration (6.41) is a hypothesis on a given sequence, x (s+1) = projX X (x s - ρ s • g s), with a given selection of subgradients g s; the subgradient inequality is required on all of , and , are convex and continuous on all of .projX X y is a minimizer of over (junk value when none exists; every statement assumes nonempty, closed and convex). optimalSet f X is the set of minimizers of on ; is Metric.infDist · X* ^ 2.sInf (f '' X); is divergence of the partial sums.projX (existence, uniqueness, nonexpansiveness, the obtuse-angle characterization), a proof of Theorem 6.4, and the two proof steps on pp. 155–156.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 third mission of the series on Assumptions of Physics by G. Carcassi and C. A. Aidala (book, v3.0, 2025), formalizing the order-theoretic core of Part II, Chapter 3, "Properties and quantities". The chapter explains when the possibilities of an experiment can be labelled by numbers: a domain can be described by a quantity exactly when its possibilities already carry a linear order whose order topology is the natural topology. It then shows that integer-valued quantities correspond to sparse orders and decidable domains, and real-valued quantities to dense, complete, separable orders. The mission imports the definitions of mission I (Assumptions of Physics I), which must be launched first.
For an experimental domain with possibilities and natural topology (mission I), a property with values in a topological space fully characterizes if it is a homeomorphism . A quantity is a property whose value space is linearly ordered and carries the order topology. A linear order on is a natural order if its order topology equals . A linear order is sparse if every chain between two elements is finite and dense if between any two elements there is an infinite chain; it is complete if every non-empty bounded subset has a supremum.
These results say that numerical labels are not added to experimental domains from outside: an integer or real quantity can be assigned only when the domain already has the corresponding order structure, and that order is fixed by narrowness of verifiable statements. Theorem 3.51 is a classical characterization of real intervals that the book takes without proof. The results are proved informally in the book (3.51 is only sketched there); no machine-checked formalization of the domain-level statements is known to the drafters.
Theorem 3.9 needs transport of a linear order along a homeomorphism and the fact that order isomorphisms are homeomorphisms of order topologies. Theorem 3.51 needs the uniqueness of Dedekind completions of a countable dense order and must handle every kind of endpoint behaviour of a contiguous subset of . Proposition 3.46 must cover finite as well as infinite domains: the book's proof uses a bijection with , which exists only for countably infinite possibility sets.
Quantities are types Q with Mathlib's LinearOrder, TopologicalSpace and OrderTopology; full characterization is Nonempty (D.Possibility ≃ₜ Q); a natural order is a LinearOrder structure on D.Possibility whose Preorder.topology equals the natural topology. "Contiguous subset" is Set.OrdConnected. For continuous quantities the subset carries its own order topology, as in Definitions 3.6 and 3.52. In Theorems 3.44 and 3.46 the value type ranges over Type, which is enough because sparse orders are countable. Sections 3.3 and 3.6 (references and their ordering, statement (3) of Theorems 3.44 and 3.53, Theorem 3.38) are left for a later mission: they need a separate formal theory of references.
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.
Resource-constrained project scheduling asks for start times of the activities of a project so that prescribed time lags between activities are respected and, at every moment, the activities in progress do not require more of any renewable resource (staff, machines, reactors) than is available. When the time lags include maximum time lags (deadlines relative to other activities), even finding a feasible schedule is NP-hard, and the feasible region is in general neither convex nor connected. Branch-and-bound methods for this problem (the problem in the notation of Neumann, Schwindt & Zimmermann) do not search over schedules directly. They search over strict orders of the activities, that is, over sets of precedence constraints " starts after has finished".
This mission formalizes the theory behind that search, as developed by Bartusch, Möhring & Radermacher (1988) and presented in §2.3 of Neumann, Schwindt & Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003). Its goal, Theorem 2.3.10, says when a strict order resolves every resource conflict.
A project has activities , where and are fictitious activities marking the project's start and completion and are the real activities (). Activity has duration , with and for real activities. Time lags are encoded in the project network : an arc with integer weight imposes . The book's standing assumptions give, for every node , a path from to of nonnegative length and a path from to of length at least .
A schedule is a vector with and . It is time-feasible if for all arcs. The set of time-feasible schedules is .
Each renewable resource has a capacity , and activity uses units of it while in progress, with . The active set at time is , and is resource-feasible if for all and all . The feasible region consists of the schedules that are both time-feasible and resource-feasible.
A strict order is an asymmetric, transitive relation. Its order polyhedron is
is time-feasible if , and feasible if moreover . The order network adds to , for each , an arc of weight , or raises the weight of an existing arc to . A schedule induces the strict order .
A set is forbidden if for some resource . It is a minimal forbidden set if no proper subset of it is forbidden. denotes the set of minimal forbidden sets.
For every time-feasible strict order ,
Theorem 2.3.10 turns the feasibility of a strict order, which is a statement about infinitely many schedules and all times , into a finite check: one longest-path computation in for each minimal forbidden set. Together with Proposition 2.3.3 and the structural Theorem 2.3.7, it shows that is a finite union of polyhedra indexed by feasible strict orders. This justifies the enumeration schemes of Chapter 2 of the book (branching on the pairs that break up a minimal forbidden set) and the notions of active and stable schedules developed in later sections.
All results in this mission are proved in the literature. For the resource-feasibility criterion, the book cites Bartusch et al. (1988) instead of proving it. To our knowledge, none of these results has been machine-checked. A formal development would give a verified foundation for the order-based description of the feasible region, on which later missions of this series (active schedules, delaying modes, stable schedules) build.
The sufficiency half of the goal is short once the criterion is available: a path of length in forces on the whole order polyhedron. The necessity half carries the content. If for some minimal forbidden set no path in between elements of reaches the required length, one must construct a schedule in in which all activities of are simultaneously in progress. This means adding the reverse constraints for all to the temporal system without creating a cycle of positive length, while keeping and . The obvious reading "no single arc gives a precedence, so they can overlap" fails because maximum time lags combine into long paths through activities outside . The standing assumption that every node is reachable from by a path of nonnegative length is needed here: without it the equivalence is false.
Fin (n + 2): 0 is the project start and Fin.last (n + 1) the project completion. Durations and resource data are natural numbers, arc weights are integers, and start times are real numbers.Finset (Fin (n+2) × Fin (n+2)), required to be asymmetric and transitive.Project.StandingAssumptions, which is a hypothesis of every theorem: ; and otherwise; no loops; and ; and the two path conditions of p. 8.Minimal, taken among forbidden sets and among feasible strict orders respectively.Network. Contributions of this general lemma layer are welcome.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.
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.
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.
Almost every model in queueing theory is analysed through a Markov chain. The number of customers in an M/M/c queue is a continuous-time birth–death chain; the number left behind by departing customers of an M/G/1 queue is a discrete-parameter chain on (the imbedded Markov chain); networks of queues are chains on vectors of queue lengths. Before any steady-state formula (Erlang's formulas, the Pollaczek–Khintchine formula, product forms) can be used, one has to know that the chain has a steady state at all: that it is positive recurrent, so that a stationary distribution exists and equals the limiting distribution.
Chapter 1 of Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, DOI 10.1002/9781118625651), collects the two ingredients the rest of the book stands on: the Poisson process with its exponential interarrival times (§§1.7–1.8), and the classification theory of discrete-parameter Markov chains (§1.9), ending with Foster's criterion (Theorem 1.2), a sufficient condition for positive recurrence in terms of a drift inequality. The criterion goes back to F. G. Foster, On the stochastic matrices associated with certain queuing processes, Ann. Math. Statist. 24 (1953) (DOI 10.1214/aoms/1177728976), and is the ancestor of the Foster–Lyapunov method used for stability of queueing networks and stochastic systems.
This mission is the first of a series formalizing the book chapter by chapter.
A homogeneous discrete-parameter Markov chain on is given by a transition matrix with and for every . The -step transition probabilities are the entries of .
The first-passage probability is the probability that the chain started in enters for the first time at step ; for it is the probability of first return at step . The return probability is and the mean recurrence time is . A state is positive recurrent if and ; the chain is positive recurrent if every state is.
The chain is irreducible if for every pair of states some is positive, and aperiodic if for every state the greatest common divisor of is . A stationary distribution is a probability vector with , i.e. for every .
For the Poisson part, are independent interarrival times, each exponentially distributed with rate ; the arrival epochs are , and counts the arrivals in .
An irreducible, aperiodic chain is positive recurrent if there exist with
Foster's criterion reduces positive recurrence, a statement about return times, to exhibiting one test function with negative drift outside a single state. In the book it is the tool that establishes the existence of steady state for imbedded chains of the M/G/1 and G/M/1 queues (Chapter 5); its generalizations are the standard stability proofs for queueing networks. Theorem 1.1 then supplies what positive recurrence buys: the stationary distribution exists, is unique, equals , and is the limit of the transition probabilities. The Poisson results justify the "Markovian" arrivals and services of Chapters 2–4.
All of these results are classical and proved in the literature; the book states Theorems 1.1 and 1.2 without proof. The Prove2Me platform already holds machine-checked versions of related Markov chain theorems in other missions (Levin–Peres–Wilmer's and Durrett's countable-chain convergence theorems), stated with different definitions and hypotheses. What this mission adds is a formal development in the book's own terms — first-passage probabilities , mean recurrence times , gcd periodicity — on which the later missions of the series (imbedded chains, birth–death processes) can build, together with a formal proof of Foster's criterion, which is not on the platform.
For Foster's criterion the natural first step, taking expectations of the drift inequality along the chain, only shows that the expected value of decreases while the chain stays away from . Turning that into a bound on the expected return time to requires an optional-stopping or telescoping argument over a random time, with the value possibly unbounded, and a separate argument that positive recurrence of state propagates to all states of an irreducible chain. The book's hypotheses include aperiodicity, which the argument does not use.
For Theorem 1.1, identifying the stationary distribution with requires relating the matrix powers to the first-passage probabilities (a renewal decomposition), and uniqueness over countably many states needs care with infinite sums. For the Poisson results, the difficulty is measure-theoretic: the distribution of the sum of exponential variables, and conditioning on the event for the order-statistics property.
States are natural numbers; the transition matrix is a real function with nonnegative entries and rows summing to one (as a convergent series). The return probability and the mean recurrence time are valued in , so null recurrence () is representable. Irreducibility is the per-pair notion. Stationary equations are stated componentwise with convergent series.
In Foster's criterion the series are required to converge for every , which is the book's condition together with the finiteness implicit in the inequalities for ; is real-valued and nonnegative. Dropping the convergence requirement would let a divergent row series (whose Lean sum is ) satisfy the inequality vacuously; allowing would make the hypothesis trivially satisfiable. Neither is permitted.
The closed forms stated explicitly are: (Theorem 1.1(a), with both existence and uniqueness), the Poisson probabilities (1.14), the Erlang tail integral and the Poisson CDF (1.15), the density (1.16), and for the nonhomogeneous law. Equations (1.14) and the nonhomogeneous law are stated as "solves the equations with the initial conditions if and only if equals the closed form", so both existence and uniqueness are asserted.
The Poisson results use random variables on a probability space, with Mathlib's expMeasure for the exponential law and cond for conditional probability. The derivation of the forward equations from the axioms of §1.7 is not formalized; the Poisson law is reached from the equations and, separately, from exponential interarrival times.
Not formalized: Theorem 1.1(b) and the word "ergodic" in 1.1(c), which rest on the book's informal notion of ergodicity; Theorem 1.3, whose phrase "for Theorem 1.1 to be valid" for a continuous-time chain is not pinned down.
The Markov chain definitions are reusable by every later mission that studies an imbedded chain. Contributions welcome: proofs of the milestones, and supporting lemmas (Chapman–Kolmogorov, renewal decomposition of , class properties of recurrence).
Many sales are contracted before the buyer knows what the good is worth to her. An airline sells a ticket months before the trip, a hotel sells a refundable or non-refundable room before the traveller's plans are settled, and a supplier signs a capacity contract before demand is realised. At the time of contracting the buyer holds some private information about her future valuation (how likely she is to travel), and after contracting she learns more (whether she actually travels). Sequential screening is the mechanism design problem of a seller facing such a buyer.
The chapter formalized here, Daniel Krähmer and Roland Strausz's Dynamic Mechanism Design (Chapter 11 of Börgers' textbook), develops the problem along two lines. The first is dynamic private information: one sale, two rounds of private information. The second is dynamic allocations: repeated sales, one fixed valuation.
Timeline:
A seller sells one indivisible good. Before contracting, the buyer privately observes her ex ante type , with distribution function and density . After accepting the mechanism she privately observes her ex post type , , which is her valuation. Conditionally on it has distribution function and density . Both and are continuously differentiable in , , and higher is good news in the sense of first-order stochastic dominance: for .
A direct mechanism is a pair , . The buyer first reports , then . Write , and . The mechanism is incentive-compatible if truth about is optimal after every report of , and truth about is optimal against every subsequent reporting function . It is individually rational if for all . The seller maximizes expected revenue . The virtual valuation is
and Assumption 11.1 requires to be increasing in and . The exercise price is .
Under Assumption 11.1 the optimal mechanism is
where is the expression of Proposition 11.5 for , and the lowest type pays
The goal asserts that this mechanism is incentive-compatible, individually rational and optimal. It also characterizes all optimal mechanisms: an incentive-compatible, individually rational mechanism is optimal if and only if almost everywhere off and . When is null, this becomes and almost everywhere.
The path to the goal, in the book's order:
Three extensions follow. Propositions 11.9 and 11.10 show that the privacy of the additional information costs the seller nothing. Proposition 11.11 gives the optimal mechanism with several buyers. Proposition 11.12 shows that with dynamic allocations and a fixed valuation, repeating the static posted price is optimal.
The result gives a practical rule: sell an option. Ex ante type pays a fee for the right to buy later at the exercise price , and decreases in . This explains refund and cancellation menus in advance-purchase markets. Proposition 11.10 adds that information the buyer receives after contracting generates no rents under Assumption 11.1. A seller therefore gains from contracting early and from disclosing information after contracting. Proposition 11.12 shows that, under full commitment, a monopolist gains nothing from responding to past purchases.
On the formal side, the results are proved in the literature and in the book, but none of them is machine-checked. The mission produces a verified envelope theorem in a two-dimensional type space where incentive compatibility does not imply monotonicity. It also produces a verified revenue-equivalence formula for sequential mechanisms, and the first verified optimal-mechanism results with dynamic information.
The static argument of Chapter 2 does not carry over directly. Incentive compatibility with respect to does not make increasing in . The buyer's first-period utility is an expectation over a whole schedule , so single crossing has no bite. The characterization therefore splits into necessary conditions (the envelope formula in , which needs Lipschitz continuity of from the bound ) and a sufficient condition (monotonicity in both arguments, via first-order stochastic dominance), and the two meet only under Assumption 11.1.
Definition 11.2(ii) quantifies over all off-path reporting functions. The revelation principle does not remove them, so Proposition 11.2 is needed before any envelope argument applies.
Pointwise maximization of the virtual surplus pins down only where and only almost everywhere. The optimal mechanism is therefore not unique in the pointwise sense the page states.
F θ τ and is q τ θ. Functions are total on or , and conditions quantify over the type intervals only. and are fields pinned by HasDerivWithinAt on .Ruled out. Stating only that the cutoff mechanism is incentive-compatible and individually rational, or only that it beats posted prices, would trivialize the goal. The goal asserts optimality among all admissible incentive-compatible, individually rational sequential mechanisms with randomized allocations, together with the explicit fee and (11.12).
Infrastructure. A complete development needs envelope theorems for suprema of equi-differentiable families, integration by parts with absolutely continuous functions, differentiation under the integral sign, and change of variables . The single-buyer lemmas (Propositions 11.2–11.7) are reusable for the multi-buyer case through the interim mechanism . Proofs of any milestone, and sorry-free lemmas on the definitions, are welcome.