Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A retailer that decides which products to display, an online platform that decides which items to show in a recommendation slot, and an airline that decides which fare classes to open all face the same problem: the set of options offered changes what customers buy, and the substitution pattern is not known in advance. The multinomial logit (MNL) model is the standard model of this substitution in revenue management (Talluri and van Ryzin 2004), and optimizing the offered set under a known MNL model is a classical, efficiently solvable problem (e.g. Rusmevichientong, Shen and Shmoys 2010, for a capacity constraint).
The MNL-Bandit asks what happens when the MNL parameters are unknown and must be learned from the purchases themselves, while revenue is being earned. Earlier approaches (Rusmevichientong, Shen and Shmoys 2010; Sauré and Zeevi 2013) separate exploration from exploitation and need the gap between the best and the second-best assortment to be known. Agrawal, Avadhanula, Goyal and Zeevi (Oper. Res. 2019, arXiv:1706.03880) give a single upper-confidence-bound policy whose regret is of order up to logarithmic factors, with no such knowledge. This mission formalizes that result, Theorem 1 of the paper.
There are products with known revenues . At each time the seller offers an assortment from a family of feasible subsets of , and one customer either buys a product or buys nothing (). Given , the choice follows the MNL model with attraction parameters and :
independently of the past. The expected revenue of is . The family is described by totally unimodular constraints, with the incidence vector of , totally unimodular and integral (cardinality constraints are the main example). A policy chooses from the past choices, and its regret is
The seller knows and but not .
Algorithm 1 works in epochs: epoch offers one assortment repeatedly until a customer buys nothing. Let be the number of purchases of in epoch , the number of the first epochs that offered , and the average of over those epochs. The algorithm forms the upper confidence bounds
starting from , and offers next the assortment in that maximizes .
Under Assumption 4.1 (every , and is closed under taking subsets) there are absolute constants such that for every instance and every horizon ,
The constants are not fixed: the goal asserts the order of the regret, which is what the paper claims.
The milestones follow the proof in Appendix A of the paper:
Theorem 1 shows that learning the choice model costs only revenue, with no dependence on how separated the instance is. The paper also proves a lower bound of order under a -cardinality constraint (its Theorem 2), so for small the bound is optimal up to logarithmic factors. The epoch device used here reduces the analysis of a choice model with substitution to unbiased i.i.d. estimates of each .
The result is proved in the paper (Appendix A, with the concentration bounds in Appendix D). It has not been machine-checked. A formal proof would also settle several printed slips that the formalization had to repair (listed under Formalization scope). The concentration bounds for geometric variables, Theorem 5 and Corollary D.1, are useful outside this mission.
The estimates are counted in epochs whose assortments are chosen adaptively from earlier estimates, so they are not independent a priori. The paper's argument that they are i.i.d. geometric with mean has to be made rigorous for an adaptive policy. The variables are unbounded, so the standard Chernoff–Hoeffding bounds for bounded variables do not apply, and the number of samples is random, which requires a union bound over all its possible values. Finally, the regret is a sum over customers while the analysis is per epoch, and the two are linked through the expected epoch length under a random number of epochs and a horizon that cuts the last one.
Fin N; a choice is none (no purchase) or some i. The parameter is normalized to , as the paper allows. Algorithm 1 is deterministic, so a history of horizon is a sequence of choices with the product law , and every expectation is a finite sum. The revenue is the published definition ChoiceCDLP.MNL.mnlObjective v r 1 S.The paper's own proofs are in its Appendices A and D.
A reentrant line is a queueing network in which every customer follows one fixed route but may return to a station after visiting another one. A manufacturing line can have this pattern when a product revisits the same machine at different processing stages. A station can then have little nominal workload and still face unstable queues under an unfortunate service order. Dai and Weiss studied this gap between nominal capacity and fluid stability for reentrant lines in their 1996 paper. The four-class line associated with Lu and Kumar is their sharp example: its behavior changes at a simple cross-station inequality that is different from either station's ordinary workload constraint.
The paper establishes several positive stability results for other disciplines and networks, then gives an exact boundary for the Lu–Kumar line. Here the exact boundary is the focus. The result concerns fluid models, deterministic large-scale approximations of queue trajectories. It does not assert positive Harris recurrence or transience of the underlying stochastic network in both directions. The paper cites Dai's earlier implication from a stable fluid model to a stable stochastic discipline, but the converse was still open in its concluding discussion (Dai and Weiss 1996, pp. 119 and 133).
There are four customer classes, encountered in order . Classes and use station ; classes and use station . Each class has a positive mean service time and service rate . The external arrival rate is normalized to one. The nominal workloads are and , both assumed strictly below one. These assumptions say that each station has enough average capacity for its own stages, but they leave the scheduling decision unresolved.
At time , is the amount of class- fluid, and is the cumulative service time devoted to that class. The fluid equations balance the inflow and outflow of each class. Outside fluid enters class at unit rate; completion of class feeds class until class exits. Service times and idle times are nondecreasing, and a station's idle time can increase only when its total queue content is zero. A pair with these properties is a work-conserving fluid solution.
The Lu–Kumar priority discipline gives class priority over class at station , and class priority over class at station . Its fluid model adds the priority complementarity condition: service capacity available to a priority prefix can be unused only when that prefix has no immediate workload. For either model, fluid stability means that some common time empties every admissible solution with , with all queues remaining zero for . Instability is the negation of this statement; it does not require every solution to diverge.
Theorem 5.1 and Remark 1 give two connected classifications, under , , and :
The first clause captures the paper's existence of an unstable work-conserving policy: on the unstable side, the named priority discipline supplies one; on the other side, every work-conserving fluid model is stable. The second clause records the particular policy classification stated in Remark 1. Equality belongs to the unstable side: the paper exhibits a periodic nonempty solution there (Dai and Weiss 1996, pp. 125–127).
The milestones follow the paper's own statements and proof claims. The real-analysis extinction criterion of Lemma 2.2(ii) and the maximum-of-components criterion of Lemma 3.2 provide the stability language. Display (3.2), already available as a proved platform theorem, identifies the derivative of an attained maximum at a regular point. The priority condition (4.4) implies the ordinary work-conserving condition (1.13). The unstable half records one first cycle, one solution with every scaled cycle, and instability of the priority model. The stable half records the authors' explicit parameter choice, the two linear Lyapunov conditions, and stability of every work-conserving fluid solution.
The threshold says that the two station-load inequalities alone do not characterize stability of all work-conserving service orders. The extra inequality determines when the entire work-conserving fluid class is stable; its failure admits a concrete priority discipline with a nonempty trajectory. At the boundary , growth need not be strict: periodic fluid behavior already defeats finite-time stability. The result therefore distinguishes the paper's global stability region from the larger parameter region in which both stations are nominally underloaded (Dai and Weiss 1996, Remark 1, p. 125).
A machine-checked development would give reusable definitions for a four-stage reentrant fluid model, its priority complementarity condition, and the precise unit-initial-state notion of stability. The local Lean statements in this proposal compile, but their proofs remain open. The published maximum-derivative fact is the one already proved platform component used by this mission. The other milestones identify the mathematical work needed to formalize the known 1996 result, rather than presenting the result as a new open conjecture.
The ordinary load test controls how much service each station needs on average, but it does not control which class receives service when several buffers at a station are nonempty. In the Lu–Kumar priority discipline, serving a high-priority downstream class changes the future arrival pattern seen by the other station. Thus a direct argument from and to queue extinction fails. On the stable side, checking a single station's workload is also insufficient: its content may fall while earlier-stage fluid continues to feed it. The paper formulates two linear components and a finite maximum; the challenge is to obtain a uniform negative drift whenever that maximum is positive, including times when one station is empty and the other determines the active component (Dai and Weiss 1996, pp. 126–128).
Classes and stations are Fin 4 and Fin 2, with zero-based Lean indices: paper class is Lean index . The fixed station map is . Service times remain real parameters with explicit positivity hypotheses. Paths are total functions of real time, while equations and conclusions apply only on . The external arrival rate is one, and initial size is the sum , since class contents are nonnegative. The nominal-load assumptions are the two strict inequalities in (5.1). The named priority ranking is a permutation; it encodes only the station-local comparisons that matter.
Conditions (1.13) and (4.4), printed as complementarity or “increases only when empty,” use an equivalent interval-constancy condition in Lean. No extra Lipschitz or continuity assumption is placed on solutions: the fluid equations and monotone capacity constraints are intended to supply that regularity. Derivatives at regular points are represented with HasDerivAt. Lemma 2.2(ii) uses the non-strict bound , the version used by the paper's applications, although its displayed hypothesis prints . The p. 127 line involving prints ; (5.3) fixes the intended coefficient as .
The goal uses Definition 1.3 exactly: one uniform emptying time for all solutions of unit initial content. An impossible solution predicate, or an instability claim that only asks for a nonzero state at time zero, would not represent the paper's theorem. The mission needs finite-index sum and maximum infrastructure, absolute continuity and almost-everywhere differentiation on nonnegative time, plus elementary algebra of service rates and the cycle scaling. These components can be reused in later fluid-network missions. Contributions that preserve the source's hypotheses and boundary case are welcome.
A multiclass queueing network can be unstable even when every station has enough capacity on average: the queue lengths grow without bound although each server's nominal load is below one. Kumar and Seidman, Lu and Kumar (1991) and Rybko and Stolyar (1992) exhibited such networks under simple priority disciplines. This raised the question of which networks are stable under every reasonable policy, and which policies are stable in every network. Dai (1995) reduced the stability of a queueing network to the stability of its deterministic fluid model, so that the question becomes one about solutions of a system of linear equations and inequalities.
Dai and Weiss (1996) use this reduction to study reentrant lines, the model of semiconductor wafer fabrication in which a single route visits the same machines many times. Section 6 of their paper treats Kelly-type lines, in which every visit to a station has the same mean service time. Kelly (1979) showed that such networks with exponential service times are stable under FIFO and have a product-form stationary distribution. Theorem 6.1 shows that with two stations, and a route that never visits the same station twice in a row, stability holds under every work-conserving policy, not only FIFO. This mission formalizes that theorem.
A reentrant line has stations and classes . Fluid enters class at rate , moves from class to class on service, and leaves after class . Class is served at station with mean service time and rate . The constituency of station is and its nominal workload is . The traffic condition (1.7) is for every .
A fluid model solution is a pair : is the fluid in class at time and the cumulative service time given to class by time . They satisfy, for ,
with nondecreasing, and the idle time , where , is nondecreasing. The solution is work-conserving if increases only at times when station holds no fluid. The immediate volume of station is .
The line is of Kelly type with station means if for every class . Its routing has no immediate feedback if for every . A set of fluid solutions is stable (Definition 1.3) if there is a such that every solution in the set with is empty from time on.
For a two-station Kelly-type reentrant line without immediate feedback that satisfies (1.7), the work-conserving fluid model is stable: there is with
for every work-conserving fluid solution . The number of classes is arbitrary, of either parity, and the route may start at either station.
The milestones follow the proof on p. 130 and the two general lemmas it uses: the extinction criterion of Lemma 2.2 (ii); the derivative of a maximum at an active index, display (3.2), already proved on the platform; the piecewise-linear Lyapunov Lemma 3.2; the drift identity for , with ; the comparison ; and the verification that meet the hypotheses of Lemma 3.2 with .
The result. Theorem 6.1 gives a class of networks in which stability needs no knowledge of the scheduling policy: any policy that never idles a server with work waiting is stable whenever the nominal loads are below one. For queueing networks this is the property usually called global stability. Through Theorem 1.1 of the paper (Dai 1995, Theorem 4.3) the fluid statement implies positive Harris recurrence of the corresponding multiclass queueing network under every work-conserving head-of-the-line policy. The paper's Remarks 2 and 3 show the boundary: with immediate feedback (the line with all means ), or with three stations, a Kelly-type line can be unstable. A two-station Kelly-type line without immediate feedback is a unidirectional ring with one customer type, so the theorem is a special case of the ring-network result the paper proves as Theorem 6.2. That result is an open goal on the platform (ProcessingNetworks.GlobalStability.ring_globally_stable, Dai and Harrison's Theorem 8.24) in a different encoding of the fluid model.
Formalizing it. The theorem is proved in the paper, and the mission formalizes that proof. No machine-checked proof of the result, or of the Lyapunov lemmas it uses, is known to exist. The mission also produces reusable pieces: a fluid model of reentrant lines in the paper's own formulation, an extinction lemma for absolutely continuous functions, and the max-of-linear Lyapunov lemma, which the paper uses again in §§3 and 5.
The obvious Lyapunov function, the total workload, does not work: a work-conserving policy may starve a station while the other one is busy, so the total content need not decrease. The paper's components each decrease at the constant rate while station is busy. When station is idle, can grow, and the argument then needs the comparison , which requires the alternating route. The analytic difficulty is the passage from these pointwise statements to extinction. Fluid paths are only Lipschitz. The maximum need not be differentiable where the maximum switches, and the drift statements hold only almost everywhere. Lemma 2.2 (ii) and the derivative-of-a-maximum fact (3.2) make this step rigorous. The proof for odd is not printed ("can be proved similarly"), and the formal goal covers it.
All objects live in the namespace DaiWeissFluid.KellyType. The conventions are fixed as follows.
Fin K, Fin I). The paper's class is Lean k - 1.ℝ → Fin K → ℝ, and every equation is imposed for only. Derivatives are taken at via HasDerivAt.The goal must not be trivialized. It quantifies over all work-conserving solutions with , and this set is nonempty: a sorry-free witness with is checked locally. Neither the Kelly-type hypothesis nor the absence of immediate feedback may be dropped (Remark 2), nor may the goal be generalized beyond two stations (Remark 3). Restricting it to even , or to a route starting at station 1, would weaken it.
Contributions welcome: proofs of the general Lemmas 2.2 (ii) and 3.2, which apply across the whole series; the drift identity, which is pure algebra from (1.8); the continuity facts for fluid paths (Lipschitz bounds from (1.10)–(1.12)); and the final assembly.
The simplex method solves linear programs quickly in practice, yet for most pivot rules there are inputs on which it takes exponentially many steps (Klee and Minty, 1972). Smoothed analysis, introduced by Spielman and Teng (JACM 2004), explains the gap: it measures the expected running time when every constraint row of a worst-case input is perturbed by a small random amount of size . For the shadow vertex pivot rule, the running time is controlled by a purely geometric quantity, the number of edges of a random polygon, and the smoothed complexity of the method is essentially an upper bound on that number.
Timeline (bounds on the expected shadow size of smoothed unit LPs, as surveyed in §1.1 of the paper). Borgwardt (1987) proved for rows drawn from a centered Gaussian, asymptotically as ; this is the case of the model below. Spielman and Teng (2004) gave the first smoothed bound, . Deshpande and Spielman (FOCS 2005) improved the dependence on to . Vershynin (SIAM J. Comput. 2009) reduced the dependence on to polylogarithmic, . Dadush and Huiberts (arXiv:1711.05667, STOC 2018, SIAM J. Comput. 2020) proved for Gaussian perturbations by a simpler argument, which also gives bounds for Laplace perturbations.
Fix dimensions and a shadow plane, a two-dimensional linear subspace , chosen independently of the randomness. The constraint vectors are independent, and is Gaussian with center , , and standard deviation in every coordinate, i.e. with density .
Let . The shadow polygon is . An edge of a convex set is a segment , , which is an extreme subset of ; is the number of edges. The number of pivots of the shadow vertex method on the unit LP between two objectives spanning is at most (the paper's Lemma 11 and Theorem 12).
The proof passes through general row distributions with density and mean , described by four parameters: the log-Lipschitz constant (); the line variance (the least variance of restricted to a line); the -th deviation (the least with for all unit ); and the cutoff radius (the least with ). The Gaussian is not log-Lipschitz; the Laplace–Gaussian distribution , whose density equals the Gaussian one inside the ball of radius around and decays like outside, replaces it.
The paper states ; the constant above is the one its proof produces (Theorem 22's proof, Lemma 45, Lemma 46).
The bound gives the best known smoothed complexity of a simplex method, with only dependence on the number of constraints. Section 4 of the paper turns it into a complete two-phase shadow vertex algorithm with expected pivots. The parametrized Theorem 22 applies to any perturbation family with bounded parameters, so it also yields shadow bounds for Laplace and other noise models.
The result is proved; it has not been machine-checked. A formalization adds a verified chain from four distributional parameters to a polygon edge count. The intermediate statements have independent value: an expected-perimeter bound for random polygons, the deterministic chord-length identity for simplices, and tail estimates for the Laplace–Gaussian distribution.
The expected number of edges is a sum, over all index sets, of the probability that their simplex meets in an edge; there are far too many terms for per-set estimates to give a bound polylogarithmic in . The paper's route (inspired by Kelner and Spielman) instead compares the expected perimeter with the expected length of an edge, and the hard part is a lower bound on the expected length of an edge conditioned on it appearing. That conditioning is on a probability-zero configuration (the simplex lying in a fixed hyperplane), and its analysis needs Blaschke's change of variables, the shape decomposition of the simplex, and log-Lipschitz shifts of densities. On the Gaussian side, the density is not log-Lipschitz, which forces the Laplace–Gaussian detour and a comparison of edge counts under two different laws.
is EuclideanSpace ℝ (Fin d), is Fin n, is the natural logarithm. The Gaussian is the published SmoothedSimplex.Shadow.gaussian, the edge relation is the published Hirsch.Adj, and the rows' joint law is Measure.pi. Edges are segments counted once; the perimeter is the sum of edge lengths. Expectations are lower Lebesgue integrals in , and every edge-count bound also asserts almost-everywhere measurability of the count, so the integral is a genuine expectation. Conditional expectations are stated multiplied out (no division by a probability), and the parameters of Definitions 15–18 are upper-bound predicates (lower bound for the line variance), which is how every statement of the paper uses them.
Hypotheses added relative to the page, each implicit there: ; and in Theorem 22; positivity of log-Lipschitz densities; the standing of §3 in Lemma 44. Lemmas 39 and 41 are stated on the explicit conditional densities that the paper derives in Lemma 37, instead of through regular conditional distributions; Lemma 39 takes the conclusion of Lemma 21 as a hypothesis, as its proof uses it. Two printed slips are corrected: Lemma 46's formula is stated for , as its sentence and proof have it, and Lemma 35 refers to Definition 33 (not 34).
The goal mentions only Gaussian rows, , and the edge count of . It cannot be trivialized by an unsatisfiable parameter hypothesis or a bound on edge lengths, since it has neither; and it counts edges of the polygon, not of the polytope .
A complete development needs: Gaussian and Laplace–Gaussian tail bounds; measurability of the edge count of a random polygon; the perimeter monotonicity of convex sets; Blaschke's change of variables (Theorem 7 of the paper, quoted from Blaschke 1935), which Mathlib does not have; and the regular conditioning of Lemmas 32, 37 and 38. The Blaschke formula, the perimeter facts for convex polygons, and the tail bounds are reusable well beyond this mission. Contributions to any milestone, or to these supporting results as separate theorems, are welcome.
A mixed state of a -dimensional quantum system is a positive semidefinite matrix of trace . Writing down takes about real numbers, and is exponential in the number of qubits, so learning in full is expensive. Holevo's theorem and the random access code bounds of Ambainis, Nayak, Ta-Shma and Vazirani say that an -qubit state carries far fewer usable classical bits than its amplitudes suggest. Shadow tomography, introduced by S. Aaronson (arXiv:1711.01053), makes this quantitative: given known two-outcome measurements , how many copies of an unknown are needed to estimate every acceptance probability to within ?
Aaronson shows that copies suffice, polylogarithmic in and . The question this mission addresses is the converse: how many copies are necessary. Section 6 of the paper proves two lower bounds. Theorem 16 gives even when and the are diagonal (a classical distribution). Theorem 19, the goal here, strengthens the dimension term to for genuinely quantum states.
Timeline:
Fix a dimension . A two-outcome measurement is a Hermitian matrix with ; it accepts with probability . The tensor power is the matrix of independent copies. A strategy using copies is a measurement of with finitely many outcomes , given by positive semidefinite matrices with , together with outputs . It succeeds on when, with probability at least over , for every .
The proof works with these further objects, all defined in the mission:
There are a universal constant and a threshold such that for all , all with and all , some measurements on force every strategy that succeeds on every mixed state to use
copies. The goal fixes only the shape , not a constant, so a sharper constant does not invalidate it.
The milestones follow the proof, which sets and :
Theorem 19 shows that the dependence of shadow tomography cannot be removed, and that for shadow tomography is as hard as full tomography: as grows the bound becomes the tomography lower bound, which it therefore contains. Compared with the classical Theorem 16, it shows that quantum states need quadratically more copies in the dimension term. The factor matches the upper bound of Proposition 20 for the decision version, so the -dependence of the lower bound is tight in that setting.
The results are proved in the paper; none of them has a machine-checked proof that we know of. Formalizing the argument requires von Neumann entropy and its additivity on tensor products, the bound , a Holevo-plus-Fano step that turns successful estimation into mutual information, and the existence of many nearly orthogonal half-dimensional subspaces. Each is reusable well beyond this mission.
The obvious attempt adapts the classical argument of Theorem 16, which hides subsets of in a biased distribution. Quantum states allow hidden subspaces instead of subsets, which is where comes from, but two steps change character. First, the hiding family must be shown to exist: Eq. (2) is a concentration statement for random subspaces, and the lemma the paper cites for it (Lemma 18) is misstated, as explained below. Second, the information bound must be carried out for quantum states: the step "learning from requires " needs Holevo's bound and Fano's inequality, adjusted for success probability rather than certainty.
Matrices are Matrix n n ℂ over a finite index type; the goal uses . Conventions committed to:
WildeQIT.IsDensityOperator (positive semidefinite, trace ), reused as a reference item.Fin k → Fin D, with deterministic outputs ; classical randomness can be absorbed into the outcome set.vnEntropy returns on non-Hermitian matrices, which no statement uses.A trivializing formalization is ruled out: the goal does not mention , , , or , the success condition quantifies over all mixed states rather than a vacuous class, and the measurements are fixed before the strategy.
Not drafted:
Contributions welcome: proofs of the milestones; a Haar-measure version of Eq. (2); von Neumann entropy infrastructure (additivity, the dimension bound, concavity); Holevo's bound and Fano's inequality for finite-dimensional states.
The simplex method solves linear programs very fast in practice, yet for most pivot rules there are inputs on which it takes exponentially many steps (Klee and Minty, 1972, for Dantzig's rule; Goldfarb, 1983, for the shadow-vertex rule). Average-case analyses (Borgwardt, 1980s; Smale, 1983) explained good behaviour on random inputs, but random inputs look nothing like real ones. Spielman and Teng introduced smoothed analysis to close this gap: the input is chosen by an adversary and then perturbed by a small Gaussian, and the running time is measured in expectation over the perturbation. They proved that the shadow-vertex simplex method has smoothed complexity polynomial in the number of constraints , the dimension and (Spielman–Teng, J. ACM 2004; this mission follows the preprint arXiv:cs/0111050v7). The work received the Gödel Prize (2008) and the Fulkerson Prize (2009).
Timeline. Borgwardt (1977–1987) bounded the expected number of shadow-vertex pivots for rotationally symmetric random data. Spielman and Teng (2001, STOC; journal 2004) proved the first smoothed bound, with a shadow bound of order — the theorem of this mission. Deshpande and Spielman (FOCS 2005) improved the shadow bound, Vershynin (2009) reduced the dependence on to polylogarithmic, and Dadush and Huiberts (STOC 2018) obtained for small .
Fix and . The data are vectors , the constraint vectors of the linear program subject to for all . Each is a Gaussian of standard deviation centered at a point with : it has density
and the are independent (joint density ).
For a direction , is the set of index sets with such that is linearly independent, the simplex is a facet of , and lies in the cone . In polar terms, is the set of tight constraints at the vertex of the feasible polyhedron that maximizes .
For linearly independent , the shadow is the set of index sets that belong to for some nonzero . Its size is the number of vertices of the projection of the feasible polyhedron onto the plane ; the shadow-vertex method walks along this polygon, one pivot per vertex. Finally
for every , , every pair of linearly independent , every and all centers of norm at most .
The milestones follow the paper's proof, leaves first.
The result. Theorem 4.0.1 is the geometric heart of the smoothed analysis of the simplex method. Section 4.3 of the paper extends it to arbitrary centers, covariances and right-hand sides, and Section 5 combines these extensions with a two-phase method to show that the simplex method has polynomial smoothed complexity. The same shadow bound underlies later analyses of the simplex method, of perturbed polytopes' diameters, and of condition numbers of random linear programs.
Formalizing it. The theorem has been proved, and improved constants are known, but none of this is machine-checked. A formal proof would verify a long and delicate argument: a change of variables of integral geometry (Blaschke's formula), several conditional-density estimates, and explicit constants in the millions. The mission also produces reusable statements about Gaussian vectors and convex hulls of random points.
The obvious approach is to count, for each candidate facet , the probability that appears in the shadow; there are candidates, so a union bound is exponential in . The paper avoids this by discretizing the angle of (Lemma 4.0.6) and bounding, for each fixed direction, the probability that the optimal facet changes within a small angular step. That needs a lower bound on the angle between and the boundary of its optimal facet, conditioned on the facet being optimal. The conditioning changes the distribution of , so the bound cannot come from the Gaussian density alone. The proof changes variables to the facet's normal , offset and in-plane coordinates (Corollary 2.5.3), whose Jacobian contributes the factors and . It then shows that both the distance of the origin to a face of the in-plane simplex and the angle of incidence are unlikely to be small. Measure-theoretic bookkeeping is as hard as the geometry: densities known only up to normalization, conditioning on events of positive measure, and the measure-zero degeneracies the paper sets aside.
Points live in EuclideanSpace ℝ (Fin d). Constraint vectors are indexed by Fin n (0-based), so the paper's is . The Gaussian of standard deviation centered at is Lebesgue measure with the density above, and the joint law is the product measure. Lemma 4.0.6 also uses Mathlib's multivariateGaussian with a positive definite covariance. Expectations of shadow sizes are lower Lebesgue integrals of -valued counts, and their measurability is part of each conclusion. "Density proportional to " and conditional probabilities are stated cross-multiplied, , so no appears.
The shadow is the set of index sets , and the direction is excluded. Including it would add every facet of to the shadow, since lies in every cone, and make the goal false. is represented exactly in , never by a real infimum. Where the paper omits a hypothesis it uses, it is added and recorded in the item: the standing assumptions , and (Lemma 4.2.3 is false without a bound on ), unit length of the reference vector , , and for strict inequalities. Lemma 2.3.7 is stated with rather than the page's , which fails in an edge case.
Infrastructure a complete development needs: Gaussian tail and chi-square estimates; faces and facets of convex hulls; the Blaschke change of variables and the latitude–longitude change of variables on the sphere (not in Mathlib); surface measure on (Mathlib's Measure.toSphere); and the disintegration of the joint law used in the combination lemma. The Gaussian estimates, the combination lemma and the Blaschke formula are useful beyond this mission. Proofs of any milestone, and of supporting lemmas such as the change-of-variables formulas, are welcome.
A perfect graph is one whose coloring problem has a particularly sharp answer on every induced subgraph: the fewest colors needed is exactly the size of its largest clique. This makes a local obstruction, a clique, certify the optimum number of colors throughout the graph. Claude Berge proposed in 1961 that perfection could be recognized by the absence of two kinds of induced odd cycles, one in the graph and one in its complement. The equivalence became known as the strong perfect graph conjecture. Chudnovsky, Robertson, Seymour, and Thomas proved it in their 2006 paper, which also proves a structural decomposition of the graphs under study. The paper connects this question to graph coloring, Shannon capacity, and linear and integer programming. Chudnovsky et al., pp. 51–54
The earlier complement theorem was proved by Lovász in 1972 and appears as Theorem 1.1 in the paper. The strong conjecture remained unresolved for roughly four decades; the authors' Theorem 1.2 settles it. Their proof places a second result, Theorem 1.3, beside the equivalence: a graph with no forbidden odd hole or antihole must either belong to a basic class or admit one of several specified decompositions. The graph classes and decompositions are therefore part of the statement of the route to the main result, not merely vocabulary for a proof. Chudnovsky et al., pp. 52–56
All graphs here are finite and simple. The complement has the same vertices as , and two distinct vertices are adjacent in exactly when they are not adjacent in . For a vertex set , the notation means the induced subgraph on . A clique is a set of pairwise adjacent vertices. Its largest possible size in a graph is , and is the minimum number of colors in a proper vertex coloring of .
A hole is an induced cycle of length at least four. An antihole of is a hole in . A graph is Berge if every hole and antihole has even length. Thus a perfect graph requires for every , while a Berge graph satisfies a restriction on induced cycles in both and . “Induced” matters: a cycle with a chord is not a hole. Chudnovsky et al., pp. 51–52
For the structural milestones, a basic graph is a bipartite graph, the complement of one, a line graph of a bipartite graph, the complement of such a line graph, or a double split graph. The latter consists of paired vertices and with the within-pair and between-pair adjacencies specified on pp. 52–53. A proper 2-join partitions the vertices into two sides with two prescribed complete cross-edge blocks, connected-component conditions on both sides, and a special odd-path condition. A proper homogeneous pair is a pair of vertex sets whose outside vertices split into four nonempty adjacency classes. A balanced skew partition has one side disconnected and the other disconnected in the complement, together with parity restrictions on induced paths and antipaths. Chudnovsky et al., pp. 52–54
The goal is the exact equivalence for every finite simple graph:
No order bound, chosen graph class, or decomposition hypothesis is attached to the goal. Chudnovsky et al., p. 52, 1.2
Theorem 1.1 says that perfect implies perfect. Theorem 1.5 says that a minimum imperfect graph, a Berge nonperfect graph with the smallest vertex count among all such graphs, cannot admit a balanced skew partition. Theorem 13.5 says that a recalcitrant graph—a Berge graph with the listed line-graph, double-split, 2-join, homogeneous-pair, and balanced-skew outcomes absent—has or bipartite. Theorem 1.3 states the decomposition conclusion:
The milestone order records the two reduction results, the later structural capstone, and the decomposition statement it yields. The paper's other section results that establish 13.5 are posed in the remaining missions of this series. Chudnovsky et al., pp. 52, 54–55, 154
Theorem 1.2 gives a forbidden-induced-subgraph characterization of perfect graphs. Its cycle condition is intrinsic to the graph and its complement; its coloring condition quantifies over every induced subgraph. Together with Theorem 1.3, it ties a numerical property of colorings to explicit graph structures and separations. The complement theorem and the exclusion of decompositions for a minimum imperfect graph explain why the structural alternatives have the strength needed for the equivalence. Chudnovsky et al., pp. 52–56
The mathematical theorem was proved in the cited paper. This mission poses its statements in Lean and seeks machine-checked proofs; the draft theorem declarations are open targets. The definition layer is useful beyond this mission: induced holes, Berge graphs, perfection, balanced skew partitions, and the decomposition predicates can support the later missions without changing what each source statement means. No machine-checked proof of these draft targets is claimed here.
The forward implication can be tested on induced odd cycles, but that observation does not settle the converse. Excluding odd holes and antiholes does not give an immediate coloring of an arbitrary induced subgraph. The paper instead establishes a detailed account of what a Berge graph can look like when it is not in a basic class. The delicate point in turning this account into Theorem 1.2 is that each decomposition outcome must be incompatible with a minimum imperfect graph. Ordinary skew partitions are too broad for that role; the balanced parity conditions are part of the statement. The structural conclusion 13.5 collects restrictions established across many later sections, so formalizing its prerequisites is a substantial graph-theoretic task. Chudnovsky et al., pp. 52–56, 154
Lean uses SimpleGraph V with finite vertices, decidable vertex equality, and the Mathlib complement, induced subgraph, chromatic number, clique number, bipartiteness, and line graph. A hole is a list in cyclic order whose adjacency relation agrees exactly with the cycle edges; a path is likewise listed in one orientation with exactly its consecutive edges. Antiholes and antipaths use the complement graph. The empty vertex set is connected, matching p. 54. The double split partition is encoded by an equivalence from the four indexed parts to the whole vertex type, making disjointness and coverage explicit. A minimum imperfect graph is globally minimal by vertex count, among all finite Berge graphs.
No hypothesis beyond the paper's finite, simple graph convention is added to the goal or numbered milestones. In particular, “Berge” includes holes in both and ; “perfect” ranges over every induced subgraph; and the complement occurs only in those decomposition outcomes where the paper places it. A non-induced cycle or a missing complement condition would make the formal target different. The definitions and Lean proofs of the graph classes, their boundary cases, and the structural milestones are welcome contributions. Later missions pose the paper's intervening numbered results rather than duplicating them here.
Interior-point methods minimize a linear function over a convex set by following the minimizers of as , where is a self-concordant barrier for . Each Newton step of such a method shrinks by a factor , where is the self-concordance parameter of , so controls the iteration count of every interior-point method built on (Nesterov and Nemirovski 1994; Nesterov 2004).
Timeline:
Beyond optimization, the entropic barrier is the mirror map that pairs naturally with the exponential-family sampling scheme in bandit linear optimization, which the paper discusses in its §3.1.
Let be a convex body: compact, convex, with non-empty interior . The log-Laplace transform of is
and the entropic barrier is its Fenchel dual
For a function write , , for its directional derivatives. Following Definition 1 of the paper:
The proof works with the canonical exponential family , the probability measure with density , its mean , covariance and third central moment ; with for and its density ; and with the section marginal .
For every and every convex body , is a -self-concordant barrier for with
The result. Theorem 1 gives, for every convex body, an explicit barrier whose parameter is up to a second-order term, against the of the universal barrier, and it is optimal up to that term because is necessary for some bodies. The barrier is defined by a single formula, its derivatives are moments of an explicit probability measure, and its parameter bound reduces to a variance bound for one-dimensional log-concave marginals. Lemmas 2 and 4 are self-contained facts about log-concave laws on (a sharp third-moment bound and a variance-localization bound) that are usable outside this paper.
Formalizing it. The theorem is proved in the paper; nothing here is formalized elsewhere. The platform has a definition of self-concordance (reused here) and results for given self-concordant functions, but no universal or entropic barrier, no exponential family over a convex body, and no moment bounds for log-concave laws. A complete development produces machine-checked versions of the duality facts of Lemma 1, of the two log-concave lemmas, and of the Brunn–Minkowski consequence for section volumes. Two steps of the paper are sketched rather than proved in full: the end of the proof of Lemma 2 ("We omit further details of this proof", p. 12) and, in Lemma 4, a normalization step that cites a lemma stated for isotropic densities. A formal proof either fills or replaces them.
Self-concordance of reduces to self-concordance of by a general duality fact, and that reduces to Lemma 2; the difficulty there is the sharp constant , since generic moment comparisons for log-concave laws give a worse constant. The parameter bound is the hard part. The obvious bound follows from standard concentration for log-concave measures, but any argument that loses a constant factor proves only the 1994 result. The requires the one-dimensional marginal of the tilted measure to be compared with a Gaussian of variance to within a factor , using the fact that is -concave and not merely log-concave. The paper does this pointwise near the mode (Lemma 3) and controls the tails separately (Lemma 4). The pointwise argument assumes smooth, which holds for smooth bodies, and an approximation argument passes to general convex bodies.
is EuclideanSpace ℝ (Fin n), so is the dimension, not a separate parameter. A convex body is compact, convex, with non-empty interior; a lower-dimensional set is excluded, which rules out a formalization in which the barrier and self-concordance clauses hold vacuously.
is a real supremum. On it is the true supremum; elsewhere Lean returns a junk value that no statement reads. The barrier property is a limit within at every frontier point.
Self-concordance (2) is the published ConvexOptimization.IsSelfConcordantOn on interior K, stated by line restrictions with an absolute value. It is equivalent to (2), because flips the sign of the third derivative.
The goal states the parameter as the explicit number . The page says , and (3) is monotone in , so this is the same claim. An existential is not used.
Corrections and implicit hypotheses:
Section volumes use Mathlib's unnormalized -dimensional Hausdorff measure. The normalization constant cancels in and does not affect -concavity. and are fixed pointwise functions, because Lemma 3 evaluates at a maximizer.
Log-concavity on is the published ConvexOptimization.LogConcaveOn on the whole line.
Needed infrastructure that is reusable beyond this mission:
Contributions to any of these, or proofs of single milestones, are welcome.
The k-server problem (Manasse, McGeoch and Sleator, 1990) is the central problem of online computation: servers sit on points of a metric space, requests arrive one at a time at points of the space, and each request must be served by moving a server to it, at a cost equal to the distance travelled. An online algorithm decides without knowing future requests; its quality is its competitive ratio, the worst-case ratio between its cost and the cost of an optimal offline schedule. Paging (caching) is the special case of a uniform metric, and weighted paging the case of a weighted star.
Timeline of the upper bounds for general metrics:
Let be a finite metric space with points and a number of servers. A configuration places server at . A deterministic online algorithm maps each prefix of the request sequence to a configuration that has a server at the last request; its cost on a sequence is the total distance travelled. is the least cost of any schedule serving from the initial configuration . A randomized algorithm is a probability distribution over deterministic online algorithms, all starting at ; it is -competitive if there is a constant such that its expected cost on every request sequence is at most .
The paper works with three auxiliary objects. A σ-HST is a rooted tree whose leaves are the points, in which all edges from a node to its children have one common length, equal to times the length of the edge above that node; the distance between two leaves is the length of the tree path. A weighted σ-HST only requires that the edge above a non-root internal node be at least times each edge below it. In the fractional k-server problem on a tree, the state is a vector of server probabilities on the leaves with and , a request at leaf forces , and moving from to costs , where is the mass below node and the length of the edge above . In the allocation problem on a weighted star with weights , requests carry a location , a monotone cost vector (the cost of serving with servers there) and a server quota .
There is a universal constant such that for all , every metric space with points and every initial configuration , some randomized online algorithm starting at is
In the order the proof uses them:
The theorem broke the exponential gap between the lower bound and the upper bound for randomized k-server, and showed that randomization helps on every finite metric, not only on uniform or specially structured ones. Its two-level method (a fractional algorithm on trees driven by per-node allocation problems, followed by an online rounding) became the template for later work, including the bound on HSTs of Bubeck, Cohen, Lee, Lee and Mądry (STOC 2018) and Lee's bound on general metrics (FOCS 2018).
The result is proved, in this paper. As far as is known it has no machine-checked proof. Formalizing it means formalizing the analysis of an online algorithm driven by a continuous-time process, a potential-function argument with exact constants, a tree contraction with a distortion bound, and an online randomized rounding against a transportation cost. The allocation, HST and rounding statements are reusable for other online problems on trees (metrical task systems, weighted paging).
For a deterministic or randomized algorithm on a tree, the natural recursion splits the servers of each node among its children. Coté, Meyerson and Poplawski showed that this works if each node solves an allocation problem with a strong guarantee: hit cost within a factor of optimal. Integral allocation algorithms cannot achieve this; the integrality gap example of the paper (p. 8) gives a factor . The fractional relaxation avoids the gap, but then the rounding step must keep a randomized state consistent with a fractional state at constant-factor cost, and the HSTs obtained from general metrics have depth growing with the aspect ratio, which a depth-dependent ratio cannot afford. Each of the three reductions (allocation to fractional k-server, deep HST to shallow weighted HST, fractional to randomized) loses only polylogarithmic or constant factors, and the main theorem needs all three at once.
The k-server model, randomized algorithms and competitiveness are the published definitions KServer_model and KServer_randomized; competitiveness carries an additive constant fixed before the request sequence. Trees are finite rooted trees with a parent map, a depth function and positive edge lengths; points of the k-server problem are the leaves, and the theorems take an arbitrary finite metric space together with a bijection to the leaves and the hypothesis that the distance equals the tree distance. Fractional k-server states have exactly units of mass, each leaf at most , and fractional algorithms are measured against the integral offline optimum. The allocation optimum is the integral optimum; cost vectors are finite, non-negative and non-increasing; the diameter of the star is . The cost of changing a randomized state is the transportation cost over couplings, with minimum-matching cost between configurations. Every is an explicit constant quantified before the instance, except that in Theorems 7 and 24 and Lemma 25 it may depend on .
Formalizations that make the targets trivial are excluded: the fractional state must place a full server on every request and stay in , the benchmark is the integral optimum (not the algorithm's own or the fractional cost), and no constant may depend on , , the metric or the tree, since otherwise Theorem 1 would follow from the bound.
The proof of Theorem 1 also uses the embedding of Fakcharoenphol, Rao and Talwar [18] of a finite metric into a distribution over σ-HSTs with expected distortion . It is an external ingredient, not a result of this paper, and is not a milestone; contributions formalizing it (or Bartal's earlier embedding) are welcome, as are formalizations of the integral optimum's properties on trees (Lemmas 21–22 of the paper), which are not stated here.
Hadwiger's conjecture (1943) asserts that for every integer , every graph with no minor is -colourable. It is a far-reaching strengthening of the four-colour theorem, and it is widely described as one of the central open problems of graph theory (Bollobás, Catlin and Erdős called it "one of the deepest unsolved problems in graph theory"). The interest is structural: the four-colour theorem concerns planar graphs, and Hadwiger's conjecture proposes that the only obstruction to -colourability that matters is the presence of a complete graph as a minor.
Timeline.
The case (graphs with no minor are -colourable) is the first open case.
All graphs are finite and simple. A minor of a graph is any graph obtained from a subgraph of by contracting edges. Equivalently, a graph on vertex set is a minor of if there are branch sets , , which are pairwise disjoint, each inducing a connected (nonempty) subgraph of , and such that for every edge of some vertex of is adjacent to some vertex of . has a minor if the complete graph is a minor of , i.e. contains pairwise disjoint connected vertex sets, every two joined by an edge.
A graph is -colourable if its vertices can be coloured with colours so that adjacent vertices receive different colours; is the least such . Write for the statement "every graph with no minor is -colourable". A graph is -degenerate if every nonempty set of vertices contains a vertex with at most neighbours inside the set. The stability number is the largest size of a set of pairwise non-adjacent vertices.
A proof of the conjecture would give a structural explanation of the four-colour theorem that does not depend on planarity, and would settle the chromatic number of every minor-closed class defined by excluding a single complete graph. Partial results already drive the theory of graph minors: bounds on the average degree of -minor-free graphs are the standard input to colouring, and linear Hadwiger-type bounds are used in structural and algorithmic graph theory.
On the formal side, only the smallest cases have Lean proofs: the platform already contains proofs of the cases under a different encoding of minors (namespace Hadwiger), which may be reused after bridging the definitions. The cases , Wagner's bound, the degeneracy lemma, the small extremal bounds and the Duchet–Meyniel theorem have elementary proofs and are realistic targets. The cases depend on the four-colour theorem, whose formal proof exists in Coq but not in Lean; formalizing them here requires either porting that proof or proving the reduction to it. The general conjecture is open.
The natural approach — contracting the colour classes of an optimal colouring — does not produce a minor, because colour classes are independent sets and contraction is only allowed along edges. Degeneracy arguments only give bounds of order , since dense random graphs with no large clique minor have average degree of that order; closing the gap to requires using large chromatic number itself, not just density. Already for the statement is equivalent to the four-colour theorem, so no short proof is expected for any .
Graphs are SimpleGraph V on a finite vertex type V : Type. Minors are encoded by branch sets (IsMinor), complete minors by HasCompleteMinor G t (the complete graph on Fin t is a minor of G), colourability by Mathlib's SimpleGraph.Colorable, and edge counts by the cardinality of the edge set. is the definition HC t. Logarithms are natural logarithms; asymptotic bounds are stated with an explicit existential constant and a ceiling. The case is included; HasCompleteMinor G 0 holds for every graph, so no statement becomes vacuous through a degenerate minor definition.
Useful reusable infrastructure: minor models and their composition, contraction of connected sets, greedy colouring of degenerate graphs, and edge-counting for minor-free graphs. Contributions of intermediate lemmas along the milestones are welcome.
A classical way to recognize an algebraic function is through the arithmetic of its Taylor coefficients. Eisenstein's theorem (1852) says that if a power series is algebraic over , only finitely many primes occur in the denominators of its coefficients. The converse fails in general: many transcendental power series have integer coefficients. Lam and Litt (arXiv:2501.13175) conjecture that the converse does hold for power series that solve an algebraic differential equation at a non-singular point, and that even a weak control on denominators — primes may appear, but only after roughly coefficients — already forces algebraicity.
For linear differential equations, the conjecture is a strengthening of the Grothendieck–Katz -curvature conjecture, one of the central open problems about algebraic solutions of linear differential equations (arXiv:2501.13175). The bounded-denominator form is Problem 1 on Litt's list of open problems (problemsilike.com/1).
Timeline.
Let be a formal power series with rational coefficients and write for its -th formal derivative. Let be a rational function in variables. The series solves the algebraic ODE defined by if
and is defined at . Concretely, for polynomials with and .
For , is the subring generated by . For a function from the primes to , the coefficients of are -integral if for every prime the numbers lie in (denominators prime to ); is superlinear if .
For solving an algebraic ODE as above, the following are equivalent:
Together the four milestones imply the goal; the last two are the open content of the conjecture.
A proof would give an arithmetic criterion for algebraicity of solutions of arbitrary algebraic differential equations, and, for linear equations, would imply the Grothendieck–Katz -curvature conjecture (arXiv:2501.13175). Lam and Litt draw algebro-geometric consequences from the cases they prove.
For formalization: the conjecture is open, so the goal and the two open milestones are research targets. Eisenstein's theorem is a classical result; formalizing it is concrete, self-contained work. The implication (2)⇒(3) is elementary. The cases proved by Lam and Litt are candidates for further milestones.
Integrality of coefficients alone does not detect algebraicity: there are transcendental power series with integer coefficients that satisfy linear differential equations, such as . Its equation is singular at , which the non-singularity hypothesis on excludes; the conjecture asserts that at non-singular points such examples cannot occur. Even for linear equations the statement contains the Grothendieck–Katz conjecture, which is open in general.
PowerSeries ℚ with the formal derivative; rational functions are the fraction field of MvPolynomial (Fin (n + 1)) ℚ, where variable 0 is and variable i + 1 is .IsAlgebraic (Polynomial ℚ) f, i.e. over (equivalently over ).List.TFAE of the three conditions.Useful infrastructure: formal derivatives and substitution for power series, algebraic power series and their coefficient arithmetic (Eisenstein), and -adic valuations of coefficients. Formalizations of Eisenstein's theorem and of the special cases proved by Lam and Litt are welcome.
FormalConjectures/LittProblems/1.lean. https://github.com/google-deepmind/formal-conjecturesBrocard's problem asks for all natural numbers such that is a perfect square. Henri Brocard raised the question in 1876 and again in 1885, and Srinivasa Ramanujan independently posed it in 1913 in the Journal of the Indian Mathematical Society. Only three solutions are known, and the problem is listed as Erdős problem #398 (erdosproblems.com/398). It is one of the simplest-looking Diophantine equations mixing a multiplicative object (the factorial) with an additive shift, and it is a standard test case for conjectures such as the abc conjecture.
No unconditional proof of finiteness is known.
For a natural number , the factorial is , with . A Brown number pair is a pair of natural numbers with
The three known pairs are , and , since , and .
For the conditional milestone, the radical of a natural number is the product of the distinct primes dividing . The abc conjecture asserts: for every there is such that for all positive integers with and ,
This says both that the three known pairs are solutions and that there are no others.
A resolution would settle a question open since 1876 and would be one of the rare complete solutions of a factorial Diophantine equation of this kind. The conditional finiteness result is a standard illustration of how the abc conjecture controls equations of the form .
For the formalization, the known-solutions milestone is a finite computation. The search-bound milestone is a large verified computation; a machine-checked certificate for it would be a reusable artifact. The conditional finiteness milestone formalizes a published argument that assumes the abc conjecture as a hypothesis. The goal itself is an open problem; none of these statements is known to have a machine-checked proof on this platform at the time of drafting.
Congruence obstructions cannot rule out large solutions: for every modulus and every one has , so is a square modulo . Local arguments alone therefore cannot close the problem. The known finiteness argument depends on the abc conjecture, which is itself unproved in the standard form used here. Computer searches only give lower bounds on any further solution.
ℕ); ranges over , so the sign of is not an issue. The factorial is Mathlib's Nat.factorial, with .Prop-valued definition used as a hypothesis in the conditional milestone; it is not asserted anywhere. The exponent is a real power.Brocard.The second part of Hilbert's 16th problem (Paris, 1900) asks for the maximal number and the relative position of the limit cycles of a planar polynomial differential system
where are real polynomials of degree at most . Smale listed it in 1998 among the mathematical problems for the next century and remarked that, apart from the Riemann hypothesis, it seems the hardest of Hilbert's problems (Smale 1998). Even for it is not known whether the number of limit cycles is uniformly bounded.
J. Llibre's survey Sobre el problema 16 de Hilbert (La Gaceta de la RSME 18 (2015), 543–554) organises the question into seven problems and concentrates on a more tractable restriction: algebraic limit cycles, i.e. limit cycles contained in a real algebraic curve. For this restriction there is an explicit conjecture for the maximal number (Conjecture 1 of the survey, first stated in Llibre–Ramírez–Sadovskaia 2010). This mission formalizes that conjecture as its goal, together with the results of the survey on which it rests.
Timeline (as reported in the survey):
A polynomial vector field is a pair of real polynomials in ; its degree is . A solution is a differentiable curve with for all . A periodic orbit is the image of a non-constant periodic solution. A limit cycle is a periodic orbit that is isolated among periodic orbits: some open set contains no periodic orbit other than .
A limit cycle is algebraic if it is contained in the zero set of a non-zero real polynomial . The algebraic Hilbert number is the supremum, over all polynomial vector fields of degree at most , of the number of algebraic limit cycles (a value in ).
A curve is invariant with cofactor if . A family of irreducible curves is generic if (i) no curve is singular, (ii) the top-degree homogeneous part of each curve is square-free, (iii) distinct curves meet transversally, (iv) no three distinct curves share a point, and (v) the top-degree homogeneous parts of distinct curves are coprime.
The equality asserts both that the number of algebraic limit cycles is bounded by the right-hand side for every field of degree at most , and that the bound is attained.
A proof of the goal would settle Problems 6 and 7 of the survey: it would give a uniform bound, depending only on the degree, for the number of algebraic limit cycles, and identify the sharp value. The conjecture is consistent with every example known to the survey: the generic bound of Theorem 4 is sharp for even , and the known non-generic examples exceed the generic bound only in odd degree and by one. Conjecture 2 () is its first open case.
On the formal side, the milestones require a reusable library of planar dynamics that is currently absent from Mathlib: periodic orbits and limit cycles of planar vector fields, hyperbolicity via the divergence integral, inverse integrating factors, invariant algebraic curves and Darboux-type arguments, and topological configurations of Jordan curves. Theorems 1, 2, 4 and 5, Proposition 3 and the cubic example are proved in the literature but, as far as the proposal author knows, not formalized; the goal and Conjecture 2 are open.
The obvious route bounds the number of ovals of the invariant curve (Harnack's theorem) and relates the degree of the curve to the degree of the field. This fails because a field of degree can have invariant curves of arbitrarily high degree, so no a-priori degree bound on the curve is available; Theorem 4 obtains one only under the genericity conditions (i)–(v), and the degree-3 example shows that non-generic curves behave differently. On the formal side, the dynamical milestones (Theorems 2 and 5, the cubic example) need Poincaré–Bendixson-type planar topology and uniqueness of solutions, which Mathlib does not yet provide.
MvPolynomial (Fin 2) ℝ with variable 0 as and 1 as ; points are ℝ × ℝ. The degree of a field is the maximum of the total degrees of and , and ranges over fields of degree at most , matching equation (1) of the survey.Set.encard values in ℕ∞, so an infinite family is , never silently ; is an iSup in ℕ∞, so the goal also asserts finiteness.HasDerivAt at every real time). A limit cycle is isolated among periodic orbits contained in a neighbourhood. An algebraic limit cycle lies in the zero set of some non-zero polynomial, with no degree restriction on the curve.ℕ∞, not an inequality over a possibly empty family.Contributions welcome: a planar ODE library (uniqueness, flows, Poincaré–Bendixson), Darboux theory of integrability, and proofs of the classical milestones.
Large retailers hold point-of-sale and loyalty-card data that their suppliers cannot observe, and many of them sell access to it through data-sharing programs; others share the same data for free, or with only some suppliers (Shang, Ha & Tong 2016, §1). When two competing manufacturers sell through one common retailer, sharing a demand signal with a manufacturer changes how he sets his wholesale price, which in turn changes the retailer's margins and the rival's demand. Whether the retailer wants to share, with how many manufacturers, and at what price, is therefore a question about a multistage game with incomplete information.
Shang, Ha and Tong answer it for linear demand, a linear-expectation signal and quadratic production costs, under two contracting protocols. This mission covers the production economy case (marginal cost decreasing in volume, §6 of the paper), in which the retailer may have an incentive to share information even without payment. A companion mission covers production diseconomy (§5).
Two manufacturers sell substitutable products through a common retailer. Demand for product is
where is the retail price, measures competition intensity and is a demand shock with mean and variance . The retailer observes a demand signal with and a linear-expectation structure , where is the signal weight. Producing units costs with ; the paper writes and assumes (the Assumption, p. 251). Retailing is costless.
The game has three stages.
The ex ante profits of the pricing equilibrium are denoted , , , for a manufacturer and for the retailer, the number of informed manufacturers. , , denote the equilibrium number of informed manufacturers without contracting, under concurrent and under sequential contracting.
For every and , pricing equilibria exist, concurrent outcomes and sequential SPEs exist, and for every concurrent outcome and every SPE (either first mover)
where is the retailer's profit after side payments and the manufacturers' total profit net of them. The second inequality is asserted for all except at most two values depending only on . The comparisons about every pricing equilibrium family exclude the single value (see Formalization scope). The paper says "higher"; the inequalities are weak because both sides coincide on intervals of positive length.
Proposition 8(d) says that a common retailer who sells information prefers to sell it sequentially, and that the manufacturers bear the cost: sequential offers let her extract a larger payment from the first manufacturer, because his outside option depends on what she will do with the second. Together with Propositions 6 and 7 it explains why retailers under production economy share with only a subset of suppliers once economies of scale or competition are strong, and why a retailer may share data for free, a practice the diseconomy model cannot produce.
The results are proved in the paper, partly by "it is straightforward" arguments (the proofs of Lemmas 2–5 are omitted). No part of the paper is formalized. A formalization adds a machine-checked account of the equilibrium selection at the boundary payments, where the paper's case analysis is informal, and of the points at which the retailer is indifferent between outcomes.
The pricing stage is a Bayesian game with a continuum of strategies: an informed manufacturer's strategy is an arbitrary square-integrable function of the signal. Lemma 1's uniqueness needs the Assumption (without it the manufacturer's problem is not concave) and a conditional-expectation argument, not a finite-dimensional computation. The comparisons of Lemma 5 are sign conditions on rational functions of whose thresholds , are implicit roots. The contracting stage is where the naive argument fails: at the boundary payments several equilibria give the retailer the same payoff but the manufacturers different payoffs, so "the" outcome is not well defined there, and a direct comparison of closed-form profits at the paper's selected equilibria does not cover every equilibrium.
Lean represents manufacturers by Fin 2, statuses by an inductive type with informed and uninformed, and a pricing strategy by a function of the signal value. The committed conventions are these.
The ex ante profits in every statement are those of an equilibrium of the pricing game on the signal model, not the §4.2 closed forms; a formalization that defined them by the closed forms would reduce the goal to algebra and a game, and is ruled out. The model layer (signal model, pricing equilibrium, payoff table, both contracting games) is shared, name for name, with the production diseconomy mission. Contributions are welcome on each milestone, and on reusable pieces: linear-expectation signals, and pointwise optimization under conditional expectation.
Several classical theorems of combinatorial optimization say that a family of sets arising from a graph packs: the maximum number of pairwise disjoint members equals the minimum size of a set meeting every member. König's theorem on bipartite graphs, Menger's theorem, the max-flow min-cut theorem of Ford and Fulkerson, Edmonds' branching theorem and the Lucchesi–Younger theorem all have this form (Seymour 1977, (1.1)–(1.5)). In the capacitated version (weights on elements, integral flows) the max-flow min-cut theorem says more: the packing property survives every deletion and replication of elements. Clutters with this stronger property are called Mengerian. For each – matrix they are exactly the systems whose covering linear program and its dual have integral optima for every integral weight vector, which is why the notion matters to integer programming and polyhedral combinatorics.
Seymour's paper answers the question for the class of binary clutters, the clutters coming from binary matroids, which includes path collections, cut collections and odd-circuit collections of graphs. Earlier, Gallai's theorem implied that ports of regular matroids are Mengerian (Seymour 1977, p. 200); combined with Tutte's excluded-minor characterization of regular matroids, this showed that binary clutters without or minors are Mengerian. Seymour shows that the second excluded minor is unnecessary, so a single small clutter is the only obstruction.
All sets are finite. A clutter is a finite collection of finite sets, no member of which is contained in another; and are the two trivial clutters. Its ground set is . The blocker is the collection of minimal subsets of that meet every member of , and is the minimum cardinality of a member of .
is Mengerian if , or if for every weight map there is an integral packing with for each and
For a set , the deletion is and the contraction is the collection of minimal members of (minimal, not minimal nonempty). A minor of is any clutter obtained by a finite sequence of deletions and contractions.
A clutter is binary if is odd for all and ; this is condition (3.2)(ii) of the paper, which is equivalent to being a port of a binary matroid. Finally
the triangles of with its edges labelled .
For the structure theory, a circuit of a binary clutter is a minimal nonempty with even for every ; and are parallel when is a circuit, and the point is the parallel class of . With , is critical if . In a critical binary clutter, means that every member of containing contains while , and is initial if no has . MBC abbreviates "Mengerian binary clutter".
For every binary clutter ,
In the order the proof uses them:
The theorem is an excluded-minor characterization of the max-flow min-cut property. For binary clutters it decides exactly when the covering system , has integral optimal primal and dual solutions for every integral cost vector, and it identifies as the single obstruction. Its matroid form (the Corollary, p. 220) states that for a matroid the port is Mengerian for every element if and only if is binary and has no minor. Consequences discussed in the paper include the two-commodity setting of (3.5): the clutter of minimal edge sets joining to or to is Mengerian exactly when the graph does not reduce to the configuration of its Figure 2. The theorem is also a basis for later work on ideal and Mengerian clutters, such as Cornuéjols' book Combinatorial Optimization: Packing and Covering (SIAM, 2001).
The result has been proved since 1977. To our knowledge no machine-checked proof exists. Mathlib at the pinned revision has matroids but no clutters, blockers, clutter minors, or matroids representable over GF(2). This mission builds that layer. The minor-closedness of the Mengerian property (2.3), the parity decomposition (3.6)(iii) and the structure theory of critical Mengerian binary clutters (4.3)–(4.6) are results in their own right and are useful beyond the main theorem.
The "only if" direction is short: minors of Mengerian clutters are Mengerian, and fails with unit weights. The "if" direction is, in the author's words, "very much harder". A natural first idea is to show directly, by LP duality, that the covering polyhedron of a -free binary clutter is integral. This does not work: integrality of the polyhedron is the weak max-flow min-cut property, and itself has that property while not being Mengerian, so no argument that sees only fractional optima can separate the two cases. The paper's proof works with a minimal counterexample and derives the minor from the structure of critical Mengerian binary clutters in Section 4; its intermediate claims (5.2)–(5.39) hold only for that minimal counterexample, which is why they are not milestones here.
Elements form a type α with decidable equality. A clutter is L : Finset (Finset α) with the clutter axiom as a hypothesis, is the union of members, and deletion and contraction take an arbitrary finite set . Weights and packings are -valued. The minimum in the Mengerian condition is expressed as "some of least weight has weight equal to the packing value", never as an infimum. is Mengerian by the paper's convention, and , which the paper leaves undefined, has the junk value in Lean; every item reading excludes or is vacuous there. "Minor" is the reflexive–transitive closure of single deletions and contractions. "Has a minor" means that some minor equals the image of (on Fin 6, with the paper's labels shifted down by one) under an injective relabelling Fin 6 ↪ α. Binary clutters are defined by (3.2)(ii); the paper defines them as ports of binary matroids and quotes (3.2) [15, 28] for the equivalence, and Mathlib has no GF(2)-representable matroids at this revision. Circuits are defined intrinsically, which makes (3.6)(ii) hold by definition.
Four readings would change the theorem and are ruled out: real-valued packings (the weak max-flow min-cut property, which has, so the goal would be false), a non-minimal blocker or one not restricted to , dropping the exception, and reading " minor" as literal equality instead of isomorphism.
A complete development needs the blocker calculus ((2.1), (2.2), cited from [28] with proofs omitted), the parity theory of binary clutters, and the replication operation . The clutter layer (blocker, minors, Mengerian, binary, circuits) is reusable for later work on ideal clutters, Lehman's theorem and the Corollary's matroid form. Proofs of any milestone, of the helper facts , (2.1) and (2.2), and of the equivalences in (3.2) are welcome.
In quantum mechanics the spectrum of a Hamiltonian splits into two parts that behave very differently under perturbation. Isolated eigenvalues of finite multiplicity (bound states) move, split or disappear when the operator is changed even slightly; the rest of the spectrum, which carries scattering states and accumulation points of eigenvalues, is far more rigid. Weyl's theorem makes this rigidity precise: if two self-adjoint operators have resolvents that differ by a compact operator, their essential spectra coincide. It is the standard first step in locating the spectrum of a Schrödinger operator : one shows that is a relatively compact perturbation of , concludes , and is left with the discrete eigenvalues below zero.
The result goes back to H. Weyl's 1909 work on compact perturbations of bounded self-adjoint operators; the resolvent formulation for unbounded operators is the one used in modern texts such as Reed–Simon (Vol. IV, Sec. XIII.4) and Teschl's Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009), Section 6.4, which this mission follows.
Let be a complex Hilbert space and a linear operator with domain . For , the resolvent exists when maps bijectively onto with a bounded inverse. The resolvent set is the set of such , and the spectrum is .
The discrete spectrum is the set of eigenvalues of that are isolated points of and whose eigenspace is finite dimensional. The essential spectrum is .
A sequence with , for every (weak convergence to zero) and is a singular Weyl sequence for at .
An operator is compact if it maps bounded sets to relatively compact sets; denotes the compact operators. An operator is relatively compact with respect to if and for one . is bounded if and on ; the infimum of admissible is the -bound. A symmetric operator has defect indices .
For self-adjoint and ,
The result. Weyl's theorem reduces the determination of the essential spectrum of a perturbed operator to that of a simpler reference operator. Combined with Lemma 6.22 and the Kato–Rellich theorem, it yields for every relatively compact symmetric ; Lemma 6.23 extends this to perturbations of the form . These are the inputs to the HVZ theorem for -body systems, to the spectral analysis of one-particle Schrödinger operators with decaying potentials, and, via Theorem 6.20, to the observation that boundary conditions at a limit-circle endpoint do not affect the essential spectrum of a Sturm–Liouville operator. The Weyl criterion is independently useful: it is how points are shown to lie in in concrete examples.
Formalizing it. The results are classical and proved in every text on the subject. None of them is formalized: Mathlib has compact operators and the adjoint of a densely defined LinearPMap, but no resolvent set or spectrum for unbounded operators, no discrete or essential spectrum and no relative compactness. This mission asks for formal proofs of Teschl's statements and, with them, a reusable layer of definitions (resolvent of a LinearPMap, , , singular Weyl sequences, relative compactness) on which later chapters (free Schrödinger operator, HVZ theorem) can build.
The obvious route to all of these statements goes through the spectral theorem: Teschl's proof of the Weyl criterion uses spectral projections and spectral measures , and his characterization (6.27)–(6.28) of by ranks of spectral projections presupposes the functional calculus. Mathlib has no spectral theorem for unbounded self-adjoint operators, so this route requires either building it or finding arguments that avoid it. The definition of used here is deliberately the PVM-free one of p. 145, which makes the statements expressible now but moves the difficulty into the proofs: showing that a point of carries a singular Weyl sequence requires controlling approximate eigenvectors near a non-isolated spectral point or an eigenvalue of infinite multiplicity without projections.
A second difficulty is domain bookkeeping. , , and all involve unbounded operators with different domains, and identities such as the second resolvent formula must be established on the correct domains. Theorem 6.20 requires relating the resolvents of two self-adjoint extensions through the finite-dimensional defect spaces.
The Hilbert space is {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]; separability is not assumed, since no statement of the section needs it. Unbounded operators are Mathlib LinearPMaps H →ₗ.[ℂ] H, self-adjointness is Mathlib's IsSelfAdjoint (which implies a dense domain), and symmetric operators are densely defined by definition, as in the book. The resolvent is the bounded two-sided inverse of of p. 73 (IsResolventAt), and , are defined from it; Mathlib's Banach-algebra spectrum is not used. "For one " is an existential over and the two resolvents. Compactness is Mathlib's IsCompactOperator, which on a Hilbert space agrees with the book's norm closure of finite rank operators. for bounded is K +ᵥ A (domain ); for unbounded is the LinearPMap sum with domain . The -bound is valued in and is for an operator that is not bounded. The defect indices are "equal and finite" when both defect spaces are finite dimensional with equal finrank.
No projection-valued measure or functional calculus is taken as data, and none is needed: every statement is phrased without . For this reason the second half of Lemma 6.21, for , and the form-compactness results Lemma 6.26 and Corollary 6.27 of Section 6.5 are not part of the mission.
A trivializing formalization is ruled out: the discrete spectrum requires all three of "eigenvalue", "isolated in " and "finite-dimensional eigenspace", so is neither empty nor all of by definition, and the resolvent hypothesis of Weyl's theorem is an existential over genuine resolvents, never a junk value outside .
A complete development needs the resolvent identities for LinearPMaps, the relation between self-adjointness and real spectrum, weak convergence of bounded sequences, and the fact that compact operators map weakly null sequences to norm-null ones. The definitions of resolvent, , relative compactness and -bound are shared with other chapters of this series and are intended for reuse. Contributions of general lemmas on LinearPMap resolvents are welcome.
Stochastic fictitious play is a basic model of learning in repeated games. Each period every player best responds to the empirical frequencies of the opponents' past play, after the player's payoffs have been hit by a fresh random shock. It was introduced by Fudenberg and Kreps (1993), is a standard object in the theory of learning in games (Fudenberg and Levine, The Theory of Learning in Games, 1998), and underlies the quantal-response and logit-learning models used in experimental economics and multi-agent reinforcement learning. The question is whether the players' beliefs settle down, and on what.
Potential games, in which all players receive the same payoff, cover pure coordination games and, after the usual payoff transformations, congestion games and weighted potential games. For them Hofbauer and Sandholm (Econometrica 70, 2002) proved that stochastic fictitious play converges almost surely, and that under a generic regularity condition the limit is a single linearly stable rest point of the perturbed best response dynamic.
Timeline. Fudenberg and Kreps (1993) and Kaniovski and Young (1995) established convergence in 2×2 games. Benaïm and Hirsch (1999) related the process to its mean ordinary differential equation and proved convergence in some player, two strategy games. Hofbauer (2000) and Hofbauer and Hopkins (2000) constructed Lyapunov functions for the deterministically perturbed dynamics. Hofbauer and Sandholm (2002) combined these with a representation theorem for random utility models and with Pemantle's (1990) nonconvergence theorem to obtain the result formalized here.
A player game has finite strategy sets and utilities on pure profiles . The game is a potential game if for all players and all profiles. Mixed profiles form , and player 's payoff vector is .
Player 's payoffs are perturbed by a random vector with a strictly positive density on . The choice function is , assumed continuously differentiable, and the perturbed best response is .
In standard stochastic fictitious play, shocks are independent over time and across players. From an arbitrary initial pure profile, at time each player plays a maximizer of , where the beliefs are the time averages
The mean dynamic of this process is the perturbed best response dynamic
A rest point of (P) is hyperbolic if every eigenvalue of restricted to the tangent space of has nonzero real part, and linearly stable if every such eigenvalue has negative real part. and denote the rest points and the linearly stable rest points.
By Theorem 2.1 of the paper, for an admissible deterministic perturbation , so (P) coincides with the deterministically perturbed dynamic (PV), in which the argmax replaces .
For every potential game, every family of densities meeting the conditions above, every probability space, independent shock family and initial profile:
In attack order: Theorem 2.1 (the representation), Proposition 4.1 (the function is a strict Lyapunov function for (PV)), the identification of the critical points of with the rest points of (PV), Proposition 4.2 ( under smoothness), Proposition 4.3 (under hyperbolicity is finite and equals ), and Lemmas A.5 and A.4 (a uniform nondegeneracy condition for the noise of the process).
The result. Theorem 6.1(iii) says that decentralised, boundedly rational learning in common-interest games does not cycle or wander: beliefs converge to a rest point of the perturbed dynamic, and generically to one that is linearly stable, hence a local maximizer of the perturbed potential . Rest points approximate Nash equilibria as the noise vanishes (Proposition 3.1 of the paper), so the theorem is a selection result for equilibria reached by learning. It is also a template for the stochastic-approximation analysis of learning algorithms whose mean dynamic has a Lyapunov function.
Formalizing it. The theorem is proved in the paper, but none of its ingredients is machine-checked: the random utility representation, chain recurrence of flows, Lyapunov arguments for (PV), and the stochastic-approximation step (Benaïm–Hirsch, Benaïm, Pemantle) are all absent from Mathlib and from this platform. A complete development produces a reusable stochastic-approximation layer, not only this theorem.
The obvious argument, "(P) has a strict Lyapunov function, so the process converges to its rest points", fails twice. First, a strict Lyapunov function does not by itself make every chain recurrent point a rest point (the paper cites counterexamples of Akin and of Benaïm); the step needs either Sard's theorem for a function or finiteness of the rest points, and the stochastic-approximation theory controls the process only through the chain recurrent set. Second, convergence to linearly stable points requires showing that the process avoids unstable rest points. This rests on Pemantle's theorem, whose nondegeneracy hypothesis must be verified uniformly over states and directions (Lemma A.4). Neither step follows from the ODE alone: the theorem is about the random process .
Players are Fin p with p ≥ 2, strategies Fin (n α) with n α ≥ 1, and mixed profiles live in the ambient space (α : Fin p) → Fin (n α) → ℝ, on which every vector field is defined. Choice probabilities are probabilities of strict argmax events under volume.withDensity (f α). The process is defined pathwise from the shocks, ties broken by the smallest index (a null event), and the theorem quantifies over every probability space and every independent shock family with the given laws. Derivatives of are those of composed with the projection onto the plane . Eigenvalues are the complex roots of the characteristic polynomial of the derivative restricted to the tangent space of . Solutions of a dynamic are differentiable curves on that stay in , and chain recurrence uses -chains with times .
A formalization about the ODE (P) in place of the process , a fixed noise law such as logit, or convergence to in place of would prove a different and weaker statement. These are excluded.
Needed infrastructure: the random utility representation (mission I of this series), flows and chain recurrence of vector fields on compact sets, Sard's theorem for real-valued functions, and the stochastic-approximation theorems of Benaïm–Hirsch (1999, Thm 3.3), Benaïm (1999, Props. 5.3 and 6.4) and Pemantle (1990, Thm 1). The last three are reusable well beyond this mission, and contributions of any of them are welcome.
Several complex variables studies functions of that are holomorphic in every coordinate. It underlies complex geometry, the theory of analytic spaces, and parts of mathematical physics and harmonic analysis. Every later topic of the subject (domains of holomorphy, pseudoconvexity, the -problem, the Bergman kernel, analytic varieties) starts from the same foundation: a function that is holomorphic in each variable separately and locally bounded is jointly smooth and is locally the sum of a convergent power series. This mission formalizes that foundation as it appears in the first chapter of Jiří Lebl's textbook Tasty Bits of Several Complex Variables (jirka.org/scv).
Historically, the step from separate to joint regularity is due to Osgood (1899), who showed that a continuous (later: locally bounded) function that is holomorphic in each variable separately is holomorphic; Hartogs (1906) later removed the boundedness assumption altogether, a much harder theorem not covered here.
Points of are . For a center and a polyradius with every , the polydisc is
a product of open discs . Its distinguished boundary is the torus , and denotes the closed polydisc.
A function on an open set is holomorphic (the book's Definition 1.1.2) if it is locally bounded (every point of has a neighborhood on which is bounded) and complex-differentiable in each variable separately: for every and every , the one-variable limit
exists. A map is holomorphic if every component is.
A multi-index is , with , and . A power series is summed over all multi-indices; since has no natural order, convergence means absolute convergence, and the series converges uniformly absolutely on a set when converges uniformly for . The Wirtinger derivative is for , and applies exactly times for each .
Let be a polydisc. If is continuous and holomorphic in , then there are coefficients with
the series converging uniformly absolutely on every compact subset of . Conversely, a function defined on by such a series is holomorphic on . Both directions are part of the goal.
In attack order:
Theorem 1.2.1 is the statement that makes the theory of several complex variables possible: it identifies the book's elementary, one-variable-at-a-time definition of holomorphy with local representability by power series. Uniqueness of the coefficients, the Cauchy estimates, the identity theorem, the maximum principle, and holomorphy of compositions and of implicit functions all follow from it, and every later chapter of the book (Hartogs figures, pseudoconvexity, the Bergman kernel, Weierstrass preparation) uses it without comment.
Mathlib already develops complex analysis in several variables for Fréchet-differentiable maps: analyticity of DifferentiableOn ℂ functions, torusIntegral, Cauchy integrals over circles, and Osgood-type regularity for maps on are available or published on the platform. What this mission adds is the bridge from the weaker separate notion of holomorphy, with local boundedness, to these results, stated with multi-index power series and uniform absolute convergence on compact sets exactly as in the textbook. The results are classical and fully proved in the book; none has a machine-checked proof in this form.
The hypothesis controls only along complex lines parallel to the coordinate axes, plus a bound. Nothing in the definition says that is continuous, let alone jointly differentiable, so no joint limit, Fréchet derivative, or change of the order of integration is available at the start. Every tool that the one-variable theory and Mathlib's multivariable library supply presupposes joint regularity; the obstacle is to obtain it from separate information.
A second difficulty is bookkeeping: power series over have no natural order, so convergence must be handled as unconditional summation with a uniformity statement over compact sets, and iterated Wirtinger derivatives must be related to derivatives of the series term by term.
Fin n → ℂ; multi-indices are Fin n → ℕ. A polyradius is ρ : Fin n → ℝ with the hypothesis ∀ k, 0 < ρ k; the polydisc is defined coordinatewise (not Metric.ball, which only gives equal radii).IsHolomorphicOn f U: local boundedness plus complex differentiability at of (via Function.update). Openness of is a hypothesis wherever the book says "open". Maps into are holomorphic componentwise.DifferentiableOn ℂ. That makes Proposition 1.1.3 and the first half of the goal off-target (they would follow from existing library results) and is not the book's definition.closure (polydisc a ρ); "continuous on , holomorphic in " keeps both hypotheses.HasSum (unconditional summation) of the terms to , and uniform absolute convergence on a set means the finite partial sums of , directed by inclusion, converge uniformly on . Mathlib's HasFPowerSeriesOnBall is not used: its balls for the sup norm are equiradial polydiscs only.torusIntegral, whose parametrization includes the Jacobian and orients each circle positively. The integrands are continuous on the compact torus, so no integrability hypothesis is needed.deriv along and ); iterates it. is LinearMap.det of the real Fréchet derivative, which is basis independent.A complete development needs the one-variable Cauchy integral formula (in Mathlib), iterated circle integrals and torusIntegral, and summation over Fin n → ℕ. The regularity bridge from separate to joint holomorphy and the multi-index power-series API are reusable across the whole series of missions on this book; contributions of either as standalone lemmas are welcome.
Chapter 8 is where discrete convex analysis explains why it needed two separate notions —
M-convexity (exchangeability) and L-convexity (submodularity) — rather than one. The answer is
conjugacy: under the classical Legendre-Fenchel transform, the two classes turn out to be exactly
dual to each other, the discrete analogue of the fact that convex analysis's transform is
self-dual within a single class of convex functions. Mission 10-conjugacy-i proved the
integer-lattice version of this fact (Theorem 8.12) but explicitly deferred the polyhedral
version — Theorem 8.4, the chapter's own headline "Conjugacy theorem" — noting it needed a
real-variable M-/L-convex-function layer the series had not yet built. That layer now exists,
built across missions 23-24-ch06*-mconvexfunctions and 26-27-ch07*-lconvexfunctions. This
mission proves Theorem 8.4 and its companions: the polar-cone correspondence it induces, its
nonpolyhedral generalization, the separation and Fenchel-duality theorems for M♮-/L♮-convex
functions, and the basic theory of M2-convex functions (sums of M-convex functions), which the
Edmonds intersection theorem's own combinatorics is built from.
Fix a finite ground set . For , the Legendre-Fenchel transform is . A polyhedral convex function is M-convex () if it satisfies (M-EXC[R]); is L-convex () if it satisfies (SBF[R]) and (TRF[R]). A concave function is always represented via , an ordinary convex function, so every "" hypothesis is restated as "" — an equivalent formulation avoiding any need to represent in the codomain. A polyhedral cone's polar is . A function is M2-convex if it is the sum of two M-convex functions.
The classes of polyhedral M-convex functions and polyhedral L-convex functions are in one-to-one
correspondence under the Legendre-Fenchel transform: ,
, and the transform is an involution (,
) on each class, with the identical statement for the M/L
variants. This is the theorem mission 10-conjugacy-i deferred, citing exactly the missing
infrastructure this series has since built.
Twelve further results build the surrounding theory. Proposition 8.2 gives the easy
two-variable case of the general submodularity-preservation fact (Theorem 8.1, already a
milestone of mission 10-conjugacy-i); Proposition 8.3 is the technical minimizer-difference
lemma the goal's harder direction is built from. Theorem 8.5 derives the M-convex/L-convex cone
polarity from the goal, and Theorem 8.6 extends the correspondence beyond the polyhedral case to
general closed proper convex functions. Proposition 8.14 and Theorems 8.15-8.16 build the
separation theory for M♮-/L♮-convex and concave function pairs, with integral witnesses when the
functions are integer valued; Theorem 8.21 (parts 1-2) derives the Fenchel-type strong-duality
equality these separation theorems make possible. Propositions 8.29-8.30 and Theorem 8.31
(plus Theorem 8.32, found by direct reading immediately after 8.31) build the basic theory of
M2-convex functions: their domains and minimizer sets are M2-convex, they are integrally convex,
and their global optimality reduces to a finite local check.
The goal is the theorem that retroactively explains this entire series' two-track structure:
missions 20-25 (M-convex sets and functions) and 08/21/26-28 (L-convex sets and functions) are
not two independent theories that happen to share techniques — they are conjugate images of each
other, so every theorem proved on one side has a dual counterpart automatically available on the
other via Theorem 8.4. This is made concrete immediately: Theorem 8.5's cone polarity and the
diagram the book draws connecting , , and submodular
set functions (already correspondences this series proved independently, in
missions 24-ch06d-mconvexfunctions and 28-ch07d-lconvexfunctions) are shown to be facets of
one single conjugacy fact rather than three separate coincidences. The separation and Fenchel
duality theorems (8.15, 8.16, 8.21) are the discrete analogues of the two theorems every convex
optimization course opens with, and the book is explicit that they are not corollaries of the
classical versions plus convex extensibility — they carry genuinely combinatorial content,
specializing to Frank's discrete separation theorem and Edmonds's intersection theorem as
examples the book itself gives.
None of these results are open — they are Murota's account of the duality at the heart of
discrete convex analysis, the reason the theory needed two dual notions rather than one. What
this mission contributes is a faithful, machine-checked formal statement of each, completing a
theorem mission 10-conjugacy-i explicitly left for a future session once the necessary
polyhedral apparatus existed, and including one result (Theorem 8.32) the platform's own
automated extractor missed; no comparable formalization exists on the platform (see
Formalization scope).
The naive approach to the goal's harder direction (L⇒M) would try to verify the exchange inequality for directly from the definition of the transform; the book's actual proof instead identifies the exchange inequality with a statement about weighted minimizers of itself via Proposition 8.3 (the minimizer-difference bound), converting a claim about the conjugate function into a claim about 's own combinatorial structure — a genuine change of perspective, not a direct calculation. Proposition 8.3's own proof is the hardest single argument in this block: it derives the minimizer-difference bound by a contradiction argument that constructs an explicit pair of "worse" minimizers via a join/meet perturbation and derives a strict inequality from Theorem 7.29's translation inequality — a multi-step combinatorial argument with no direct shortcut.
Ground-set elements are a Fintype V with DecidableEq; convex functions are WithTop ℝ
valued throughout (never EReal, except for the Legendre-Fenchel transform itself, whose
defining supremum/infimum can genuinely be infinite). All thirteen numbered results found in this
chunk's page range — the twelve in BRIEF.md's own table plus Theorem 8.32 — are placed, with one
documented scope reduction: Theorem 8.21 states only its real-attainment parts (1)-(2), not the
integer-attainment refinement of parts (3)-(4), which needs a separate argument no other result
in this chunk requires — see HARD.md. Concave functions are always represented via
and every inequality restated as , avoiding WithTop ℝ
negation entirely. This chunk's own BRIEF.md inherited the chapters-4-7 page-offset boilerplate
(printed = PDF 19); chapter 8 uses offset 18, confirmed against the PDF's own footers — every
citation here uses the corrected offset. This mission's base vocabulary is redeclared from
missions 10-conjugacy-i, 20-ch04b-mconvexsets, 21-ch05b-lconvexsets,
23-24-ch06*-mconvexfunctions, and 26-27-ch07*-lconvexfunctions rather than imported, since
sibling drafts in this series cannot yet reference one another. Contributions completing any of
the thirteen sorrys are welcome; the goal and Proposition 8.3 carry the most independent proof
content.
An investor with a fixed planning horizon, an initial fortune, and a personal attitude toward risk (a utility function) wants to allocate wealth between a riskless bond and several risky assets, rebalancing at each of periods, to maximize the expected utility of terminal wealth. This is the oldest and most basic problem of mathematical finance's dynamic-programming tradition, going back to Samuelson (1969) and Merton (1969, continuous time). Bäuerle and Rieder's Chapter 4 is where the abstract finite-horizon Markov Decision Process theory built up in Chapter 2 — the Bellman equation, existence of optimal policies under compactness and continuity, propagation of concavity through the value function — is first put to genuine financial work: the multiperiod terminal-wealth problem is shown to be exactly an instance of that general theory, and the reduction pays off immediately in six closed-form solutions for the standard families of utility functions used throughout the literature (power, HARA, logarithmic, exponential).
An investor with utility function (Definition 3.4.1: strictly increasing, strictly concave, continuous) and wealth invests in a bond (interest rate on ) and risky assets with relative risk (Chapter 3). The one-period problem: admissible investments , , . The multiperiod problem is the -stage Markov Decision Model with state space (wealth), action space , transition , zero one-stage reward, terminal reward ; its value functions are over Markov portfolio strategies .
with strictly increasing, strictly concave and continuous, and an optimal portfolio strategy realized by maximizers of the recursion. This is the structural result every closed-form solution below specializes.
Eight milestones: the one-period existence/regularity theorem the induction step reduces to (Theorem 4.1.1); the upper bounding function that makes Chapter 2's existence machinery apply (Proposition 4.2.1); the zero-mean special case (Theorem 4.2.4); and four utility-specific closed forms plus the binomial-model comparative-statics lemma (Theorems 4.2.6, 4.2.11, 4.2.13, 4.2.15; Lemma 4.2.9).
Theorem 4.2.2 is the template for every dynamic portfolio problem in the rest of this book (consumption-investment in Chapter 4 §4.3-4.4, mean-variance and index tracking later in Chapter 4, and the partially-observed and jump-market analogues in Chapters 6 and 9): check a handful of structural conditions on the market data, and the existence, regularity, and recursive computability of the optimal policy follow automatically from Chapter 2's general theory rather than needing a bespoke argument each time. The six closed-form corollaries are the results practitioners actually use: the power/HARA/log/exponential-utility feedback rules are the standard textbook portfolio formulas (the logarithmic case is Kelly betting; the exponential case's wealth-independent optimal amount is the CARA-utility hallmark used throughout insurance and reinsurance mathematics), and Lemma 4.2.9's monotonicity result is the discrete-time analogue of the Merton ratio's dependence on the market's risk premium.
No result of this chunk was found on the platform (searched "terminal wealth", "portfolio optimization", "power utility", "HARA utility"). The proofs are complete in the book and mostly short (each utility-specific theorem reduces to checking the Structure Assumption via a transformation to a fraction-of-wealth variable); this mission's contribution is the precise formal statement of each closed form, with its own explicit recursion for , since the six theorems share a structure but genuinely differ in which one-period sub-problem and which scaling variable (, , or a wealth-independent constant) each uses.
The obvious shortcut for the goal is to prove existence of an optimal policy and its concavity/monotonicity properties by separate, ad hoc arguments at each stage; the actual content of Theorem 4.2.2 is that both reduce, via Theorem 4.1.1, to a single one-period fact applied identically at every stage — the induction step is exactly "if [strictly increasing/concave/continuous with linear growth], then is a utility function on up to the growth bound, so Theorem 4.1.1 applies directly to ." Missing this reduction leads to reproving compactness/upper-semicontinuity arguments from Chapter 2 by hand at every stage instead of invoking Theorem 4.1.1 once per stage. For the six closed-form theorems, the shared trap is conflating the different one-period sub-problems: the power- and HARA-utility theorems solve the same sub-problem (4.7) after a wealth-shift transformation, while the exponential-utility theorem's sub-problem (4.13) has a fundamentally different scaling (the optimal amount, not fraction, is wealth-independent) — collapsing these into one "utility-agnostic" statement would hide exactly the distinction the book is making.
The multiperiod value function V is defined as an explicit supremum over admissible Markov
portfolio strategies (not the Bellman recursion itself, and not full history-dependent
strategies), following the book's own citation of Theorem 2.2.3 to justify restricting to Markov
strategies for this model; this keeps the goal's parts (b)/(c) genuine content rather than
restatements of the value function's own definition. The one-period vocabulary
(OnePeriodD/OnePeriodU/OnePeriodV, NoArbitrageOnePeriod) is a self-contained restatement
matching §4.1's own notation (a single , , no time index), independent of chunk 03's
full market/portfolio apparatus, since Theorem 4.1.1's own content is exactly this one-period
reduction. Proposition 4.2.1's proof cites two facts as already established elsewhere in the
book (a concave function is dominated by an affine function; no-arbitrage bounds admissible
actions linearly in wealth) — both are taken as explicit hypotheses of the Lean statement rather
than re-derived, since re-deriving them is not this proposition's own content. HARA and power
utility share one sub-problem definition (Afrac/vPower, Eq. (4.7)); logarithmic and
exponential utility each need their own (AfracLog/vLog, vExp, Eqs. (4.11), (4.13)) since
their admissibility sets and objective functions genuinely differ (a strict vs. non-strict
inequality; a fraction vs. an absolute amount).
No trivializing formalization: each of the six closed-form theorems states its own explicit recursion for (a finite product or sum over of genuinely different per-stage terms) rather than a shared abstract "some sequence exists with " — the latter would hide exactly which recursion each utility function produces, the actual content the brief for this chunk flags as the point of having six near-identical theorems rather than one parametrized statement. Optimal strategies are stated in their exact feedback form (, or the HARA-specific affine shift, or the wealth-independent exponential-utility amount), not merely asserted to exist.
Many data sets are large matrices of which only a small fraction of the entries is observed, and of which the underlying object is believed to have low rank: user–item rating tables in collaborative filtering, distance matrices in sensor-network localization, and measurement matrices in structure-from-motion. Matrix completion asks when the missing entries can be recovered exactly. Rank minimization subject to the observed entries is intractable in general. Its convex relaxation, nuclear-norm minimization, is a semidefinite program, and the question is how many randomly placed entries it needs.
Timeline:
Fix of rank with singular value decomposition , where and , are orthonormal. Let , , and let be the sign matrix. The tangent space at is the image of the projection
and .
obeys the strong incoherence property with parameter if every entry of and is within of the corresponding entry of , and every entry of is at most in absolute value.
An observation set is either a uniformly random -subset (the uniform model) or contains each entry independently with probability (the Bernoulli model). keeps the entries in and zeroes the rest. The program is
where is the sum of the singular values.
The analysis uses the centered operators and , where and . It also uses the random matrices , where the operator is applied to from the right. denotes the spectral norm.
There is an absolute constant such that, for every fixed as above and uniformly sampled entries,
The constant is not fixed; the goal asserts only its existence.
provided the right-hand side is below . 3. Lemma 8.1. An exact expansion of in powers of with explicit recursive coefficients. 4. Lemma 8.2. The coefficients are at most , with . 5. Lemma 3.3. On the event , the same terms with obey the bound with an extra factor . 6. Theorem 3.6 (Moment bound II). Let and . Then
Theorem 1.2 shows that a polynomial-time convex program recovers an incoherent low-rank matrix from a number of entries that is linear in and within a polylogarithmic factor of what any method requires. It turned nuclear-norm minimization from a heuristic into a method with near-optimal guarantees, and much of the later work on low-rank recovery, robust PCA and phase retrieval uses its framework of dual certificates, tangent spaces and incoherence.
The theorem is proved; formalizing it is the remaining work here. None of these results has a machine-checked proof. The platform already has the Candès–Recht definitions (nuclear norm, SVD data, Bernoulli model, tangent projection), the deterministic Lemma 3.1, and the Bernoulli-to-uniform transfer. This mission adds:
Shorter later proofs (Gross, Recht) use a different incoherence condition. A formal proof of the goal along either route is welcome, provided it proves the statement as given.
The obvious approach bounds each term of the Neumann series for the certificate separately, using noncommutative Khintchine inequalities and decoupling. This is what Candès and Recht did, and it fails beyond small : the entries of these matrices are coupled through the same random indicators, and the bounds degrade with . That is where their comes from.
The moment method avoids this but has its own obstruction. Taking absolute values inside the expansion of loses a factor of , which gives the quadratic dependence of Theorem 1.1. The linear bound needs sign cancellations among the coefficients of to be tracked through a nested induction over "generalized spider" configurations (Section VI). Replacing by (Lemma 3.3) is necessary for those cancellations. Without it the diagonal coefficients are of size instead of .
Matrix (Fin n) (Fin n) ℝ (MatrixCompletion.RealMatrix). The SVD is the platform structure SVD M r. Logarithms are natural. Probabilities are the platform's finite sums: successProb (uniform -subsets), bernoulliEventProb and bernoulliExpectation. The spectral norm is spectralNorm. The definitions of matrix_completion_{basic,svd,bernoulli,tangent} are reused, not restated.successProb is for ; it does not exclude any case the paper covers. The failure probability stays and is not traded for a constant. The constant may not depend on , , or , so it cannot be chosen to make (I.12) unsatisfiable. For fixed , (I.12) is satisfiable with for every large and every .A stochastic processing network (SPN) — buffers holding waiting work, activities that consume items from buffers and produce items into others, driven by stochastic arrivals and service requirements — is stable, in the sense of mission I's Definition 3.6, exactly when its ambient Markov chain is positive recurrent. That definition is correct, but it is a statement about an infinite-state continuous-time Markov chain, and Markov chains of that kind almost never admit a hand-computed stationary distribution or a directly verifiable positive-recurrence criterion for anything beyond the smallest examples. What is needed is a method that turns "is this specific queueing network, under this specific control policy, stable?" into a tractable, purely deterministic question. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) supplies exactly this method in Chapter 6, and the theorem that licenses it — Theorem 6.2 — is introduced by the authors themselves as "the fulcrum that supports all other results developed in this book." Every stability theorem in the remaining eight chapters of the book (feedforward and generalized Jackson networks, the Rybko–Stolyar boundary, back-pressure control, proportionally fair allocation, task allocation, packet networks) is an application of this one theorem to a model-specific fluid model.
The method traces to Rybko and Stolyar's 1992 study of a single two-station network and to J. G. Dai's 1995 unification of fluid-limit stability arguments across general queueing networks (Annals of Applied Probability 5, 49–77), with independent contemporaneous work by A. Stolyar for discrete state spaces and a parallel probabilistic route through reflecting Brownian motion due to Dupuis and Williams (1994). This mission formalizes the version of the argument specific to Dai and Harrison's general SPN framework.
Under a fixed control policy, an SPN with buffers and activities generates four
continuous-time processes: the cumulative departure process , the
cumulative service-completion process , the cumulative service-effort
process , and the buffer-contents process . The
model's first-order data — the material-requirement matrix , the
expected-output matrix , the vector of mean service times, the
capacity-consumption matrix , the -vector of server-pool capacities, and the vector
of external arrival rates — determine six basic relationships that Chapter 2 derives
directly from the SPN's construction, and that this mission packages as IsFluidModelSolution.
To study scaling limits, Section 6.3 constructs, on one common probability space, a whole family of versions of the SPN's processes, one for each initial state of the ambient chain: the superscripted . Writing for the total initial buffer content, the fluid-scaled processes are
A fluid limit path (Definition 6.6) is any limit of such a family, along a sequence of initial states with , uniform on compact time intervals (u.o.c.). A fluid model solution is any four-tuple satisfying the six equations above, whether or not it arises as an actual limit — a purely deterministic notion.
where "fluid limit... is stable" (Definition 6.1) means: there is such that every fluid limit path has for all . This is the weakest possible target: it asserts only that fluid limit paths are eventually driven to zero, with no rate or further structure attached, and it is exactly the hypothesis every later chapter's Lyapunov argument is built to establish.
Theorem 6.5 (existence of fluid limits): along any sequence of initial states with , the fluid-scaled processes have a u.o.c.-convergent subsequence, and every such limit is automatically a fluid model solution — the bridge from the purely equational Definition 6.3 (used by every later chapter) to the genuinely stochastic Definition 6.1 (needed by this theorem). Its proof rests on two convergence lemmas (6.7: compactness of the scaled service-effort process via an equicontinuity argument; 6.8: the scaled completion process converges exactly when the scaled effort process does) and, behind Lemma 6.8, a uniform strong law of large numbers for a "delayed" random walk (Lemma 6.9). A separate uniform-integrability result (Lemma 6.10) supplies the remaining ingredient the goal theorem's proof needs to convert an almost-sure fluid-scale limit into the expectation bound mission I's Lemma 3.7 requires.
The result itself. Theorem 6.2 converts a probabilistic stability question about an infinite-state Markov chain into a real-analysis question about a deterministic dynamical system: does every solution of a fixed, checkable system of equations reach zero in finite time, uniformly in its starting size? Every one of the book's remaining eight chapters answers a version of this question for a specific policy and concludes SPN stability via this theorem alone — none of them re-derives positive recurrence directly.
Formalizing it. No prior formalization of fluid limits, fluid models, or scaling-limit
stability of any stochastic system exists on Prove2Me (q=fluid limit, q=fluid model, q=u.o.c. convergence, q=queueing network stability all return zero hits). This mission is a from-scratch
formalization of the model data, the fluid equations, the per-state process family, and the two
notions of fluid stability, together with the five supporting results and the goal theorem that
connects them — the shared infrastructure the rest of the fourteen-mission series depends on.
The obvious shortcut — state Theorem 6.2 using fluid model stability (Definition 6.3, the purely equational notion) in place of fluid limit stability (Definition 6.1) — would produce a strictly easier, unfaithful theorem: fluid model solutions are not restricted to arise as actual scaling limits, so the genuine content of Theorem 6.2 (that convergence of a stochastic family forces a probabilistic conclusion) would be lost, and the theorem would reduce to a tautology once Theorem 6.5 is assumed. The two notions are visually almost identical in the book's own text ("-attraction to the origin," applied to two different objects) and keeping them distinct is this mission's central discipline. A second difficulty is that Mathlib has no existing theory of stochastic-process scaling limits, u.o.c. convergence, or the specific renewal/SLLN machinery (Lemma 6.9's uniform strong law for a state-dependent "delayed" random walk) the proof needs — every one of these had to be defined from the ground up rather than instantiated from a general framework.
The ambient chain's state space is an arbitrary countable type, following mission 01; the
per-state process family SPNProcessFamily takes as given real-valued
functions satisfying exactly the pathwise properties (Eqs. 2.31–2.32) that Section 6.4's proofs
use, since Chapter 2's construction of these processes from primitive stochastic elements is that
chapter's own "recap" of already-established facts, not a numbered result of Chapter 6.
UOCConverges is stated by its direct --on-every-compact-interval meaning, and
Lemma 6.9's "" is likewise stated by its direct - meaning rather than a
Lean supremum expression, because the state space may be countably infinite and an explicit
supremum over an unbounded-above family of reals would silently collapse to a junk value of zero
in that case — a real risk of trivializing the statement that this formalization avoids outright.
A formalization that reused FluidModelStable as the goal theorem's hypothesis, or that dropped
from Theorem 6.5, would each be a trivializing shortcut of exactly the kind ruled
out above. The five definitions (FluidEquationData, IsFluidModelSolution, SPNProcessFamily,
FluidLimitPath, FluidLimitStable) are the primary reusable contribution — the shared
vocabulary every later mission in the series restates in its own namespace, since drafts do not
import one another. Contributions completing the six by sorry proofs are welcome.
Integer programming asks whether a system of linear inequalities has a solution . In fixed dimension it is solvable in polynomial time: Lenstra (1983) proved this by showing that a convex body without integer points is "flat" in some integral direction, so that the search splits into few lower-dimensional subproblems. Kannan's 1987 paper in Mathematics of Operations Research sharpened this approach. It computes a Korkine–Zolotarev ("reduced") basis of a lattice, solves the shortest and closest vector problems exactly in operations, and runs integer programming in arithmetic operations. Underneath the algorithm sits a purely geometric statement, Theorem (5.5): a lattice-free convex body meets only boundedly many integer translates of some integral subspace.
Timeline.
is Euclidean space with dot product and length , and is the set of integer vectors. For linearly independent , the lattice is the set of integer combinations , , and is a basis. Gram–Schmidt orthogonalisation gives and unit vectors , and , so and . The determinant is . is the length of a shortest nonzero vector of . The projected lattice is the image of under orthogonal projection onto the complement of . A basis is reduced (Definition 2.6) if for every and for .
A convex body is a convex set of positive volume, which for a convex set means nonempty interior. A subspace has a basis of integer vectors if it is the real span of integer vectors. Its integer translates are the sets with .
In Lean, is EuclideanSpace ℝ (Fin k), a basis is b : Fin m → EuclideanSpace ℝ (Fin k), the lattice is lattice b = Submodule.span ℤ (Set.range b), is gsLen b j, is gsCoeff b i j, is latticeDet b, is lambdaOne, is projLattice b j, and a reduced basis is IsReduced b.
For and every bounded convex set with nonempty interior and there is a subspace spanned by integer vectors with and
The printed theorem allows "an dimensional space " with and bound . Taken literally that is trivial (, one translate). The proof on the same page takes , of dimension , and remarks that this "ensures that the subspace is always of dimension at least 1". The goal states that reading.
Theorem (5.5) is a structural form of the flatness theorem. For it says that a lattice-free convex body meets fewer than consecutive integer hyperplanes of some integral direction. For smaller it gives a finer decomposition of into translates, each a lower-dimensional integer program. This is the recursion behind fixed-dimension integer programming, and statements of this form are used in lattice-point enumeration, in the geometry of numbers (covering minima), and in cutting-plane theory (lattice-free bodies define split and intersection cuts). Propositions 4.2 and 4.3 are the correctness core of exact closest-vector enumeration.
The results are proved in the literature, though Theorem (5.5) is proved "albeit sketchily" in the paper itself. As far as is known, none of them is formalized: Mathlib has Minkowski's convex body theorem and the ZLattice API, but not Gram–Schmidt lattice invariants, Korkine–Zolotarev bases, Hermite-type bounds, nearest-plane rounding, or any flatness theorem. This mission produces the first machine-checked versions. It also corrects three statements that are wrong as printed (below), so the formal statements are the ones that can be relied on.
The naive route to (5.5) is to take a flat direction directly: bound the lattice width of and count hyperplanes. That needs a flatness theorem with an explicit bound below , which is itself the hard part. The paper's argument instead needs John's theorem (every convex body lies between an ellipsoid and its -fold dilation), a reduced basis of the transformed lattice, and a counting argument across projected lattices that combines Minkowski's bound on each with the covering estimate of Proposition 4.2. None of John's theorem, reduced bases or the projected-lattice counting is in Mathlib.
Proposition 4.3 is also delicate as printed: the per-coordinate count on p. 24 undercounts the integers in a closed interval, so the printed arithmetic cannot be transcribed as it stands. Proposition 2.16 in the paper is the correctness of the algorithm SHORTEST. Here only the existence of a reduced basis is needed, which requires attainment of on every projected lattice and a lifting argument (Proposition 1.9).
Conventions: indices are 0-based (Fin m), so the paper's is projLattice b (j-1) and its bound is m ^ (m - i). Gram–Schmidt is Mathlib's unnormalised gramSchmidt. Lattices are Submodule ℤs of a real Euclidean space generated by a linearly independent family, and is allowed, because (1.12) and 4.2 are applied to projected lattices. The goal counts translates as sets with Set.encard, so the bound includes finiteness. is assumed convex, bounded and with nonempty interior, but not closed.
Three printed statements are corrected, and the corrections are recorded in each item's Formalization Note.
Trivializing formalizations are ruled out: the goal forbids , which gives one translate, and , where no translate meets . It requires nonempty interior (the empty set would satisfy everything) and counts with encard (an infinite count cannot become ).
Out of scope: the paper's algorithms (SHORTEST, SELECT-BASIS, ENUMERATE, CLP, CLP′, ILP) and their operation and bit counts (Theorems 2.17, 3.9, 4.5, 5.4), because Mathlib has no cost model. Also out of scope is §6 (NP-completeness of the closest vector problem and Cook reductions), because Mathlib has no complexity classes. The definitions of this mission (lattice, gsLen, gsCoeff, latticeDet, lambdaOne, projLattice, IsReduced) are reusable for any later work on lattice reduction. Contributions are welcome at every level: John's theorem, Hermite-type bounds, Korkine–Zolotarev existence, and the counting lemmas.
Max -cover is the basic coverage problem of combinatorial optimization. The input is a collection of subsets of a finite ground set and a number ; the task is to choose subsets that together cover as many points as possible. It models facility and sensor placement, the selection of a small committee or feature set representing a population, and budgeted versions of set cover. It is also the prototype of maximizing a monotone submodular function under a cardinality constraint.
The greedy algorithm covers at least a fraction of the optimum. This bound goes back to Hochbaum and Pathria and, for general submodular functions, to Nemhauser, Wolsey and Fisher (1978). For two decades it was not known whether a polynomial-time algorithm could do better. Uriel Feige answered the question in A Threshold of ln n for Approximating Set Cover (J. ACM 45(4), 1998, pp. 634–652, doi:10.1145/285055.285059), Section 5. His Theorem 5.3 (p. 648) states: "For any , max -cover cannot be approximated in polynomial time within a ratio of , unless ." Together with the greedy bound, it makes the exact approximation threshold of max -cover.
Timeline:
An instance consists of points , a list of subsets of the points, and a number . Its value is the largest number of points covered by at most of the sets. Instances are written over a three-letter alphabet:
Following p. 648, a polynomial-time algorithm approximates max -cover within a ratio if on every input it outputs a number with
The algorithm need not name the sets. This is the non-constructive notion of approximation.
The proof is a reduction from the MAX 3SAT-5 problem. A 3CNF-5 formula has exactly three literals per clause, over three distinct variables, and every variable occurs in exactly five clauses. The reduction goes through a -prover proof system for such a formula with clauses:
The max -cover instance of §5 attaches to every random string a copy of the explicit partition system. Its points are the vectors in with , so . Its partitions are labelled by the -bit strings, and each splits the points by the value of one coordinate. There are points in all. For each prover , question and answer , the set collects, for every on which receives , the th part of the partition of labelled by the values that gives to the distinguished variables of . The budget is , where is the number of questions a single prover can receive.
conditional on the two cited results below. The ratio is left free (any ), so the goal records the shape of the threshold and not a particular constant.
The result closes the approximability of max -cover: the greedy algorithm cannot be beaten by any constant unless P = NP. Consequences:
Status: the theorem has been proved since 1998. It has not been formalized; neither the reduction nor the underlying proof systems exist in Mathlib or on this platform. This mission produces:
The cited PCP-based gap (Theorem 2.1.1) and parallel repetition (Theorem 2.2.2) remain hypotheses. They are separate, much larger formalization projects.
The obvious argument uses the soundness of the proof system directly: a large cover should force consistent answers. It fails because a cover may spend many sets on a few random strings and cover them completely, while covering the rest partially without any two sets from the same partition. What saves the argument is exact counting. For sets from pairwise different partitions, coverage is exactly , a concave function of the number of sets used. Since the sets meet a random string times on average, Jensen's inequality caps the total coverage of such "unstructured" strings at about , which tends to . A further obstacle is that the reduction must run in polynomial time. The paper therefore takes and constant (unlike the set-cover reduction, where ), and the soundness bound must beat at a constant . The quantifier order ( large first, then large) is part of the difficulty.
A second obstacle is the machine model. The goal is a statement about polynomial-time Turing machines, so the reduction and the decision procedure built from a hypothetical approximation algorithm must be compiled into Cook's one-tape machines.
CookPvsNP_defs (a published platform definition): one-tape Turing machines, , , polynomial-time computable functions, CNF formulas and their encoding. "P = NP" is P Bool = NP Bool, the form in which CookPvsNP.P_ne_NP states the open problem.Thm211. Raz's theorem enters as RazRepetition, its consequence stated on p. 642: the -fold clause–variable game on a far-from-satisfiable 3CNF-5 formula has acceptance probability at most . This is weaker than Raz's general theorem, so the conditional statement is stronger. No hypothesis about max -cover is assumed.A trivializing formalization is ruled out: every cited input is a named, satisfiable proposition about 3CNF formulas or the two-prover game, never about max -cover, and the approximation hypothesis is satisfiable for ratios up to .
Needed infrastructure, reusable beyond this mission:
Contributions to any of these, or to either cited theorem, are welcome.
Set cover is the problem of covering a finite ground set with as few members of a given family of subsets as possible. It models facility location, crew scheduling, test-suite minimization and many other selection problems in operations research, and it is one of the canonical NP-hard problems. The greedy algorithm, which repeatedly picks the subset covering the most uncovered points, finds a cover at most about times larger than the optimum on an instance with points (Johnson 1974; Lovász 1975; Chvátal 1979). Whether any efficient algorithm does substantially better was open for two decades.
Timeline of the lower bounds:
This mission formalizes Feige's theorem, the result that fixed as the threshold.
An instance consists of points and a list of subsets . A cover is a set of indices whose subsets together contain every point. The instance is coverable if every point lies in some . It is written as a string: in unary, then each subset as its characteristic vector.
A deterministic polynomial-time algorithm approximates set cover within if, for some threshold and every coverable instance with points, the value it outputs satisfies , where is the size of a smallest cover.
is the class of languages that a deterministic one-tape Turing machine decides within steps, for some constant . Machines, and are those of the published definition CookPvsNP_defs.
The proof passes through three objects, each defined in the mission:
The statement fixes no constant beyond . The parameters , and of the reduction are choices made inside the proof. The goal carries three cited results as hypotheses: Theorem 2.1.1 (MAX 3SAT-B gap), the consequence of Raz's parallel repetition theorem for the clause–variable game, and the Naor–Schulman–Srinivasan construction of partition systems.
The result. Combined with the greedy algorithm, Theorem 4.4 shows that is the approximation threshold of set cover under a mild complexity assumption. Set cover reduces approximation-preservingly to many covering problems, so the threshold transfers to them. Examples are dominating set, several facility-location and group Steiner problems, and hitting-set formulations used in scheduling and testing. The -prover system with two acceptance predicates and the partition-system gadget became standard tools for later hardness-of-approximation proofs.
Formalizing it. The theorem is proved and has been strengthened (Dinur–Steurer 2014), but no machine-checked proof of any inapproximability of set cover is known. This mission contributes:
Thm211, RazRepetition, NaorPartitionSystems) and a hypothesis of the goal.
RazRepetition is only the consequence of Raz's theorem that the paper uses (p. 642): a error bound for the repeated clause–variable game on 3CNF-5 formulas far from satisfiable.NaorPartitionSystems relaxes "time linear in " to polynomial time and renders " polynomial in " as . Both relaxations weaken the hypothesis.