Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
We introduce two dual, purely quantum protocols: for entanglement distillation assisted by quantum communication (mother'' protocol) and for entanglement assisted quantum communication (father'' protocol). We show how a large class of children'' protocols (including many previously known ones) can be derived from the two by direct application of teleportation or super-dense coding. Furthermore, the parent may be recovered from most of the children protocols by making them coherent''. We also summarize the various resource trade-offs these protocols give rise to.
This mission is the statement-level formalization of A family of quantum protocols (arXiv:quant-ph/0308044v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
14 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Mother: qubit-assisted entanglement distillation (Mother resource inequality (♀); seed pinned to the first new parent result, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
8 results of the paper are not stated yet, because the library lacks an interface they need:
The new approach to the theory of complex representrations of the finite symmetric groups which based on the notions of Coxeter generators., Gelfand-Zetlin algebras, Hecke algebra, Young-Jucys-Murphi generators and which hardly used inductive structure - is systematically developed. The appearence of Young diagrams, tables is naturally explained - the set of content vectors of all Young tables is the spectra of Gel'fand-Zetlin algebra. The first steps of the theory (the list of the irrediucible representatinos, branching rule, Young orthopgonal form, Murnagan-Nakayama rule etc.)are established.This appraoch canbe used for other classical series, wreath products with symmetric groups. This paper is the revcised version of the paper of the same authors which was published in Selecta MAth. (New Series) V.2(1996).
This mission is the statement-level formalization of A New Approach to the Representation Thoery of the Symmetric Groups. 2 (arXiv:math/0503040v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
27 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 5.8: Young branching, content spectrum, and equivalence relations (Theorem 5.8, PDF p. 22). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
23 results of the paper are not stated yet, because the library lacks an interface they need:
Before the thermodynamic limit, macroscopic averages need not commute for a quantum system. As a consequence, aspects of macroscopic fluctuations or of constrained equilibrium require a careful analysis, when dealing with several observables. We propose an implementation of ideas that go back to John von Neumann's writing about the macroscopic measurement. We apply our scheme to the relation between macroscopic autonomy and an H-theorem, and to the problem of equivalence of ensembles. In particular, we show how the latter is related to the asymptotic equipartition theorem. The main point of departure is an expression of a law of large numbers for a sequence of states that start to concentrate, as the size of the system gets larger, on the macroscopic values for the different macroscopic observables. Deviations from that law are governed by the entropy.
This mission is the statement-level formalization of Quantum Macrostates, Equivalence of Ensembles and an H-Theorem (arXiv:math-ph/0601027v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
16 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 3.1: equivalence of the three quantum ensembles (Theorem 3.1: equivalence of the three quantum ensembles, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
3 results of the paper are not stated yet, because the library lacks an interface they need:
A connected algebraic group in characteristic 0 is uniquely determined by its Lie algebra. In this paper an algorithm is given for constructing an algebraic group in characteristic 0, given its Lie algebra. Using this an algorithm is presented for finding a maximal reductive subgroup and the unipotent radical of an algebraic group.
This mission is the statement-level formalization of Constructing algebraic groups from their Lie algebras (arXiv:math/0612557v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Chevalley: connected algebraic subgroups generate by uniformly bounded products (Theorem 1 (Chevalley), PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
5 results of the paper are not stated yet, because the library lacks an interface they need:
Work of Clifford, Munn and Ponizovski{\u\i} parameterized the irreducible representations of a finite semigroup in terms of the irreducible representations of its maximal subgroups. Explicit constructions of the irreducible representations were later obtained independently by Rhodes and Zalcstein and by Lallement and Petrich. All of these approaches make use of Rees's theorem characterizing 0-simple semigroups up to isomorphism. Here we provide a short modern proof of the Clifford-Munn-Ponizovski{\u\i} result based on a lemma of J. A. Green, which allows us to circumvent the theory of 0-simple semigroups. A novelty of this approach is that it works over any base ring.
This mission is the statement-level formalization of On the irreducible representations of a finite semigroup (arXiv:0712.2076v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Every simple semigroup module has an apex (Theorem 5, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
7 results of the paper are not stated yet, because the library lacks an interface they need:
We present an algorithm for the explicit numerical calculation of SU(N) and SL(N,C) Clebsch-Gordan coefficients, based on the Gelfand-Tsetlin pattern calculus. Our algorithm is well-suited for numerical implementation; we include a computer code in an appendix. Our exposition presumes only familiarity with the representation theory of SU(2).
This mission is the statement-level formalization of A numerical algorithm for the explicit calculation of SU(N) and SL(N,C) Clebsch-Gordan coefficients (arXiv:1009.0437v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
7 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is GT Littlewood–Richardson acceptance and multiplicities (§VIII, Eq.(31), Appendix B, PDF p. 9). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
2 results of the paper are not stated yet, because the library lacks an interface they need:
We describe a new method for approximating an arbitrary qubit unitary with precision using a Clifford and T circuit with gates. The method is based on rounding off a unitary to a unitary over the ring and employing exact synthesis. We also show that any qubit unitary over the ring with entries of the form can be exactly synthesized using Clifford and T gates using two ancillary qubits. This new exact synthesis algorithm is an improvement over the best known exact synthesis method by B. Giles and P. Selinger requiring elementary gates.
This mission is the statement-level formalization of Synthesis of unitaries with Clifford+T circuits (arXiv:1306.3200v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Approximate Clifford+T synthesis with two ancillas (Theorem 1, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
In this note we collect several characterizations of unitary representations of a finite dimensional Lie group which are trace class, i.e., for each compactly supported smooth function on , the operator is trace class. In particular we derive the new result that, for some , all operators , , are trace class. As a consequence the corresponding distribution character is of finite order. We further show is trace class if and only if every operator , which is smoothing in the sense that , is trace class and that this in turn is equivalent to the Fr'echet space being nuclear, which in turn is equivalent to the realizability of the Gaussian measure of on the space of distribution vectors. Finally we show that, even for infinite dimensional Fr'echet-Lie groups, and are smoothing if and only if is a Schwartz operator, i.e., all products of with operators from the derived representation are bounded.
This mission is the statement-level formalization of On the characterization of trace class representations and Schwartz operators (arXiv:1512.02451v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 1.1: integrated operators preserve smooth vectors (Lemma 1.1, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
20 results of the paper are not stated yet, because the library lacks an interface they need:
In this paper we consider the -function (the Holevo capacity of constrained channel) and the convex closure of the output entropy for arbitrary infinite dimensional channel. It is shown that the -function of an arbitrary channel is a concave lower semicontinuous function on the whole state space, having continuous restriction to any set of continuity of the output entropy. The explicit representation for the convex closure of the output entropy is obtained and its properties are explored. It is shown that the convex closure of the output entropy coincides with the convex hull of the output entropy on the convex set of states with finite output entropy. Similarly to the case of the -function, it is proved that the convex closure of the output entropy has continuous restriction to any set of continuity of output entropy. Some applications of these results to the theory of entanglement are discussed. The obtained properties of the convex closure of the output entropy make it possible to generalize to the infinite dimensional case the convex duality approach to the additivity problem.
This mission is the statement-level formalization of On entropic quantities related to the classical capacity of infinite dimensional quantum channels (arXiv:quant-ph/0411091v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
27 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §6, unnumbered Theorem: convex-duality additivity equivalence and consequences (§6, unnumbered Theorem: convex-duality additivity equivalence and consequences, PDF p. 19). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
We show that for a fixed amount of entanglement, two-mode squeezed states are those that maximize Einstein-Podolsky-Rosen-like correlations. We use this fact to determine the entanglement of formation for all symmetric Gaussian states corresponding to two modes. This is the first instance in which this measure has been determined for genuine continuous variable systems.
This mission is the statement-level formalization of Entanglement of formation for symmetric Gaussian states (arXiv:quant-ph/0304042v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Symmetric Gaussian entanglement of formation (Proposition 2: entanglement of formation of symmetric two-mode Gaussian states, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
Previous work on the classical information capacities of bosonic channels has established the capacity of the single-user pure-loss channel, bounded the capacity of the single-user thermal-noise channel, and bounded the capacity region of the multiple-access channel. The latter is a multi-user scenario in which several transmitters seek to simultaneously and independently communicate to a single receiver. We study the capacity region of the bosonic broadcast channel, in which a single transmitter seeks to simultaneously and independently communicate to two different receivers. It is known that the tightest available lower bound on the capacity of the single-user thermal-noise channel is that channel's capacity if, as conjectured, the minimum von Neumann entropy at the output of a bosonic channel with additive thermal noise occurs for coherent-state inputs. Evidence in support of this minimum output entropy conjecture has been accumulated, but a rigorous proof has not been obtained. In this paper, we propose a new minimum output entropy conjecture that, if proved to be correct, will establish that the capacity region of the bosonic broadcast channel equals the inner bound achieved using a coherent-state encoding and optimum detection. We provide some evidence that supports this new conjecture, but again a full proof is not available.
This mission is the statement-level formalization of Classical capacity of bosonic broadcast communication and a new minimum output entropy conjecture (arXiv:0706.3416v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Conditional coherent-state capacity region (Section IV, Eqs. (1), (16)-(17); PDF pp.1,3-5, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
We introduce a new form for the bosonic channel minimal output entropy conjecture, namely that among states with equal input entropy, the thermal states are the ones that have slightest increase in entropy when sent through a infinitesimal thermalizing channel. We then detail a strategy to prove the conjecture through variational techniques. This would lead to the calculation of the classical capacity of a communication channel subject to thermal noise. Our strategy detects input thermal ensembles as possible solutions for the optimal encoding of the channel, lending support to the conjecture. However, it does not seem to be able to exclude the possibility that other input ensembles can attain the channel capacity.
This mission is the statement-level formalization of The bosonic minimum output entropy conjecture and Lagrangian minimization (arXiv:0906.2758v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Thermal and displaced thermal stationary witnesses and local output-entropy minima (Unnumbered main result: thermal stationarity and local output-entropy minima, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
11 results of the paper are not stated yet, because the library lacks an interface they need:
Between 2017 and 2019 thousands of start-ups sold utility tokens in initial coin offerings (ICOs): digital vouchers that grant access to a product that does not yet exist, sold before launch and often enforced by a smart contract. The financial literature mostly treats ICOs as a way to raise capital. Shakhnov and Zaccaria (SSRN 3613261; published in Management Science, 2023, doi:10.1287/mnsc.2023.4917) ask a different question: what does a token sale do to a monopolist's pricing power when the product has network effects?
Their answer turns on commitment. A token can restrict who may use an early version of the product, so the seller can sell to high-valuation users first and serve the rest later at a lower price, without the incentive to renege that would otherwise destroy such a scheme. The paper characterises when this two-price strategy beats an ordinary one-price sale. The prediction is that token sales are more attractive for products with strong network effects and for more able entrepreneurs, and the paper's empirical section tests it on ICO data. This mission formalizes the theory: the comparison of the two strategies in Sections 5–6 and Appendix A.
A monopolist sells a digital product to a unit mass of consumers. Consumer types are uniform on with ; measures how much more an engaged ("active") user values the product than a basic user, and the paper reads it as entrepreneurial ability. If a share of consumers is active, a basic user gets utility (display (1)), where is the network intensity, and an active user of type gets .
The paper writes every price as a threshold: choosing means exactly the types become active, so
is the non-discriminatory price at which everyone buys.
The optimal payoffs are and over the pairs . Strategy is an equilibrium when . The closed forms are
The main analysis restricts to .
For :
and is strictly decreasing on .
In attack order:
The result says when a token sale pays. A token adds no technology to the product. It only lets the seller commit to a two-price schedule, and that commitment pays exactly when the network is valuable enough to cover the cost . Because the threshold falls with , more able entrepreneurs need weaker network effects to gain from an ICO. This is the comparative static the paper takes to the data. It also shows that network effects can make price discrimination unprofitable for a single-price monopolist (Proposition 1). A commitment device can make it profitable again (Proposition 3).
The paper's arguments are short calculus on closed forms, but several of its claims are stated on closed intervals where they fail at an endpoint. Its Appendix A also assumes the sign of to prove its monotonicity. A machine-checked version settles the exact ranges and gives the positivity of an independent proof. No part of the model has been formalized before.
Each step is elementary, and the difficulty lies in the case structure. The traditional-sales profit has a jump at : (6) is not the limit of (7), so the optimum cannot be read off a derivative. For the ICO the two pieces do join continuously, but the strategy space has two prices, and the late price must be shown optimal at . The ICO optimum is the root of a cubic's derivative, which involves a square root. Comparing the two optimal payoffs needs the sign of , and a direct expansion of in terms of does not settle it. Finally, the monotonicity of is a statement about on the whole range , which the paper argues via a derivative whose printed formula contains a slip.
Everything lives in the namespace UtilityTokens.ICOChoice, with one definitions module UtilityTokens.ICOChoice.Setting. All quantities are real-valued functions of and of the strategy :
sSup) of the profits over the strategy sets. They are not their closed forms, and Propositions 1–2 prove the suprema are attained maxima.sSup and division return junk values outside those ranges.Deviations from the page:
Not formalized: consumer types as a probability distribution, the participation constraints and the fixed point from which (3), (8), (9) are derived (taken as primitives), the renegotiation argument of p. 20, the welfare computation of pp. 24–26, Appendix B () and the empirical Section 3. The infrastructure needed is only Mathlib's real analysis (Real.sqrt, HasDerivAt, monotonicity on intervals); nothing outside Mathlib is required. Proofs of any milestone are welcome, as are lemmas splitting the goal into its three conjuncts.
In a linear bandit problem, a learner chooses a vector and observes a noisy scalar response that carries information about an unknown parameter. Regret analyses often need to control the sum of the learner's uncertainty in the directions it chooses. The familiar elliptical potential lemma does this when uncertainty is represented by the inverse of a deterministic, successively updated Gram matrix. Bayesian learning presents a different object: the posterior covariance of the unknown parameter given the observations. It changes with the realized data and can increase on an individual sample path. Hamidi and Bayati's technical note establishes a potential bound for this posterior object under general prior and noise distributions and uses it to analyze linear Thompson sampling.
The deterministic lemma and the posterior result answer related but distinct questions. In the deterministic setting, the update is fixed by the chosen vectors. Here, actions may depend on earlier observations and the next posterior covariance is itself random. The mission concerns the latter claim, including the observation model that gives the covariance its meaning.
Let be a probability space with an increasing filtration . An unknown parameter obeys almost surely. At time , the learner chooses an -measurable action with almost surely. An observation , measurable at time , has conditional mean and conditional variance at most when both and are known. No Gaussian law or independent noise model is part of these assumptions.
Write for the posterior covariance matrix. The quantity is the remaining parameter uncertainty in the chosen direction. The matrix function used to measure accumulated uncertainty is
The matrix order means that is positive semidefinite. Conditional expectations of matrices are taken entrywise. The filtration can contain information beyond the actions and observations; it need not be generated by them.
The first target is the source's stochastic variance reduction inequality. For every , almost surely,
The matrix potential targets are the concavity of on the positive semidefinite cone and equation (2.2): if , then
Two scalar and covariance bounds from the proof complete the milestone list: on , and almost surely. The main target, a conditional formulation of Theorem 2.1, is
The source prints an unconditional expectation on the left although can be random. Conditioning on supplies a coherent general statement; it becomes the printed display when the initial information is trivial. The goal retains the explicit factor and the horizon inside the log determinant.
The result controls a cumulative, adaptively selected posterior quadratic form using only the initial posterior covariance, the horizon and the conditional noise bound. It permits a regret analysis of linear Thompson sampling without replacing the prior by a Gaussian model. In the source, this bound feeds the Bayesian regret theorem for that algorithm; that later theorem is outside this mission's scope. Its proof would also require formalizing the sampling policy and its action-selection law.
The formal development fixes a reusable interface for finite-dimensional posterior covariance under a filtration: a parameter, adapted actions, conditional moments of observations, and an entrywise matrix covariance. It also states the matrix potential claims separately from the probability model, so those claims can serve other analyses of covariance updates. The statements compile locally as open Lean theorems; this mission does not claim machine-checked proofs of them. The deterministic elliptical potential statement already available elsewhere uses a Gram-matrix update and does not establish this posterior result.
Posterior covariance is not pathwise decreasing. The paper's Section 2 example has an observation after which . A bound that assumes for every outcome therefore fails at the first stochastic step. The issue matters especially when actions are adapted: later actions can point toward directions whose posterior variance became large after earlier data. Conditional covariance reduction is a matrix inequality, while the target is a scalar sum of quadratic forms; its potential must remain valid across those different objects.
Lean uses vectors Fin d → ℝ and the Euclidean dot product, so the unit-ball assumptions mean . The posterior covariance is the conditional expectation of centered coordinate products. The expectation of a covariance matrix is defined entrywise; matrix order is positive semidefiniteness of the difference. The conditioning sigma-algebra for is , not merely . Every observation is explicitly square-integrable, so Lean's totalized conditional variance cannot silently return zero for a non-square-integrable input. The source's bound on the parameter already supplies its integrability.
Rounds start at ; the finite sum uses . At it is empty and both sides of the goal are zero. No positivity assumption on is imposed, since the statements use and the zero-denominator covariance correction has zero numerator. The log determinant is used on positive semidefinite covariance matrices with nonnegative scalar argument, where its determinant is positive. The paper's square-root factorization of is represented by its equal direct matrix formula. A deterministic Gram matrix in place of , an independent-observation construction in place of the conditional-moment model, or a supremum-norm ball would change the theorem. The separate matrix and probability lemmas, conditional expectation infrastructure, and finite-dimensional matrix order are the principal reusable components.
Capacitated vehicle routing asks how to serve clients from a depot with vehicles that can carry only a limited load. In the unsplittable version, one vehicle must deliver each client's entire demand. This makes the choice of routes interact with bin packing: a short tour can fail because its total demand exceeds the vehicle's capacity. Approximation algorithms are therefore useful when exact optimization is impractical, and their guarantees must account for both travel distance and capacity. Friggstad et al., arXiv:2111.08138v1, pp. 1–2.
The paper distinguishes unit-demand, splittable-demand and unsplittable-demand CVRP. Earlier tour-partitioning methods gave constant-factor guarantees, while the paper's first main result is a combinatorial algorithm with ratio , where is an approximation ratio for metric traveling salesman tours. Taking gives the paper's stated ratio. The paper also gives a separate linear-programming-based improvement, which is outside this mission. These are results already proved mathematically; the mission concerns their precise Lean statements and a machine-checked proof of the combinatorial result. Friggstad et al., arXiv:2111.08138v1, pp. 2–3.
An instance consists of a finite set of clients, a separate depot , a symmetric nonnegative metric cost , and a demand for each client. A vehicle has capacity . A route starts and ends at , visits a sequence of clients, and carries at most one unit of total demand. A feasible solution is a collection of routes in which every client appears exactly once. Its cost is the sum of its routes' travel costs, and is the least such cost. The normalization to unit capacity and the positivity of every demand are standing assumptions of §2. Friggstad et al., arXiv:2111.08138v1, p. 4, Definitions 3–4.
For a threshold , a client is small when and big when . The radial sums are
The last sum is the cost of giving each big client its own depot route. Lemma 6 says . Friggstad et al., arXiv:2111.08138v1, pp. 4–5.
Algorithm 1 fixes . It obtains one traveling-salesman tour through the small clients and another through all clients. A consecutive split partitions the visiting order of a tour into capacity-feasible routes; is the minimum cost of such a partition. The algorithm also finds a minimum-cost matching with loops on the big clients, whose one- or two-client routes cost . It returns the cheaper of a matching plus a split of , and a split of . Friggstad et al., arXiv:2111.08138v1, pp. 7–8, Algorithm 1.
The first targets are the paper's intermediate bounds: Lemma 6's radial lower bound; the TSP lower bound used in §3.1; Claims 8–9 on the probabilities of the tank events; Lemma 7's -tank cost guarantee; Lemmas 10–11 on the matching; and the two branch estimates (4)–(5). These are the mission's milestones in the order in which their results are needed. Friggstad et al., arXiv:2111.08138v1, pp. 4–8.
The goal is Theorem 1. Let be the minimum depot tour length through exactly the client set , and suppose
For the specific cost
the goal says that a feasible solution attains and, for every feasible solution ,
Quantifying over every feasible solution expresses the ratio against without relying on a default value of a real infimum. Friggstad et al., arXiv:2111.08138v1, p. 2, Theorem 1; pp. 7–8, Algorithm 1.
The theorem supplies a cost guarantee for a concrete routing algorithm with a fixed threshold and two prescribed branches. It applies to unequal, indivisible client demands, while a unit-demand model cannot express the main capacity issue. The instance obtained from a -approximate TSP routine is a directly interpretable guarantee. The stronger LP-based theorem in §4 is a separate result and is not needed to establish this one. Friggstad et al., arXiv:2111.08138v1, pp. 2, 7–9.
A completed formalization would connect the paper's demand-aware CVRP model to a reusable published metric-route module, add definitions for optimal consecutive tour splitting and loop-allowed matching, and certify the stated branch and radial inequalities. Related platform results cover unit-demand VRP and TSP bounds, but their capacity and demand conventions differ. This mission introduces the unsplittable-demand statements rather than treating those unit-demand results as interchangeable.
The direct shortcut from a TSP tour to CVRP routes does not control capacity: a segment cheap in distance may carry too much demand. The big clients are especially restrictive at , since no feasible route can contain three of them. The tank lemma has to relate a partition of a fixed visiting order to the four radial terms with the exact coefficients shown above. The final ratio depends on comparing the two algorithm branches, including both matching bounds; an arbitrary feasible solution with a small cost would not establish a guarantee for Algorithm 1. Friggstad et al., arXiv:2111.08138v1, pp. 5–8.
Lean represents the nodes by Fin (n+1), with depot and all other nodes as clients. A route is a nonempty list of clients, and a solution is a list of routes whose concatenation contains each required client once. The metric and route-cost functions come from the published SupplyChainTheory_vrp definition module; its unit-demand feasibility predicate is not used. The number of clients may be zero. Costs and demands are real, capacity is exactly , and every client demand lies in . The value at the depot is unused.
Each optimum in the statement is a real infimum over a finite, nonempty, nonnegative cost set for a valid instance. Singleton routes make the split and matching candidate sets nonempty; an ordering exists for every finite client set. The TSP inputs list exactly their intended client sets, and their guarantees refer to the corresponding TSP optima. The explicit condition records what the paper means by an approximation ratio. Lemma 7 is stated for any client subset because Algorithm 1 applies it both to the small-client tour and the all-client tour. Display (5) is an upper bound: the printed equality replaces the tour cost by upper bounds. The running-time assertions are outside this cost formalization. Friggstad et al., arXiv:2111.08138v1, pp. 5–8.
The goal bounds the cost of the specified algorithm, including attainment by a feasible solution. Merely asserting that some feasible solution has cost at most would be trivial, since an optimal solution already does. Contributions to the finite-tour, consecutive-split, radial, matching and tank-event lemmas are useful beyond the final ratio.
Many consequential outcomes (a faculty position, a high-paying job) are the end of a long pipeline of earlier stages: neighbourhood, elementary school, high school, college, graduate school. Inequities that compound along such a pipeline are hard to correct by intervening only at its last stage, and a planner with a limited budget would like to decide where along the pipeline to invest. Arunachaleswaran, Kannan, Roth and Ziani (arXiv:2002.06592) introduce the pipeline intervention problem, a stylized optimization model of this question, and study it under a social-welfare objective and two fairness-motivated maximin objectives. The problem is non-convex: the welfare is a product of the decision matrices, so standard convex-optimization guarantees do not apply. Their positive result for social welfare is an additive fully polynomial-time approximation scheme (FPTAS) for networks of constant width, based on a dynamic program over a discretization of the budget and of the probability simplex. This mission formalizes that result.
A layered graph has layers , each with nodes (the width). Between consecutive layers and every node is connected to every node. Write for the simplex of probability distributions on and for the set of left stochastic matrices: nonnegative entries, every column summing to . An instance consists of
Changing into costs . With budget , the feasible set consists of the tuples with each , equal to on non-malleable entries, and . The social welfare of a tuple is , and is its maximum over .
Algorithm 1 fixes , the budget grid , , and a finite -net in (every is within distance of some element). Working backwards from the last layer, for each layer , grid budget and net distribution (or itself at ), it solves Program (7): maximize over agreeing with off with , for every smaller grid budget and every , and stores the best product . It returns .
For every instance, every , every and every -net : Algorithm 1 has a run; every run returns a tuple with
and the algorithm solves at most instances of Program (7).
Theorem 1 shows that, for networks of constant width, the welfare-maximizing intervention can be approximated to within an additive in time polynomial in , and , even though the problem is non-convex in the matrices. The same dynamic program, run over population-wise distributions, gives the paper's FPTAS for the ex-post maximin objective (Theorem 2), and through a no-regret reduction for the ex-ante maximin objective (Lemma 2). The paper also shows that the width restriction cannot be removed: approximating the maximin objective is NP-hard for polynomial width.
The result is proved in the paper; to our knowledge none of it has been machine-checked. The formalization makes the algorithm itself a mathematical object (a run relation with arbitrary tie-breaking) and checks the guarantee for every run and every net. It also pins down two statements the paper gets slightly wrong: the running-time count of Theorem 1, whose proof omits one budget loop, and the net size of Claim 2, which fails for large ; both are stated here in corrected form. Lemma 1, Corollary 2 and the simplex net are reusable for any Markov-chain or dynamic-programming result over distributions.
The welfare is multilinear but not concave in the tuple, so one cannot simply solve one convex program. Splitting the problem layer by layer requires knowing the distribution arriving at each layer, which ranges over a continuum; replacing it by a net point introduces an error at every layer, and the argument must show that these errors add up linearly rather than compound. A second source of error is the budget: the optimal split of across layers is generally not on the grid, and moving it onto the grid must cost little welfare at each layer even though the matrices interact multiplicatively. The bookkeeping that keeps the total loss at is where a careless formalization fails.
The development lives in the namespace PipelineInterv.Welfare. Transitions are indexed by Fin K with , 0-based; matrices are Matrix (Fin w) (Fin w) ℝ with M i j the probability of moving from j to i, and is Mathlib's Matrix.colStochastic. The norm and are written out, never the default sup norm. The standing assumptions of §2 (left stochastic , , ) are one predicate; the paper's without-loss-of-generality conventions (, distinct rewards) are not imposed. is expressed as "for every feasible tuple", equivalent by Remark 3. Algorithm 1 is a relation on tables: a table is a run when every stored entry is the product of a smaller-budget entry and a Program (7)-feasible matrix that maximizes the objective over all such choices; ties are arbitrary. The net is any finite -net contained in , and the budget grid is cut at .
The goal cannot be satisfied trivially: the run relation contains the optimality clause (without it any table of feasible matrices would be a run), the net is a finite set, and the goal asserts that a run exists, so the guarantee is never vacuous. The running-time clause is a count of Program (7) instances, not an asymptotic time bound; solving each instance is a linear program in variables.
A complete development needs: ℓ1 contraction of column-stochastic matrices, the Hölder bound , the existence of maximizers of a linear function over the compact Program (7) feasible set, an explicit grid net of the simplex, and the two inductions (over transitions for Claim 1, backwards over layers for the invariant). Proofs of the milestones, alternative arguments and lemmas about the suffix and prefix products are welcome.
Why do financially constrained firms charge different markups from otherwise similar firms? A firm can use a low price to attract customers today, but it may also need current cash to pay for production and avoid costly outside financing. Dou and Ji put these two incentives into a dynamic model in which the customer base affects future demand and cash holdings affect financing choices. Their SSRN working paper derives a compact expression for the resulting firm-level markup. This mission isolates that expression and the pricing calculations that support it.
The question matters for interpreting observed prices. A high price need not reflect only weak product-market competition: it may also reflect the firm's current valuation of liquidity relative to future customers. Conversely, a firm with a valuable opportunity to build a customer base may discount its product even when doing so reduces immediate operating profit. Proposition 3.1 of Dou and Ji, in the monopolistically competitive part of their model, states this trade-off through a single markup wedge. The paper separately analyzes a monopoly industry and connects the model to quantitative and empirical exercises; those results are outside this mission.
A firm's customer base measures the stock of customers attracted by firm at time . The firm sets its own price while treating the industry price index as given. The industry's price elasticity is , and the elasticity of substitution among firms' goods is , with . The firm's demand is
Sales add to the customer base at rate , while customers leave at rate . Production uses rented capital: productivity and rental rate give marginal cost . The markup is the ratio of the firm's price to this cost, . Firm cash changes with operating profit and with its return net of a cash-carrying cost. The expected drifts per unit time used here are
Here is the firm's proposed price, and and are its current customer base and cash. The marginal value of customer base and marginal value of corporate liquidity weight those drifts in the price-dependent objective . The paper calls them Lagrangian multipliers of the respective state evolutions. The markup wedge is . Under the stated sign conditions, it is nonnegative. These objects come from the model and the appendix to Proposition 3.1.
The goal states that a positive price globally maximizes over positive prices exactly when its markup satisfies Proposition 3.1:
The equivalence includes existence and uniqueness of the positive maximizing price under . The goal keeps the wedge as a quantity computed from the firm's parameters and marginal values. It does not designate the formula itself as the definition of an optimal price.
Four milestones follow the printed sequence of Online Appendix A.1: the derivative of expected customer-base growth (A.2), the derivative of expected cash growth (A.4), the equivalence between the resulting stationary condition and the price formula (A.5)–(A.6), and the conversion of that price formula into the markup expression (A.8). The SSRN version is the citation basis; printed page 33 is PDF page 34. The goal remains the proposition rather than any one appendix equation.
The formula separates two channels in a firm's price decision. The factor is the familiar constant-elasticity markup when attracting customers has no additional value. The nonnegative wedge reduces this markup according to the customer-base value relative to the liquidity value . It therefore supplies a precise interpretation of how the firm's financial position and its incentive to expand its customer base interact in pricing. This is the paper's stated “sufficient statistic” interpretation of the wedge, within its equilibrium model (Dou and Ji, Proposition 3.1).
The result is proved in the paper. The work here is to give its model quantities, derivative identities, stationary-price equation, and global optimal-price characterization machine-checkable Lean statements. The appendix equations are individually useful when formalizing other pricing results from the same model. The current mission statements carry sorry placeholders: building them checks their syntax and types, while the proofs remain for solvers.
A zero price derivative gives a candidate price, but by itself does not establish a global maximum among all admissible prices. The objective includes a negative power of price and has an open domain , so its behavior as price approaches zero or becomes large matters. Its candidate price is positive only in the regime . The paper gives the stationary relation in Appendix A.1; a complete formal proof of the goal must connect that relation to the global optimization claim without assuming the answer as an input.
Lean represents the paper's real-valued parameters in one Params structure and uses Real.rpow for demand powers. The predicates and functions concern one firm at one instant; firm and time indices are suppressed. The industry price index, customer base, cash balance, and marginal values are supplied as real numbers. Prices range over positive reals, and IsOptimalPrice means a global maximum of over that domain. The model records the expected deterministic drift per unit time. Brownian noise, the separate payout or equity-issuance control, the equilibrium price-index aggregator, and the full stochastic HJB state equation are outside the price comparison because they do not enter these displayed appendix derivatives when the index and controls are fixed.
The source states in the model but explicitly discusses after Proposition 3.1, so the standing predicate allows . It also describes in the equilibrium discussion; the formal theorem uses the weaker mathematical condition . It takes and, as implicit economic domain conditions, . The added condition makes the proposed optimal price positive and the global maximizer finite. The firm-price domain is . These commitments should be read as the domain of the formal claim, rather than as an assertion that every parameter choice produces an equilibrium of the full stochastic model.
An optimal price is defined by maximizing the drifts-based objective, not by the markup identity or stationary-price formula. The definition module, derivative milestones, and a proof of the global characterization are all available work. The real-power calculus and maximization arguments can be reused for other constant-elasticity pricing problems.
Retailers run two kinds of temporary promotion on staple products. A price reduction (PR) cuts the price of every unit for a while; a buy-one-get-one (BOGO) offer leaves the price of the first unit alone and discounts a second unit bought at the same time. Both are common in grocery retail, and in practice the manufacturer sets the wholesale price before the retailer decides which promotion to run. Which promotion a retailer should prefer, and how the choice moves profit between the manufacturer and the retailer, is a basic question in the operations and marketing literature on trade promotions.
Li, Khouja, Pan and Zhou (SSRN 3561162; Management Science, 2022, doi:10.1287/mnsc.2022.4638) model this as a two-echelon Stackelberg game with consumers who value a second unit less than the first. Their headline result for the case without consumer stockpiling (Corollary 4, pp. 23–24 of the working paper) is that, whenever both promotions are adopted in equilibrium, the manufacturer is indifferent between them while BOGO gives the retailer, and the supply chain as a whole, strictly more profit. This mission formalizes that statement about the equilibria of the model.
A unit mass of consumers has valuations uniform on . In each of two periods a consumer values the first unit at , a second unit at with , and further units at nothing. A consumer buying units in period 1 and in period 2 takes the purchase option .
Each consumer picks a utility-maximizing option. At wholesale price the retailer's profit is the expected margin of the chosen options, and the demand is the expected number of units. The manufacturer, with unit cost , earns .
There are three games. In the BOGO game the retailer may set a single price or run a BOGO; in the PR game, a single price or a PR; in the NP game, only a single price. In each, the manufacturer leads: an equilibrium is a wholesale price and a retailer strategy that is a best response at every , such that maximizes . The thresholds of the paper are
Fix and with . Take equilibria of the three games and write (BOGO), (PR), (NP) for the manufacturer's and retailer's profits. Then
and for also , , , and the retailer's share of supply-chain profit is strictly largest under BOGO; at , . Across two values in the region, the price gap , the advantage and the BOGO share strictly decrease.
The corollary separates the two effects of a promotion. Because both promotions lead to the same wholesale price and the same expected demand, the manufacturer's profit does not depend on which one the retailer runs; the entire extra supply-chain profit from BOGO goes to the retailer. This is the paper's case that BOGO is a profit-reallocation device within the channel rather than a demand-creation device. The comparison with the NP benchmark shows that, in this region, both the retailer and the supply chain gain from running BOGO rather than no promotion.
The paper's working-paper version contains no proofs (they are in a supplementary file), and none of the statements has a machine-checked proof. A complete development here checks the full chain from consumer choice to the manufacturer's optimum. It also pins down the exact domain of the claims: the strict comparisons fail at , Proposition 3 as printed leaves uncovered, and Proposition 4 b) does not hold as an equilibrium statement, because the PR demand jumps at . The statements in this mission are corrected accordingly.
The closed forms of Table 3 make Corollary 4 a matter of rational-function algebra once the equilibria are known, and that is the trap: the content lies in showing that the equilibria are exactly the Table 3 outcomes. The retailer's problem is a piecewise maximization over several consumer segmentations, compared against the single-price option on the same menu. The manufacturer's problem is then a maximization against a discontinuous best response, whose thresholds , , involve square roots. In the PR game the retailer is indifferent at between two policies with different demands. Any argument that treats the best response as a continuous function of fails there.
All quantities are real numbers. Profits and demands are interval integrals over of the margin and the number of units of the option each consumer chooses. Among tied options a consumer takes the one with more units, which affects only a null set. Feasible prices are nonnegative with and ; the page's strict has no optimum at . Wholesale prices range over . The retailer's strategy is a function of the wholesale price, so the equilibrium is subgame perfect, and ties of the retailer are resolved by the strategy, not by assumption. All of Corollary 4's claims are stated for every equilibrium, so the goal cannot be discharged by substituting Table 3, and profits are defined from consumer choices, not by the paper's formulas. The strict comparisons between BOGO and PR, and the share comparisons, carry , with the equality at as its own clause, as the corollary itself states.
The development needs piecewise integration of step functions, the maximization of concave quadratics on intervals, and inequalities with square roots. The definitions file BOGOPromo.NoStockpile.Model is self-contained. Contributions of proofs of the milestones, and of auxiliary lemmas computing the retailer's profit on each consumer segmentation, are welcome.
Investors pay for information, and the amount of information they produce changes over time. In periods when many investors are informed, more information becomes available, which makes being informed cheaper and attracts still more informed investors; when few are informed, the reverse happens. Glasserman, Mamaysky and Shen, Dynamic Information Regimes in Financial Markets (Management Science), build an overlapping-generations (OLG) asset market in which this feedback produces persistent information regimes, and use it to explain sudden price drops that occur without a change in fundamentals.
The paper extends the noisy rational-expectations framework of Grossman and Stiglitz (1980) and the OLG market of Allen, Morris and Shin (2006) with a state variable that tracks how much of the next dividend is knowable. Before regimes, price drops or information choice can be studied, the market stage must have an equilibrium for every possible fraction of informed investors. This mission formalizes that existence result.
Dividend. , with and normal innovations of variance . The innovation splits as : is known only to informed investors, is public, and is unknowable at time . Their variances are , and .
Information state. The fraction of knowable innovation lives on the grid and evolves as
where clips to and rounds up to the grid, and is the fraction informed in state .
Investors. Each generation lives one period, invests at the gross riskless return and chooses a demand for the risky asset by a mean-variance criterion with risk aversion . The variance of next period's price enters through a conjectured variance . Informed investors see ; uninformed investors see only , , and the price , and update about from the price. The supply of the asset is with and normal of variance .
Equilibrium. A linear price process is
It clears the market if the optimal demands satisfy in every state and for every realization. The conjecture is self-consistent if
A market equilibrium is a price process and a positive self-consistent conjecture with market clearing. In Lean these are Clears, SelfConsistent and MarketEquilibrium in InfoRegimes.MarketEq.Model.
Write . If and
then for every a market equilibrium exists. The shock law of , the coefficients and the grid size are arbitrary.
Proposition 4.1 makes the fraction informed a free input of the market stage. The paper's information equilibrium (Proposition 4.2), its two-regime dynamics and its price-drop analysis all take a market equilibrium for a given as their starting point. Footnote 15 shows that equilibria need not be unique: even in the single-state case there is a low-variance and a high-variance equilibrium.
The result is proved in the paper's Electronic Companion (Section EC.2), which states more general parameter conditions. No machine-checked version exists. A formalization pins down exactly what "market equilibrium" means here: optimal demands with Bayesian updating from prices, clearing for all realizations, and self-consistency of the variance conjecture. It also yields reusable components: the mean-variance demand, the Gaussian signal-extraction identity, and a present-value identity for finite Markov chains.
Market clearing alone is linear algebra: for a fixed conjecture , collecting terms determines the price coefficients, and the intercept solves a linear equation with a discounted stochastic matrix. Self-consistency is the hard part. The coefficients and depend on through the expected variances , and the uninformed investors' signal extraction, so (26) is a nonlinear fixed-point equation for on the grid, coupled across states through the transition kernel. Footnote 15 shows that it can have several solutions, and that without a bound such as (27) it can have no real solution at all. The obvious approach, iterating the map from a starting conjecture, need not converge to anything without a contraction estimate, and the paper reports that the high-variance root is unstable.
All quantities are real. The grid is Fin (m+1) with and . The standing assumptions are , and , plus the added bound : the paper never states the range of , while and (27) need . The page's is read with the standing as ; and are written as and . The law of is an arbitrary probability measure, and transition probabilities are its values on preimage sets. Conditional expectations given are finite sums against this kernel at the current state's .
Demands are maximizers of the explicit mean-variance objectives, not closed-form formulas. Uninformed demand depends only on , and the Gaussian posterior mean and variance (B.7)–(B.8) are written in closed form. Clearing is required for every realization . A trivializing formalization is ruled out: MarketEquilibrium does not hard-wire , , or , and it is not "the self-consistency map has a fixed point", which is milestone 7's hypothesis, not the goal.
Useful infrastructure: positivity and row sums of the transition kernel, continuity of the self-consistency map in , and a fixed-point theorem on a box. Brouwer's theorem is not in Mathlib, but it is Proved on the platform as AGT.brouwer_fixed_point and Plasticity.Ext.Brouwer. Proofs of any milestone, and alternative routes to the goal, are welcome.
Not in this mission: Proposition 4.2 (existence of an endogenous fraction informed), the microfoundation of §3, and the numerical analysis of §§5–6.
A stochastic game (Shapley, 1953) is a dynamic game in which the players' actions influence the evolution of a state variable. Whether every multiplayer stochastic game admits an -equilibrium for every is open even for finitely many states and the long-run average payoff; it is open as well for the general class in which each player's payoff is an arbitrary bounded Borel-measurable function of the infinite play, introduced by Blackwell (1969). This class contains the discounted and long-run average payoffs and the winning conditions of verification (Büchi, parity, Müller).
Flesch and Solan (arXiv:2208.12096; Mathematics of Operations Research, 2024) prove a weaker, unconditional statement: every such game has a subgame that admits an -equilibrium. Their tool is the Martin function, a real-valued function on histories which reduces playing well in the stochastic game to playing well in a one-shot game at each history.
Timeline.
A stochastic game consists of
A history of stage is a finite prefix with positive transition probabilities; is the set of histories and the final state of . A behavior strategy assigns a mixed action to every history. A profile and a history determine a probability measure on runs that continue . Player 's payoff in the subgame is , and the minmax value there is
A profile is an -equilibrium in if no player gains more than by a unilateral deviation, measured by . The subgame is -solvable if it has one (Definition 4.8).
A function induces at every the one-shot game , in which player receives ; its minmax value is .
For every stochastic game as above and every ,
The history may depend on and is not required to start in a prescribed initial state.
The result. Theorem 4.9 is the strongest unconditional existence statement known for multiplayer stochastic games with general payoffs. When the payoffs are shift-invariant (long-run average, limsup, parity) the solvable subgame yields an initial state with an -equilibrium (Corollary 4.10). This recovers the results of Thuijsman and Vrieze (1991) and Vieille (2000c) for the long-run average payoff. Theorem 4.4 along the way answers a question of Simon (2016): no three-player zero-sum-on-every-play game has all minmax values strictly positive.
Formalizing it. The result is proved on paper; nothing of it is machine-checked. A formalization produces:
Kernel.traj;The first idea, to play the profile of Theorem 4.4 everywhere, fails: keeps every player above the minmax value, but it is not an equilibrium, because a player may prefer some actions in the support of its own mixed action or may steer the play to histories where its own minmax value is high. Handling the first problem needs a compact set of runs on which payoffs are almost constant and a way to identify who left it. That second ingredient is the blame function of Alon, Gunby, He, Shmaya and Solan (2022), which is not available on the platform. Handling the second needs the fictitious hitting counts of (8)–(10) and a careful choice of punishment thresholds. Theorem 3.1 itself is not proved in the paper: it rests on Martin's (1998) determinacy of Blackwell games, on the multiplayer extension of Ashkenazi-Golan et al. (2022a, Theorem 3.6 and Claim 3.5, with the modification of footnote 3), and on the countable-state method of Maitra and Sudderth (1998).
Fintype with decidable equality and are nonempty. States form a nonempty Countable type, and action sets are nonempty Fintypes, the same in every state. The transition is p : S → (∀ i, A i) → PMF S.Feasible.playMeasure G σ n h is Kernel.traj of the one-stage kernel (independent mixed actions, then ) started at . Its runs begin with , so ∫ f i ∂(playMeasure G σ n h) is .⨅/⨆; they are the paper's values because payoffs and Martin functions are bounded.AGT.IsMixedNash.Kernel.traj (conditioning on the first coordinates), Lévy's upward and zero-one laws (the platform's FamousTheorems.levy_upward_theorem is Proved), and existence of Nash equilibria in finite games (AGT.nash_existence, Proved). It also needs regularity of probability measures on Polish spaces, and either a proof of Theorem 3.1 or the blame-function result of Alon et al. Contributions to any of these, and proofs of the milestones independently of one another, are welcome.Many combinatorial optimization problems are linear programs over a polytope with exponentially many facets, and one way to solve them by a polynomial-size linear program is to write the polytope as the projection of a higher-dimensional polytope with few facets. The minimum number of facets needed is the extension complexity of the polytope. It is now understood for most textbook polytopes: flows, matchings (Rothvoß 2017), arborescences, travelling-salesman tours and stable sets (Fiorini et al. 2015). Matroids are a notable exception.
For a matroid , the independence polytope is the convex hull of the characteristic vectors of the independent sets. Rothvoß showed by a counting argument that many matroids have independence polytopes of exponential extension complexity (Math. Program. 2013), so a polynomial bound can only hold for special classes. Regular matroids, those representable over every field, are the natural class: they contain the graphic and cographic matroids, and Seymour's decomposition theorem describes all of them.
Timeline:
A matroid has a finite ground set and a family of independent sets; . For , is its characteristic vector, and
An extended formulation of a set of size is a system , with exactly inequalities such that if and only if some satisfies the system. The extension complexity is the least such . The paper defines as the minimum number of facets of a polytope projecting onto , and on p. 1 it gives the extended-formulation form as an equivalent definition.
A matroid is regular if it is represented over by a totally unimodular matrix : a set is independent exactly when the corresponding columns of are linearly independent. It is binary if it is represented over . It is graphic if it is the cycle matroid of a multigraph (independent sets are forests) and cographic if its dual is graphic. A cycle is a disjoint union of circuits. For binary , the sum has ground set , and its cycles are the sets , with a cycle of , that lie in that ground set. This sum is a 1-, 2- or 3-sum when the two ground sets share zero, one or three elements, under the side conditions of p. 3. In the 3-sum case the shared set is a triangle, a 3-element circuit of both parts. A matroid is 3-connected if it is neither a 1-sum nor a 2-sum.
The constant is not fixed; the exponent is the paper's. Section 8 of the paper sketches an improvement to without proof, so the goal keeps the proved exponent.
The result. Theorem 1 shows that linear optimization over the independent sets of any regular matroid is a linear program of size polynomial in , written down without any algorithm. Regular matroids are the largest classical matroid class for which such a bound was in question, and the bound separates them from general binary matroids. The proof also gives an extended formulation for the circuit dominant of a regular matroid, a separate result that this mission does not include.
Formalizing it. The theorem is proved on paper and has no machine-checked proof. Formalizing it needs a Lean theory of matroid sums (1-, 2- and 3-sums defined through cycle spaces), decompositions of regular matroids along trees, and extended formulations, with explicit bounds on how the size of an extended formulation behaves under products, intersections with hyperplanes and convex hulls of unions. Seymour's decomposition theorem enters only through Theorem 6, which can be taken as a black box while the polyhedral part is formalized.
The obvious induction fails at 3-sums. For 1- and 2-sums, the extension complexities of the parts add (Lemma 3), and an induction gives a polynomial bound. For a 3-sum, the best known symmetric formulation for has size with (p. 4). A constant larger than 1 compounded over a decomposition tree of logarithmic depth only gives a quasi-polynomial bound, and over an unbalanced tree an exponential one. So the parts of a 3-sum have to be treated differently, and the decomposition tree has to be rebalanced into a star whose leaves have at most about half the elements.
The cographic centre is a second obstacle: the formulation of the centre's part is known only when every triangle shared with a leaf is the set of edges at a degree-3 node of the underlying graph, and getting there requires the decomposition tree of Proposition 27.
Matroid α over one ambient type ; the parts of a sum share elements of (the triangle elements) that are not in . Statements that construct decompositions (Theorem 6, Proposition 27, Lemma 4) take infinite, so that fresh elements exist; otherwise "not a 2-sum" could hold for want of room.IsEFOfSize and extensionComplexity (size = number of inequalities, equations free). Every upper bound is the existence of an extended formulation of the stated size, and bounds in terms of the parts quantify over extended formulations of the parts. This rules out the trivializing reading with an infimum that is on sets with no extended formulation.Creditors can observe a firm's liabilities while learning its asset value only after a delay. In the model of Benzoni, Garlappi, and Goldstein, this gap matters when the firm has exhausted its ability to issue more debt: creditors know that the firm has stayed above its default boundary, but do not know how close it is to that boundary now. Even though asset value moves continuously, the creditors' next observation can reveal that default has already occurred. The resulting jump-to-default intensity is an instantaneous default rate based on the creditors' delayed information. It enters the paper's analysis of bond values and the term structure of credit spreads.
The held source is the Federal Reserve Bank of Chicago's 2019 working paper, Asymmetric Information, Dynamic Debt Issuance, and the Term Structure of Credit Spreads. The journal article appeared in 2023 under the title used in this mission's name. Page and equation numbers below refer to the working paper, whose numbering has not been reconciled with the journal version.
Let be the firm's log distance to default at time : default occurs when this value first reaches zero. Under the risk-neutral measure, the paper models its motion after the firm exhausts debt capacity as . Here is drift, is volatility, and is standard Brownian motion. The creditors observe the lagged value , where the information lag is positive. In Regime 4, , and the creditors also know that default has not occurred by . Thus on the conditioning event. The regime is described in §3.3.1 and equations (22)–(27) of the working paper.
Write for the standard normal cumulative distribution function. For an initial distance and a horizon , is the probability of staying above zero throughout that horizon. The paper gives
It sets for . The killed transition density is the difference of a Gaussian transition density from and an image term from , multiplied by the indicators of and . Its exact normalization and image coefficient are those of equations (D.2)–(D.3) in Lemma 1 of the Online Appendix. The conditional density of the unobserved current value , given and survival, is .
For a short future horizon , the conditional default probability from state is . The quotient
is the last line of the intensity definition (D.19). The Regime 4 intensity is its limit as decreases to zero. It depends on the lagged distance , rather than on calendar time separately.
The goal is Corollary 1, equation (32), on printed p. 16 of the working paper. For , it identifies the right limit of , the boundary derivative of , and a closed form:
The right derivative is used because the density vanishes for and can have a nonzero derivative from positive values. The paper writes an additional indicator in (32); the target states its meaningful branch , where the conditional density exists. The milestones follow the Appendix's sequence: Lemma 1 normalizes the killed density; (D.20) gives the small-horizon default limit close to the boundary; the boundary value used in (D.22) vanishes; (D.24) fixes a Gaussian tail integral; (D.25) identifies the intensity with the boundary derivative; and the final differentiation supplies the closed form. These are statements of the Online Appendix, pp. 11–19, not separate economic assumptions.
Equation (32) gives a default rate computable from a lagged observable and model parameters. It connects the paper's structural default boundary to an intensity seen by creditors who lack the current asset value. This provides a quantitative ingredient for the paper's Regime 4 debt valuation and credit spread comparisons. Its time independence in that regime follows from the fixed lag and stationary transition law; earlier regimes have a different information set and are outside this mission.
The paper proves the formula informally in the Online Appendix. The present mission asks for machine-checked proofs of the stated identities and limits. The published normal CDF definition is available on Prove2Me, while the killed-density normalization and the hazard limit remain theorem targets here. A complete development would also provide reusable analytic results about Gaussian tails, image densities, boundary derivatives, and integration on a half-line. No theorem in this proposal is claimed as already machine-checked.
For each fixed , the chance of crossing zero during a very short interval tends to zero. Taking that pointwise limit inside would miss the intensity: values of that shrink with still contribute after division by . The paper's passage from its conditional density and short-horizon survival formula to (D.25) is the substantive limit claim. A proof must also justify that is strictly positive, so the conditional density and the displayed denominator are meaningful, and must distinguish the right derivative at zero from a two-sided derivative.
Lean uses real parameters with , , and ; the drift has no sign restriction. The positivity conditions make every square root and division in the conditional density meaningful. The horizon approaches zero through positive reals. Integrals are Lebesgue integrals over with respect to the standard measure, matching the paper's . The standard normal CDF is imported from the published BlackScholesModel_Core definition.
The Brownian layer is represented by its explicit killed Gaussian density and survival law, which the paper takes from Harrison's first-passage result. A process-level Brownian motion, stopping time, and conditional probability construction are outside this mission. These laws are fixed formulas in the model definition; the paper's derived normalization, intensity limit, and closed form remain theorem statements. In particular, the intensity is the right limit of , and is computed from the explicit killed density and survival probability. Defining intensity as or taking as an arbitrary density would erase the goal. Contributions establishing the analytic limit, positivity, integral, and differentiation milestones are all in scope.
Classical sample-size calculations for a clinical trial fix a significance level and a power and solve for the number of patients. They do not ask what the trial is for. A value-based design asks instead: given what it costs to recruit patients and what a better adoption decision is worth to the patients treated after the trial, how long should the trial run and how fast should it recruit? Health technology assessment bodies such as NICE already decide adoption on cost-effectiveness grounds, and Bayesian decision-theoretic trial design goes back to the value-of-information literature of the 1990s and 2000s (Claxton & Posnett 1996; Chick, Forster & Pertile 2017).
Alban, Chick and Forster (Management Science 2023) make the two decisions explicit, recruitment duration and recruitment rate , and let the regulatory context decide the population that benefits after the trial. Their asymptotic result, Proposition 5, says that the optimal number of patient pairs grows as the square root of that population, and that the optimal expected net gain per post-trial patient converges to a value that does not depend on the switching costs.
A new technology N is compared with a standard S. A fraction of patients is on N before the trial. Patients are randomised in pairs; recruiting at rate for a time yields pairs. The incremental net monetary benefit of N over S has prior , each pair gives an observation , and . After pairs the posterior mean has predictive law with .
After the trial the decision maker adopts N, adopts S, or keeps the current mix, paying fixed switching costs . Without discounting, the expected net gain of a design with is
where is the cost per patient, the setup cost of recruitment capacity, and switches on rewards to trial patients. Without a trial, . The post-adoption population is either a fixed pool, , or set by a fixed horizon, , with incidence and observation delay . The paper also treats discounting at rate ; the asymptotic results take .
Problem (5) maximises over , where Table EC.1 takes and . With and , the paper distinguishes four cases: I (, fixed pool), II (, fixed horizon), III (, fixed pool), IV (, fixed horizon).
Write , for the standard normal density, for the standard normal linear loss, and
Assume and . For every selection of optimal designs, with :
with (Case I) or (Case IV). In Case II the denominator is , and in Case III (corrected, see below) it is . The goal also asserts that optimal designs exist once the population is large.
The closed form (8) of through ; existence of an optimal design (Proposition 1); the reductions to one decision variable (Propositions 2–4); and the four case lemmas EC.1–EC.4 of Appendix C.4, which together give Proposition 5. Lemma EC.4 adds the finer statement that in Case IV both and grow like .
The result turns an optimisation without a closed-form solution into a rule of thumb: for a large population, the optimal trial enrols about patients. The authors show in their ProFHER application that the approximation is accurate at realistic sizes. It also explains two qualitative facts, that fixed-pool and fixed-horizon contexts reach the same value per patient, and that switching costs become irrelevant at scale.
The paper proves these results with asymptotic arguments that are sketched in places ("by rearranging and some additional asymptotic approximations"). A formal proof makes every limit exchange explicit. The formalization also corrects a misprint: the Case III constant in Proposition 5 and the constant in (EC.4) are printed without the setup-cost term , and the proof's own optimality condition shows that it belongs there. None of these results has been machine-checked before; the platform has the normal linear loss and nothing on clinical-trial design.
The objective is not concave in , has a jump where the trial stops running, and its optimiser has no closed form. The square-root law concerns an arbitrary optimiser as the population grows. So it is not enough to differentiate an asymptotic approximation of and solve the first-order condition. One must show that every optimiser escapes every bounded set, that the exact first-order condition holds there, and that the error terms of and of the indifference points and vanish at the right rates. In Case IV two decision variables diverge at different rates, and the fixed horizon couples the trial length to the post-trial population.
All quantities are real. A design is a pair . The post-adoption term of is a Bochner integral against gaussianReal µ0 σZ², and is the published InventoryControl.normalLoss. is defined by the expectation (7) and (9), never by the closed form (8), which is a milestone. Optimality is IsOptOn f S x: and on .
Decision sets follow §3.6.1: in Cases I and II, with ; in Case III, with ; in Case IV, both are free. Under a fixed horizon, is added, because beyond it , outside the model (§2.4.1 requires ). The finite box statements use , , and a fixed pool has , as in Table EC.1. Other added hypotheses: the standing sign conditions of §2 and Table EC.1 (; ; ; ), (used in the proof of Proposition 1), and .
Limits are asserted for every selection of optimisers. A separate conjunct asserts that optimisers exist for large populations, so the statement cannot be satisfied vacuously by an empty set of optimisers. It is not about a stationary point of an approximation, and is never replaced by a formula.
Two printed slips are corrected and labelled. In Proposition 5, Case III has constant , and (EC.4) has the factor in its denominator. Both follow from the cost of pairs at fixed , which is ; at the corrected constant matches a numerical optimum to four digits, the printed one does not. The branch of Lemma EC.4, Proposition 6 (discounting) and the comparative statics of §3.5 are not formalized.
A complete development needs Gaussian expectations of piecewise-linear functions, semicontinuity arguments on a box with a jump, and asymptotic analysis of argmax sets. The Gaussian-loss identities are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of the case lemmas.
The monotone complementarity problem (MCP) asks, for a continuous monotone map on the positive orthant, for a pair with , , and for every . It contains linear programming, convex quadratic programming, the monotone linear complementarity problem and the Karush–Kuhn–Tucker conditions of smooth convex programs. Interior-point methods solve it in polynomially many Newton-type steps when a strictly positive, well-centered starting point is known, but in general no such point is known, and the problem may be infeasible or feasible without any positive feasible point.
Andersen and Ye (Mathematical Programming 84, 1999) extended the homogeneous self-dual embedding of linear programming to the nonlinear MCP: one embeds the problem into a homogeneous problem that always has a trivial interior starting point, solves it by a path-following method, and reads off either a solution or a certificate of infeasibility. Section 8.4 of Ye, Interior Point Algorithms: Theory and Analysis (Wiley 1997, doi:10.1002/9781118032701) presents this construction, the convexity property of the residual set it rests on, and the analysis of one step of the algorithm. This mission formalizes that section.
Vectors are compared componentwise; is the all-ones vector, , , the Euclidean norm and the open orthant. A map is monotone if for all ; denotes its Jacobian.
The residual set is , and for the slice .
The homogeneous map on , with points written , is
The homogeneous model (HMCP) asks for with minimizing .
A map on is scaled Lipschitz with a monotone increasing if
The algorithm works in with and . At an iterate let and . The direction solves
and for a step size the new iterate is and .
Assume is scaled Lipschitz with , and let
If and , then and
The goal remains true when is only assumed differentiable on and scaled Lipschitz; this variant is posed beside the goal (see Formalization scope).
Theorem 8.29 is the one-step invariant behind the iteration bound of the homogeneous algorithm: combined with Lemma 8.28 it shows that the infeasibility residual and the complementarity gap shrink by the same factor per step while the iterates stay in a fixed neighborhood of the central path. Together with Theorem 8.25 (v)–(vi), which identifies solutions and infeasibility certificates of the MCP from maximal complementary solutions of the homogeneous model, this yields an algorithm that needs no feasible starting point and detects infeasibility. The convexity of (Theorem 8.23) is the structural fact that makes the homotopy path of the homogeneous model well defined.
These results are proved in the book (with Theorem 8.19, which Theorem 8.23 uses, left as an exercise). None of them is formalized on the platform: the existing Andersen–Ye material covers only the linear complementarity case, as a set-valued operator, and no statement about scaled Lipschitz maps or the nonlinear homogeneous map exists. A completed development gives a machine-checked analysis of an interior-point step for a nonlinear problem, with every constant explicit.
The algebra of Lemmas 8.27 and 8.28 depends on the identities and , which require differentiating a map defined through ; working with as a Fréchet derivative rather than a hand-written block matrix is part of the work. In Theorem 8.29 the nonlinearity enters only through the scaled Lipschitz bound, which applies only when , so the step must first be shown to stay well inside the orthant before the neighborhood estimate can be closed; the norms involved (, , and the scaled norms , ) must be chained in the right order. Theorem 8.23 is of a different kind: its proof passes through the homeomorphism of Theorem 8.19, whose proof the book leaves as an exercise, and a compactness argument along a homotopy.
Two points in the printed text need care. The block matrix (8.24) displayed for has a spurious transpose in its lower-left block; with the printed matrix Lemma 8.24 would fail for nonsymmetric , and the statements here use the true Jacobian. The printed proof of Theorem 8.25 (iii) (the scaled Lipschitz constant of from that of ) establishes the bound with , not the stated , and only for ; that part is not in this mission, and Theorem 8.29 assumes the scaled Lipschitz property of directly, as the book does.
Vectors are Fin N → ℝ, a point of is z : Fin (n+1) → ℝ with Fin.init z and z (Fin.last n) , and every Jacobian is Mathlib's fderiv. The standing assumptions of §8.4 are explicit hypotheses of every theorem: continuous and monotone on the open orthant , and differentiable there wherever or appears (the section assumes this silently). In the scaled Lipschitz condition, "monotone increasing" is read as nondecreasing on and ranges over . The direction is any solution of (8.42)–(8.43). The new dual iterate is defined by the first line of (8.47); its closed form is a conclusion. The book writes no in the statements of this mission: , , and are the book's explicit constants. is a total function in Lean (division by returns ), but every statement evaluates it and its derivative only at .
A trivializing formalization is excluded: the scaled Lipschitz hypothesis is not vacuous (it holds, for instance, for with any admissible ), the direction is not assumed to have any property beyond (8.42)–(8.43), and the monotonicity of and the identities (8.41) are proved milestones, not hypotheses of the goal.
Beyond the paper. One variant is posed: central_step_strong (strengthened) drops the continuity and monotonicity of from Theorem 8.29, because the scaled Lipschitz condition already forces , the only use the proof makes of monotonicity.
The development needs Fréchet derivatives of compositions with , finite-dimensional norm inequalities, and, for Theorem 8.23, invariance of domain or a direct proof of Theorem 8.19. The definitions (monotone maps on the orthant, the scaled Lipschitz condition, the homogeneous map) are reusable for the remaining parts of Theorems 8.25 and 8.26. Contributions of a proof of Theorem 8.19, and of the faithful Theorem 8.25 (iii), are welcome.
Primal-dual interior-point methods for linear programming come with two kinds of guarantee. The worst-case one is a bound of iterations to reduce the duality gap below . The asymptotic one says what happens to the duality gap near the end of the run, where practical codes spend their final iterations. For the predictor-corrector method of Mizuno, Todd and Ye (1993), Ye, Güler, Tapia and Zhang (1993) showed that the same algorithm that achieves the best known worst-case bound also drives the duality gap to zero quadratically. The proof needs neither nondegeneracy nor convergence of the iterates. Chapter 7 of Yinyu Ye's Interior Point Algorithms: Theory and Analysis (Wiley 1997, DOI 10.1002/9781118032701) gives a self-contained account. This mission formalizes its LP core.
Timeline, as attributed in the chapter's notes (§7.5): Zhang, Tapia and Dennis first obtained superlinear convergence of a primal-dual method assuming the iterates converge, and quadratic convergence assuming nondegeneracy. Quadratic convergence for general LP, with neither assumption, was first established by Ye, Güler, Tapia and Zhang, and independently by Mehrotra and by Tsuchiya. The monotone LCP version (§7.3) is due to Ye and Anstreicher, who also showed that the predictor step cannot converge superlinearly when no strictly complementary solution exists (Proposition 7.13). Monteiro and Wright extended that negative result to Newton-like methods in general.
Fix a real matrix of rank , and . Consider the standard-form pair
An interior point is a triple with , , , . Write , , for the all-ones vector and . The neighbourhood of the central path is
The strict complementarity partition collects the indices on which some optimal is positive () and those on which some optimal slack is positive (). The predictor direction at is the solution of
It is the case of the direction defined by , , . The scaling is , and denotes the Euclidean norm of the subvector of indexed by . Algorithm 4.5 (predictor-corrector, ) starts in . At each iteration it takes the largest step along that keeps the iterate in , then a full step along back towards the central path.
The order of convergence of a sequence (Definition 1.1) is the supremum of the with . Quadratic convergence (Definition 1.2) means .
For every there is a constant , depending only on and , such that at every with the predictor direction satisfies
The goal fixes no value of : it asserts only that one constant serves every point, which is the content the later results use.
Theorem 7.5, together with Lemma 7.3, says the whole predictor direction is . Through the step-size bound of Lemma 4.17 this gives and hence : quadratic convergence of the duality gap (Theorem 7.6). The same least-squares structure yields the LCP version (Theorem 7.12) and the variants of §7.4. Bounds of this kind on the directions near the optimal face also underlie finite termination and basis identification schemes.
On the formal side, no machine-checked development of interior-point asymptotics is known to the authors of this mission. Mathlib has the linear algebra (ranges, block matrices, least squares through orthogonal projection) but no linear-programming duality theory beyond what other missions supply. A formal proof would supply the Goldman–Tucker partition, the uniform bounds (7.6) and a Hoffman-type bound for least-squares solutions in reusable form.
Everything rests on a constant being uniform. For a single interior point, any bound holds with some depending on the point, so the content is entirely in choosing before the point. The natural first attempt bounds the direction through and on all indices, and this fails: on the entries grow like , and on they shrink like . Only the split along the optimal partition, with the least-squares characterization of the "large" components and the uniform bounds (7.6), balances the two. Relation (7.6) itself requires the partition to be strict (Goldman–Tucker) and an a priori bound on the iterates. For Theorem 7.6 the algorithm's step-size rule has to be carried as defined: a largest step over an interval of neighbourhood memberships.
Vectors are Fin n → ℝ and matrices Matrix (Fin m) (Fin n) ℝ. All norms are Euclidean. and are defined as unions of supports of optimal solutions; that they partition the indices is a consequence solvers must prove, not an assumption. The standing assumption appears as a hypothesis.
Instantiations of the book's (p. 213: "may depend on and/or the original problem data, but … independent of the iteration "):
A constant chosen after the point would make the goal trivially true; the statements quantify first to rule this out. Algorithm 4.5 is run for every (no termination test), and its step is the greatest admissible , not a supremum. The order of convergence and all limits superior take values in EReal, so infinite values are not collapsed to junk reals. Lemma 7.4's second problem is stated as corrected (the printed objective is ill-typed and the sign of is inconsistent with (7.4)); see the findings.
Beyond the paper. One strengthened variant: Theorem 7.5 on for every and without the rank condition. The book's proof uses the neighbourhood only through , and the rank of enters nowhere.
Needed infrastructure: LP duality and strict complementarity (Goldman–Tucker), a Hoffman-type bound for minimum-norm solutions, and weighted least squares. The definitions of the neighbourhood, the direction and Algorithm 4.5 are shared with the chapter 4 analysis and are reusable for other interior-point results. Contributions proving any milestone independently are welcome.