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?
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.
Steady-state formulas describe a queue that has been running forever. Many practical questions are about a queue that has not: a call centre just after opening, a server just after a reset, a system under a burst of load. For these, the relevant quantity is the transient distribution of the number in the system at a finite time . It is also what determines how fast the steady state is approached, and it is needed for the busy period: the length of time a server stays busy once a customer arrives at an idle server.
For the single-server Markovian queue M/M/1 the transient distribution has an explicit closed form in modified Bessel functions. Its history is short and well documented. Ledermann and Reuter (1954) obtained it by spectral analysis of the birth–death process. Bailey (1954) found it by generating functions and Laplace transforms, and Champernowne (1956) by combinatorial methods. Bailey's route is the standard textbook derivation, and it is the one Gross, Shortle, Thompson and Harris outline in §2.11 of Fundamentals of Queueing Theory (4th ed., 2008). Abate and Whitt (1989) showed that computing with the resulting series is numerically delicate, which is one reason for having the formula pinned down exactly.
This mission formalizes §§2.11–2.12 of that book: the transient laws of M/M/1/1, M/M/1 and M/M/∞, and the M/M/1 busy period.
Customers arrive in a Poisson stream of rate . Each service takes an exponential time of rate , and . The number in the system is a continuous-time Markov chain on , and its state probabilities satisfy the forward (differential–difference) equations. For M/M/1 started with they are, for ,
with if and otherwise. The other systems are variants:
A family solves a system on when each has, at every , the prescribed derivative (a right derivative at ). It is a probability solution when and for every . The modified Bessel function of the first kind is
and the Laplace transform of is for .
With ,
The goal asserts five things for every and every , with no restriction on :
The formula (2.75) is the exact finite-time law of the most basic queue. It gives the rate at which M/M/1 approaches equilibrium, and it gives the distribution of the queue under overload (), where no steady state exists. It is the reference against which numerical transient methods, such as the uniformization of Chapter 8 of the same book, are checked. The busy-period density and its mean (2.79) enter server-utilisation and vacation models, and the Laplace-transform method used here recurs in the M/G/1 analysis of Chapter 5.
All of these results are classical and proved in the literature. None of them is machine-checked, as far as the platform's catalogue and Mathlib show. The chain from a countable system of linear ODEs, through generating functions and a root-location argument, to a Bessel series is a standard pattern in applied probability, and a formal version of it is what this mission adds. The formal statements also make explicit what the book leaves implicit: the sense in which the equations hold at , and the class in which the solution is unique.
The forward equations (2.72) form an infinite linear system. The obvious approach is to treat it like a finite system of ODEs, whose solution is a matrix exponential, and read off (2.75). That fails for two reasons. The generator is an infinite matrix, so its exponential needs a functional-analytic setting. And uniqueness is not automatic for infinite systems: it needs a class, such as probability solutions, and an argument that works in that class.
The Bessel form is a second, independent difficulty. The transform is fixed by a root-location argument in the complex plane. Inverting the transform, or verifying (2.75) directly, requires manipulating the three-term Bessel recurrence and exchanging infinite sums. The tail sum has to be controlled uniformly enough to be differentiated term by term. For the factor is non-positive, so the nonnegativity of is not visible from the formula.
Conventions committed to:
ℕ (Fin 2 for M/M/1/1).HasDerivWithinAt on Set.Ici 0 at every . Uniqueness is asserted among solutions that are probability distributions at every time.The closed forms stated exactly as in the book are:
The book derives (2.79) by a steady-state ratio argument valid for M/G/1. Here it is stated for M/M/1, as the mean of the explicit density.
A statement of (2.75) that only asserts the right-hand side is well defined, or checks only , is ruled out: the goal requires the ODE system, the initial condition, the probability property and uniqueness. For the same reason, the M/M/∞ law is tied to the system (2.76) and does not reduce to a Taylor expansion.
Needed infrastructure that Mathlib lacks:
The Bessel and Laplace definitions, and the uniqueness lemma for birth–death forward equations, are reusable beyond this mission. Contributions of those as separate lemmas are welcome.
Every call center, hospital ward, cloud server pool and telephone exchange that is sized by formula is sized by one of a handful of explicit expressions from Markovian queueing theory. The two oldest are A. K. Erlang's: the Erlang-B (loss) formula of 1917, which gives the fraction of calls lost when trunks carry an offered load of erlangs, and the Erlang-C formula, which gives the probability that a customer of a -server queue must wait. Both are still the default dimensioning rules of telecommunications and call-center workforce management (Gans, Koole & Mandelbaum 2003).
This mission formalizes Chapter 2, §§2.1–2.10, of Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory, 4th ed. (Wiley 2008), which derives these formulas from a single result about birth–death processes and closes with the modern answer to the staffing question.
Timeline. Erlang (1917) obtained the loss formula; Vaulot (1927), Pollaczek (1932), Palm (1938) and Kosten (1948) completed its proof for general service times. Halfin and Whitt (1981) showed that in the queue the delay probability converges to a limit strictly between and exactly when the number of servers exceeds the offered load by an amount of order . This is the quality-and-efficiency-driven (QED) regime on which square-root staffing rests.
A birth–death process is a continuous-time Markov chain on the states that moves from to at rate (a birth, or arrival) and, for , from to at rate (a death, or departure). A steady-state solution is a probability sequence (, ) solving the global balance equations (2.1):
The queues of the chapter are birth–death processes with particular rates. The queue has , and traffic intensity . The queue has , (2.30), offered load and . The loss system is the same with for . The queue has .
The explicit functions are the Erlang-B formula
the Erlang-C formula, defined for ,
and, with , the standard normal density and distribution function,
For offered loads ,
It is stated as three facts: maps into ; each has exactly one preimage ; and for every the two limits are equivalent.
The results. Items 1–9 are the working formulas of Markovian capacity planning: a stationary law for each basic model and the measures read off from it. (2.54) and (2.55) are how and are computed in practice, since the factorials of the closed forms overflow for . The Halfin–Whitt theorem is the reason the rule holds a fixed service level, and it is the entry point to the QED heavy-traffic literature (diffusion limits of many-server queues, Garnett–Mandelbaum–Reiman, Gamarnik–Momčilović).
Formalizing them. All results are classical and proved in the literature. The book states the Halfin–Whitt theorem without proof, and (2.54)–(2.55) are left to exercises. The formalization would supply machine-checked versions of the Erlang identities and of the Halfin–Whitt limit theorem. No Lean development of either was found on the platform when this mission was drafted. A related Erlang-B statement from Kelly and Yudovina is on the platform, stated with detailed balance on a finite state space.
The stationary laws are induction plus geometric and exponential series, and the Erlang identities are finite algebra. The difficulty is concentrated in the goal. is a ratio of a Poisson-type tail to a truncated exponential sum in which both and grow. The naive route, substituting Stirling's formula term by term, fails: the sums have significant terms, each of relative size , and the error has to be controlled uniformly over them. The converse direction also requires showing that is strictly monotone. Without that, convergence of does not force convergence of .
Rates are real sequences indexed by , and a steady-state solution is a real sequence with HasSum p 1, nonnegative entries, and the balance equations (2.1) exactly as printed (global balance, not detailed balance). Every "the steady-state solution is X" is stated in both halves: X is a steady-state solution, and every steady-state solution equals X; the book's existence conditions (, , convergence of the series) are part of the statements. The system is the -indexed process with for , as §2.5 sets it up; the statement records that states above carry no mass.
The closed forms that are fixed in Lean: over Finset.Icc 1 n; and exactly as displayed above; = gaussianPDFReal 0 1, = the CDF of gaussianReal 0 1; , as evaluated on p.69; as a convergent series.
is a total function in Lean, but its value for carries no meaning. The goal assumes for , the book's standing condition . A statement about some other function with the same limiting behaviour, or with and left abstract, would not be this mission. Neither would one-directional or existence-only versions of the stationary laws.
Not included: the waiting-time distributions (2.28) and (2.39), which need an FCFS waiting-time model with arrival-point probabilities; the measures (2.45)–(2.48); finite-source and state-dependent models (§§2.8–2.10). Useful contributions beyond the milestones are Poisson tail estimates at the scale and monotonicity of . Both are reusable in other many-server heavy-traffic statements.
Many sales are contracted before the buyer knows what the good is worth to her. An airline sells a ticket months before the trip, a hotel sells a refundable or non-refundable room before the traveller's plans are settled, and a supplier signs a capacity contract before demand is realised. At the time of contracting the buyer holds some private information about her future valuation (how likely she is to travel), and after contracting she learns more (whether she actually travels). Sequential screening is the mechanism design problem of a seller facing such a buyer.
The chapter formalized here, Daniel Krähmer and Roland Strausz's Dynamic Mechanism Design (Chapter 11 of Börgers' textbook), develops the problem along two lines. The first is dynamic private information: one sale, two rounds of private information. The second is dynamic allocations: repeated sales, one fixed valuation.
Timeline:
A seller sells one indivisible good. Before contracting, the buyer privately observes her ex ante type , with distribution function and density . After accepting the mechanism she privately observes her ex post type , , which is her valuation. Conditionally on it has distribution function and density . Both and are continuously differentiable in , , and higher is good news in the sense of first-order stochastic dominance: for .
A direct mechanism is a pair , . The buyer first reports , then . Write , and . The mechanism is incentive-compatible if truth about is optimal after every report of , and truth about is optimal against every subsequent reporting function . It is individually rational if for all . The seller maximizes expected revenue . The virtual valuation is
and Assumption 11.1 requires to be increasing in and . The exercise price is .
Under Assumption 11.1 the optimal mechanism is
where is the expression of Proposition 11.5 for , and the lowest type pays
The goal asserts that this mechanism is incentive-compatible, individually rational and optimal. It also characterizes all optimal mechanisms: an incentive-compatible, individually rational mechanism is optimal if and only if almost everywhere off and . When is null, this becomes and almost everywhere.
The path to the goal, in the book's order:
Three extensions follow. Propositions 11.9 and 11.10 show that the privacy of the additional information costs the seller nothing. Proposition 11.11 gives the optimal mechanism with several buyers. Proposition 11.12 shows that with dynamic allocations and a fixed valuation, repeating the static posted price is optimal.
The result gives a practical rule: sell an option. Ex ante type pays a fee for the right to buy later at the exercise price , and decreases in . This explains refund and cancellation menus in advance-purchase markets. Proposition 11.10 adds that information the buyer receives after contracting generates no rents under Assumption 11.1. A seller therefore gains from contracting early and from disclosing information after contracting. Proposition 11.12 shows that, under full commitment, a monopolist gains nothing from responding to past purchases.
On the formal side, the results are proved in the literature and in the book, but none of them is machine-checked. The mission produces a verified envelope theorem in a two-dimensional type space where incentive compatibility does not imply monotonicity. It also produces a verified revenue-equivalence formula for sequential mechanisms, and the first verified optimal-mechanism results with dynamic information.
The static argument of Chapter 2 does not carry over directly. Incentive compatibility with respect to does not make increasing in . The buyer's first-period utility is an expectation over a whole schedule , so single crossing has no bite. The characterization therefore splits into necessary conditions (the envelope formula in , which needs Lipschitz continuity of from the bound ) and a sufficient condition (monotonicity in both arguments, via first-order stochastic dominance), and the two meet only under Assumption 11.1.
Definition 11.2(ii) quantifies over all off-path reporting functions. The revelation principle does not remove them, so Proposition 11.2 is needed before any envelope argument applies.
Pointwise maximization of the virtual surplus pins down only where and only almost everywhere. The optimal mechanism is therefore not unique in the pointwise sense the page states.
F θ τ and is q τ θ. Functions are total on or , and conditions quantify over the type intervals only. and are fields pinned by HasDerivWithinAt on .Ruled out. Stating only that the cutoff mechanism is incentive-compatible and individually rational, or only that it beats posted prices, would trivialize the goal. The goal asserts optimality among all admissible incentive-compatible, individually rational sequential mechanisms with randomized allocations, together with the explicit fee and (11.12).
Infrastructure. A complete development needs envelope theorems for suprema of equi-differentiable families, integration by parts with absolutely continuous functions, differentiation under the integral sign, and change of variables . The single-buyer lemmas (Propositions 11.2–11.7) are reusable for the multi-buyer case through the interim mechanism . Proofs of any milestone, and sorry-free lemmas on the definitions, are welcome.
Classical Bayesian mechanism design assumes that the designer knows the agents' beliefs about each other: typically a commonly known prior over independent private values. Wilson's critique (1987) observed that mechanisms tuned to such a prior can depend on details that no designer knows, and a literature on robust mechanism design replaced the fixed prior by a large family of possible beliefs. Chapter 10 of Börgers, An Introduction to the Theory of Mechanism Design (OUP 2015), develops this programme in the framework of Bergemann and Morris (2001, 2005): agents' information is described by a type space, the designer is uncertain which beliefs agents hold, and mechanisms are compared across all type profiles at once.
Timeline of the results formalized here:
There are finitely many agents , and agent has a set of payoff types. An outcome gives agent the utility , which may depend on all payoff types. A type space consists of nonempty sets of types, a payoff type map and a belief map , where . Different types may share a payoff type and differ only in their beliefs, and vice versa. A common prior is a distribution on from which every type's belief is obtained by conditioning. A type space has a large variety of certainties if for every and some type with payoff type is certain that the others' payoff types are . The space of finite types collects every infinite hierarchy of beliefs ("I believe that you believe that …") that is generated by a type of some finite type space.
A mechanism has strategy sets and an outcome rule . Strategies form a Bayesian equilibrium if each type maximizes expected utility under its own belief; it is belief-independent if types with equal payoff types play alike, and ex post if each type's choice stays optimal when it becomes certain of the others' types. A direct mechanism asks agents for their types, a reduced direct mechanism only for their payoff types. In the quasi-linear case outcomes are and , with paid by agent ; a direct mechanism is .
On a finite type space with quasi-linear utilities, suppose that for every agent no belief in is a convex combination of the others, and that in the direct mechanism no type wants to imitate another type with the same belief. Then there is a direct mechanism in which truth telling is a Bayesian equilibrium, with
The goal fixes neither the transfers nor any bound on them; it asserts the existence of a truthful mechanism with the same alternatives and the same interim payments.
The other fourteen numbered results of the chapter: conditional independence of payoff types under a full-support common prior (10.1); three revelation principles (10.2–10.4); existence of Bayesian equilibria of finite mechanisms on (10.5); betting between agents with inconsistent beliefs (10.7); ex post implementation of unique equilibrium outcomes and alternatives (10.8, 10.9); emptiness of the set of undominated auctions under interim Pareto welfare and under ex post revenue (10.10, 10.11); Hylland's characterization of random dictatorship (10.12); and three comparisons of random dictatorship with random dictatorship with compromise (10.13–10.15).
Proposition 10.6 reduces the design problem on a finite type space to incentive constraints among types with the same beliefs: belief types can always be elicited by side payments that leave interim utilities unchanged. With a common prior and Proposition 10.1 this yields optimal mechanisms by solving an independent-types problem for each profile of belief types (§10.8; Farinha Luz 2013 carries this out for auctions). Proposition 10.7 and its consequences 10.10–10.11 show why the same construction cannot be used without a common prior: inconsistent beliefs allow unbounded bets, so interim or revenue criteria admit no undominated mechanism. Propositions 10.12–10.15 show that relaxing belief independence escapes Hylland's impossibility result in the voting problem.
None of these results is formalized elsewhere to our knowledge. The book proves only some of them (10.1, 10.5, 10.8, 10.9, 10.13–10.15 are proved or outlined; 10.6 is sketched; the proofs of 10.2–10.4 are omitted as standard; 10.7 and 10.10–10.12 are stated without proof), so formalization also produces complete proofs of results the book leaves informal. Two printed statements are corrected (see Formalization scope).
The obvious approach to Proposition 10.6 applies the Crémer–McLean construction type by type. This fails because several types may share a belief: a side payment that depends on the reported belief cannot separate them, and the convex-independence condition concerns the set of distinct beliefs rather than the indexed family of types.
For the results on , a type is an infinite belief hierarchy, and a strategy must be one function on all finite types simultaneously. Existence (10.5) cannot be obtained by applying Nash's theorem to a single finite type space, because a type belongs to many finite type spaces and must play the same strategy in all of them. Hylland's theorem (10.12) requires a full characterization of strategy-proof random rules on a cardinal preference domain.
PMF X); expected utilities are sums. The book leaves the measure structure of type spaces unspecified (p.179, note 3); finite type spaces, and point beliefs are covered exactly. A Bayesian equilibrium requires every type's expected utility to exist (absolute summability) under every mixed strategy.Fin 2, candidates , strict private vNM utilities with every strict utility attained; mechanisms map to lotteries over candidates; rankings are bijections C ≃ Fin 3.Welcome contributions: a finite Farkas/separation lemma in the form needed for 10.6 (the platform has Polyhedral.farkas_lemma), basic API for PMF-valued type spaces (products of mixed strategies, conditioning), and the hierarchy map of finite type spaces, which all milestones share.
Voting rules, committee procedures and any other method that turns individual rankings into one collective choice face the same question: can the rule be designed so that no participant ever gains by misreporting their ranking? The Gibbard–Satterthwaite theorem (Gibbard, 1973; Satterthwaite, 1975) answers no. When at least three alternatives can be chosen and all strict rankings are admissible, the only rules immune to manipulation are dictatorships. The result is the starting point of mechanism design without money. It explains why the positive results of the transferable-utility chapters of the book (Groves, VCG, posted prices) depend on quasi-linear preferences, and why research on voting turned to restricted preference domains and weaker solution concepts.
This mission formalizes Chapter 8 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), §§8.2–8.3. The book's route to the theorem follows Reny (2001). Strategy-proofness implies Maskin monotonicity, and every monotone rule with full range over at least three alternatives is dictatorial. The second step is the Muller–Satterthwaite theorem (Muller and Satterthwaite, 1977), which is stronger than Gibbard–Satterthwaite because monotonicity is weaker than strategy-proofness. The chapter closes with the classical escape route: on single-peaked preferences (Moulin, 1980) the median voting rule is strategy-proof and not dictatorial.
Timeline. Arrow (1951/1963) proved the impossibility of non-dictatorial preference aggregation under independence of irrelevant alternatives. Gibbard (1973) and Satterthwaite (1975) proved the manipulation version independently, and Satterthwaite showed the two theorems are equivalent. Muller and Satterthwaite (1977) showed that on the full domain strategy-proofness is equivalent to a monotonicity condition (strong positive association). Moulin (1980) characterized strategy-proof rules on single-peaked domains that depend only on reported peaks. Reny (2001) gave the short common proof of Arrow's and the Muller–Satterthwaite theorems that the book follows.
There is a finite set of agents and a finite set of alternatives. Each agent has a preference relation over ; reads " is weakly preferred to ". Every is a linear order: complete, transitive, and the only indifference is among identical alternatives. Its strict part is . The set of all linear orders over is , and a profile is . is the profile obtained from by replacing agent 's preference with .
A direct mechanism is a function (Definition 8.1). It is
"The range of is " means that every alternative is chosen at some profile.
For §8.3 the alternatives are labelled . A preference is single-peaked if it has a top alternative and declines monotonically to the right and to the left of it. is the set of single-peaked preferences, and on the restricted domain DSIC and dictatorship are read with all profiles and deviations taken from .
This is the book's own capstone ("the core of the proof", p.144). No constant needs to be fixed, and the statement is strictly stronger than the necessity half of Gibbard–Satterthwaite.
The result itself. Proposition 8.5 turns an incentive question into a purely ordinal one: any full-range rule that is Maskin monotone is a dictatorship once three alternatives are available. With Proposition 8.2 it gives Gibbard–Satterthwaite. Proposition 8.6 marks the boundary of the impossibility: with a one-dimensional ordering of alternatives and single-peaked preferences, the median voter rule escapes it.
Formalizing it. All results are classical and proved. The platform already has a proved Gibbard–Satterthwaite theorem (AGT.gibbard_satterthwaite, Algorithmic Game Theory III), derived from Arrow's theorem in the alternative Mathlib environment c5ea0035…. It uses strict-order profiles and a one-agent-deviation monotonicity. This mission adds Maskin monotonicity, the Muller–Satterthwaite theorem, Reny's direct proof route, and the single-peaked possibility result, none of which is on the platform, all in the default environment.
Propositions 8.2–8.4 are short. The difficulty is in Proposition 8.5. Its proof moves one alternative up or down agents' rankings one agent at a time, and it has to keep the chosen alternative pinned at every step using only monotonicity, set-monotonicity and unanimity. It needs a pivotal agent, whose identity depends on the pair of alternatives, and then an argument that the pivots for different alternatives coincide. The argument uses a third alternative in an essential way. With two alternatives the conclusion is false (majority rule), so any argument that never uses cannot succeed. Formally, each "move just below in agent 's ranking" is an explicit construction of a new linear order, together with a check that the monotonicity hypothesis applies. The figures on pp.146–149 describe these orders only partially ("the other alternatives in arbitrary order"). For Proposition 8.6, the obstacle is that DSIC must be checked against every single-peaked misreport, not only misreports of the peak.
LinPref A (relation rel, completeness, transitivity, antisymmetry). A profile is ι → LinPref A for a finite agent type ι, and a direct mechanism is (ι → LinPref A) → A. is a Fintype. "The range of is " is Function.Surjective f, and is 3 ≤ Fintype.card A.∃ i, ∀ R a, f R ≥_{R_i} a, with the agent chosen before the profile. A weaker monotonicity (one-agent deviations only) or a weaker dictatorship ("some agent's top is chosen at some profile") would trivialize the goal and is ruled out.lab : A ≃ Fin K (labels ). The restricted domain is a predicate on LinPref A, and DSIC, dictatorship and full range are relativized to profiles in the domain (IsDSICOn, IsDictatorialOn, HasFullRangeOn). Values of the mechanism off the domain are never consulted.A group of agents must choose one alternative from a set (whether to build a public project, who receives an object, which of several policies to adopt). Each agent privately knows how much each alternative is worth to them, and money can be transferred. A designer who wants the welfare-maximizing alternative must ask the agents for their valuations, and must set payments so that no agent gains by misreporting, whatever the others report. This requirement, dominant strategy incentive compatibility, does not depend on what agents believe about one another, which is why it is the standard robustness benchmark in public economics, auction design and algorithmic game theory.
The Vickrey–Clarke–Groves (VCG) mechanisms solve this problem for every efficient decision rule. The central question of Chapter 7 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), is whether they are the only solution, and what can be implemented in dominant strategies at all.
Timeline:
There is a finite set of agents and a set of alternatives. Agent has a type from an abstract set . If alternative is chosen and agent pays , agent 's utility is . A type vector is ; omits agent , and replaces agent 's type by .
A direct mechanism consists of a decision rule and transfer rules . It is dominant strategy incentive-compatible (DSIC) if for all , and ,
A decision rule is efficient if maximizes over at every . A mechanism is VCG if is efficient and every agent's transfer has the form
for some function of the other agents' types. The chapter also uses positive association of differences (PAD: if and every agent's utility advantage of over every other alternative strictly increases from to , then ), flexibility (the range has at least three elements), ex post individual rationality and ex post budget balance ().
If every is a convex subset of a Euclidean space and every is convex and continuous on , then every DSIC mechanism with an efficient is a VCG mechanism: for each there is with
The goal leaves , the number of agents and the dimensions free; it asserts only the form of the transfers.
Every numbered result of Chapter 7 except Proposition 7.6 (see Formalization scope):
Corollary 7.1 turns the VCG construction from one solution into the complete answer. Any question about efficient dominant-strategy mechanisms (revenue, budget balance, individual rationality) reduces to a question about the functions . With Proposition 7.10 it gives a necessary and sufficient condition for efficient, budget-balanced dominant-strategy implementation. That condition fails in bilateral trade, and the failure does not use individual rationality. Roberts' theorem plays the same role for inefficient rules: on unrestricted domains, weighted welfare maximization is essentially all that can be implemented.
All of these results are proved in the literature, and none is formalized. The platform has VCG incentive compatibility and weak monotonicity for valuation-based types (the Algorithmic Game Theory IV mission). It has no uniqueness theorem, no revenue equivalence for multidimensional convex types, no Rochet theorem and no Roberts theorem. The book proves Corollary 7.1 from Proposition 7.3, but proves 7.3 itself only by reference to Krishna and Maenner. It states Roberts' theorem without proof.
The uniqueness claim does not follow from incentive compatibility alone. With finitely many types it is false, because any transfers inside the gaps left by the incentive constraints work (Börgers §5.8). The work lies in showing that, along every segment in the convex type set, an agent's equilibrium utility is pinned down by the decision rule. The equilibrium utility is a pointwise supremum of convex functions, one for each report, and the chosen alternative can change at uncountably many points of the segment. A differentiable envelope argument is therefore not directly available. At the boundary of the type set, convexity alone does not prevent upward jumps, which is why continuity is part of the hypotheses. Roberts' theorem needs a separate, combinatorial analysis of the sets of utility differences at which each alternative is chosen, and flexibility is essential there.
Agents form a finite type ι with decidable equality. Types are arbitrary types Θ i, and utilities are u : ∀ i, A → Θ i → ℝ. The profile is Function.update θ i θ'. is the product Others Θ i over j ≠ i, so each and is a function of the others' types only; a constant or a function of the full profile would change the theorem. In the goal and Proposition 7.3, is a convex set S i in EuclideanSpace ℝ (Fin (d i)).
Deviations from the page, each forced by a counterexample recorded in the item's natural-language statement:
The trivializing formalization to avoid is proving Proposition 7.4 (VCG DSIC) in place of the goal (DSIC efficient VCG). A development that proves the goal needs reusable infrastructure: convex functions restricted to segments, absolute continuity of continuous convex functions on compact intervals, and an envelope theorem for suprema of convex functions. Proofs of Rochet's and Roberts' theorems in this abstract setting are also welcome.
Almost every screening, auction and regulation model asks the same preliminary question: which allocation rules can be made incentive-compatible by some choice of payments? In the one-dimensional models of auction theory and nonlinear pricing the answer is monotonicity: higher types must receive higher allocations. Many applications are not one-dimensional, though. Examples are multi-object auctions, multi-product pricing, and lotteries over several outcomes. For those, a characterization that uses no structure at all is needed. Rochet (1987) gave one: an allocation rule is implementable exactly when it is cyclically monotone, a condition that originates in Rockafellar's characterization of subdifferentials of convex functions. Later work on dominant-strategy implementation, the "weak monotonicity" literature of algorithmic mechanism design, and revenue equivalence all build on it.
This mission formalizes Chapter 5 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015): all nine numbered results of the chapter.
Timeline. Rockafellar (1970, Theorem 24.8) characterized the cyclically monotone maps between vector spaces as the subgradient selections of convex functions. Rochet (1987) extended the idea to arbitrary alternatives and types with quasi-linear utility and proved that implementability is exactly cyclical monotonicity. Krishna and Maenner (2001) proved revenue equivalence on convex type spaces with utilities convex in the type. Bikhchandani, Chatterji, Lavi, Mu'alem, Nisan and Sen (2006) showed that for finitely many alternatives, weak monotonicity (the two-type case of cyclical monotonicity) already suffices on rich, order-based domains. Saks and Yu (2005) proved the same on convex domains.
A designer and one agent choose an alternative from a set . The agent has a type in a nonempty set . With utility function , her payoff from when she pays is . Neither nor carries any structure.
A direct mechanism is a decision rule and a transfer rule . It is incentive-compatible if for all . A decision rule is implementable if some makes it incentive-compatible. It is weakly monotone if for all pairs of types. It is cyclically monotone if for every finite sequence of types with ,
A complete and transitive order of induces a partial order on types: if values every -higher alternative strictly more, relative to an -lower one, than does, and neither type distinguishes -indifferent alternatives. The type set is one-dimensional if any two distinct types are -comparable, and bounded if all utility differences lie in for some . It is rich if, for some reflexive and transitive relation , every function with is some type's utility function. A mechanism is individually rational with outside option if every type does at least as well as with and no payment.
for arbitrary , nonempty and .
Rochet's theorem turns the existence of payments, an infinite system of linear inequalities in unknowns , into a condition on the decision rule alone. It underlies the characterization of implementable rules in multidimensional screening, the taxation principle, and the dominant-strategy characterizations of Chapter 7 (applied agent by agent). Propositions 5.4–5.6 recover the "monotone allocation" results of the one-dimensional chapters from it. Proposition 5.8 is the general form of the payoff-equivalence lemmas used for optimal auctions.
All results are classical and proved on paper, except Propositions 5.7 and 5.8, whose proofs the book omits and refers to the literature. None of them is formalized on Prove2Me. The platform's algorithmic-game-theory series has the weak-monotonicity half in a multi-agent valuation model (types are valuations ), not the abstract-type statement, and has no cyclical-monotonicity or Rochet result.
Necessity is a two-line telescoping argument. Sufficiency needs a transfer rule built from the decision rule, and the first idea fails: prices attached to alternatives chosen pair by pair (which weak monotonicity supplies) need not be globally consistent. Figure 5.1 of the book gives a three-type example that is weakly monotone but not implementable. The transfer must come from a supremum over all finite chains of types starting at a fixed type. The supremum is finite only because of cyclical monotonicity, and no finiteness, compactness or boundedness is available. Proposition 5.8 needs an envelope argument along segments in without differentiability. Proposition 5.7 needs a combinatorial argument that uses richness of the domain.
Alternatives and types are arbitrary Lean types A, Θ with Nonempty Θ, and the utility is u : A → Θ → ℝ. A cycle of length is a map Fin (m+1) → Θ with equal first and last entries, and its summands are indexed by Fin m. Relations are predicates A → A → Prop. For Propositions 5.3 and 5.8, types form a subset S of Ω → ℝ (resp. Fin n → ℝ) used as a subtype. Lotteries are stdSimplex ℝ Ω, and the subgradient inequality is required only at points of S.
The explicit statements are fixed as follows:
Two statements are corrected from the page, each with a counterexample to the literal version recorded in its item:
Both directions of Rochet's theorem are required. The necessity half alone, or a version with finite , finite or bounded utilities, is a different and much weaker theorem and does not close the goal.
The development needs finite telescoping sums, suprema of sets of reals (sSup with an explicit bounded-above argument), convex functions on sets and one-dimensional convex analysis (Proposition 5.8). The definitions file is reusable for Chapters 6–8 of the series. Contributions of alternative proofs, for example Proposition 5.6 through Rochet's theorem, are welcome.
Bayesian mechanism design assumes that the designer knows a common prior from which every agent's beliefs about the others are derived. Chapter 4 of Börgers' An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015, DOI 10.1093/acprof:oso/9780199734023.001.0001) drops that assumption. The designer is unwilling to rely on anything about what agents believe about each other, and therefore requires that truth telling be optimal for every type whatever the other agents report (dominant strategy incentive compatibility) and that participation be worthwhile after all reports are known (ex post individual rationality). The chapter revisits the three examples of Chapter 3 (single unit auctions, public goods, bilateral trade) and asks which mechanisms survive these requirements.
The answer differs sharply between examples. In auctions nothing is lost: an expected-revenue-maximizing auction can be implemented in dominant strategies. With a budget constraint, the class collapses. For a public good shared by two agents, the only dominant-strategy, ex post individually rational mechanisms that exactly balance the budget are fixed cost shares; in bilateral trade they are fixed-price mechanisms. These results go back to the dominant-strategy literature on public goods (Serizawa 1999, Econometrica) and on bilateral trade (Hagerty and Rogerson 1987, Journal of Economic Theory), as the book's §4.5 records (p.93), and they explain why simple posted-price and cost-sharing rules are common in practice.
Every agent has a type in an interval. In the auction and the public good examples the interval is with ; is the set of type vectors, and is without its -th entry. A direct mechanism asks every agent to report a type and maps the reports to an outcome.
A mechanism is dominant strategy incentive-compatible if for every agent, every true type, every false report and every report profile of the others, truthful reporting yields at least as much utility. It is ex post individually rational if every type's utility at every type vector is at least its outside option: for buyers and public good agents, (keeping the good) for the seller. A canonical mechanism (Definitions 4.3–4.5) allocates according to strictly increasing continuous scores and charges each agent the smallest report with which the outcome would have been the same.
For and a decision rule whose production set is closed, a direct public good mechanism is dominant strategy incentive-compatible, ex post individually rational and ex post budget balanced if and only if there are with and, for all ,
Both directions are part of the goal; the "only if" direction is the content.
Proposition 4.4 shows that the optimal auctions of Chapter 3 remain available without any assumption on beliefs, while Propositions 4.8 and 4.12 show that under exact budget balance, dominant strategy implementation forces rules that ignore reported valuations except through a yes/no participation decision. Together they mark the boundary between settings where the Bayesian and the belief-free approaches coincide and settings where the belief-free requirement is severe. This contrast motivates the robust mechanism design of Chapter 10.
These results are proved in the book: Propositions 4.5 and 4.8 in full, the others with proofs omitted or "analogous". No machine-checked proof of them appears on the platform or in Mathlib. The platform has a single-parameter characterization in a different model (AGT.single_parameter_characterization: valuation profiles, win sets, normalized losers' payments) and the second-price dominance fact; neither covers public goods, bilateral trade, budget balance or randomized allocations. The mission would add a machine-checked belief-free counterpart of Chapter 3, including the two characterization theorems whose printed proofs leave cases to the reader.
The characterizations (Propositions 4.2, 4.5, 4.9) are standard single-agent arguments applied to every profile of the others. The goal is harder. Proposition 4.5 describes each agent's incentives separately, for each report of the other agent, with thresholds and payments that may vary with that report. Budget balance couples the two agents' payments at every type vector. The step that fails when attempted naively is going from "a threshold for each " to "one fixed threshold for each agent": the thresholds may lie outside the type interval, several degenerate configurations occur (an agent whose report never matters, a good that is always or never produced), and the printed proof treats the degenerate cases by assuming and leaves one of them "analogous". The closedness hypothesis is what makes the relevant minimal types exist; without it the boundary of the production set is not determined. Proposition 4.12 has the same structure with the seller's orientation reversed.
Fin 2 for the goal, and a pair (θS, θB) : ℝ × ℝ for bilateral trade. A deviation is Function.update θ i x for θ ∈ Θ; quantifying over θ ∈ Θ quantifies over .sInf/sSup of sets that are nonempty and closed whenever they are used.Contributions welcome: proofs of the characterization milestones (4.2, 4.5, 4.9), which the goal and Proposition 4.12 use; a proof of the goal covering the degenerate cases the book leaves to the reader; and the three-agent counterexample of p.90 as a separate statement.
Stock exchanges, commodity markets and trading platforms are institutions for trade between parties who each know something the other does not. The simplest version is bilateral trade: one seller, one buyer, one indivisible good, and each side privately knows its own value. The question is whether any trading institution can make the two trade exactly when trade is efficient, with both taking part voluntarily and without a subsidy from outside. Myerson and Satterthwaite (1983) showed that, apart from trivial cases, none can. The result is one of the basic impossibility theorems of economic theory. It explains why bargaining under private information is inefficient, and it is the benchmark every later analysis of double auctions and market design compares against.
This mission formalizes Section 3.4 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015): the impossibility theorem, the pivot-mechanism argument that proves it, the second-best and profit-maximizing trading mechanisms, and the uniform example.
Timeline. Vickrey (1961) noted the tension between efficiency and budget balance in markets with private values. Chatterjee and Samuelson (1983) studied the sealed-offer double auction and its linear equilibrium for uniform values. Myerson and Satterthwaite (1983) proved the impossibility for general independent distributions with overlapping supports, and computed the second-best mechanism; for uniform values it coincides with the Chatterjee–Samuelson linear equilibrium. Börgers (2015) gives the pivot-mechanism proof formalized here.
A seller owns one indivisible good; a buyer may buy it. The seller's value has distribution with density on ; the buyer's value has distribution with density on . The two intervals are nondegenerate and may differ, and the values are independent. The seller's utility is if she sells for and if she keeps the good and receives ; the buyer's is if he buys and pays , and otherwise.
A direct mechanism is a trading rule on and transfers (received by the seller) and (paid by the buyer). Conditioning on one agent's type gives the interim trade probabilities , the interim transfers , and the interim utilities and . The mechanism is incentive-compatible if truthful reporting is a Bayesian equilibrium, individually rational if and for all types, ex post budget balanced if for every , and ex ante budget balanced if . A first-best trading rule trades when and not when , with any choice at ties. The seller's virtual cost is and the buyer's virtual valuation is ; the distributions are regular if both are increasing.
An incentive-compatible, individually rational and ex post budget balanced direct mechanism with a first-best trading rule exists if and only if
for some , exact budget balance , and the incentive-compatible payments with binding participation of and .
The theorem locates the source of inefficiency in bilateral bargaining in private information itself, not in any particular bargaining protocol: no mechanism, however clever, achieves efficient voluntary trade without a subsidy. It is the reason efficiency in markets is studied as a limit (large double auctions approach efficiency as the number of traders grows), and why a trading platform's fee structure is analyzed as a second-best problem. The pivot-mechanism argument is the same one that proves the impossibility of first-best public-goods provision (Proposition 3.7), so the two formalizations share their structure.
All results of this section are classical and proved on paper. None is formalized on Prove2Me, and Mathlib has no mechanism-design library. The platform has the Chatterjee–Samuelson linear equilibrium as an open statement about one particular game; this mission states results about all mechanisms. A complete development yields a reusable one-dimensional envelope/payoff-equivalence library for two agents with differently oriented types (the seller's incentive constraint runs from high types down), and the Lagrangian optimality argument for a linear objective under a single linear constraint.
The obvious attempt to prove impossibility looks for a contradiction between incentive compatibility and budget balance state by state. That fails: incentive compatibility and participation are interim constraints, so any single state admits budget-balanced transfers consistent with them, and the contradiction exists only after integrating over the prior. Two points need care. The seller's orientation is reversed: her trade probability is decreasing and her participation constraint binds at the highest type. And the deficit of the pivot mechanism must be shown to have positive probability, which uses that the supports overlap in a set with nonempty interior. The optimal-mechanism results additionally need that the trading rule implied by a Lagrange multiplier satisfies the monotonicity constraint, which is where regularity enters, and that a multiplier exists which makes the budget constraint bind.
A type vector is a pair θ : ℝ × ℝ with θ.1 the seller's and θ.2 the buyer's value. The prior is Lebesgue measure on with density . Densities are measurable, strictly positive on the closed supports and integrate to one; nothing else, such as continuity, is assumed. The trading rule is real-valued with values in on (deterministic, as in Definition 3.9). The measurability the book omits (Ch. 2 note 2) is built into the admissible class: , , are measurable with integrable transfers. "Increasing" is weak monotonicity, the book's convention.
Explicit formulas the statements carry: the first-best rule (3.61) with free tie rule, the pivot transfers of Definition 3.10, the rule (3.70) with parameter , the exact budget equation of Proposition 3.13 (ii), the payment formulas and , the profit rule , and the thresholds and .
The goal quantifies over every first-best trading rule and imposes budget balance as the ex post equality . Dropping budget balance, weakening it to , or fixing one tie rule would give a different, and in the first case false, statement. The pointwise "if and only if … for all " characterizations of Propositions 3.13–3.16 are stated with necessity almost everywhere, since an optimal trading rule is determined only up to null sets. For Proposition 3.14 necessity is also restricted to : under weak regularity that tie set can have positive probability, and profit does not depend on the trading rule there.
Contributions welcome: proofs of the milestones, a two-agent payoff-equivalence lemma for the seller's reversed orientation, and a sorry-free construction of the pivot mechanism's integrability facts.
Whether a community can finance a shared project out of voluntary contributions, when each member knows only her own benefit from it, is one of the founding questions of mechanism design. Bayesian mechanism design began with mechanisms for the provision of public goods: d'Aspremont and Gérard-Varet (1979) and Arrow (1979) showed that the efficient decision can be made Bayesian incentive compatible with a budget that balances in every state, provided agents cannot opt out. Once participation is voluntary, this is no longer possible, and Güth and Hellwig (1986) studied the best mechanism under that constraint. The same tension between efficiency, incentives, voluntary participation and budget balance drives the Myerson–Satterthwaite theorem for bilateral trade, which the next mission of this series formalizes.
This mission formalizes Section 3.3 of Tilman Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), which treats the public goods problem in the independent private values model with a continuum of types. The section proves an impossibility theorem for first best provision and then characterizes the best mechanisms that respect the budget: the welfare-maximizing (second best) mechanism and the profit-maximizing one, with a worked two-agent uniform example.
A community of agents , , decides whether to produce an indivisible, nonexcludable public good, , at cost . Agent pays a transfer and obtains utility . Her type is private information, drawn independently across agents from a distribution with density , strictly positive on the common support , . The type space is and .
A direct mechanism is a decision rule and transfer rules . For agent reporting , is the probability of production and the expected transfer, taken over the other agents' types, and . The mechanism is incentive compatible (IC) if for all , and individually rational (IR) if for all . It is ex post budget balanced if for every , and ex ante budget balanced if this inequality holds after integrating both sides against .
Welfare is . The first best decision rule is if and otherwise; a first best mechanism uses and transfers that add up to exactly in every state. The pivot mechanism uses and
The virtual valuation is , and is regular if is strictly increasing.
In the two cases on the right, producing is efficient for every type vector or for none; in every other case efficient provision cannot be financed voluntarily.
the budget binds, , and . 6. Proposition 3.9 (profit maximization): under regularity, the profit-maximizing IC and IR mechanism produces iff , with the same formula for . 7. Proposition 3.10 (Example 3.3: , uniform types on , ): the second best produces iff , where is the unique root in of if , and if . 8. Proposition 3.11 (same example): the profit maximizer produces iff .
Proposition 3.7 says that with voluntary participation no mechanism both takes efficient production decisions and pays for them, outside the degenerate cases. It is the reason the rest of the section, and much of the applied literature on public goods, studies constrained optimum mechanisms: Proposition 3.8 describes what the best budget-respecting mechanism gives up (it undersupplies the good, producing only when valuations exceed a bound strictly above the cost), and Proposition 3.9 quantifies the further distortion under a monopoly supplier. The example makes the three thresholds explicit and comparable.
All results of the section are classical and proved in the book, several of them only sketched there (Proposition 3.9 is stated without proof; Proposition 3.8 invokes an infinite-dimensional Kuhn–Tucker theorem whose applicability is not checked). None of them is formalized in Lean. The mission produces a machine-checked account of the envelope and revenue-equivalence arguments with interim expectations over independent types, a checked pivot-mechanism deficit computation, and a checked Lagrangian characterization; the uniform example additionally certifies the book's arithmetic.
The naive argument for the goal fails at the first step: a mechanism that implements with a balanced budget in every state is not obviously comparable to one that is only IC and IR, because IC constrains interim expectations while budget balance is ex post. The impossibility needs a reduction of the whole class of IC, IR mechanisms with rule to a single extremal one, which requires the payoff equivalence formula for interim utilities and an exact integral identity for expected revenue in terms of virtual valuations. The strict deficit of the pivot mechanism then needs a case analysis over which agents are pivotal and a positive-probability argument. For Proposition 3.8, pointwise maximization of a Lagrangian is not enough: one must show the multiplier exists and is positive, that the maximizer satisfies the monotonicity constraint, and that uniqueness holds only up to null sets.
Agents are Fin N with ; types are vectors in Fin N → ℝ; the type distribution is the product of the marginal measures on , which encodes independence. and integrate the decision and transfer rules against this distribution with agent 's coordinate overwritten by her report. Decision rules are deterministic, with values in on , as in Definition 3.4. Ties in the first best rule produce, as in the book's note 2 to Chapter 3; the second best and profit-maximizing rules use strict inequalities, as printed.
The book omits measurability and the existence of conditional expectations; the class of direct mechanisms here requires and each to be Borel measurable, each integrable, and each conditional expectation of given one agent's type to exist. The characterizations in Propositions 3.8–3.11 are stated in two directions: the stated rule, for every , is sufficient; necessity holds for almost every , since changing on a null set of type vectors changes nothing that is optimized. The explicit formulas the mission commits to are: the pivot transfers above; the second best rule with multiplier and the binding budget identity; ; the cubic for ; for ; and for the profit maximizer.
A trivializing formalization of the goal takes "first best" to mean only the decision rule ; the pivot mechanism would then be a witness in every case, so first best here also requires transfers adding up to exactly in every state.
Reusable infrastructure includes interim expectations over independent product distributions, the payoff and revenue equivalence lemmas for IC mechanisms, and the virtual-valuation identity for expected revenue; these are shared with the auction and bilateral trade chapters of the series. Contributions to any milestone, and to general lemmas about product measures with densities on boxes, are welcome.
A seller with one indivisible good and several potential buyers, each of whom privately knows how much the good is worth to them, has to choose a selling procedure: a posted price, an English auction, a sealed-bid auction with a reserve price, or something more elaborate. Which procedure raises the most expected revenue? Myerson's answer (Myerson 1981) is the foundation of optimal auction design. It underlies reserve-price setting in practice, the analysis of sponsored-search and ad-exchange auctions, and the modern algorithmic mechanism design literature, which treats Myerson's auction as the benchmark against which simple and approximately optimal auctions are measured.
This mission formalizes Section 3.2 of Tilman Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), the textbook treatment of Myerson's result in the independent private values model with Bayesian incentive compatibility. It is the second mission of a series covering the book.
Timeline. Vickrey (1961) showed that the second-price auction makes truthful bidding a dominant strategy and compared auction formats. Myerson (1981) characterized the revenue-maximizing mechanism for independent private values with possibly asymmetric distributions; Riley and Samuelson (1981) obtained the symmetric case and the optimal reserve price independently. The revelation principle in the Bayesian form used here goes back to Myerson (1979) and Dasgupta, Hammond and Maskin (1979).
There are potential buyers . Buyer values the good at ; if he receives it and pays his utility is , and otherwise . The seller's utility is . The valuations are independent; has cumulative distribution function and density with on the common support , where . The type space is and the joint density is .
A direct mechanism asks buyers to report their types and consists of an allocation rule , where , and payment rules . Its interim quantities are the expected allocation probability, payment and utility of buyer conditional on his own type:
The mechanism is incentive-compatible if for all (truth-telling is a Bayesian Nash equilibrium) and individually rational if for all . The virtual valuation of buyer is
and the distribution is regular if is strictly increasing.
Under regularity, among all incentive-compatible and individually rational direct mechanisms, a mechanism maximizes the seller's expected revenue exactly when, for every buyer ,
the allocation identity holding for almost every ; and such a mechanism exists.
The theorem identifies the revenue-maximizing selling procedure among all procedures, not among a parametric family: by the revelation principle, no auction format, however elaborate, and no equilibrium of it can beat the mechanism of Proposition 3.4. Its consequences include the optimality of first- and second-price auctions with reserve price when buyers are symmetric, the revenue equivalence of standard auction formats, the fact that an asymmetric optimal auction may sell to a buyer without the highest value, and the monopoly inefficiency that the optimal seller sometimes withholds the good. The envelope characterization of Bayesian incentive compatibility (Proposition 3.2) is the tool reused throughout the rest of the book, in public goods provision, bilateral trade and dynamic screening.
The result is classical and fully proved in the literature. What is missing is a machine-checked version at this generality: asymmetric distributions, an arbitrary lower support end , Bayesian (interim) rather than dominant-strategy constraints, and optimality over all incentive-compatible and individually rational mechanisms. Existing formalizations on the platform treat the i.i.d. case with values on .
The obvious argument maximizes the virtual surplus pointwise and declares victory, but this ignores that the seller's feasible set is constrained by monotonicity of every ; the pointwise maximizer is feasible only because regularity makes increasing, and that has to be proved for the interim probabilities, which integrate over the other buyers' types. The revenue identity links interim payments, which integrate over the other buyers' types, to an integral over the whole type space weighted by the virtual valuation, and it is only valid for mechanisms whose lowest types' payments are pinned down. The necessity direction requires showing that ties and zero virtual values are null events, which rests on strict monotonicity of every and on the absolute continuity of the type distribution. Finally, the envelope step requires convexity and almost-everywhere differentiability of , with care at the endpoints of the type interval.
Buyers form a finite type with at least two elements. The prior is the measure on with density on and no mass outside it; each is measurable, strictly positive on and integrates to ; . Allocation and payment rules are total functions whose values on are constrained, and , are prior expectations with the -th coordinate fixed. "Increasing" is weak monotonicity, as in the book; regularity is strict monotonicity of on (Assumption 3.1).
The following conventions are committed to:
The envelope and payoff-equivalence lemmas, and the revenue identity, are reused in later missions of this series, so proofs of the milestones are welcome independently of the goal.
A seller with one good and one buyer whose valuation she does not know faces the simplest problem of mechanism design: choose a selling procedure, anticipating that the buyer will act in his own interest given what he knows. The textbook answer, "post the monopoly price", is usually derived by optimizing over prices alone. The question that opens Börgers' An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015, doi:10.1093/acprof:oso/9780199734023.001.0001) is whether the seller could do better with anything else: negotiation, lotteries, menus of price–probability pairs, or any extensive game she can commit to.
Chapter 2 answers this for one buyer, and in doing so introduces the tools the rest of the book, and most of auction theory, reuse: the revelation principle, the envelope characterization of incentive compatibility, payoff and revenue equivalence, and the virtual valuation. The book's exposition of §2.2 follows Manelli and Vincent (2007), and the nonlinear pricing model of §2.3 is due to Mussa and Rosen (1978, doi:10.1016/0022-0531(78)90085-6); both attributions are the book's own (§2.5, p.29).
The buyer's type is his valuation for the good. His utility is if he receives the good and pays , and if he only pays . The seller's belief about is a cumulative distribution function with density on an interval , , with throughout and .
A direct mechanism is a pair , : the buyer reports a type , receives the good with probability and pays . Write . The mechanism is incentive-compatible if for all , and individually rational if for all . The seller's expected revenue is .
For the extreme-point argument, denotes the space of functions on with the norm, and the set of increasing functions with values in . A point of a convex set is an extreme point if for every at least one of , lies outside .
In the nonlinear pricing model of §2.3 the good is divisible, quantity costs the seller with , and the buyer's utility is , with , , , and . The seller maximizes expected profit . The distribution is regular if the virtual valuation is increasing.
If , then the mechanism
maximizes expected revenue among all incentive-compatible, individually rational direct mechanisms. The comparison class contains every randomized rule with values in ; the statement fixes no distribution and no constant.
Proposition 2.5 says that the elementary monopoly price is not a restriction of the seller's options but the solution of the unrestricted design problem, including every lottery and every indirect procedure. Its one-buyer argument is the template for Myerson's optimal auction (Chapter 3 of the book), whose revenue formula is the multi-buyer form of Lemma 2.4. Proposition 2.6 exhibits the two standard features of screening, no distortion at the top and downward distortion below, which recur in regulation, insurance and contract theory.
All results of the chapter are classical and proved in the book. None of them is formalized on Prove2Me, and Mathlib has neither the revelation principle, the envelope lemma for incentive-compatible mechanisms, nor a maximum principle for linear functions on compact convex sets (Mathlib has the Krein–Milman lemma, IsCompact.extremePoints_nonempty, but not Bauer's maximum principle). The mission therefore produces the first machine-checked foundation for the one-agent screening model on which chapters 3, 4 and 11 of the book build.
The obvious argument for the goal compares the posted price with other posted prices; that comparison is one line and is not the theorem. The content is the comparison with randomized mechanisms: an arbitrary increasing with values in may do better than every deterministic threshold rule unless one shows that expected revenue is linear in and that its maximum over the infinite-dimensional set is attained at an extreme point. That step needs compactness of in and a maximum principle on compact convex sets in a normed space, neither of which is finite-dimensional linear programming. The envelope step (Lemma 2.3) needs absolute continuity of a convex function on a closed interval, including its endpoints, where need not be differentiable. For Proposition 2.6 the pointwise maximizer of the virtual surplus must be shown to be monotone and to satisfy incentive compatibility, which is where regularity enters.
Types are real numbers; every function of the type is a total function and every condition quantifies over only. "Increasing" means weakly increasing (the book's note 3). The distribution is a structure carrying the density , positive and integrable on with total mass , and tied to it by . No measurability or integrability hypothesis is placed on mechanisms: incentive compatibility makes monotone and bounded and measurable, so every expected revenue is a genuine integral.
The explicit formulas are part of the statements: the posted-price mechanism of Proposition 2.5 with ; the payment formulas of Lemmas 2.3–2.4 and Proposition 2.2; in Lemma 2.5; and in Proposition 2.6 the two-case rule for and the payment . The goal fixes , for existence and quantifies over every incentive-compatible, individually rational completion at the tie.
The space is of almost-everywhere classes, because the book's "norm" on bounded functions vanishes on null functions; is the set of classes with an increasing -valued representative, and Lemma 2.7 is an almost-everywhere statement, as the book's notes 4–6 already indicate. Proposition 2.4 is stated for a nonempty compact convex set in a real normed space and a linear map continuous on that set. The revelation principle models a general mechanism as the buyer's reduced strategy set, an arbitrary type, with a purchase probability and an expected payment for each strategy.
A goal that compared the posted price only with other posted prices, or only with deterministic mechanisms, would be trivial and is excluded: the competitors range over all incentive-compatible, individually rational direct mechanisms with valued in .
Reusable beyond this mission: the one-agent envelope and revenue-equivalence lemmas (needed again in Chapters 3, 4 and 11), compactness of monotone functions in , and the maximum principle for linear functions on compact convex sets. Contributions to any of these are welcome.
Chapter XI of Richard Bellman's Dynamic Programming (Princeton University Press, 1957; DOI 10.2307/j.ctv1nxcw0f) studies decision processes whose state is a vector of nonnegative quantities, for example the probabilities that a system is in each of states, or the stocks of commodities, and whose transitions are linear maps chosen stage by stage by a controller. Maximizing a linear functional of the state at every stage leads to the nonlinear difference equation
and, in the limit of small time steps, to differential equations of the form and, when two opposing controllers act, .
These equations are the multiplicative counterpart of the additive Bellman equation. Their growth rate is the natural object for controlled population models, controlled Markov chains observed through their unnormalized state vectors, and economic growth models with a choice of technology. Bellman announced the discrete results in "A Markovian decision process" (J. Math. Mech. 6, 1957) the same year as the book, and R. A. Howard's Dynamic Programming and Markov Processes (MIT Press, 1960) developed policy iteration for the related average-reward problem. The central discrete result of the chapter, Theorem 2, is an early instance of what is now called nonlinear Perron–Frobenius theory (Lemmens and Nussbaum, 2012).
Fix . Row of the matrix carries its own control , ranging over a set ; the joint control is in , and . Bellman insists on this row-wise structure (§ 3): "the set of q's for each row is distinct from the corresponding set for any other row ... so that there is no interaction between the various maximizations". The maximum of a vector over is then taken row by row.
The Perron root is the characteristic root of of largest absolute value, the spectral radius of as a complex matrix. The conditions (10.3) of the chapter are:
For the continuous processes, and , and a solution of , , on is a continuous with , which is the book's "satisfying the equation almost everywhere". The successive approximations are , .
Under (10.3) there is exactly one for which
has a solution with all . That solution is unique up to a positive factor, and
Theorem 2 identifies the optimal long-run growth rate of a controlled multiplicative process with the largest Perron root among the admissible matrices, and shows that the optimal process has a single positive stationary direction. Theorem 3 turns this into the asymptotics of the value iteration : after normalization by the iterates converge to a multiple of the eigenvector. Theorems 1 and 4 are the existence and uniqueness results that justify defining continuous-time controlled processes and differential games by these equations. Theorem 5 recovers the min-max theorem for ratios of bilinear forms (Chapter X) as the long-run limit of a scalar differential game.
The results are classical, and none of them is formalized. Mathlib has the spectral radius and irreducible matrices but no Perron–Frobenius theorem and no Brouwer fixed point theorem; the platform has a statement of the Perron theorem for a single positive matrix (ClassicalGaps.perron_positive_matrix). A formal proof of the goal therefore also produces a reusable monotone, positively homogeneous eigenvector theorem on the positive orthant.
The map is not linear, so the linear-algebra proof of the Perron theorem through the characteristic polynomial does not apply. Existence of a positive eigenvector needs a fixed point argument for a nonlinear map of the simplex (Bellman uses Brouwer's theorem). The identification must connect the nonlinear eigenvalue with the spectra of the individual matrices, which requires the Perron theory of each , including the fact that the Perron root dominates every complex eigenvalue in modulus. For Theorem 3, the iterates may switch controls infinitely often when is infinite, so an argument that the optimal control is eventually constant does not settle convergence. For Theorems 1 and 4, the right-hand side is only measurable in and Lipschitz in with an integrable constant, so the classical Picard–Lindelöf theorem with a continuous right-hand side does not apply directly.
Everything lives in the namespace BellmanDP.Markovian. Vectors are Fin N → ℝ and matrices are Matrix (Fin N) (Fin N) ℝ. Row 's control type is Q i with admissible set S i, and the joint admissible set is Set.pi Set.univ S. The Perron root is (spectralRadius ℂ (A.map (algebraMap ℝ ℂ))).toReal, the largest modulus of a complex eigenvalue; it is not defined as a positive eigenvalue with a positive eigenvector, which would make the Perron–Frobenius content of the goal definitional. The maximized eigen-equation is stated with IsGreatest, so the maxima are attained. The goal and Theorem 3 assume ; for every would qualify.
Conventions and repairs:
Degenerate readings are ruled out: the maxima are attained or taken over nonempty compact sets, never Lean's junk sSup of an unbounded set, and the Perron root is spectral rather than defined through the conclusion. Contributions welcome: a proof of the single-matrix Perron theorem in the form needed here, a Brouwer or Kakutani fixed point theorem for the simplex, and a Carathéodory existence theorem for with an integrable Lipschitz constant, each reusable well beyond this mission.
Assumptions of Physics by Gabriele Carcassi and Christine A. Aidala (book, v3.0, 2025) is a programme to derive the mathematical structures of physical theories from explicit physical requirements. Part II, "Physical Mathematics", begins (Chapter 1) by making precise what it means for a statement to be experimentally verifiable, and shows that a single physical requirement (only countably many tests can be run in an indefinite amount of time) is enough to force the familiar structures of point-set topology onto the space of outcomes of any experiment. This mission formalizes that chapter. It is the first mission of a series on the book; all declarations live in the namespace AssumptionsOfPhysics so that later missions can build on them.
A logical context is represented by its set of possible truth assignments, and a statement (up to logical equivalence) by its truth set . Negation, conjunction and disjunction are complement, intersection and union; the certainty is and the impossibility is ; " is narrower than " means , and are compatible when .
An experimental domain is a family of statements that contains and , is closed under finite conjunction and countable disjunction, and has a countable basis : every element of is obtained from by finite conjunctions and countable disjunctions. Its theoretical domain is the closure of under negation, finite conjunction and countable disjunction. A possibility is a non-impossible that, for every , is either narrower than or incompatible with it; denotes the set of possibilities. The verifiable set of a statement is , and the natural topology on is the topology generated by . A domain is decidable if it is closed under negation.
The chapter's results identify the open sets of a topology with verifiable statements and its points with complete experimental answers (possibilities). Second countability and the axiom are thereby derived rather than assumed, and the cardinality bound limits which mathematical objects can carry experimental meaning. Later chapters of the book (domain combination, properties and quantities, ensemble spaces) rely on these facts. The results are proved informally in the book; no machine-checked formalization of them is known to the drafters. A formalization fixes the precise hypotheses under which they hold (for instance, whether a basis must be countable in Propositions 1.46, 1.48 and 1.60) and provides a reusable library for the rest of the series.
The individual statements are elementary, but several of the book's proofs are informal about two points that a formal proof must handle. First, the possibilities must be shown to cover the space of assignments and to be atoms of ; the book argues through minterms of a countable basis, which needs a "disjunctive normal form" for countably generated families. Second, the natural topology is defined via arbitrary unions while experimental domains are only closed under countable disjunction; showing that every open set is still of the form (Proposition 1.57) requires a second-countability / Lindelöf-type argument rather than direct closure.
Statements are subsets s : Set Ω of an arbitrary type Ω (possibly empty); the experimental domain is the structure ExperimentalDomain Ω, whose field stmts is the family . Generation by finite conjunction and countable disjunction (FinConjCountDisj) includes the empty conjunction and the empty disjunction ; generation with negation (NegFinConjCountDisj) includes . Possibilities form the type D.Possibility, which carries the natural topology as an instance; topological notions (SecondCountableTopology, T0Space, T1Space, DiscreteTopology) are Mathlib's. The primitive notion of verifiability (Axiom 1.27) is not modelled separately: membership in is what all results of the chapter use. Statements involving "a basis" quantify over every basis (countable or not), as in the source. Contributions of reusable lemmas, in particular a disjunctive-normal-form lemma for countably generated families of sets, are welcome.
Chapter IX of Richard Bellman's Dynamic Programming (Princeton University Press, 1957; Princeton Landmarks edition 2010, DOI 10.2307/j.ctv1nxcw0f) recasts problems of the calculus of variations with constraints as dynamic programming processes. A variational problem with an inequality constraint on the control, such as , is awkward for the classical Euler–Lagrange theory: the optimal control switches between the constraint boundary and the interior, and the number and location of the switches are unknown in advance. Bellman's proposal is to replace the continuous problem by a discrete-time one and to solve that by the recurrence relations of dynamic programming, a procedure he describes as the more reliable computational one "in cases treated to date" (§ 11, p. 260).
That proposal is sound only if the discrete values converge to the continuous value as the time step goes to zero. Chapter IX states one such convergence result, Theorem 2 of § 12, and proves it through an Euler-scheme error estimate. The same chapter works through an example (§§ 10–11) whose discrete version is described by Theorem 1. Both are the subject of this mission. The convergence of time-discretized dynamic programming to the continuous value function has since become a standard topic of numerical optimal control (for example the semi-Lagrangian schemes analysed by Capuzzo-Dolcetta and Falcone), and Bellman's § 12 is an early rigorous instance of it.
A state evolves on a horizon under a control with , a running reward and dynamics
Writing with a fractional control turns and into and (phiForm). The continuous value is
over measurable with values in , where solves on (IsTrajectory, contValue).
For the discrete problem uses step and steps (horizonSteps): for ,
and (eulerTraj, discretePayoff, discreteValue). A discrete control defines the step control on (stepControl).
The example of §§ 10–11 has a gain function with , , , as , (IsGainFunction; is one), and value functions (uSeq)
Assume (11): (a) and have continuous second partial derivatives; (b) for , ; (c) throughout that region, or throughout. Then for all , , the set of continuous payoffs is nonempty and bounded above, and
Milestones 3–5 are stated for , as in the book's proof ("Given and "); the goal is stated for , as in the theorem.
Theorem 2 says that the value of a constrained continuous-time control problem can be computed, to any accuracy, by the finite recurrence of dynamic programming on a time grid. Its upper half (12.14) gives a rate: the discrete value never exceeds the continuous one by more than . The lower half (12.17) needs no rate and holds because measurable controls are approximated by step controls. Theorem 1 is a discrete counterpart of the transition curve computed in § 10: below the threshold the whole state is invested, above it an interior amount, and the thresholds increase with the number of remaining stages.
As far as the mission's author could establish, none of these results has a machine-checked proof. The Euler error estimate is classical and has a Gronwall-type proof; Mathlib contains Gronwall's inequality (Analysis/ODE/Gronwall) and Picard–Lindelöf for continuous right-hand sides, but no convergence theory for the value of discretized control problems. The book leaves the proof of Theorem 1 to the reader.
The upper bound (12.14) follows from the Lemma once the continuous and the discrete trajectories are known to stay in a common bounded strip ; that uniform bound is what assumption (11b) provides and must be established first. The lower bound is where the obvious argument fails: an arbitrary measurable control is not a step control on the grid , and passing to a step control changes the trajectory, so the payoff must be shown continuous under almost-everywhere convergence of controls. This uses the trajectory's dependence on the control in , not only on the initial value. Solutions exist in the Carathéodory sense only, so the integral form of the equation is required. For Theorem 1 the induction must carry concavity of and a strict comparison of marginal values across , and is not differentiable at , where .
States, controls and rewards are real; (or ), with the hypotheses imposed where the book imposes them. The conventions:
A trivializing formalization is ruled out: the discrete and continuous values are defined from and by the book's recursions and integrals, not assumed as hypotheses, and the corrected step count is not a free parameter.
Needed infrastructure: Carathéodory existence and uniqueness for Lipschitz right-hand sides with measurable controls, Gronwall estimates for the Euler scheme, and approximation of measurable controls by step functions. All three are reusable beyond this mission, and contributions of any of them are welcome.
Chapter II of Richard Bellman's Dynamic Programming (Princeton University Press, 1957) solves a discrete gold-mining process: a single machine can be used in one of two mines, each use extracts a fixed fraction of the gold remaining in that mine, and each use carries a fixed risk of destroying the machine. Maximizing the expected total gold leads to an index rule: work the mine whose ratio of expected yield to risk is larger. Chapter VIII, A Continuous Stochastic Decision Process, passes to continuous time. Decisions are taken at every instant, and effort may be divided between the mines. The optimal policy is characterized by first-order conditions on switching functions, the objects of Pontryagin's later maximum principle.
It is also an early continuous-time index policy of the kind later central to bandit theory. Chapter VIII treats two mines, then a third decision that works both mines at once.
Mine A holds units of gold and mine B holds . At time a proportion of the machine's effort goes to A and to B (Eq. (7.3)). With the gold remaining, the probability that the machine still works and the expected gold mined, the process is defined by Eq. (7.2):
with , , , . The mining rates and the failure rates are positive. The objective is the expected total gold .
In the three-choice problem (§ 12) a third decision removes gold from A at rate and from B at rate , and fails at rate . A control is a triple with (Eq. (12.2)). For a horizon , the switching functions of Eq. (12.5) are computed along a control. For instance,
They measure the first-order gain from shifting effort towards each decision at time . The linear forms
and the quantity (Eqs. (13.2)–(13.3)) organize the analysis.
For the two-choice process, the maximum of is attained by the policy
The formal statement asserts that some admissible control follows this rule along its own trajectory, and that every such control maximizes over all measurable controls with values in .
Theorem 1 gives a closed-form optimal feedback policy for a continuous-time stochastic scheduling problem. The policy depends only on the slope , and on the line it is a mixed (chattering) policy: the discrete optimum becomes a mixture in the continuous limit. Lemmas 1–5 are a hand-made maximum principle for controls that enter linearly, read almost everywhere. "Theorem 8" says exactly when a composite decision is useless: means that removes gold at a higher failure cost than an equivalent mixture of and .
On the formal side, none of these results is formalized anywhere. Mathlib has no theory of controlled differential equations or of necessary conditions for optimal control. The platform's maximum principles (BertsekasDP.pontryagin_minimum_principle, VectorSpaceOpt.pontryagin_minimum_principle) assume smooth dynamics and a finite horizon with differentiable costs. They do not cover this process, with measurable controls and an improper-integral objective. A formal proof of Theorem 1 would be a complete optimality proof for a continuous-time index policy with chattering controls. The book's argument for Theorem 1 is partly informal; a complete proof, by that route or another, is the target.
The optimization is over an infinite-dimensional set of measurable controls on an infinite horizon, and the objective is not concave in the control. The first-order conditions of §§ 8–9 are necessary, not sufficient, so they do not by themselves prove that the rule is optimal. The book's argument combines them with qualitative facts (the rule is used thereafter once used above the line, and is preferred near the -axis). Making this rigorous requires comparing an arbitrary control with the rule, not just perturbing near an optimum. It is also not known in advance that an optimal control exists, so arguments of the form "let be optimal" need an existence step or a direct comparison. For the lemmas, the switching functions must be shown absolutely continuous, with the derivative formulas (13.1) holding almost everywhere, before "equal on an interval" can be turned into " on the interval".
0, 1, 2 for .Useful infrastructure: the derivative formulas (13.1) for the , a first-variation lemma for under bounded perturbations of a measurable control, and a comparison principle for deteriorating projects. The last is reusable for other continuous-time index policies. Proofs of any milestone, and alternative arguments for Theorem 1, are welcome.