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?
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.
The single-server queue with general interarrival times and general service times, written G/G/1 in Kendall's notation, is the model left when every distributional assumption is removed from the classical single-server queue. Customers arrive one at a time, wait in line in first-come, first-served order, and are served one at a time. Almost nothing about it can be computed in closed form. What survives is a recursion for the waiting times of successive customers and the integral equation of its steady state, due to Lindley (Lindley, 1952). Every exact and approximate treatment of the G/G/1 waiting time, including the bounds of the next chapter of the book, starts from that equation.
This mission is the eighth of a series formalizing Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, DOI 10.1002/9781118625651). It covers Chapter 6, "General Models and Theoretical Topics". The chapter also treats the G/E_k/1 characteristic equation (§6.1), the M/D/c queue (§6.3) and maximum-likelihood estimation for M/M/1 (§6.7), which appear here as further milestones.
Timeline. Lindley (1952) derived the recursion and the integral equation and showed that a limiting waiting-time distribution exists when the mean service time is smaller than the mean interarrival time. Loynes (1962) gave the stationary solution as a supremum over the past of a random walk, for stationary rather than independent inputs. Clarke (1957) derived the maximum-likelihood estimators for M/M/1, and Crommelin (1932) the M/D/c generating function. Chaudhry, Harris and Marchal (1990) located the roots of the G/E_k/1 characteristic equation.
The interarrival times are independent with common distribution , the service times are independent with common distribution , and the two sequences are independent. Both and are lifetime laws: probability distributions on . The means are and , and the traffic intensity is .
The line delay of the th customer satisfies Lindley's recursion
Write for the distribution of with and independent. Since is independent of , one step of the recursion sends the distribution of to the distribution of with independent of . A stationary delay distribution is a probability distribution that this step maps to itself; its CDF is .
If and are finite and , then a stationary delay distribution exists, and the CDF of every stationary delay distribution satisfies
The goal consists of the existence statement and the equation together. The equation alone is close to unfolding one step of the recursion. Existence is what ties it to a queue in steady state.
Lindley's equation characterizes the stationary G/G/1 waiting time without any distributional assumption. The M/M/1, M/G/1 and G/M/1 waiting-time distributions of earlier chapters are its special cases. The transform relation (6.12) reduces the G/G/1 delay to a factorization problem for . The recursion and the equation are the starting point of Kingman's bound, of heavy-traffic approximations and of simulation of single-server systems.
All of these results are classical and proved. As far as a search of the platform shows, none of them is formalized. The platform's forward-coupling mission proves convergence to a stationary workload of a continuous-time queue that it assumes to exist. It proves neither the existence of a stationary law of Lindley's discrete recursion nor Lindley's equation. The mission therefore produces a machine-checked account of the G/G/1 recursion on distributions, a Loynes-type existence theorem for it, and the Wiener–Hopf transform identity. Its definitions (lifetime laws, the law of , the law map of the recursion, two-sided transforms) are reusable for Kingman's bound in the next mission of the series.
The obvious route to existence is to iterate the recursion from and take a limit. The distributions of from zero increase stochastically, but a limit of CDFs need not be a probability distribution: mass can escape to infinity, and it does when . Ruling this out under is the whole content of the existence half. It is a statement about the entire past of the input sequences, not about one step of the recursion, and the book asserts it without argument ("In the steady state () …", p.285).
The transform identity (6.12) needs the right strip of convergence, which the book does not state. is finite only where the interarrival time has an exponential moment.
Distributions are Mathlib measures on . and are probability measures with no mass on , with integrable identity where means are used. is stated as with . Independence is encoded by product measures: is the image of under , and one step of the recursion is the image of under . Stieltjes integrals over are Lebesgue integrals over the closed half-line, so the atom is counted. Transforms take complex arguments.
The closed forms carried by the statements are the following.
A stationary delay distribution is a fixed point of the law map of the recursion, not an arbitrary CDF assumed to satisfy (6.8). A statement of (6.8) for "any CDF with on " would assume its own conclusion, and is excluded. The statement for M/D/c includes existence of a steady state under as well as the formula for every steady state.
Not formalized: §6.1.1–6.1.2 (G/PH_k/1, quasi-birth–death processes), §6.4 (semi-Markov processes, whose limit theorems the book quotes without hypotheses), §6.5 (random-order and last-come service, series representations), §6.6 (design and control), and the rest of §6.7.
Contributions are welcome on the random-walk representation of the recursion, on the existence theorem under , and on the transform identities. The first two are reusable for any single-server or storage model driven by a reflected random walk.
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.
Most queueing models with a closed-form answer assume Poisson arrivals. In practice the times between arrivals are often far from exponential: scheduled appointments, batch releases from an upstream process, or arrivals timed by a machine cycle. The G/M/1 queue keeps the service side exponential and makes no assumption about the arrival stream beyond independent, identically distributed interarrival times. It is the standard counterpart of the M/G/1 queue, and its solution is the one used in teaching and in practice whenever the input is not Poisson (Gross, Shortle, Thompson & Harris, Fundamentals of Queueing Theory, 4th ed., Wiley 2008, §5.3.1, DOI 10.1002/9781118625651).
The answer has an unusually clean form. The number of customers that an arriving customer finds in the system is geometric, exactly as in the M/M/1 queue, with the traffic intensity replaced by a number that depends on the whole interarrival distribution through a single scalar equation. This mission is the seventh of a series formalizing the book chapter by chapter; it covers the G/M/1 half of §5.3 (printed pp.259–263).
Customers arrive at a single server. The interarrival times are independent with common law , a probability distribution on with CDF and finite mean , . Service times are independent exponential random variables with rate , and the discipline is first come, first served.
Let be the number of customers in the system just before the th arrival. Between two arrivals the server completes a Poisson number of services (truncated by the number present), so is a Markov chain on . Its transition probabilities are built from
the probability of exactly completions during one interarrival time (Eq. (5.50)): , for , and otherwise (Eq. (5.51)). A stationary arrival-point distribution is a probability vector with and (Eq. (5.52)); is the long-run probability that an arrival finds customers present.
The characteristic equation of the chain is
where is the probability generating function of (Eq. (5.55)). Equivalently (Eq. (5.56)), where is the Laplace–Stieltjes transform of the interarrival law. The traffic intensity is .
If , there is a number with and , it is the only complex root of in the open unit disk, and
is a stationary arrival-point distribution and the only one. The root is part of the conclusion, not an assumption.
The result. Equation (5.60) reduces the analysis of a queue with arbitrary renewal input to one scalar root. Every arrival-point performance measure of the M/M/1 queue then carries over with replaced by : the mean number found by an arrival, the mean queue found by an arrival, and the full distributions of line delay and system time seen by arrivals (Eqs. (5.61)–(5.63)). The same root drives the multiserver G/M/c analysis later in §5.3 and the relation between arrival-point and time-average probabilities in §6.3. The result also illustrates a point the book stresses: is the distribution seen by arrivals, and it equals the time-average distribution only when the input is Poisson.
Formalizing it. The mathematics is classical (the embedded-chain method goes back to Kendall, 1953) and fully proved in the textbook literature; nothing here is open. To our knowledge none of it has a machine-checked proof: the platform had no G/M/1, embedded-chain, or Rouché-type statement when this mission was drafted. The work is to formalize the known argument, which touches analytic facts about power series with nonnegative coefficients, a mixture-of-Poisson computation, a counting of roots in the unit disk, and the uniqueness of the stationary law of an irreducible countable chain.
Locating a real root in is a one-variable question. The hard step is excluding every other complex root inside the unit disk: a real-variable argument says nothing about complex roots, and the book's route relies on Rouché's theorem, which Mathlib does not have. A second point is uniqueness of the stationary vector: showing that the geometric vector solves does not show that no other probability vector does, and the goal asserts both. Computing requires interchanging a sum with the integral against , which is where the finite mean of the interarrival law enters.
The interarrival law is a measure A : Measure ℝ with IsProbabilityMeasure A, A (Set.Iio 0) = 0, integrable identity, and ∫ x ∂A = 1/λ (the structure IsInterarrivalLaw). Every theorem also assumes and . The integrals defining and are over , closed at . The generating function takes complex arguments; real roots are written with the real-to-complex coercion. A stationary vector is a function q : ℕ → ℝ with , HasSum q 1, and HasSum (fun i => q i * p i j) (q j) for every .
The explicit closed forms the statements carry are: the transition matrix (5.51); the equations (5.53); (5.56); ; (5.60); and (5.61); and (5.62); and (5.63). The waiting-time CDFs are defined as in §2.2.5 of the book: with the Erlang type- CDF, and likewise with completions. The means in (5.63) are and .
A trivializing formalization would take " solves " as a hypothesis of the goal, which turns (5.60) into a geometric-series check; here existence, location and uniqueness of the root, and uniqueness of the stationary vector, are all conclusions.
Out of scope for this mission: the M/G/c and M/G/∞ results of §5.2 and the multiserver G/M/c analysis of §5.3.2. Reusable pieces include a Rouché-type or fixed-point counting lemma for power series with nonnegative coefficients summing to one, and the uniqueness of stationary laws for irreducible chains on . Contributions of either kind are welcome.
The M/G/1 queue is the single-server queue with Poisson arrivals and an arbitrary service-time distribution. It is the first queueing model beyond the birth–death family in which exact formulas survive. It is also the model a practitioner reaches for when service times are measured and visibly not exponential: repair times, transmission times of variable-length packets, machining times. Its central result is the Pollaczek–Khintchine formula, first obtained by Pollaczek (1930) and Khintchine (1932). It expresses the stationary queue in terms of the service distribution, and it shows that the mean wait grows linearly in the squared coefficient of variation of service. That makes variability, and not only load, a measurable driver of congestion.
The textbook treatment followed here is Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory, 4th ed. (Wiley 2008), §5.1. It derives the result through Kendall's (1953) imbedded Markov chain of system sizes at departure epochs. It then obtains the transforms of the waiting times and the busy-period functional equation of Takács (1962).
Customers arrive in a Poisson stream of rate . Service times are independent with distribution , a probability distribution on with mean , and the discipline is first-come first-served. The traffic intensity is .
Let be the number of customers the th departing customer leaves behind. The number of arrivals during one service time equals with probability
and is a Markov chain on whose transition matrix has first row and, for , entries for and otherwise. A stationary distribution is a probability vector with . Its generating function is , and that of the arrivals per service is , for complex . The Laplace–Stieltjes transform of a distribution on is . In the Lean development these are arrivalProb, transitionMatrix, IsStationaryDist, pgf, utilization and lst in the namespace QueueingFundamentals.MG1.
If and , the chain has a stationary distribution, and every stationary distribution satisfies and
with at each such . It leaves the service distribution completely general.
The transform formula determines the whole stationary departure-point distribution from the service distribution. Its derivatives at give every moment of the system size, including the mean-value formula (5.7). Combined with the transform identity (5.32), it gives the waiting-time transforms (5.33)–(5.34). Those in turn give the classical geometric-series representation of the line-wait distribution through the residual service time. The busy-period equation is the starting point for busy-period moments and for the M/G/1 analysis of priority and vacation models later in the book.
All results here are classical and proved in the literature. As far as a search of the platform shows (2026-09-28), none is machine-checked: there is no M/G/1 queue, imbedded departure-point chain, Laplace–Stieltjes transform of a service distribution, or busy-period equation on Prove2Me. Mathlib has Poisson distributions and measure convolution but no generating-function theory for countable Markov chains, no Laplace–Stieltjes transform, and no identity theorem in the form these statements need. The mission produces a checked statement of the Pollaczek–Khintchine formulas that later queueing developments (vacations, priorities, M/G/1-type chains) can build on.
Turning the stationary equations into (5.14) is formal power-series algebra. The difficulties lie elsewhere. First, the formula must hold for complex on the closed disk, which needs the non-vanishing of away from . That fact fails for , where has a fixed point inside the disk. Second, (5.15) evaluates from by a limit at the point where the formula is , and this uses , an interchange of sum and integral. Third, the existence half of the goal requires positive recurrence of a chain with unbounded jumps. The book obtains it from Foster's criterion, which is not in Mathlib. Fourth, the waiting-time and busy-period transforms are stated for all real , while the generating-function route reaches only . Extending the identity requires either analyticity arguments or a direct derivation. A formal proof of (5.14) alone does not touch any of these.
The service distribution is a Measure ℝ with IsProbabilityMeasure B and B (Set.Iio 0) = 0; no density is assumed. The arrival rate is lam : ℝ with 0 < lam. Stationarity is IsStationaryDist P π: nonnegative entries, HasSum π 1, and HasSum (fun i => π i * P i j) (π j) for every j. That is global balance on ℕ, as the book writes it. Generating functions take a complex argument with ‖z‖ ≤ 1; transforms take a complex argument, and the waiting-time and busy-period statements use real s. The mean and variance of B are Bochner integrals, and every statement that uses them assumes Integrable. The mean busy period assumes 0 < E[S], so that is the book's service rate.
Closed forms carried by the statements: (5.15); (5.16); (5.14); (5.7); (5.32); (5.33); (5.34); (5.37); for the mean busy period.
The waiting-time distribution enters through the book's FCFS relation , and through ; both are hypotheses, as in the book. The busy-period distribution enters through the equation (5.36) in CDF form, with -fold convolutions built from Mathlib's Measure.conv.
The goal is not the algebraic consequence of (5.12) for an arbitrary sequence: must be a probability vector, is determined as , and the existence of a stationary distribution is part of the conclusion, so the statement cannot hold vacuously. The departure-point/time-average equality (§5.1.3, via PASTA) is not formalized.
Useful infrastructure, reusable beyond this mission: generating functions of stationary distributions on ℕ, Poisson mixtures, Laplace–Stieltjes transforms of measures on , and a Foster-type drift criterion for countable chains. Contributions proving any milestone, or those tools, are welcome.
Networks of queues model systems in which a job visits several service stations in turn: jobs in a computer system alternating between CPU and disks, machines cycling between operation and repair, parts routed through a job shop. In a closed network no job enters or leaves; a fixed population of customers circulates among nodes. Closed networks are the standard model of multiprogrammed computer systems and of machine-repair and finite-source systems, and they are the setting of chapter 4 of Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, doi:10.1002/9781118625651).
The chapter's results form a short line of computational ideas:
This mission formalizes that line, ending at (4.26).
A closed Jackson network has nodes , each with a single server whose service times are exponential with rate . A customer finishing service at node moves to node with probability ; the routing matrix has nonnegative entries and rows summing to one, and it is irreducible: every node can be reached from every other. The state is , the number of customers at each node, with ; this state space is finite.
The steady-state distribution is the probability vector on the state space that solves the flow-balance equations (4.14),
where has one more customer at and one fewer at , and terms with a negative subscript or with at an empty node vanish. The traffic equations (4.16) are ; they determine up to a positive factor. The normalizing constant is
and more generally, with for -server nodes ((4.13)), and Buzen's function .
For each population write for the marginal distribution at node , , for the mean number at node , and
for the throughput of node .
For every node ,
It involves only the steady-state distributions and quantities computed from them; it holds for every irreducible routing matrix and every choice of rates.
The product form reduces a -state Markov chain to the constants , and Buzen's recursion computes them in operations. Mean-value analysis goes further and avoids , whose magnitude can overflow or underflow for large populations; it is the method used in capacity planning of computer systems. The recursion (4.26) extends MVA from means to full marginal distributions, so a single pass over yields every nodal distribution.
All of these results are classical and proved in the literature; the book proves (4.26) itself. What the mission adds is a machine-checked development of them from the global balance equations: the product form with its uniqueness, the convolution identities, the marginal formulas, and the correctness of the MVA iteration as stated by the book, all over one shared definition layer. A search of the platform on 2026-09-28 found no formal statement of Buzen's algorithm or of MVA. The platform has Kelly's closed migration process theorem (KellyStochasticNetworks.closed_migration_equilibrium), which shows that the unnormalized product form satisfies the equilibrium equations under Kelly's conventions; the normalization, uniqueness and everything downstream of the product form are new here.
The combinatorial identities (Buzen's recursion, the tail marginal) are reindexings of finite sums over compositions of ; in Lean the work is in bijections between the state spaces for different and . The substantive step is uniqueness in the product-form theorem: the global balance equations have a one-dimensional solution space only because the chain on the -customer states is irreducible on the population level, which is a property of the network chain and not of the routing matrix alone. The goal and MVA also need a positive solution of the traffic equations, which is not among the hypotheses and has to come from irreducibility of . The book's own intuitive derivation of MVA via the arrival theorem is not the route the statements require; they are stated in terms of the steady-state distributions alone.
Nodes are Fin k (book node is index ); states are n : Fin k → ℕ with ∑ i, n i = N, collected in a Finset, and all sums are finite. A distribution is a real function on that is nonnegative, vanishes off the -customer states and sums to one there. The balance equations are (4.14) verbatim with the book's boundary convention (p.188), not detailed balance. All results except Buzen's algorithm and (4.22) are for single-server nodes, as in the book; (4.13)'s multiserver factor enters only (4.19)–(4.22).
Closed forms instantiated in the statements: the product form ((4.15)); as the explicit sum (4.18)/(4.19); from (4.13); from (4.20); ((4.22)); (p.208); ((4.23)); (MVA step (iii)(b)).
Two trivializing formalizations are ruled out: in (4.26) and (4.24) is the throughput computed from the steady-state distribution, not a free constant (which would make (4.26) a definition); and is defined by the sum (4.20), so the recursion (4.21) is a theorem rather than rfl. The product-form statement is an equivalence, so it asserts both that the product form is a steady state and that it is the only one.
Needed infrastructure: bijections between compositions of into and parts, uniqueness of stationary distributions of irreducible finite continuous-time chains (stated directly via the balance equations), and existence of positive solutions of for irreducible stochastic . The last two are reusable beyond this mission. Contributions welcome: proofs of the milestones in any order, and helper lemmas on these three points.
Not formalized: open Jackson networks (4.11) and Burke's theorem (4.5)–(4.6), multiclass networks (§4.2.1), the multiserver recursion (4.27) and cyclic queues (§4.4).
In many service systems a customer who finds every server busy does not join a queue. A caller who hears a busy signal hangs up and redials later; a request rejected by a saturated server is resent after a timeout; an aircraft that cannot land circles and tries again. These retrial queues are the subject of a substantial literature in telephone traffic engineering, computer networks and call-centre design, surveyed in the monograph of Falin and Templeton (1997) and the bibliography of Artalejo (1999). Their analysis is harder than that of ordinary queues: the blocked customers form an orbit whose size is part of the state, so even the simplest model is a two-dimensional Markov chain, and explicit stationary distributions are rare.
This mission is the fourth of a series formalizing Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008). Its goal is the explicit stationary distribution of the single-server retrial queue, Eq. (3.57) of §3.5.1, one of the few retrial models solvable in closed form. Chapter 3 of the book treats Markovian queues that are not birth–death processes: bulk arrivals, bulk service, Erlang phases, priority disciplines and retrials. The milestones also collect three capstone formulas from the chapter's other sections: the bulk-input queue, the partial-batch bulk-service queue, and Cobham's formula for nonpreemptive priorities (Cobham, 1954).
In the retrial queue customers arrive according to a Poisson process with rate and are served one at a time by a single server, with exponential service times of mean . An arrival that finds the server busy enters the orbit and stays there for an exponential time with mean , after which it tries again; each customer in orbit retries independently. No customer leaves because of impatience. With the number in service and the number in orbit, the pair is a continuous-time Markov chain on states , , . Writing for the steady-state probability of , the rate-balance equations are
Following the book's convention (§1.9, and the footnote on p.118), a steady-state solution is a nonnegative solution of these equations whose total mass equals . The traffic intensity is , and the partial generating functions are and .
The other models of the mission use the same convention. In the bulk-input queue , batches arrive at rate with batch-size probabilities , , and batch-size generating function . In the partial-batch bulk-service queue , single arrivals come at rate and the server serves up to customers together in an exponential time of mean . In the nonpreemptive priority queue there are classes with rates and , loads and cumulative loads .
For and , the numbers
form a steady-state solution of (3.47)–(3.49), and every steady-state solution equals them.
The generating functions satisfy (3.50)–(3.52) on , including the separable equation
their closed form is (3.55),
and the mean orbit size is (3.58), .
The bulk-input generating function (3.3), with , and the mean (3.4); the unique root of and the geometric law (3.9); and Cobham's formula (3.41)/(3.43), the unique solution of the linear system (3.40).
The closed form (3.57) makes every performance measure of the retrial queue explicit. The server is busy a fraction of the time, exactly as without retrials. The mean orbit size (3.58) is the mean queue length multiplied by , and the mean time in orbit (3.59) follows from Little's law. These formulas quantify the cost of retrials against an ordinary queue and are the reference case against which approximations for multi-server retrial systems are checked.
The results are classical and proved in the book, partly through exercises (Problems 3.39–3.41). None of them is formalized in any proof assistant, as far as the platform's catalogue shows: there is no retrial, bulk or priority queue on Prove2Me. The mission produces machine-checked statements and, once solved, proofs of the chapter's main closed forms. It also produces a small reusable layer: generating functions of probability sequences on the closed unit disc, and the "probability solution of the balance equations" pattern for chains with countable state spaces.
The derivation in the book is formal. It differentiates power series term by term, divides by , integrates , and fixes the constant by setting , without justifying any of these steps. A formal proof has to show that the series converge and are differentiable on , that the differential equation determines up to a constant, and that the values at are the limits of the values inside the disc (Abel's theorem). The uniqueness half of the goal is the hardest part. The book never proves it; it follows from the ODE argument only once every step is shown to hold for an arbitrary probability solution. Verifying that (3.57) solves (3.47)–(3.49) is only the easy half. The same pattern recurs in the bulk-input queue, where is a removable singularity of (3.3). In the bulk-service queue the root is only characterized as the unique root in , so existence and uniqueness of the root are part of the claim.
A steady-state solution is a pair p0 p1 : ℕ → ℝ (resp. one sequence p : ℕ → ℝ) that is pointwise nonnegative, has total mass as a HasSum, and solves the book's balance equations exactly as printed, global balance and not detailed balance. Every "the steady-state solution is X" is stated with both halves: X is a steady-state solution, and every steady-state solution equals X. Stating only that (3.57) solves (3.47)–(3.49), without normalization or uniqueness, would be a trivializing formalization. So would taking as a given root in (3.9), or taking the in (3.41) as numbers assumed to satisfy it. None of these is used. The closed forms instantiated are (3.52), (3.55), (3.57), (3.58), (3.3), (3.4), (3.9), (3.41) and (3.43), each written out in full, with the real power as Real.rpow.
The conventions are as follows. The retrial generating functions take real arguments, on for the differential equations and on for the closed form. The bulk-input generating function takes complex arguments with , , because (3.3) is at . The condition is a hypothesis of every retrial statement. For the bulk-service queue the book's unnamed condition is stated as . For bulk input, is assumed throughout, and the mean (3.4) is asserted under the further condition , which it requires. For Cobham's formula only the algebraic content is formalized; the mean-value argument that yields (3.40) and (3.42) is not.
Needed infrastructure: power series of summable nonnegative sequences on the closed unit disc (convergence, term-by-term differentiation, Abel continuity), the binomial series for real , and uniqueness of invariant probability vectors for irreducible chains. All of this is reusable beyond the mission. Proofs of any milestone, of the easy half of the goal, or of the needed series facts are welcome contributions.