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.
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 backward stochastic differential equation (BSDE) prescribes the value of a process at a terminal time and asks for an adapted process that reaches it while following a given drift. In mathematical finance the price of a contingent claim, and its hedging strategy, solve such an equation; when the market has frictions (different borrowing and lending rates, for example) the drift, called the driver, is nonlinear and no closed form exists. Numerical methods for BSDEs are therefore methods for pricing and hedging under nonlinear models, and also for semilinear parabolic PDEs, which BSDEs represent probabilistically.
Gobet, Lemor and Warin (Ann. Appl. Probab. 15 (2005), arXiv:math/0508491) proposed and analysed a simulation scheme in which every conditional expectation of a backward time-stepping recursion is replaced by a least-squares regression on finitely many functions, as in the Longstaff–Schwartz method for American options. Their analysis splits the total error into three parts: time discretization (Theorem 1, from Zhang's results), replacing conditional expectations by projections on function bases (Theorem 2), and replacing those projections by empirical regressions on simulated paths (Theorem 3). This mission formalizes the second part.
Timeline. Zhang (Ann. Appl. Probab. 14 (2004)) and Bouchard and Touzi (Stoch. Proc. Appl. 111 (2004)) established the rate of the time discretization. Bouchard and Touzi's regression error (their reference [6] in the paper, Theorem 4.1 there) was expressed through the residuals of the scheme's own iterates. Gobet, Lemor and Warin (2005) gave the bound in terms of the residuals of the discrete BSDE, together with estimates on .
Fix a horizon , dimensions , a drift and a diffusion matrix , both Lipschitz in ((H1)), and a driver with
For put and . On a probability space with a filtration , the increments are -measurable, independent of and Gaussian ; is the -th component. The Euler scheme is , . An -adapted process extends by extra state variables, and the terminal value is , square integrable.
Write . The discrete BSDE is and, for ,
A function basis () is square integrable with invertible Gram matrix . is the orthogonal projection of onto the span of the basis, and .
The projection–Picard scheme with iterations (Definition 1) produces and , starting from , where minimizes
Finally .
For small enough,
Theorem 2 shows that the projection errors of a backward regression scheme only add up over the time steps, with a constant that does not grow with , and that they are measured by the residuals of the discrete BSDE itself. That makes the influence of the basis directly computable (the paper's §6 does so for Voronoi-cell indicators), and shows that Picard iterations already give an error of the order of the time discretization. Combined with Theorem 3 it gives the complete error budget of the algorithm.
The result is proved in the paper; to our knowledge none of it is machine-checked. A complete development provides a formal -regression calculus for discrete BSDEs (projections on random bases, conditional expectations against Gaussian increments, contraction of Picard maps in ) and a backward discrete Gronwall lemma, all reusable for other regression schemes. One printed step, (14), fails at (see below), so a formal proof also certifies that the theorem survives the repair.
The obvious argument compares the scheme with the discrete BSDE one step at a time and applies Gronwall. It fails for : carries a factor , and a naive bound summed over steps explodes. A usable bound has to account for the conditional variance of given , not only its second moment. The second difficulty is that the projection does not commute with the driver: projection errors enter at every step through the nonlinear , and must be bounded by residuals of and , not of the scheme's iterates. A third is the Picard step: at the iterate is computed with , so it is not an iterate of the contraction of milestone 3, and the printed inequality (14) fails there; an extra term in is needed.
The Lean development lives in the namespace RegMCBSDE.Projection. Points are in EuclideanSpace ℝ (Fin d), the matrix norm in (H1) is the Frobenius norm, and all expectations of squares are lower Lebesgue integrals in , so no junk value of a Bochner integral can make an inequality vacuous. Component (from ) of is the paper's , and the bases are indexed by Fin (q+1) with for .
Committed readings:
Contributions welcome: proofs of the milestones, and the Mathlib-level lemmas they need (conditional expectation of a product with an independent centered Gaussian, moments of the Euler scheme, the projection identity for -measurable bases).
Backward stochastic differential equations (BSDEs) describe the price and the hedge of a contingent claim in models with nonlinear pricing rules (differential interest rates, funding costs, reflected or constrained claims), and give probabilistic representations of semilinear parabolic PDEs (El Karoui, Peng and Quenez, 1997). Their numerical solution in moderate dimension is done by simulation: a backward recursion over a time grid in which each conditional expectation is replaced by a least-squares regression on simulated paths, the same device as the regression method for Bermudan options of Longstaff and Schwartz (2001).
Gobet, Lemor and Warin (2005) split the error of such a scheme into three parts: time discretization (Theorem 1), projection on finite function bases (Theorem 2), and the replacement of projections by empirical regressions on simulated paths (Theorem 3). This mission formalizes the third part, which the authors describe as the major contribution of the paper. Its point is that the error from the simulations is controlled nonasymptotically, step by step, without blowing up as the time step shrinks, even though every regression of the backward recursion reuses the same simulated paths.
A model consists of a horizon , a drift , a diffusion satisfying the Lipschitz condition (H1), and a driver satisfying (H2): . For , , , the Euler scheme is , where the increments are independent of the past. A chain extends , and is the terminal value.
At each time , function bases (for ) and , (for the components of ) are fixed, orthonormal in the sense . The projection–Picard scheme (Definition 1) computes coefficients by Picard iterations of an least-squares problem, and sets , .
The empirical scheme (4) replaces the expectation by an average over independent simulations of the path: minimizes
The outputs are truncated: with and a smooth profile equal to the identity on , with . The regression vector is , and the good event (27) asks that the empirical matrices and be close to the identity for all .
For , orthonormal bases with , such that the bounds of Proposition 2 hold, and small enough, for ,
where collects second moments of , and , written out in full in the goal statement. The constant and the threshold on depend only on the model and on .
Theorem 3 is nonasymptotic: together with Theorems 1 and 2 it lets one compare the three error sources and choose , the bases and jointly for a target accuracy. The rate shows how many paths a finer time grid requires, and the term shows that Picard iterations suffice. The term involving isolates the event on which the empirical regression matrices are badly conditioned, which the truncation keeps under control.
The result is proved in the paper; nothing in this mission is open mathematically. No machine-checked proof of any part of it is known. A formal proof would check a long chain of estimates whose constants the paper tracks only as a generic , and would settle the two misprints in the printed statement (see below). The definitions layer (Euler scheme, regression schemes, empirical regression matrices) is reusable for other regression Monte Carlo schemes for BSDEs and for optimal stopping.
The obvious approach is to treat each regression as an independent statistical estimation problem and apply a variance bound per time step. This fails because all regressions of the backward recursion use the same paths: the response at time is itself a function of the simulations, so the regression at is not a regression of a fixed variable on independent samples. Moreover, the empirical matrix may be singular, and on that event the empirical coefficients are unbounded unless truncated. A naive per-step bound also produces a factor at each of the steps, which explodes; the proof must keep the accumulated constants of order one.
RegMCBSDE.Simulation. Continuous time is not used: the increments are any family that is -measurable, independent of and -distributed for some filtration. That covers the Brownian case. (H3), a condition on the terminal functional of the continuous path, is dropped. So is the Markov representation of , which no statement uses.Contributions welcome: proofs of the milestones, in particular (28)–(29) (finite-dimensional linear algebra) and (34) (independence and orthonormality), and a construction showing that measurable minimizers of (4) exist.
Robust dynamic programming replaces the single transition law of a Markov decision process by a set of laws, and values a policy by its worst-case expected reward over that set. Iyengar (Robust dynamic programming, CORC Tech Report TR-2002-07, 2004; Math. Oper. Res. 30(2), 2005) and Nilim and El Ghaoui (Robust control of Markov decision processes with uncertain transition matrices, Oper. Res. 53(5), 2005) showed that under a rectangularity assumption the robust value satisfies a robust Bellman equation. Each step of that equation solves, for every state–action pair, an inner problem
the worst-case expectation of a value vector over the ambiguity set . Robust value iteration is only as practical as this inner problem is cheap.
The ambiguity sets of interest come from statistics: when transition probabilities are estimated from data, natural sets are confidence regions around the empirical distribution. Section 4 of Iyengar's report studies three such families: relative-entropy balls (Lemma 4), a χ² approximation of them (Lemma 5), and an outer approximation (Lemma 6). This mission formalizes the χ² case. The relative-entropy case is already posed on the platform as RobustMDP.EntropyInner.kl_ball_inner_problem_dual (Nilim–El Ghaoui series), up to the sign change .
Let be a finite set of states and let be the probability measures on . For and write
Fix a centre with for every (in the paper is the empirical next-state distribution of one state–action pair) and a radius . The χ² set (46) is
Since , the relative entropy is at most the χ² distance, so lies inside the relative-entropy ball of radius : it is a conservative approximation of it. The Lean development names these objects expect, variance, chiSqDist, chiSqSet, relEntropy and the dual objective dualObj q t v μ , all in the namespace RobustDP.ChiSquare.
For every value vector ,
where ranges over vectors with componentwise. Both extrema are attained. The lemma's complexity claim, for (48), is a statement about an algorithm and is not part of the mission.
Two further results stand on the same definitions: the inequality of Section 4.2, and the analogue of Lemma 5 established in the proof of Lemma 6 (p. 20):
The result. Lemma 5 reduces a worst-case expectation over a curved convex set of probability vectors to a concave problem in one scalar, which the paper solves by sorting. This makes robust value iteration with χ² ambiguity sets about as expensive as nominal value iteration, up to a logarithmic factor. The identity also explains the shape of the answer: a mean minus a standard-deviation penalty, applied to a value vector truncated from above at the level . The truncation comes from the constraint .
Formalizing it. The result is proved in the paper; no machine-checked proof is known. A complete formalization gives a verified finite-dimensional duality theorem for a quadratic constraint combined with polyhedral constraints, which is the computational core of χ²-ambiguity robust MDPs and of χ²-divergence distributionally robust optimization in general. Lemma 6's printed formula (57) is false (see below); the mission poses the corrected identity that the paper's proof establishes.
The obvious argument drops the constraint . Without it, the minimum of the linear function over the ellipsoid follows from Cauchy–Schwarz and equals . The page notes (p. 19) that earlier work solved only this relaxed problem. With the minimizer of the relaxation can leave the simplex, so the problem has an ellipsoidal constraint, a polyhedral constraint and an equality at once. The multiplier of is what Lemma 5 has to handle. Equality of the primal minimum with the dual supremum needs a duality theorem that is not in Mathlib in this form. Attainment of the dual maximum over the unbounded cone needs an additional argument, namely that an optimal multiplier has the truncation form (53).
Fintype; vectors are functions S → ℝ; is Mathlib's stdSimplex ℝ S. Nonemptiness of follows from . Finiteness is the standing restriction of Section 4 (p. 15).IsLeast and IsGreatest of image sets, so the goal asserts attainment on both sides, as the page's "minimize" and "max" do.0 ≤ μ). The multiplier of the equality ranges over . The page's "" in (50) is a misprint: the proof of Lemma 6 writes , and the optimal may be negative.⨆ over an unbounded set, would make the statement junk.Sample covariance matrices are the basic object of multivariate statistics: principal component analysis, signal detection and factor models all start from the eigenvalues of computed from samples of an -dimensional vector. When is comparable to , the eigenvalues of no longer approximate those of the population covariance . The question is then whether a few large population eigenvalues ("spikes") are visible in the sample spectrum at all, and how the top sample eigenvalue fluctuates when they are.
Baik, Ben Arous and Péché (Ann. Probab. 33 (2005) 1643–1697) answered this for complex Gaussian samples. They found a sharp threshold , where , now called the BBP phase transition. This mission formalizes the supercritical half of the answer, Theorem 1.1(b).
Timeline.
Let , , , be independent standard complex Gaussians: with independent real normal variables of mean and variance . Fix a unitary matrix and positive population eigenvalues . The samples are
which are independent mean-zero complex Gaussian vectors with covariance . The sample covariance matrix is , and is its largest eigenvalue.
The regime has with and in a compact subset of . A fixed number of the differ from . For some the top coincide, , with common value in a compact subset of . The others, , lie in a compact subset of .
The limit law is the finite GUE distribution. Let . Then
which is the law of the largest eigenvalue of a Gaussian unitary ensemble matrix (Definition 1.2).
The milestones follow the proof in §4, in attack order:
Here are the orthonormal polynomials for the weight and their leading coefficients.
The result. Below the threshold the top eigenvalue sticks to the bulk edge . Above it, Theorem 1.1(b) and Corollary 1.1(b) show that separates from the bulk to the explicit location . Its fluctuations shrink from order to order , and their law is the top eigenvalue of a GUE, with the multiplicity of the spike. This gives:
Formalizing it. The result is proved in the paper and is not open. Nothing in this mission has a machine-checked proof yet. A complete development would include:
The two contour lemmas (4.1, 4.2) and the Hermite identities are elementary and are footholds. Proposition 4.1 and Lemma 1.1 are substantial. The paper does not prove Lemma 1.1 but cites it as a standard result of random matrix theory (its references [28, 41]).
The obvious route is to diagonalise the sample matrix, write down the eigenvalue density and take a limit. That density involves the Harish-Chandra–Itzykson–Zuber integral. Its large- limit is not accessible directly, because the spike enters through a determinant with nearly coincident columns.
The paper instead starts from an exact Fredholm-determinant formula (Proposition 2.1, posed in mission 1 of this series). In it the kernel factors into two contour integrals and with phase . Above the threshold the two factors are governed by different points. has a nondegenerate saddle at . For the natural saddle lies beyond the pole at , so the contour must be deformed through a pole of order , and the leading term is a residue rather than a saddle contribution. The estimates must hold uniformly in and in the remaining spikes, and the convergence must be strong enough (Hilbert–Schmidt) to pass to Fredholm determinants.
Model. Complex Gaussian samples with mean zero and no centring. , with the factor . for every unitary . This is the model of the paper's (59), (61) and Proposition 2.1; the introduction's mentions of , of centring and of the real density (1) are inconsistent with those formulas. is the supremum of the eigenvalues of the Hermitian matrix , and probabilities are measures of sets of sample arrays.
Regime. The regime is in sequence form:
The fixed margins encode the compact subsets whose open ends move with . Convergence is pointwise in .
Analytic conventions.
Ruled-out trivialisations. Five shortcuts would make the statements trivial, and none is available:
Infrastructure. The needed infrastructure is the complex Wishart model, eigenvalues of random Hermitian matrices, Fredholm determinants of integral operators, and contour integrals with uniform estimates. The Hermite and Fredholm layers can be reused for any orthogonal-polynomial ensemble. Contributions welcome:
The secretary problem asks how well an online decision maker can do when items arrive one at a time in random order and each must be accepted or rejected on the spot. With a single selection, the classical rule (observe a fraction, then take the first item better than everything seen) selects the best item with probability about , and no rule does better. Many allocation problems are not single-choice: a seller with identical goods facing bidders who arrive over time, an advertiser with a budget of impressions, an employer with openings. Each asks the multiple-choice secretary problem: how much of the best achievable total can an online rule collect when selections are allowed?
Kleinberg's 2005 SODA paper answered this for the sum objective. It gave a recursive algorithm whose expected total is at least times the sum of the largest values, so the ratio tends to as grows, and stated a matching upper bound for every algorithm, whose proof the extended abstract omits. The motivating application was online auctions: the algorithm becomes a strategyproof mechanism for selling identical items to bidders who arrive and depart over time, extending the single-item online auction of Hajiaghayi, Kleinberg and Parkes (EC 2004).
Timeline. Dynkin (1963) and the classical literature settle with ratio . Hajiaghayi, Kleinberg and Parkes (2004) turn the single-item rule into an online auction. Kleinberg (2005) proves for selections, with the explicit constant . Babaioff, Immorlica, Kempe and Kleinberg (2008) survey the resulting family of generalized secretary problems and their use in online auctions.
Let be a finite set of distinct non-negative real numbers. The elements of are revealed in a uniformly random order: each of the orders has probability . After each arrival the algorithm decides, irrevocably and using only the values seen so far, whether to select it. At most elements may be selected. Write for the set of the largest elements of (all of if ) and
for their sum, the best total any rule could collect knowing in advance.
Kleinberg's algorithm is defined by recursion on :
The expected value of the algorithm is taken over the random order and over every binomial draw at every level of the recursion.
The statement is uniform in and ; it says nothing beyond the explicit constant printed in the paper.
The paper proves the theorem by induction on . Its sketch introduces , the set of the first arrivals, , the modified value of a set (the sum of its elements lying in ), and , the number of elements of exceeding . The milestones are its stated claims, in order:
The result. Theorem 2.1 shows that random arrival order costs only a factor when many items are sold, against the constant for a single item. With the paper's matching upper bound, it pins down the optimal rate for the -choice problem. It is the base of the paper's strategyproof online auction for identical goods and a standard reference point for the later literature on secretary problems with combinatorial constraints and on online allocation in the random-order model.
Formalizing it. The paper is a two-page extended abstract, and the theorem's proof is a sketch: several steps are described as "easy", a stochastic-domination argument is stated without detail, and the behaviour of the algorithm when fewer than elements have been observed is not specified. A machine-checked proof would supply the complete argument for the explicit constant. The result is proved on paper only in this sketch; no machine-checked proof of it is known.
The obvious argument fixes and treats the threshold as if it split the remaining elements exactly. Both steps fail. With a fixed , the first arrivals are not a uniform subset of and is hypergeometric, so the clean binomial computations of the sketch are not available; the binomial choice of is what makes uniform. And the number of later elements beyond fluctuates by order : the second phase may run out of budget before reaching all of , or accept elements outside . Controlling this fluctuation, while the cap of also counts the first phase's selections, is the central step. The induction must then combine a recursive guarantee on a random, random-sized prefix with this estimate.
The Lean development fixes these conventions.
Finset ℝ with all elements non-negative; distinctness is automatic. The arrival at time (0-based) under the order is the -th smallest element of , and expectations over the order use the published uniform average SecretaryWD.DiscUpper.uniformAvg.PMF over sets of selected positions, defined by well-founded recursion on . The base case is the published SecretaryWD.DiscUpper.classicalSecretary. is Mathlib's PMF.binomial (1/2). At the algorithm selects nothing, for totality only; all statements assume .A complete development needs: the uniform-subset law of a binomially sized random prefix; conditional expectations over random subsets; tail and absolute-deviation bounds for sums of geometric variables and a stochastic-domination argument; and a careful treatment of the recursion through PMF.bind. The first and third are reusable beyond this mission, for other random-order and sample-based algorithms. Proofs of any milestone, of auxiliary lemmas about the random prefix, and of the goal by a route different from the sketch are all welcome.
Random growth models and random matrices share limit laws. The first exact instance was found by Johansson (Shape fluctuations and random matrices, Comm. Math. Phys. 2000), who showed that the last passage time of a lattice model with geometric or exponential weights has the law of the largest eigenvalue of a Laguerre (complex Wishart) random matrix. Baik, Ben Arous and Péché (Ann. Probab. 33 (2005)) extended the identity to weights whose rate depends on the row. On the matrix side this is a sample covariance matrix with a general population covariance ; on the growth side it is a corner growth model, or a series of exponential queues, with inhomogeneous service rates.
The identity is the reason the paper's main result, the phase transition of the largest sample eigenvalue as a few population eigenvalues ("spikes") cross the critical value , is also a theorem about last passage percolation and tandem queues. In the queueing reading, a spike is a slow server, and the phase transition describes how slow a few servers must be before they change the centring and the fluctuation scale of the exit time.
Timeline:
Last passage time. Attach a real weight to every site of the grid . An up/right path from to is a sequence of sites starting at , ending at , each step adding or . The last passage time is
Exponential environment. Given positive numbers , the are independent and is exponential of mean , i.e. density on . All sites of row share one rate.
Sample covariance matrix. Let , , , be independent standard complex Gaussians (real and imaginary parts independent ). For a unitary and (308), the samples are mean-zero complex Gaussian vectors with covariance , and
Schur functions and geometric weights. For a partition , the Schur function is the sum over semistandard Young tableaux of shape of . A geometric variable of parameter has .
For , positive and every unitary ,
The two sides are defined independently: one by a maximum over lattice paths of exponential weights, the other by the spectrum of a Gaussian random matrix.
The proposition makes every distributional statement about in the paper a statement about last passage percolation with row-dependent rates: the (generalised Tracy–Widom) fluctuations at the critical spike value, the Gaussian fluctuations above it, and the fixed-dimension limit. Through (312)–(313) it also covers the exit time of customers from exponential servers in series, an operations research object. The geometric formula (310) is the entry point of the RSK method for exactly solvable growth models.
These results are proved in the literature; the paper cites (310) and (311) and derives (307) from them by a limit. None of them is machine-checked as far as this series knows. Formalizing them requires a Lean development of Schur functions, the Cauchy identity and the RSK correspondence on matrices with nonnegative integer entries, and of the Wishart eigenvalue density, each reusable well beyond this mission.
The recurrence (313) is elementary. Everything else is not. The geometric formula (310) needs the RSK bijection between nonnegative integer matrices and pairs of semistandard tableaux of the same shape, together with Schensted's theorem that the first row of the shape is the last passage time; neither is in Mathlib. The passage from (310) to (307) is a scaling limit , , , in which a sum over partitions must converge to a multiple integral. The matrix side needs the joint eigenvalue density of a complex Wishart matrix with general , which uses the Harish-Chandra–Itzykson–Zuber integral. A direct coupling of the two sides is not known; the identity is an equality of laws, proved by computing both.
The development lives in the namespace SpikedWishart.LastPassage. Conventions:
expMeasure with rate .A formalization in which either side of (309) is defined through the other, or through (307), would be trivial and is excluded: both laws are defined from scratch. Contributions are welcome on RSK and Schur function infrastructure, on the Wishart density, and on the measurability of .
Potential games (Monderer and Shapley, 1996) are the finite games whose unilateral payoff differences are all differences of a single function, the potential. They always have a pure Nash equilibrium, and many natural learning dynamics (best response, fictitious play, logit response) converge in them. Most games met in applications are not exactly potential games, so a recurring question is how much of this theory survives for a game that is close to a potential game.
Candogan, Menache, Ozdaglar and Parrilo (arXiv:1005.2405, journal version Math. Oper. Res. 36(3), 2011) decompose the space of finite games into potential, harmonic and nonstrategic components. Section 6 of the paper equips the space of games with a weighted inner product under which this decomposition is orthogonal, computes the closest potential game to any game in closed form, and shows that approximate equilibria of a game and of its closest potential game correspond, with an explicit loss controlled by the distance between them. This mission formalizes that last result together with the statements it rests on.
A finite game has a finite set of players ; each player has a nonempty finite strategy set with elements, and a utility on the set of strategy profiles . For a profile , denotes with player 's strategy replaced by .
A profile is an -equilibrium if for every player and strategy (equation (2) of the paper). A game is a potential game if there is with for all , , , (Definition 2.1).
A game is identified with its tuple of utilities, an element of where . The game graph has the profiles as nodes, with an edge between two profiles that differ in exactly one player's strategy. The operator sends to its differences along the edges where player deviates, , is the gradient of the game graph, , and is the Moore–Penrose pseudoinverse. Definition 4.2 defines the potential, harmonic and nonstrategic subspaces
and a harmonic game is a game in .
Section 6 introduces the weighted inner product and norm
A closest potential game to is a potential game with for every potential game ; a closest harmonic game is defined in the same way.
Let be the closest potential game to and . Then for every , every -equilibrium of is an -equilibrium of , and every -equilibrium of is an -equilibrium of , where
The result. Theorem 6.3 reduces the study of approximate equilibria of an arbitrary finite game to a potential game, where pure equilibria exist and are maximizers of the potential. Section 7 of the paper reports that, in a companion paper, best-response and fictitious-play dynamics are shown to converge to a neighbourhood of equilibria in near-potential games, with the size of the neighbourhood governed by the distance of the game to its closest potential game. Theorems 6.1 and 6.2 make that distance computable: the closest potential game is an orthogonal projection, given by linear operators of the game graph.
Formalizing it. All four statements are proved in the paper; none of them is machine-checked anywhere known to this mission. A formal development produces a verified operator layer for games on the game graph (gradient, pseudoinverses, the projections ), a verified proof that the weighted inner product, and not the unweighted one, makes the decomposition orthogonal, and a reusable perturbation lemma for -equilibria.
Lemma 2.1 and the final step of Theorem 6.3 are elementary inequalities. The obvious way to approximate a game by a potential game, taking the identical-interest part of its zero-sum/identical-interest split, does not give the closest potential game: the paper's Table 7 (p. 35) shows a potential game whose identical-interest part is far from it. The closest potential game has to come from the projection of Section 6. The weight of the mission is in Theorems 5.1, 6.1 and 6.2. They need the decomposition theorem of Section 4 (every game splits uniquely into , , ) and properties of pseudoinverses of the operators and that Mathlib does not provide: Mathlib has no operator pseudoinverse at all. The orthogonality under the weighted product rests on the specific spectral structure of the Laplacian of the graph of a single player's deviations; it is not a general fact, and it fails for the unweighted product when the differ, so the standard orthogonal-complement machinery cannot be applied to with its default inner product.
Players are a finite type ι with decidable equality; strategy sets are finite types E m. Utilities are plain functions u : ι → (∀ m, E m) → ℝ, the shape used by the published MondererShapley.ClosedPath.IsPotentialGame, which is referenced for Definition 2.1. The operator layer works in PiLp 2 (fun _ => EuclideanSpace ℝ (∀ k, E k)) with the unweighted inner product of Section 4; edge flows carry the inner product of (7). The weighted inner product (55) and norm (56) are plain functions, not a second instance on the same type. "Closest" is the minimizing property itself, not an infimum of distances.
Hypotheses made explicit: every strategy set is nonempty (the paper's ), so ; in Theorem 6.3 the set of players is nonempty, which the maximum over players needs. The paper's "an -equilibrium for some " is stated as "a -equilibrium", which is equivalent because (2) is monotone in . Both directions of Lemma 2.1 and Theorem 6.3 are included.
The goal is stated for the closest potential game, as printed. A version for an arbitrary potential game at distance would be a different theorem, and the hypothesis is not vacuous: Theorem 6.2 shows the closest potential game exists. Theorem 6.2 is stated as an "if and only if" characterization, so it gives existence and uniqueness as well as the formula.
Contributions welcome: the Penrose identities for the pseudoinverse, the identities and , and the decomposition theorem of Section 4, all of which are reusable by the other missions of this series.
Many estimation problems ask for a low-rank matrix from far fewer linear measurements than it has entries: matrix completion, quantum state tomography, recovery of positions from partial distances. The rank minimization problem subject to is NP-hard, so one solves a tractable surrogate instead, either the nuclear-norm minimization subject to or an iterative scheme such as the iteratively reweighted least squares algorithm IRLS-M of Fornasier, Rauhut and Ward (arXiv:1010.2471).
Guarantees for these surrogates rest on conditions on the measurement map. Two are standard. The restricted isometry property (RIP) asks that nearly preserve the Frobenius norm of every low-rank matrix; it holds with high probability for many random maps, and it is what one can verify in practice. The null space property asks that no nonzero matrix in the kernel of be concentrated on few singular directions; it is what the recovery proofs actually use. This mission formalizes the bridge between them in the paper's form: a small restricted isometry constant implies the strong rank null space property (SRNSP) that drives the convergence analysis of IRLS-M.
Timeline.
Fix integers . A measurement map is a linear map ; it is given by matrices through , where . The Frobenius norm is , the nuclear norm is the sum of the singular values of , and is the Euclidean norm of the vector . A matrix is -rank if its rank is at most .
The restricted isometry constant (Definition 1.1) is the smallest such that
The map has the strong rank null space property of order with constant (Definition 6.4) if for every and every decomposition with -rank, there is another decomposition with , , , , and
In Lean these are IRLSM.RIP.ripConst A k, IRLSM.RIP.SRNSP A k η and IRLSM.RIP.measSq A X , built on the published module HighDimStat_MatrixRank_Core (traceInner, frobeniusNorm, nuclearNorm, observationOp).
If and
then satisfies the SRNSP of order with constant
The constant is the paper's explicit one; the goal asserts the full property for every kernel element and every decomposition, including .
The result. Proposition 6.8 is the step that turns a verifiable, probabilistically typical hypothesis (a small rank restricted isometry constant, which Gaussian and many other random maps satisfy once is of order ) into the deterministic null-space hypothesis under which the paper proves that IRLS-M converges to the nuclear-norm minimizer and recovers every -rank matrix exactly (Theorem 6.11, Proposition 2.1). Through Lemma 6.6 and Corollary 6.7 of the same paper, the SRNSP also gives stable recovery by nuclear-norm minimization, with error controlled by the best -rank approximation error in the nuclear norm.
Formalizing it. The result is proved on paper; it has no machine-checked proof that we know of. A complete development supplies the rank restricted isometry constant as a usable object (its monotonicity, its polarization estimate Lemma 6.9), the nuclear norm's additivity on orthogonal pieces, its comparison with the Frobenius norm, and the block-splitting of the singular value decomposition. These tools are reusable across low-rank recovery. The sibling mission of this series, IRLS-M Converges to the Nuclear-Norm Minimizer Under the Strong Rank Null Space Property, takes the SRNSP as its hypothesis; together the two give Proposition 2.1 of the paper.
The obvious argument would bound directly by the restricted isometry inequality, but that inequality controls only Frobenius norms of low-rank matrices, while the kernel element has full rank in general and the property is stated in nuclear norms. The restricted isometry hypothesis therefore cannot be applied to , or to , as a whole, and the constant depends on how the high-rank part is handled. In Lean, the singular value decomposition of a rectangular matrix and the behaviour of singular values under block operations are the main missing infrastructure: Mathlib has the spectral theorem for Hermitian matrices but little on singular values of rectangular matrices.
Matrix (Fin n) (Fin p) ℝ; the paper treats real and complex matrices indifferently. is and is traceInner.observationOp); is a sum of squares, not Mathlib's sup norm on Fin m → ℝ.n ≤ p assumption: the proof does not use it.A formalization that proved only , or only the existence of some decomposition without the bound , or that defined as any admissible constant rather than the smallest one, would not be this mission's goal.
Welcome contributions: singular value decomposition for rectangular real matrices in the Core encoding, singular values of block-diagonal and orthogonally-equivalent matrices, and proofs of the milestones in any order.
Network data often come as a single observed graph, and the simplest summary of a graph is its degree sequence, the list of the numbers of neighbours of its vertices. A statistical model in which the degree sequence is a sufficient statistic is an exponential family on graphs, and the simplest such family is the β-model: each vertex carries a parameter , and edges appear independently with log-odds . The model appears in the directed case in Holland and Leinhardt (1981), in the undirected case in Park and Newman (2004) and Blitzstein and Diaconis (2011), and it is a close relative of the Bradley–Terry model for paired comparisons.
Fitting the model means solving the maximum likelihood equations. The difficulty for classical theory is that the number of parameters, , equals the number of vertices: the parameter dimension grows with the sample, and standard consistency arguments for maximum likelihood do not apply. Chatterjee, Diaconis and Sly (2011) prove that, nevertheless, for parameters in a fixed bounded range the maximum likelihood estimate exists, is unique, and estimates every coordinate of uniformly at rate , with probability . This mission formalizes that result (Theorem 1.3 of the paper) and the lemmas of §4 on which its proof rests.
Let and . The β-model is the law of the random simple graph on vertices in which, for each pair , the edge is present with probability
independently of all other edges. Write for the degrees of . The maximum likelihood equations for an estimate are
The sup norm is .
Two further objects enter the proof. is the set of degree sequences of simple graphs on vertices and the set of expected degree sequences of as ranges over . For and the slack is
which is nonnegative for every degree sequence of a graph (the Erdős–Gallai inequalities). Finally , , is the map whose fixed points are the solutions of (3).
For every there is such that for every and every with ,
The constant depends only on , and the statement holds for all , small being absorbed into .
The theorem is a consistency result in a regime where the number of parameters is as large as the number of nodes, and it comes with a uniform rate: every vertex parameter is recovered to accuracy simultaneously, from one graph. Existence of the MLE is itself not automatic (it fails, for instance, whenever the observed graph has an isolated vertex), so the theorem also says that the estimator is defined with high probability. The paper uses the same machinery for its graph-limit results on uniform random graphs with a given degree sequence (missions 4–5 of this series), and the β-model is the base case of a large family of exponential random graph models used in network analysis.
The result is proved in the paper; this mission produces the machine-checked version. None of the statements here is formalized on the platform or in Mathlib. Theorems 1.4 and 1.5 are the goals of missions 2 and 1 of this series and are restated here; a proof there transfers directly.
Standard maximum likelihood asymptotics fix the parameter dimension and let the sample size grow; here both grow together, and the ratio of squared dimension to number of observations, , stays bounded, so the usual heuristic for when asymptotics apply is borderline at best. The likelihood is concave, but concavity alone gives neither existence of a maximizer (the supremum may be approached at ) nor a bound on its size that is uniform in . The central step, Lemma 4.1, is a deterministic bound on that does not depend on ; it requires control of how the coordinates of can spread out, expressed through a quantitative Erdős–Gallai margin. A coordinatewise argument cannot give it, because each equation of (3) involves all coordinates.
Vertices are Fin n, graphs are SimpleGraph (Fin n) with the discrete σ-algebra, and is the finite sum of point masses with the independent-edge weights ; vectors are Fin n → ℝ with Mathlib's sup norm. Probabilities are values of this measure in , compared with . Expected degrees are integrals against ; is not defined as the range of the right-hand side of (3), since that identification is part of the content of Theorem 1.4.
Every "constant depending only on …" is a quantifier placed before : in Theorem 1.3, depends on only; in Lemma 4.1, is a function of alone, bounded on compact subsets of its domain, as §4 defines the phrase; in Lemma 4.2, on and on . Choosing after and would make Theorem 1.3 trivial, since for large ; this formalization rules that out. The paper's is the hypothesis , and the paper's is the bound for every admissible (a finite nonempty family). The phrase "there exists a unique solution … that satisfies [the bound]" is read as: a solution exists, it is unique, and it satisfies the bound. Lemma 4.1 assumes , not (for existence would be immediate). Theorem 1.5 is stated, as in mission 1, for and .
A complete development needs: the β-model as a measure and its exponential-family formula; Hoeffding's inequality for sums of independent non-identical indicators transported to (Mathlib has Hoeffding for independent bounded variables); compactness in ; and the results of missions 1 and 2. The β-model measure and the Erdős–Gallai slack are reusable beyond this mission. Proofs of any milestone, and of the transfer between the independent-edge and the product-space descriptions of , are welcome.
A random conductance model puts a random conductivity on every edge of the lattice . It is the simplest discrete model of diffusion in a heterogeneous medium, and its generator is the generator of a random walk in a random environment. Classical stochastic homogenization shows that on large scales the random operator behaves like a constant-coefficient elliptic operator whose homogenized coefficient is deterministic. The characterization of , however, involves an equation on the whole lattice for every realization of the coefficients. In practice one computes a spatial average over a box of size of the energy density of an approximate corrector, as in Gloria and Otto (arXiv:1104.1291, §1). The random part of the error of this procedure is a variance. Its size as a function of determines how large a computational box must be.
Timeline:
Fix and . Sites are and is the canonical basis. An edge carries a conductivity ; such a field belongs to the class . The discrete gradients are and , and .
The conductivities are i.i.d.: they are distributed according to the product over all edges of one probability law on . No density is assumed, so atomic laws are allowed. is the expectation and the variance.
For a direction with and a cut-off , the approximate corrector solves
The zero-order term introduces the length scale . The Green's function is the solution of in weak form.
A mask is supported in the box , sums to and satisfies . The averaged energy density is
There are an exponent and a threshold , depending only on , and for each mask constant a constant , such that for every law on , every unit , every , every and every mask :
The statement fixes the shape of the bound, not the value of or , which is why it is the goal.
The milestones follow the paper's proof:
The result. The estimate says that smooth averages of the energy density fluctuate as if the density were independent from site to site, at the rate . That rate is the best possible, since the coefficients themselves are independent. In the error analysis of approximations of , this controls the random error and separates it from the systematic error caused by the cut-off . Proposition 2.1, a byproduct, shows that the approximate corrector has all moments bounded uniformly in when , which yields a stationary corrector (Corollary 2.1 of the paper).
Formalizing it. The theorem has been proved since 2011, and no machine-checked version is known. A formal proof would combine three components that are reusable well beyond this paper:
The obvious argument fails because the energy density is not independent from site to site: the corrector couples all conductivities through the inverse of a random elliptic operator. Bounding the variance needs the sensitivity of to each single conductivity, and that sensitivity is expressed through gradients of the Green's function. Pointwise bounds on that are uniform in the coefficients do not exist: the continuum counterpart fails, by examples from quasi-conformal mappings. Only averaged decay on dyadic annuli and a small gain of integrability are available, which is why the proof needs the moment bounds of Proposition 2.1. In the Green's function does not decay, so only BMO-type control is available, and a logarithm of is lost.
Statements follow the arXiv v1 reprint (arXiv:1104.1291v1) of the Annals of Probability article; theorem and page numbers refer to it.
Fin d → ℤ. An edge is the pair (z, i), and a coefficient field is a real function on edges; the theorems assume it takes values in .Measure.infinitePi of one probability measure on with .Ruling out a trivial formalization. If the constant were allowed to depend on the law or on the mask, the goal would follow from the boundedness of the energy average alone. If the variance were taken of a function that is not square-integrable, it would be by convention. The goal fixes before and and requires square-integrability as part of the conclusion.
Not formalized:
Welcome contributions are proofs of any milestone and reusable infrastructure: infinite-product variance inequalities, discrete integration by parts, and discrete maximum principles.
A standard way to build a random network with a prescribed degree sequence is to choose a graph uniformly at random from the set of all simple graphs with that degree sequence. The model arises in testing whether the exponential family with the degree sequence as sufficient statistic fits network data, in simulating networks with given degrees, and, for constant degrees, as the random regular graph (Blitzstein–Diaconis, Chatterjee–Diaconis–Sly). Quantities such as the expected number of triangles of such a graph are usually estimated by simulation.
For dense graphs, those whose number of edges is of order , the Lovász–Szegedy theory of graph limits (Lovász–Szegedy 2006) describes a large graph by a symmetric function . Chatterjee, Diaconis and Sly identify this limit for uniformly random graphs with a given degree sequence. The answer is the limit of the β-model, a random graph with independent edges whose edge probabilities are . The limit gives exact asymptotic formulas for subgraph counts without simulation.
Graphs and densities. For a finite simple graph on and a simple graph on vertices, the homomorphism density is
where is the set of edge-preserving maps . For ,
with one factor per edge. Graphs on vertices converge to the limit represented by if for every finite simple graph .
Degree sequences and scaling limits. For each let be the degree sequence of some simple graph on vertices. The sequence has scaling limit , a nonincreasing function on , if
is the set of nonincreasing functions on that are left continuous on . It carries the modified norm . is the set of all scaling limits of degree sequences.
The random graphs. is chosen uniformly from the simple graphs on with degree sequence . In a random graph with independent edges each pair is an edge with probability , independently of the other pairs. The β-model is the case .
If lies in the interior of for , there is a function , unique on , such that
and almost surely for every finite simple graph .
The proof also uses three results posed in sibling missions of this series: Proposition 1.2 (mission 4, the interior of ), Lemma 4.1 (mission 3, existence and boundedness of the MLE) and Theorem 1.5 (mission 1, geometric convergence of the iteration ). They are not restated here.
The theorem turns questions about a uniformly random graph with given degrees, a law with no independence, into questions about an explicit graphon. Every subgraph density, the limiting degree distribution, and every graph parameter continuous for the graph-limit topology of the uniform model is computed from . The function solves a continuum version of the β-model maximum-likelihood equations, which connects the combinatorial model with exponential-family statistics.
The result is proved in the paper, which is published in the Annals of Applied Probability (2011). To our knowledge it has no machine-checked proof. Formalizing it requires a Lean development of dense graph limits (homomorphism densities, graphon densities, graph-limit convergence), none of which exists in Mathlib. It also requires a bounded-differences concentration inequality, and a transfer argument from independent-edge models to models conditioned on degrees. Each of these is reusable beyond this mission.
The uniform measure on graphs with a fixed degree sequence has no independence, so concentration inequalities do not apply to it directly. The obvious route is to condition an independent-edge model on its degree sequence. This works only if the probability of the conditioning event is larger than the concentration bound, which is . A crude lower bound of is too small. Lemma 6.2 supplies , and it needs a combinatorial completion step (Claim 6.3).
The second difficulty is analytic. The maximum-likelihood parameters for different live in different dimensions. One must show that their step-function profiles converge in to a limit and that this solves the continuum equation at every point of , not only almost everywhere. Several steps of the paper's argument are only sketched. Among them are the almost-sure convergence of the β-model graphs to and the estimate (pp. 33–34).
Fin n (the paper's vertex is ), graphs are SimpleGraph (Fin n), and a test graph is a SimpleGraph (Fin k), which loses nothing because densities are invariant under relabelling.ℝ → ℝ, and only their values on matter. Uniqueness of is equality on .SimpleGraph (Fin n) is discrete.A formalization that replaces almost-sure convergence by convergence in expectation or in probability, that fixes a single coupling, or that asserts the existence of only almost everywhere states a weaker theorem and does not close this mission.
Welcome contributions include a general graph-limit library (densities, convergence, the counting lemma), McDiarmid's bounded-differences inequality for finitely many independent Bernoulli variables, the Gale–Ryser theorem in the form needed by Claim 6.3, and proofs of the milestones.
A degree sequence records how many neighbours each vertex of a graph has. In network statistics it is often the only summary of a graph that is observed or trusted, and the natural probability models for graphs in which "the degree sequence captures the information" are exponential families whose sufficient statistic is the degree sequence. Chatterjee, Diaconis and Sly (arXiv:1005.1136, Ann. Appl. Probab. 2011) call the resulting model the β-model and study its maximum likelihood theory and its use for sampling random graphs with a prescribed degree sequence.
For any exponential family, the first question about estimation is which values of the sufficient statistic can be matched by a parameter: the maximum likelihood equations say exactly "the expected statistic equals the observed one". Theorem 1.4 of the paper answers this for the β-model. Up to taking a closure, the expected degree sequences of the β-model fill the whole convex hull of the degree sequences. The paper notes that the result can also be derived from classical results on the mean space of exponential families (Barndorff-Nielsen 1978; Brown 1986; Wainwright and Jordan 2008, Theorem 3.3), and gives a self-contained proof in §3. Lemma 4.1 of the same paper uses Theorem 1.4 to show that the maximum likelihood estimator exists.
Fix and the vertex set . A graph is undirected and simple: no loops and no multiple edges. Its degree sequence is , and
is the finite set of all degree sequences. Its convex hull is a polytope in .
For , the β-model is the law of the random graph in which each pair , , is an edge with probability
independently of all other pairs. The expected degree sequences form the set
Two functions on appear in the proof. The first is with
The second is, for each ,
The Lean development names these objects betaModel, D, R, g and fy in the namespace GivenDegreeSeq.MeanPolytope.
The statement fixes no constants. The closure cannot be dropped: for the degree sequence of the empty graph lies in but not in , because every expected degree is positive.
and along some sequence. 7. The gradient (p. 16): .
The theorem describes the mean space of the β-model. Its interior contains every degree sequence that lies strictly inside the polytope, and for these sequences maximum likelihood estimation is well posed. The paper's consistency result (Theorem 1.3) and the existence part of Lemma 4.1 start from this description. The polytope is studied in its own right; its extreme points are the degree sequences of threshold graphs (Mahadev and Peled 1995).
Theorem 1.4 is proved, and as far as this mission's authors know it is not machine-checked anywhere. Formalizing it means turning the paper's short proof into a complete argument. That includes the steps the page dismisses as easy: the exponential-family formula for the independent-edge law, the expectation computation, the Hessian bound for , and the passage from a sequence of approximate critical points to the closure. Lemma 3.1, a descent-type gradient bound for a function bounded above, is a general fact of real analysis and is independent of graphs.
The inclusion is direct: an expectation is an average. The reverse inclusion is the content. For in the interior of the polytope, one would like to find with by maximizing the concave function . For on the boundary of the polytope, however, need not attain its supremum. So the argument cannot rely on the existence of a maximizer, and it has to produce points with without ever solving . Compactness arguments on fail for the same reason: the relevant sequences are unbounded.
Fin n, so the paper's vertex is the index . Graphs are SimpleGraph (Fin n), a finite type. Its σ-algebra is Mathlib's SimpleGraph.instMeasurableSpace, under which every set of graphs on Fin n is measurable.Fin n → ℝ, whose product topology is the Euclidean topology, so the closure is unambiguous. Gradients and Hessians are taken on EuclideanSpace ℝ (Fin n). There "twice differentiable" means that and its Fréchet derivative are differentiable, and the Hessian norm is the norm of the second Fréchet derivative, which equals the operator norm of the Hessian matrix.Contributions of any milestone are welcome. Lemma 3.1 and the gradient identity are self-contained calculus. The probability formula and the expected-degree identity are finite computations on graphs.
The capacitated vehicle routing problem (CVRP) asks for delivery routes from a depot that serve every client exactly once without exceeding a vehicle capacity, at minimum total length. It was introduced by Dantzig and Ramser in 1959 and is the reference problem of the vehicle routing literature: most exact methods for richer routing models (time windows, heterogeneous fleets, split deliveries) are first developed and benchmarked on it.
Exact CVRP algorithms are driven by the lower bound of a linear relaxation. Two families dominated before 2005. Branch-and-cut works with the edge variables and the rounded capacity inequalities (Lysgaard, Letchford and Eglese 2004, among others); its bound degrades as the number of vehicles grows. Lagrangean and column-generation methods work with q-routes, walks from the depot of bounded total demand that may revisit clients (Christofides, Mingozzi and Toth 1981). Fukasawa, Longo, Lysgaard, Poggi de Aragão, Reis, Uchoa and Werneck combine the two in one linear program over the intersection of the two polytopes, priced by column generation with every cut written on the edge variables. According to the abstract, the resulting branch-and-cut-and-price solves to optimality all instances from the literature with up to 135 vertices. The design is called robust because cuts are written on the edge variables and therefore never change the structure of the pricing problem.
This mission formalizes the formulation itself (§2 of the paper) and the two exact facts of its column generation (§3.1).
Let be an undirected graph on . Vertex is the depot; are the clients, client having a positive demand . Each edge has a length . There are vehicles of capacity , both positive integers.
A list of clients describes the closed walk . Its edge incidence is the number of times the walk traverses (a one-client walk traverses twice); its load is , with repetitions.
For , is the set of edges with one end in , , and . The paper's constraints on and on weights of the q-routes are
is ; is the set of satisfying (1) together with some satisfying (5), (6); the Explicit Master is the projection onto of the system (1)–(6) with one . The Dantzig–Wolfe Master (DWM) is the LP in alone obtained by substituting (5) into (1)–(4), giving the rows (8)–(11), with objective (7) . The bounds are .
For a loop-free graph with positive demands and capacity, and arbitrary lengths:
with (7) equal to . The bounds are stated in lower-bound form: every lower bound of over or is one over , and every lower bound over is at most the cost of every solution.
The formulation theorem is what makes the algorithm exact: integer points of are solutions, so branching on terminates at an optimum, and is a relaxation, so is a valid bound that dominates both classical bounds. The DWM description is what makes it computable: is optimized by column generation over q-routes, and milestones 8 and 10 show that any cut on can be added without changing the pricing problem, which remains a shortest q-route problem with edge costs .
The paper proves none of these claims formally; most are stated in a sentence, and milestone 9 is stated with "It can be shown" and no proof. To our knowledge none of them has a machine-checked proof. A formal development produces a library of walks, edge incidences, cut values and column families on a general graph that later missions on branch-cut-and-price (subset-row cuts, ng-routes, other routing variants) can import.
Most items are linear-algebra bookkeeping on finite sums, but they require a working theory of walks: edge incidences along a closed walk, the cut value of an incidence vector, and the fact that a walk from the depot crosses every client set an even number of times. The integrality statements (milestones 5 and 9 and goal part 1) are the hard part: an integer vector satisfying degree constraints need not come from routes through the depot, and the statements must exclude every other structure. For there are no capacity cuts at all, so the capacity of the routes must be recovered from the columns, and the paper states this case without proof. The obvious reduction "an integer point of is an integer combination of q-routes" fails: may be fractional even when is integral.
Vertices are Fin (n+1) with depot 0; edges are Sym2 (Fin (n+1)); the graph is an edge set E assumed loop-free where needed. Edge vectors are functions on all unordered pairs that vanish off E, which encodes . Demands , and are natural numbers; positive demands, and (the paper's standing assumptions, p. 1) are carried by the integrality statements and the goal, while is used by no statement and is omitted. Loads count repeated visits. The cut value , the demand and are the published definitions LysgaardCVRP.Shrink.cut, .demand and .roundedCapacityBound. The matrix is replaced by finitely supported weights on client lists ranging over all q-routes without 2-cycles. and OPT are never real infima, since is empty for infeasible instances.
Three trivializations are ruled out by construction: is defined from the Explicit Master display, not as ; a CVRP solution is defined by its routes, not as an integer point of a polytope; and the columns are not a fixed finite list, which would turn into a restricted master.
The strictness of "CVRP routes q-routes" (p. 2) depends on the instance and is not stated. Contributions of reusable lemmas on walks and cut values of incidence vectors are welcome, as are proofs of any milestone.
Sample covariance matrices are the basic object of multivariate statistics: principal component analysis, factor models and signal detection all start from the eigenvalues of built from observations of variables. When is comparable to , the largest eigenvalue of is no longer a consistent estimate of the largest population eigenvalue, and the question of when a "spike" in the population covariance is visible in becomes a question about the law of at large .
Timeline.
This mission formalizes the critical and subcritical side of that transition, Theorem 1.1(a) of the 2005 paper.
Let with independent real normal variables of mean and variance : a standard complex Gaussian. Let , , , be i.i.d. standard complex Gaussians. Fix an unitary matrix and positive reals , the population eigenvalues, and put . The samples are , mean-zero complex Gaussian vectors with covariance . The sample covariance matrix is and is its largest eigenvalue. Write .
The limit laws are built from the Airy function , integrated along a contour from to , and the Airy kernel
For , (with the pole above the contour) and . The Fredholm determinant of a kernel on is its Fredholm series
and
is the GUE Tracy–Widom distribution and .
Fix integers . Let with , and suppose , and stay in a compact subset of . Then for every real ,
The goal leaves arbitrary and allows to vary inside along the sequence. A companion item states Corollary 1.1(a): in probability.
Theorem 1.1(a) shows that is the exact threshold. Spikes strictly below it do not change the Tracy–Widom limit of . spikes exactly at it produce a new family of limit laws on the same scale. Together with part (b), where separates and fluctuates on the scale , it gives the first complete description of the transition. It is the reference point for spiked-model results on detection limits in PCA, for the real case (Bloemendal–Virág, Mo) and for finite-rank perturbations of Wigner matrices (Péché, Féral–Péché).
The paper's proof is complete and has been in the literature since 2005. No part of it is machine-checked. The mission produces:
The obvious approach is to compute the law of from the eigenvalue density, which is explicit (61). It fails because the density is an -fold integral whose integrand is a signed determinant, so no direct limit exists. The paper converts it into a Fredholm determinant of a double contour integral kernel. Two steps then carry the difficulty.
First, the steepest-descent analysis. With spikes at , the poles of the integrand sit exactly at the double critical point of the phase function. The contour cannot pass through the critical point and must enclose these poles, so it has to be routed at distance of order to the left of . All estimates must be uniform in and in the remaining spikes.
Second, the passage from kernel convergence to convergence of Fredholm determinants. It needs bounds strong enough to control every term of the Fredholm series, which is what the exponential tails in Proposition 3.1 provide. The functions grow polynomially, so even the finiteness of (Lemma 3.3) needs an argument.
Lean encoding:
Trivializing formalizations ruled out:
Infrastructure needed and reusable:
The Fredholm-determinant layer and the Airy function are reusable in any Tracy–Widom result. Andréief's identity and Hankel's formula are reusable well beyond random matrices.
Contributions welcome: proofs of any milestone, and lemmas that bound Fredholm series by Hadamard's inequality.
Potential games (Monderer and Shapley, 1996) are the finite games whose incentives are captured by a single function on strategy profiles: every unilateral change of strategy changes the deviator's payoff by exactly the change of a common potential. They have pure Nash equilibria, and natural learning dynamics such as better-reply and fictitious play converge in them. Most games are not potential games, however, and before Candogan, Menache, Ozdaglar and Parrilo there was no canonical way to say how far a given game is from one, or what the remainder looks like.
Their paper (arXiv:1005.2405; Math. Oper. Res. 36(3), 2011) answers this by viewing a game as a flow on a graph. The payoff differences between profiles that differ in one player's strategy form an edge flow on the game graph, and the classical Helmholtz (Hodge) decomposition of edge flows into gradient, harmonic and curl parts (Jiang, Lim, Yao, Ye, 2011) pulls back to a decomposition of the game itself. Every finite game becomes the sum of a potential game, a harmonic game and a component that carries no strategic information. The decomposition is the basis for the rest of the paper (equilibria of harmonic games, projections onto potential games, approximate equilibria) and for later work on dynamics in near-potential games.
Fix a finite set of players and, for each player , a finite nonempty strategy set with elements. A strategy profile is , and denotes the strategies of the players other than . A game is a family of utilities with , so the space of games is , where with .
Two profiles are -comparable if they are distinct and differ only in player 's strategy. The game graph has the profiles as nodes and an edge between comparable profiles. An edge flow is a function that is antisymmetric on edges and zero off edges; the space of edge flows carries . Triangular flows live on ordered 3-cliques.
The operators are: the gradient , with the edge indicator; the curl on 3-cliques; the per-player gradient , with the indicator of -comparability; and , , the flow of pairwise comparisons of . Adjoints are written and Moore–Penrose pseudoinverses . The space carries the unweighted inner product . Further, , , , and .
A game is normalized if for all and (Definition 4.1). The potential, harmonic and nonstrategic subspaces are (Definition 4.2)
and every game splits as with
where is a potential function of , i.e. .
Lemma 4.6 (the unique normalized game with the same pairwise comparisons is ) is included as a supporting theorem.
The decomposition turns questions about a game into questions about its three components. The potential component inherits the equilibrium and convergence theory of potential games. The harmonic component has a sharply different structure: harmonic games generically have no pure equilibrium, and in each of them the uniformly mixed profile is a mixed equilibrium. The nonstrategic component does not affect any equilibrium notion. The closed-form expressions also give the potential game closest to a given game, and with it bounds relating the approximate equilibria of the two games. The other missions of this series formalize those consequences; all of them rest on the operator layer and the subspaces defined here.
Theorem 4.1 is proved in the paper; to our knowledge it has not been machine-checked. A formal development produces graph-flow infrastructure that Mathlib does not yet have: edge and triangular flows with their inner products, the combinatorial gradient and curl, the Helmholtz decomposition of a finite graph, and an operator Moore–Penrose pseudoinverse on finite-dimensional inner product spaces. The paper leaves Theorem 3.1 to the literature, so a full development needs a proof of it. The pseudoinverse identities of Lemma 4.4 also have a short appendix argument in the paper that a formal proof has to make complete.
The decomposition is not orthogonal decomposition along a single map. The subspaces and are defined through , which is assembled player by player from the , while the flow conditions involve and the combined operator . Connecting the two requires the player operators to have mutually orthogonal ranges ( for ) and the explicit form of as a scaled projection. Without these, (Lemma 4.4 (iv)) and (Lemma 4.4 (v)) are not available, and they are what make the formulas for and land in and . A direct attempt to apply the Helmholtz decomposition to produces a flow decomposition, not a game decomposition; the pullback through is not formal, because is neither injective nor surjective.
Players form a Fintype ι; strategy sets are E : ι → Type with Fintype, DecidableEq and Nonempty instances, and is Fintype.card (E m). Profiles are ∀ m, E m, and is Function.update p m q. The game graph is a Mathlib SimpleGraph; comparability requires , so the graph has no loops, as the Laplacian (15) requires. is EuclideanSpace ℝ on profiles. and are type synonyms of the subspaces of antisymmetric (resp. alternating) functions, with inner products built from (7), including the factor on . Lemma 4.4 (i) fails without it. The space of games is PiLp 2 of copies of , whose inner product is the unweighted sum used on p. 14, not the weighted inner product of the paper's Section 6. Adjoints are LinearMap.adjoint. The pseudoinverse is defined explicitly as the inverse of on composed with the orthogonal projection onto .
, and are defined by (28), not as the ranges of the component maps; the direct-sum part of the goal is stated independently of the formulas, so the goal cannot be satisfied by construction. Lemma 4.4 is split into five items, one per identity. "Orthogonal decomposition" in Theorem 3.1 is stated as pairwise orthogonality plus spanning. The paper's statements have no hypotheses beyond the setting, and none were added except nonemptiness of the strategy sets, which the paper assumes by writing .
Welcome contributions: a proof of the Helmholtz decomposition on a finite simple graph, general facts about the pseudoinverse (Penrose identities, is the projection onto , invariance under rescaling of inner products), and the explicit adjoint formulas (12) and (22).
A uniformly random simple graph with a prescribed degree sequence is a basic null model in network science, statistics and combinatorics: it is what a network "looks like" when nothing but its degrees is known. Chatterjee, Diaconis and Sly (arXiv:1005.1136, Ann. Appl. Probab. 2011) show that when the normalized degree sequences converge to a limiting profile , these random graphs converge almost surely to an explicit graph limit (their Theorem 1.1). That theorem has a hypothesis: must lie in the interior of the set of all possible limiting degree profiles. A hypothesis of that kind is only useful if it can be checked, and the paper's Proposition 1.2 supplies the check, in the form of a continuum version of the Erdős–Gallai criterion (Erdős and Gallai, Mat. Lapok 1960), the classical test for whether a list of integers is the degree sequence of a simple graph.
This mission formalizes Proposition 1.2 and the steps of its proof in §5 of the paper, together with the Erdős–Gallai criterion itself, which the paper cites and uses in both directions.
A degree sequence on vertices is a vector of nonnegative integers for which some simple graph (undirected, no loops, no multiple edges) on vertices has for every . Such sequences are written in nonincreasing order .
The space consists of the functions on that are nonincreasing and left continuous at every point of . It carries the modified norm
Suppose that for every a degree sequence on vertices is given. The sequence has scaling limit , a nonincreasing function on , if
The set consists of the that arise as scaling limits of degree sequences. Its interior is taken in with the topology of : is interior if every with lies in , for some .
For and the paper defines
At , approximates the slack in the -th Erdős–Gallai inequality.
In Lean these objects are IsGraphic, InDprime, norm1', Gf, HasScalingLimit, setF and InteriorF, in the namespace GivenDegreeSeq.Interior.
A function in belongs to the interior of if and only if
Proposition 1.2 turns the hypothesis of the paper's graph-limit theorem into two explicit conditions on . With it, for example, the constant profile with , the degree profile of the Erdős–Rényi graph , is seen to be interior (Remark 3, p. 6). The proposition also describes which limiting degree profiles are robust under small perturbations: away from the boundary given by the continuum Erdős–Gallai inequality and the trivial bounds and .
The Erdős–Gallai criterion is a standard tool for degree sequences, threshold graphs and network models. To the knowledge of this mission it is formalized neither in Mathlib nor on the platform, and a proof of it here is reusable well beyond this paper. The continuum objects , , scaling limits and are shared with the companion mission on the graph-limit theorem (mission 5 of this series). The proposition is proved in the paper; none of it has a machine-checked proof.
The obvious argument passes the Erdős–Gallai inequalities to the limit and back. Going to the limit is routine. Coming back is not, for two reasons. First, the discrete inequalities must hold for every , and near the normalized slack tends to , so positivity of alone gives nothing for . The bounds and of condition (i) are what control this range. Second, the approximating integer sequences must satisfy the parity condition and stay nonincreasing, while still converging in the sense of (2).
For openness, the interior must be taken under , and positivity of near has to be recovered for every nearby from condition (i), not from uniform convergence alone. In the converse direction, perturbations must stay inside , which constrains how may be modified near a zero of .
ℝ → ℝ. Only their values on enter , , , (2) and . Integrals are interval integrals. Every is monotone, hence bounded and integrable on .Fin n, so the paper's is d n ⟨i-1,_⟩ and the paper's is f ((i+1)/n). Degree sequences are vectors in Fin n → ℕ realized by a SimpleGraph (Fin n) and are nonincreasing.Infrastructure needed: the Erdős–Gallai theorem for finite sequences (both directions); Riemann-sum approximation of integrals of monotone functions; an integer-rounding construction with a parity fix. Proofs of the Erdős–Gallai criterion, and of the analytic lemmas on , are welcome independently of the goal.
The -model is the simplest exponential random graph model in which every vertex has its own parameter. It was studied by Holland and Leinhardt (1981) in the directed case and by Park and Newman (2004) and Blitzstein and Diaconis (2011) in the undirected case, and it is a close relative of the Bradley–Terry model for paired comparisons. Its sufficient statistic is the degree sequence of the observed graph, so fitting the model to data means solving a system of nonlinear equations in unknowns, one per vertex, where can be in the thousands.
Chatterjee, Diaconis and Sly (arXiv:1005.1136, Ann. Appl. Probab. 21 (2011)) give a simple iteration for this system and prove that it converges geometrically fast whenever a solution exists, at a rate that does not deteriorate with the number of vertices, and that it detects when no solution exists. The same estimate is then used in the paper's consistency theorem for the maximum likelihood estimator (Theorem 1.3) and in its graph-limit theorem (Theorem 1.1). This mission formalizes that algorithmic result, Theorem 1.5, together with the chain of numbered displays in Section 2 that proves it.
Let and label the vertices . For , the -model puts an edge between distinct vertices and independently with probability
Given an observed graph with degrees , the maximum likelihood estimate must satisfy the ML equations
The sup norm of is . For put , and define the map by
Starting from any , the fixed-point iteration is . The fixed points of are exactly the solutions of (3).
For an matrix , the operator norm is . For , the class consists of the matrices with , and for . For , is the matrix with entries .
There are functions and , continuous, independent of and , such that for every and every : if (3) has a solution , then , it is the unique solution of (3), and for all and
and if (3) has no solution, then every orbit is unbounded.
and . 6. (10), p. 13: a single , continuous in its arguments, with and .
The theorem turns an implicit statistical object, the MLE of an -parameter model, into the limit of an explicit iteration with three guarantees: a convergence rate that depends on the size of the parameters but not on ; an a posteriori error bound in terms of the computable step ; and a certificate of non-existence. The uniqueness of the MLE comes out of the same estimate. In the paper, the a priori bound is the device that proves consistency of the MLE (Theorem 1.3, applied with ), and the two-step contraction is reused in the proof of the graph-limit theorem.
The result is proved in the paper; no machine-checked proof of it is known. The work here is to formalize the known proof. The matrix inequality of Lemma 2.1 and the derivative bounds (6)–(7) are self-contained and can be attacked independently of the iteration.
The obvious approach is to show that is a contraction and apply Banach's fixed-point theorem. This fails: every row of the Jacobian of has absolute sum exactly , so is only non-expansive in the sup norm, never strictly contracting. Contraction appears only for the two-step map , through the sign pattern of the Jacobian (positive diagonal, uniformly negative off-diagonal), and only on bounded sets, with a factor that tends to as the norms grow. A second difficulty is uniformity: the factor must be bounded away from independently of , which needs , hence . For the converse, there is no fixed point to anchor the orbit, so boundedness of the orbit has to be converted into convergence before a fixed point exists.
Fin n ; vectors are Fin n → ℝ, whose Mathlib norm is the sup norm . Matrix norms are the explicit maximal absolute row sum.Needed infrastructure: calculus of (derivatives of of a sum of exponentials), the integral form of the mean value theorem for maps , and elementary matrix-norm estimates. The class and Lemma 2.1 are reusable for other diagonally dominant iterations. Proofs of any milestone are welcome, in any order.
Firms that buy from unreliable suppliers have two broad ways to protect themselves against supply disruptions: dual sourcing, which splits the order between two suppliers so that a shortfall at one is cushioned by the other, and process improvement, which invests in a supplier's operations so that it fails less often. Wang, Gilland and Tomlin, Mitigating Supply Risk: Dual Sourcing or Process Improvement? (M&SOM 12(3):489–510, 2010), compare the two in a single-period model in which the uncertainty is in the supplier's capacity, not in a proportional yield.
Real supply bases are rarely symmetric. Suppliers differ in cost, reliability and capacity because of their history or location, and the paper (p. 501) cites evidence that global sourcing has widened those differences. This mission formalizes the paper's analytical answer to one question this raises: as two otherwise identical suppliers drift apart in unit cost, which strategy gains? The paper's answer (Theorem 7, p. 502) is that the advantage of single sourcing with improvement over dual sourcing grows with the cost gap.
A firm sells one product over one season with unit revenue , salvage value and penalty per unit of unmet demand; demand has a known law with finite mean. Supplier has unit cost , committed-cost fraction and design capacity . Its realized capacity loss has a continuous distribution indexed by a reliability index ; a larger index means a stochastically smaller loss: implies for all . Losses are independent of each other and of demand.
An order delivers and costs . The realized profit is
the second-stage expected profit is , and .
In Lean these objects are MitigateSupplyRisk.Heterogeneity.Model (with Pi2, Pi2star, PiDS, Pi1single, PiSSI, Pi1) and SymData (with costModel Δ and etaModel Δ).
For suppliers identical except in unit cost,
The statement fixes no parameter values and no particular distribution; it asserts only the direction of the effect.
Theorem 7 turns a strategy comparison into a comparative-statics statement: once SSI is preferred at some cost gap, it stays preferred at every larger gap, so the preference switches at most once along a cost-heterogeneity path. Theorem 6 shows separately that both strategies benefit from heterogeneity, which is immediate for a single-sourcing strategy but not for dual sourcing, where one supplier improves and the other deteriorates. Lemma 5 is the structural fact the paper uses for the combined strategy: improvement efforts at the two suppliers are substitutes.
The results are proved in the paper's online appendix, which this formalization does not use. To our knowledge none of them has a machine-checked proof. A formal development would supply reusable pieces: an expected-profit model for random capacity with integrable profits, envelope and convexity arguments for suprema of affine families, and monotone comparative statics for single- and dual-supplier newsvendor problems.
and are both nondecreasing in (Theorem 6), so the goal compares the growth rates of two optimal values. Neither has a closed form. Both are suprema of families affine in , so they are convex but may have kinks, and an optimal improvement level need not exist when the index set is unbounded. The comparison concerns orders at different cost levels and under different strategies, so it needs a link between the dual-sourcing order from the cheaper supplier and the single-sourcing order and its response to improvement. Evaluating each side at a fixed optimizer does not give it, because the two optimizers move with . For Lemma 5, submodularity of in for each fixed does not pass to the supremum over by itself.
Fin 2. Each is the cdf of a measure ν i a on ℝ. Expectations are Bochner integrals against the product of the two loss laws and the demand law. The integrand is bounded by a constant times , so the integrals are genuine.Model.Standing and SymData.Standing):
MonotoneOn.Contributions are welcome at every level: integrability and boundedness lemmas for , convexity of the optimal values in , the symmetry argument behind Theorem 6(b), and monotone comparative statics of single-supplier orders in the reliability index.
Many data problems ask for a matrix of low rank from far fewer linear measurements than it has entries: matrix completion (recommender systems, where a few ratings of a large user–item table are observed), system identification, and quantum state tomography. Minimizing the rank under the measurement constraints is NP-hard in general. The standard convex surrogate replaces the rank by the nuclear norm, the sum of the singular values, and recovers the low-rank matrix exactly when the measurement map is well conditioned on low-rank matrices (Recht, Fazel, Parrilo 2010; Candès, Recht 2009).
Solving the nuclear norm problem at scale is itself a numerical challenge: interior point methods do not scale, and first-order methods such as singular value thresholding (Cai, Candès, Shen 2010) need many iterations. Fornasier, Rauhut and Ward proposed an alternative, iteratively reweighted least squares for matrices (IRLS-M), which replaces the nonsmooth problem by a sequence of weighted least squares problems whose weights are recomputed from the current iterate. It is the matrix analogue of the IRLS method for sparse vectors of Daubechies, DeVore, Fornasier, Güntürk 2010, and a closely related algorithm was studied at the same time by Mohan and Fazel (Allerton 2010; journal version JMLR 2012).
Timeline. 2008–2010: nuclear norm recovery under rank restricted isometry (Recht–Fazel–Parrilo) and the rank null space property (Recht–Xu–Hassibi). 2010: convergence of IRLS for under the vector null space property (Daubechies et al.). 2010–2011: IRLS-M and its convergence under the strong rank null space property (this paper, arXiv:1010.2471, SIAM J. Optim. 21(4), 2011).
Throughout, is a real matrix with , with singular values . The Frobenius norm is , the nuclear norm is , and . A linear measurement map is given by matrices through ; the data are .
The best -rank approximation error is . The map has the strong rank null space property (SRNSP) of order with constant if every nonzero and every split with admit another split with , , , and .
For the weight of is , where and . The IRLS-M algorithm with parameters and starts from , and repeats
with the weight of at level ; it stops when . Two functionals organize the analysis: , of which IRLS-M is an alternating minimization, and with for and otherwise.
For , any , a surjective and any run :
(ii) If , the iterates are relatively compact, their accumulation points minimize on the feasible set, and the sequence converges when that minimizer is unique; under the SRNSP with , every accumulation point satisfies, for every feasible and ,
(iii) Under the same SRNSP, if a feasible matrix of rank at most exists, then .
In attack order: the weighted least squares step (Lemma 5.1, the optimality condition (5.4)); the weight step (Lemma 5.2, Proposition 5.3); monotonicity of along the run (Proposition 6.1); singular value facts (Weyl's Theorem 7.1, attainment of at the spectral truncation, Lemma 6.10, Proposition 7.2); null space theory (Theorem 6.3, the inverse triangle inequality Lemma 6.6 with (6.5), Corollary 6.7); and the two steps of the proof of (ii), the optimality condition (6.10) for and the bound (6.11).
Theorem 6.11 is the convergence guarantee of IRLS-M. Combined with the fact that a small rank restricted isometry constant implies the SRNSP (Proposition 6.8, the companion mission), it yields Proposition 2.1 of the paper: under , IRLS-M recovers every rank- matrix exactly and approximately low-rank matrices stably. Part (iii) says that the algorithm detects exact low-rank data on its own: the smoothing parameter must vanish.
The result is proved on paper; no machine-checked proof exists. A complete formalization would give a machine-checked convergence proof of an IRLS-type method; none is on the platform, for vectors or matrices. It also produces reusable matrix analysis: Weyl's perturbation bound for singular values, the nuclear norm best rank- approximation (a Mirsky-type theorem), additivity of the nuclear norm under orthogonality, the null space characterization of nuclear norm recovery, and optimality conditions for spectral functions.
Two steps resist the obvious argument. First, the weight update is a constrained minimization over the positive definite cone; identifying its solution (Proposition 5.3) requires a duality or spectral argument rather than setting a gradient to zero, because the constraint is active on small singular values. Second, in case (ii) the limit functional is convex but not strictly convex, so accumulation points cannot be pinned down by uniqueness; the analysis must instead pass the optimality condition (5.4) of the iterates to the limit, using continuity of the weights in the iterate, and derive (6.10). The step relating to needs the differentiability of unitarily invariant spectral functions, which the paper imports from Lewis and Sendov. Weyl's inequality and the spectral truncation facts, routine on paper, are not yet in Mathlib for rectangular matrices.
All matrices are real (Matrix (Fin n) (Fin p) ℝ); the paper treats real and complex matrices alike. The paper's standing assumption is a hypothesis wherever objects (, , , ) occur. Nuclear norm, Frobenius norm, trace inner product and singular values come from the published definition HighDimStat_MatrixRank_Core; sv X i is , 0-based. The measurement map is given by measurement matrices (observationOp), which represents every linear map to . The weight is defined with Mathlib's continuous functional calculus, and is cfc Real.sqrt W. The algorithm is the relation IsRun: each is some minimizer of (2.9), is free, and after a stop. Accumulation points are MapClusterPt; uniqueness of a nuclear norm minimizer is a strict inequality against every other feasible matrix.
The goal cannot be satisfied vacuously: IsRun has a run for every surjective and every (Lemma 5.1 supplies the minimizers), it carries no positivity or uniqueness assumption a real run could violate, and the theorem keeps all three parts, including the unique-minimizer clause of (i) and the error bound of (ii) for every feasible and every admissible .
Two printed slips are corrected and disclosed: (5.5) omits the factor of (5.1), and (6.5) reverses the bracket of (6.4) at . Contributions welcome: Weyl's inequality and the Mirsky-type truncation theorem for rectangular matrices, the spectral calculus behind Propositions 5.3 and (6.10), and proofs of the null space results, which are independent of the algorithm.
A -join of a graph is a set of edges such that exactly the vertices of a prescribed even set have odd degree in . Minimum -joins are a classical object of combinatorial optimization: they contain shortest paths (), Chinese postman tours and perfect matchings as special cases, and their duality with -cuts connects them to integral multiflows. Whether the minimum size of a -join equals the maximum number of disjoint -cuts has been studied extensively; equality always holds in bipartite graphs (Seymour 1981).
Sebő and Tannier (Math. Oper. Res. 2004) study the number of connected components of a minimum -join, motivated by the observation that a minimum -join with few components yields a large integral packing of -cuts. Deciding whether some minimum -join has at most components is NP-complete in general (their Theorem 5). This mission formalizes the opposite end, : Theorem 6 characterizes exactly when a minimum -join can be chosen connected, in terms of the shortest-path metric of restricted to . The result first appeared in the authors' IPCO paper Connected joins in graphs (2001); the 2004 article derives it from its theory of isometric embeddings.
All graphs are finite, simple, undirected and connected. For vertices of , is the number of edges of a shortest – path. For , is the restriction of to pairs of vertices of .
For an edge set , is the number of edges of at ; is a -join if is odd exactly when . A minimum -join has the fewest edges among all -joins; a minimal one has no proper subset that is a -join. is the set of endpoints of edges of ; is connected (a tree) when the graph is connected (a tree), and is the distance in .
An isometry from to is a map with for all . A metric on a finite set is a tree metric if there is a tree (unit edge lengths) and an isometry from to ; the pair is a realization. A realization is inclusionwise minimal if no proper subtree of contains . A tree is an -join if its vertices of odd degree are exactly those of .
For connected and nonempty of even cardinality,
The conditions are required of every minimal realization; all of them are isomorphic.
Theorem 6 turns the existence of a connected minimum -join, a question about all -joins of , into conditions on the finite metric alone plus one isometric embedding of a tree into . Tree metrics can be recognized and their minimal realization constructed efficiently (Buneman 1974), and the embedding problem is the one solved in §2 of the paper, since contains all leaves of . The authors deduce that connected minimum -joins can be found in polynomial time, which contrasts with the NP-completeness of the same question for components. A consequence stated in the paper: if the minimal realization of is not a -join, then no minimum -join is connected.
The result is proved in the paper. No machine-checked version of Theorem 6, of Lemma 2, or of the uniqueness of minimal tree realizations is known to exist; Mathlib has graph distances, trees and walks, but neither -joins nor tree metrics. The mission produces these definitions and a formal proof of the characterization; the complexity consequence is out of scope.
The central difficulty is in the necessity direction. A connected minimum -join is itself a minimal realization of (Lemma 2), so satisfies the conditions; but the conditions concern the minimal realization, and transferring them from to an arbitrary minimal realization requires that minimal realizations are unique up to a label-preserving isomorphism. That uniqueness (milestone 3) is the step where the obvious approach stops: it is a statement about all trees realizing a metric, not about the graph .
SimpleGraph V with [Fintype V] [DecidableEq V]; G.Connected is a hypothesis of every statement about (SimpleGraph.dist is on unreachable pairs). Distances are natural numbers (SimpleGraph.dist).Finset (Sym2 V). Connectivity, the tree property and refer to the graph with edge set induced on , not on all of .Fin N together with a map Fin N; this avoids quantifying over a universe. A tree metric must satisfy .Reusable beyond this mission: the -join vocabulary, the path decomposition of minimal -joins, and tree metrics with the uniqueness of minimal realizations. Contributions to any milestone are welcome, as are alternative proofs of milestone 3.
Many objective functions in engineering and statistics are nonsmooth and nonconvex: the spectral abscissa of a parametrized matrix, the largest eigenvalue of a symmetric matrix function, the norm of a closed-loop system, or a maximum of finitely many smooth functions. Such functions are typically differentiable almost everywhere, yet their minimizers usually sit exactly where the gradient fails to exist. Gradient descent then zig-zags or stalls, and bundle methods, which are designed for convex functions, lose their guarantees.
Burke, Lewis and Overton (SIAM J. Optim. 15 (2005) 751–779) proposed the gradient sampling (GS) algorithm: at each iterate, sample gradients at random nearby points, take the element of least norm in their convex hull, and search along its negative. The method needs nothing beyond gradients at points of differentiability, and it has since become a standard tool for nonsmooth, nonconvex minimization (Burke, Curtis, Lewis, Overton, Simões, 2020). This mission formalizes the paper's convergence theory.
Timeline. Goldstein (1977) introduced the -subdifferential of a Lipschitz function and a conceptual descent method built on it. Clarke's generalized gradient (Clarke 1983) supplied the stationarity notion. Burke, Lewis and Overton (2005) made Goldstein's idea implementable by random sampling and proved almost-sure convergence to Clarke -stationary points for a fixed sampling radius. Kiwiel (2007) revisited the analysis and proved convergence for a modified version of the algorithm.
Let be locally Lipschitz, and let be an open dense set on which is continuously differentiable. Write for the closed Euclidean unit ball, and fix such that the level set is compact.
The Clarke subdifferential is the convex hull of all limits with and differentiable at each . For define
and the Clarke -subdifferential . A point is Clarke -stationary if , and Clarke stationary if .
The GS algorithm. Fix , , , , , and a sample size . At iteration :
With and the radius stays fixed, : this is fixed-radius mode.
In fixed-radius mode, with probability , either the algorithm stops at some iteration with , or it runs forever and there is a subsequence with
The theorem asserts nothing about along ; the authors list as an open question.
The milestones follow the paper's argument: the minimax characterization of the search direction (Lemma 2.1), the line-search descent estimate and the descent property of the iterates (§2), the almost-sure absence of a Step 1 stop, upper semicontinuity of and the uniform covering of Lemma 3.2(iv)–(v), Lebourg's mean value theorem (Theorem 3.3), the representation , the estimate of Lemma 3.1, the inclusion , and the closed graph of .
Well-posedness of the algorithm (every sample realization admits a run), Corollary 3.5(1) (the case: ), Corollary 3.6 (Clarke -stationary points with cluster at Clarke stationary points, and with a unique stationary point in the sets converge to it in the Hausdorff sense), Corollary 3.7 (with a unique stationary point in , small forces the run near it), and Theorem 3.8 (the variable-radius mode with ).
Theorem 3.4 is the first convergence guarantee for a practical method on general locally Lipschitz, nonconvex functions that uses only gradients at points of differentiability. It holds for a fixed sampling radius, the setting where most of the work is, and Corollaries 3.6–3.7 and Theorem 3.8 transfer it to radii decreasing to zero, which is how the method is used in practice. Later gradient sampling variants and their analyses start from these results.
The results are proved on paper; no machine-checked proof of them is known. A formalization would make the probabilistic structure precise, which the paper leaves informal (see Formalization scope), and would certify the hypotheses under which the theorem holds. Already the statements record two such corrections.
The natural argument, " decreases and is compact, so the steps tend to zero, hence ", fails: can go to zero while stays bounded away from zero. The difficulty is to show that, on the event , the random samples land infinitely often in a configuration whose sampled hull nearly realizes at a fixed nearby point, uniformly over a compact set of iterates, and that the failed trial step at such an iteration contradicts the Armijo rule. The iterates depend on all past samples, so independence across iterations cannot be used directly.
EuclideanSpace ℝ (Fin n), is Mathlib's gradient, the Clarke subdifferential is the published ClarkeGradients.Shared.generalizedGradient, and is Metric.infDist 0 C. Local Lipschitz continuity is Mathlib's LocallyLipschitz; continuous differentiability on is ContDiffOn ℝ 1 f D.IsGSRun on the iterates, radii, tolerances, step lengths, least-norm vectors, directions and a stopping index , imposing Steps 0–4 up to . "" is the least admissible , and the Armijo and (2) inequalities are strict.IsRandomGSRun) lives on a probability space with a filtration : the samples are uniform on , independent within an iteration, and independent of , while are -measurable. The Step 4 choice may use the past and extra randomness but never future samples. "With probability 1" is ∀ᵐ. The paper's event , the realizations that hit every positive-measure subset of infinitely often, is not used, because no sequence has that property.Multiplying matrices is a basic operation whose asymptotic cost is measured by the number of scalar arithmetic operations needed as the matrix dimensions increase. The familiar entry-by-entry algorithm has cubic cost. The question addressed here is how small an exponent can describe exact multiplication of square matrices when algorithms may use more elaborate finite computations. OpenAI's October 2, 2026 paper establishes the bound for matrices over the complex numbers. Its Theorem 1.1 concerns asymptotic arithmetic complexity, with arbitrarily small positive slack in the exponent.
An arithmetic program is a finite sequence of register computations. A step can load a field constant, read an input entry, or add, subtract, or multiply two values from preceding registers. Constant loads and input reads have zero cost. Each addition, subtraction, and multiplication has cost one. There is no division operation in this program model. Outputs are selected registers, and a program is correct only when these outputs equal the matrix product for every pair of input matrices.
For a field , a real number is an admissible exponent if, for every real , there exists a real constant such that every integer size admits a correct program with cost at most . The constant must work uniformly for all sizes and all input entries. The chosen program may depend on and . The definition does not charge for a separate procedure that constructs these programs. The arithmetic matrix multiplication exponent is the real infimum of the set of admissible exponents.
The goal is exactly the complex-field exponent conclusion of OpenAI's Theorem 1.1:
In the Lean source, the quantity on the left is OAI.MatrixMultiplication.Arithmetic.omega ℂ. The bound on the right is the exact real rational (9 : ℝ) / 4, equal to . The inequality is non-strict. The theorem does not assert a strict inequality below , and it is not quantified over arbitrary fields.
The paper also states the corresponding algorithmic conclusion with every positive exponent slack. The goal here retains the exact infimum formulation used by its released comparator challenge. In particular, the bound should not be read as asserting that one fixed family has cost without any slack, or that an algorithm is efficient at a specified finite matrix size.
The result places above the asymptotic arithmetic exponent in a model with explicitly defined programs, outputs, correctness, and operation counts. It gives a statement that other formal developments can use without leaving those conventions implicit. The dependence on the complex field is part of that statement, so results using another field or another computational model require their own justified connection.
This is a port and verification of an existing proof, not a claim that the source theorem remains unproved. The released Lean development contains the proof entry point. Keeping the original definitions and conclusion allows compatibility changes to be reviewed independently of the mathematical claim.
An asymptotic exponent bound requires one uniform cost constant for every positive matrix size, while correctness quantifies over all pairs of matrices at each size. A computation for selected dimensions or selected inputs cannot satisfy those requirements. Arguments about tensors must also support the stated arithmetic program cost, including the operations needed for the relevant linear combinations. The infimum formulation makes its defining set and the interpretation of its bounds part of the supporting mathematics, rather than assumptions to insert into the target theorem.
The environment is Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Matrices are functions on finite index sets. Program evaluation and output selection give exact field values. The main theorem fixes the field to , excludes size zero from admissibility, and uses real powers for its cost estimates. Constants may be arbitrary complex numbers; no bit-cost interpretation is asserted.
The definition item preserves the original source block, including its rectangular matrix multiplication definitions and complex dual exponent. Those additional definitions support the shared source development but are not additional mission goals. A complete proof must establish the displayed bound without an admitted lemma, a new axiom, or an assumption equivalent to that bound. Reusable components include the arithmetic program model, finite tensor constructions, asymptotic bounds, and the bridge from tensor rank to arithmetic operations.
A backward stochastic differential equation (BSDE) prescribes the terminal value of a process instead of its initial value. Pardoux and Peng (1990) proved that a BSDE with Lipschitz driver has a unique adapted solution. Coupled with a forward diffusion it gives a forward–backward SDE (FBSDE), which represents the solution of a semilinear parabolic PDE (nonlinear Feynman–Kac formula) and, in mathematical finance, the price and hedging strategy of a contingent claim, including path-dependent ones such as lookback and Asian options (El Karoui, Peng and Quenez, 1997). In high dimension or with path-dependent payoffs the PDE route is impractical, so one wants a time-discretization of the FBSDE itself, with a proven rate of convergence.
Zhang (2004) gave such a scheme for terminal values that are Lipschitz functionals of the whole path of the forward diffusion, and proved that it converges in mean square at rate , and at rate for -Lipschitz or Markovian terminal values. The key input is a new -regularity estimate for the martingale integrand . The same regularity estimate underlies the analysis of the Bouchard–Touzi scheme (2004) and of regression-based Monte Carlo methods (Gobet, Lemor and Warin, 2005).
Fix , a probability space carrying a one-dimensional standard Brownian motion , and its natural filtration augmented by the null sets. For the FBSDE is
where , , are deterministic functions and is a deterministic functional of the path .
Assumption 2.3 asks that be continuous, -Hölder in time and Lipschitz in the space variables, that be -Lipschitz,
for càdlàg paths , all with one constant , and that . is -Lipschitz if the supremum can be replaced by .
A partition is , with and ; it is -uniform if for all . The Euler scheme is , , and its step process is on . With the backward scheme is and, for ,
with . The numerical approximations are the step processes and on .
Assume Assumption 2.3 and that is càdlàg. If does not depend on , or is -uniform, then
for , and, if moreover is -Lipschitz or , the same left-hand side is at most (6.6). The constant depends only on , , and . The goal fixes the rates and leaves unspecified.
Theorem 6.1 gives an explicit, implementable scheme for FBSDEs with path-dependent terminal values and a mean-square rate that is sharp up to the logarithm: by Remark 4.3 the factor cannot be removed for -Lipschitz functionals, since it is already present in the uniform error of the Euler step process. Theorem 3.1 is reusable on its own: any time-discretization of a BSDE whose error is measured against needs it.
All results are proved in the paper. As far as is known, none has a machine-checked proof; the platform has no prior BSDE discretization result. The work is formalizing the known proofs, which needs the Itô integral, Itô's isometry and martingale representation, the standard a priori estimates for SDEs and BSDEs, and Doob's maximal inequality in continuous time.
The obvious argument compares the BSDE and the scheme step by step and closes with a discrete Gronwall inequality (Lemma 5.4). Its error terms include , and no pointwise estimate is available: is only square integrable in time, with no continuity modulus in general. The proof therefore needs the summed -regularity of Theorem 3.1, whose proof goes through smooth approximations of the coefficients and of , the representation of by the variational process , and the martingale inequality of Lemma 3.3. The rate comes from the maximum of Gaussian increments, which an estimate of cannot see.
Time is ℝ≥0; the state space is EuclideanSpace ℝ (Fin d); the Brownian motion is the coordinate of a Fin 1-indexed standard Brownian motion; is the augmented filtration. These, the Itô integral and the class are reused from the published modules Peng1990_SMP_Stochastic and ReflectedBSDE_Existence_Setting. Every expectation and time integral of a square is a lower Lebesgue integral in , so a non-integrable error cannot make a bound vacuous; this rules out the trivializing formalization in which a Bochner integral of a non-integrable error is .
The solutions and are quantified as solutions of their equations; the Euler scheme, , , , are constructed. Each constant is chosen before the probability space, the data, the solution and the partition. Disclosed readings: (i) the log-rate statements assume , the paper's " fine enough" (p. 478); (ii) " is càdlàg" includes ; (iii) the uniformity constant of Definition 5.2 is , not , and may depend on it; (iv) the Hölder constant in time is ; (v) , , ; (vi) Lemma 3.3 uses in place of , which strengthens it; (vii) Lemma 5.4 assumes . Completeness of the probability space is not used.
Not formalized here: Lemma 2.2 (smooth approximation of , cited from Ma–Zhang), the background Lemmas 2.4–2.7, and the representation (6.3)–(6.4) of the scheme by functions of the Euler grid values. Welcome contributions: the SDE and BSDE a priori estimates under Lipschitz coefficients, Itô's isometry and martingale representation for the reused Itô integral, and Doob's inequality in continuous time; all are reusable well beyond this mission.
In a linearly parameterized bandit, the expected rewards of many arms are driven by a small number of unknown parameters. Each arm is a vector , and its expected reward is the inner product with an unknown parameter vector . Problems of this kind arise in marketing and revenue management, where each product is described by features (price, popularity, …) and the expected revenues of thousands of products are, to a good approximation, linear in a few unknown feature weights. Pulling one arm then reveals information about all of them, and a good policy has to exploit this correlation.
Rusmevichientong and Tsitsiklis (arXiv:0812.3465v2, 2010) studied this model with unbounded, sub-Gaussian noise and a prior on . They proved an lower bound, a matching policy for smooth arm sets, and the Uncertainty Ellipsoid (UE) policy for arbitrary arm sets. This mission formalizes their Theorem 4.2: when the set of arms is finite, the regret of UE grows like , within a constant factor of the Lai–Robbins lower bound for the classical multi-armed bandit (Lai and Robbins, 1985).
Timeline.
Let and let be a finite, nonempty set of arms. Fix , the value of the unknown parameter. Playing arm in period yields the reward . The noise is drawn afresh in each period from a law that depends only on the arm played, independently of the past. A policy chooses the arm of period as a function of the history . The regret given is
and for a prior of the Bayes risk is . The gap of arm is , and is the number of periods among the first in which is played.
Assumption 1.
The UE policy first plays . It then forms the least squares estimate with , and plays an arm maximizing . The uncertainty radius is
with and . Ties are broken arbitrarily.
There are constants depending only on such that for all and ,
If moreover each has a point mass at and a density bounded by on , there are depending only on with
The constants are left unspecified, as in the paper. Their existence, uniformly in and in the arm set, is the content.
The result. For a fixed finite arm set, Theorem 4.2 shows that a single anytime policy, which does not know , has regret for every parameter and Bayes risk . It does this with unbounded noise and correlated arms. The dependence on the problem enters only through the gaps and the number of arms. The companion result for general compact arm sets (Theorem 4.1) gives only . The finite case shows that the same policy adapts to the easier problem.
Formalizing it. The theorem is proved on paper. As far as is known, it has no machine-checked proof. The platform's finite-armed bandit library (Lattimore–Szepesvári) has the regret decomposition and UCB pull-count bounds for independent arms, e.g. BanditAlgorithm.bandit_regret_decomposition. Those statements live in a different model and do not apply to correlated linear rewards with a least squares estimator. This mission adds:
The arms are chosen adaptively, so the design matrix is random and depends on the noise. Applied with the realized , the classical Chernoff bound for a fixed weighted sum of independent noises is not valid. The obvious union bound over arms does not apply either: the event concerns the random matrix , not one arm. In the pull-count bound, the radius of arm must be controlled through the number of times was played, although mixes all arms, and the Gram matrix of the other arms may be singular.
EuclideanSpace ℝ (Fin r), so is Euclidean. The source is arXiv:0812.3465v2; its printed page numbers equal the PDF's.Set, and is its ncard. Theorem B.2 and Lemma B.6, which the paper states for any compact arm set, are stated for compact nonempty arm sets, as printed.A reinforcement-learning agent that does not know its environment has to act and learn at once. Each step spent gathering information about unfamiliar states is a step not spent collecting reward, and an agent that only exploits what it already knows may never find better behaviour. Chapter 8 of Kakade's thesis (Kakade 2003) turns this trade-off into a counting question. Run an algorithm for an arbitrarily long time on one unbroken path of experience, with no resets. At how many timesteps does it fail to act optimally with respect to a fixed planning horizon ? Kakade calls this number the sample complexity of exploration.
The question builds on two algorithms. (Kearns and Singh 2002) gave the first polynomial-time guarantee for near-optimal behaviour in an unknown MDP. (Brafman and Tennenholtz 2002) replaced 's explicit explore-or-exploit switch by optimism: unknown states are treated as maximally rewarding. Kakade's chapter sharpens the analysis of . For deterministic MDPs it shows that the number of non-optimal steps is at most , which matches its own lower bound. The thesis notes that its deterministic results are similar to those of Koenig and Simmons (1993), with the dependence on , and made explicit (pp. 99, 104). The later PAC-MDP literature (for example Strehl, Li and Littman 2009) took this counting notion as its standard measure of exploration efficiency.
An MDP has a finite set of states, a finite nonempty set of actions, a transition model and a deterministic reward . A deterministic MDP has a next-state map , with exactly when .
Online model. An algorithm is a deterministic function that maps the path observed so far, , to the next action . Started at , it produces one path ; is the subpath up to . The -step end time of is the smallest multiple of larger than . The -step value of the algorithm on is the normalized reward it collects until ,
and is the supremum of this quantity over all algorithms continuing from .
-step policies. A -step policy is a sequence of deterministic decision rules . Its -value is , and is the supremum over -step policies. For a set of states , the induced MDP agrees with on and makes every state outside absorbing with reward . The escape probability is the probability that the path of in leaves . A transition model is an -approximation to if for every .
For every , and there is one algorithm such that, for every deterministic MDP with rewards in , every start state and every ,
The result. The bound does not depend on . However long the agent runs, only a fixed number of its steps fail to be -step optimal. The thesis's Theorem 8.3.6 shows that every algorithm has such steps on some deterministic MDP, so for deterministic MDPs the upper and lower bounds coincide. The induced-MDP lemmas carry over unchanged to stochastic MDPs. Together with Lemmas 8.5.4 and 8.5.5, they give the chapter's general bound (Theorem 8.3.1). They are the template for later optimism-based analyses, which compare an optimistic model with the true one and charge the difference to the probability of leaving the known region.
Formalizing it. The results are proved in the thesis; neither Mathlib nor the Prove2Me catalog contains a machine-checked version of any of them. A complete development would contain:
The proof of Lemma 8.5.5 in the thesis uses a Chernoff bound of the form . This form fails for the upper tail when , so the pinned statement needs a different argument.
The algorithm must be fixed before the MDP. It knows nothing about or beyond what its own path reveals, yet the count has to hold for every MDP, every start state and every run length at once. A direct approach could explore each state-action pair once and then plan. That does not bound the count. Exploration is interleaved with exploitation, the agent can only reach unknown pairs through known states, and every step on the way is judged against the full -step optimum of the current cycle. The work lies in charging each non-optimal step to a distinct newly tried state-action pair, with at most steps charged per pair, while the planning policy is recomputed every time the set of known states grows. In the stochastic lemmas, the main issue is that is a supremum over all -step policies, so the comparison has to go through for every competing policy, not only the planner's.
IsTransitionKernel functions .List (S × A × ℝ) → S → A. The run is defined by recursion and is infinite. is the realised normalized sum up to the end time, and is the backward recursion , which is the supremum over algorithms by the Markov property. The count runs over for every .Four formalizations would make the goal trivial or false, and each is excluded:
Reusable beyond this mission are the finite-horizon value layer, the induced-MDP and escape-probability lemmas, and the concentration bound. Contributions to any of these are useful independently of the goal.