Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Queueing control problems (admission control, routing, service rate selection) are naturally modelled as Markov decision chains with a countably infinite state space and unbounded costs, for instance a holding cost that grows with the queue length. For such models the long-run average cost criterion is often the relevant one, and the central question is whether an optimal stationary policy exists and can be computed from an average cost optimality equation (ACOE). Chapter 7 of Linn I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, doi:10.1002/9780470317037) develops a verifiable set of conditions, the (SEN) assumptions, under which an average cost optimality inequality (ACOI) holds and yields an optimal stationary policy. The inequality may be strict (Example 7.3.1), and an optimal policy may induce a Markov chain without positive recurrent states.
Sections 7.4 and 7.5 answer two practical questions: when is the ACOI in fact an equation, and how can (SEN) be checked in a concrete model? The answer culminates in the (BOR) assumptions, which require only one well-behaved stationary policy and the finiteness of a set of low-cost states.
According to the book's bibliographic notes (p. 163): the (BOR) assumptions modify a line of development due to Borkar (SIAM J. Control Optim. 22, 1984, and 27, 1989; monograph 1991) and are weaker than his original conditions; the proof that (BOR) implies (SEN) is from Cavazos-Cadena and Sennott (Oper. Res. Letters 11, 1992), and the version of (BOR) used here is from Sennott (Prob. Eng. Inform. Sci. 7, 1993). Proposition 7.5.5 and the (CAV*) assumptions go back to Cavazos-Cadena (Kybernetika 25, 1989); Proposition 7.5.3 and Corollary 7.5.4 to Sennott (Oper. Res. 37, 1989).
A Markov decision chain consists of a countable state space , finite nonempty action sets , nonnegative finite costs and transition probabilities . A policy may use the whole history and randomize. For the discount value function is , the infimum of ; the average cost of is and the minimum average cost is . All of these lie in .
For a distinguished state the relative value is . The (SEN) assumptions are: (SEN1) is bounded on ; (SEN2) for a finite function ; (SEN3) for a finite constant . Under (SEN), is a finite constant, and a limit function is a pointwise limit of along some . The ACOI and ACOE read
For a nonempty set the first passage time is . The class consists of the policies that, from , enter with probability one in finite expected time ; adds a finite expected first passage cost . A (randomized) stationary policy is standard if the Markov chain it induces has and for every ; it then has a single positive recurrent class and a finite constant average cost .
Assume (BOR): (BOR1) a standard policy exists; (BOR2) for some the set is finite; (BOR3) every can be reached from by some . Then (SEN) holds and every limit function satisfies the ACOE; every average cost optimal stationary policy has a positive recurrent state in
at most positive recurrent classes and no null recurrent class; and a policy realizing the minimum in the ACOE satisfies for every .
Theorem 7.5.6 reduces the verification of the ACOE for a queueing model to three checks that do not involve the discount value function: exhibit one stationary policy with finite mean return times and costs to a fixed state (typically a stable "serve at maximal rate" policy), check that low costs occur on a finite set (automatic when the holding cost grows without bound, Corollaries 7.5.9–7.5.10), and check reachability of finitely many states. Its conclusions go beyond existence: optimal stationary policies induce chains with positive recurrent classes located in a known finite set, and ACOE-realizing policies reach them in finite expected time and cost. This is what makes value iteration and approximating-sequence methods in later chapters of the book applicable to these models.
The results are proved in the book. The present mission produces machine-checked statements of the first passage calculus for general (history-dependent, randomized) policies, of (SEN) and limit functions, and of the chain of implications from (CAV*) to the ACOE. No machine-checked version of these statements is known.
The obvious approach to the ACOE is to pass to the limit in the discount optimality equation. Exchanging this limit with requires a dominating function, and (SEN2) only gives a pointwise bound whose expectation may be infinite; Fatou's lemma then yields only the inequality. Obtaining equality requires tracking first passages to sets and showing that the discrepancy vanishes along them, which in turn needs finiteness of that is not assumed but has to be derived. On the recurrence side, the average cost criterion is a limit superior of Cesàro averages over a countable state space, and mass can escape to infinity; the finiteness of the set is what prevents an optimal policy from spending its time in transient or null recurrent states, and turning that into positive recurrence requires the renewal-type identities of Appendix C.
States form a countable type ; action sets are nonempty Finsets; costs are in ℝ≥0; transition probabilities are ℝ≥0∞-valued with row sums one on admissible actions. Policies are general: a history is a state sequence and an action sequence, and all probabilities and expectations (hitting probabilities, , , , ) are computed from the history probabilities of the process. , , and take values in ; when is missed with positive probability; the first passage time satisfies . and are in the extended reals, with the book's convention that a function bounded below has an expectation in . Limit functions are real valued. Positive recurrence, communicating classes and steady state probabilities are the notions for the chain induced by a (randomized) stationary policy. is the average cost of from .
A formalization in which the ACOE is asserted for some convenient function instead of every limit function, or in which is a natural-number cardinality that vanishes on infinite sets, would trivialize part of the goal; the statements quantify over all limit functions and use Set.encard.
A complete development needs: history-dependent policies and their path laws on countable spaces; first passage decompositions (strong Markov property at ); Abelian limits of ; Fatou and dominated convergence for series; and the renewal reward theorem for positive recurrent classes (Appendix C of the book). The first passage and Markov chain layer is reusable beyond this mission. Proofs of individual milestones, and sharper statements of the Appendix C facts they use, are welcome.
Queueing control problems (admission control, routing, service-rate selection, flow control) are naturally posed as Markov decision chains with a denumerably infinite state space, such as the number of customers in a buffer, and are usually judged by their long-run average cost per unit time. When the state space is finite, Chapter 6 of Sennott's book shows that an average cost optimal stationary policy always exists. On a countable state space this fails: Section 7.1 of the book gives examples in which no average cost optimal policy exists, and one in which no stationary policy comes within a given distance of the minimum average cost. The question addressed by this mission is under which verifiable conditions on the discounted value functions a countable-state model has a constant minimum average cost and an optimal stationary policy.
Timeline, following the book's bibliographic notes (p. 163). The book names Taylor (1965) and Derman (1966) as earlier pivotal work and Ross (1968), and his 1983 textbook, as the direct predecessor. Sennott (1989, Operations Research 37) weakened Ross's assumptions to cover models with unbounded costs, and proved the main result of Section 7.2; the (SEN) assumptions of Chapter 7 are the cleaner version of Sennott (1993). Cavazos-Cadena (1991) gave the example, adapted as Example 7.3.1 of the book, showing that under these assumptions the optimality inequality can be strict. The weaker (H*) assumptions of Section 7.7 appear, in a slightly different form, in Sennott (1995). Part (iv) of Theorem 7.2.3 is new in the book.
A Markov decision chain (MDC) has a countable state space , for each state a finite nonempty action set , a nonnegative finite cost , and transition probabilities with . A policy chooses the action at time at random according to a distribution that may depend on the whole history ; a stationary policy always chooses in state .
For an initial state , the -horizon cost is , the average cost is , and the minimum average cost is over all policies. A policy is average cost optimal if . For the discounted value function is . All these quantities lie in .
Fix a distinguished state and put . The (SEN) assumptions are:
A limit function is a pointwise limit of along some sequence . If is a stationary policy realizing the discount optimality equation , a limit point is a stationary policy with for large , for each , along some .
Under (SEN), there is a finite constant independent of ; limit functions exist, satisfy and the average cost optimality inequality (ACOI)
every stationary policy realizing the minimum is average cost optimal with and ; every limit point of discount optimal stationary policies is average cost optimal and satisfies the corresponding inequality for an associated limit function; and the average cost of any optimal policy is a limit, not only a limit supremum.
Theorem 7.2.3 is the existence theorem the rest of Chapter 7 builds on (p. 128): the ACOE results of Section 7.4, the (BOR) and (CAV) sufficient conditions of Section 7.5, and the worked queueing models of Section 7.6 all work under (SEN) and invoke it. It justifies computing an average cost optimal policy for a queueing model as a limit of discount optimal policies, and it shows that the minimum average cost is the Abelian limit of the normalized discounted value.
The results are proved in the book and in Sennott (1989, 1993, 1995), but none of them has a machine-checked proof: Mathlib has no Markov decision processes, and the platform's average cost results concern finite state spaces or Borel models with different assumptions. The formalization produces a general-policy, countable-state MDC development with extended-real values, reusable by the later missions of this series.
On a finite state space the relative value functions are bounded and the Abelian limit can be controlled directly. Here is bounded above only by a function that may be unbounded, so passing to the limit in the discounted optimality equation cannot use dominated convergence, and in general only an inequality survives in the limit; Example 7.3.1 shows that the inequality in the ACOI can be strict. Showing that a policy realizing the ACOI is optimal requires control of for a function that is unbounded above, and part (iv) requires comparing the limit inferior and limit superior of Cesàro averages for an arbitrary, possibly history-dependent optimal policy.
The state space is any countable type ([Countable S]); actions form a type with finite nonempty Finset action sets; costs are ℝ≥0; transition probabilities, costs over time and value functions are ℝ≥0∞. Policies are general: randomized and history dependent, with histories encoded as finite state and action sequences and the process law built by an explicit recursive product. Finite horizon costs have terminal cost , as the chapter prescribes.
The relative value is computed in EReal, never through a truncated real subtraction: a state with gives , so (SEN2) cannot hold through a junk value, and (SEN1) is a bound by a finite constant that itself forces . Sums and expectations of real functions are extended reals, computed as positive part minus negative part; they are never Bochner integrals and never default to when not summable. The limit is the filter 𝓝[<] 1. Limit functions and limit points follow Definition 7.2.2 literally, over arbitrary sequences in , and the (SEN), (H), (H*) sets are predicates carrying their witnesses and .
A development that bounds only as a free function, rather than the one built from the infimum over all policies, or that quantifies only over stationary policies in , proves a different and weaker theorem and does not count.
Needed infrastructure: the law of the controlled process under a general policy, monotone and Fatou-type limit interchanges for countable sums, the Abelian inequality (Proposition 6.1.1 of the book), and the existence and optimality of discount optimal stationary policies (Theorem 4.1.4). The MDC layer and these two results are shared with other missions of the series; contributions to them are welcome.
Average cost Markov decision chains model systems that run indefinitely and are judged by their long-run cost per step: admission and routing control in queues, inventory replenishment, machine maintenance. For a finite state space the classical tool is the average cost optimality equation (ACOE)
whose solution gives both the minimum average cost and an optimal stationary policy. To be useful the equation has to be solved numerically, and the method used in practice is value iteration: compute the minimum -horizon costs and extract and from their growth. This mission formalizes Sections 6.4–6.6 of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, doi:10.1002/9780470317037): when the minimum average cost is constant, the ACOE holds, any solution of it is optimal, and value iteration converges, provided the optimal policies are aperiodic. When they are not, a transformation of the model makes them so.
Related classical work includes Blackwell's discrete dynamic programming (1962) and Schweitzer–Federgruen's analysis of undiscounted value iteration (1977); Sennott's treatment derives the ACOE from the discounted value function as , which is the route that extends to countable state spaces in later chapters of the book.
A Markov decision chain (MDC) has a finite state space ; in each state a finite nonempty action set ; nonnegative costs ; and transition probabilities . A policy may use the whole history and randomize; a stationary policy always chooses in state and induces a Markov chain with transitions .
For a policy and initial state : is the expected cost of the first steps, the expected -discounted cost, and the average cost. The value functions are the infima over all policies: , and the minimum average cost . A policy is average cost optimal if .
Section 6.2 of the book provides a stationary policy that is discount optimal for all close to (a Blackwell optimal policy), and Section 6.3 builds from it a relative value function . For a distinguished state put
For a distinguished state the finite horizon relative value function is .
A positive recurrent class of a Markov chain is aperiodic if for , where is the steady state distribution. Assumption OPA ("optimal policies are aperiodic") requires every positive recurrent class of every average cost optimal stationary policy to be aperiodic. The aperiodicity transformation with keeps states and actions, scales costs by , and sets for , .
If and Assumption OPA holds, then for any distinguished state
solves the ACOE, and every limit point of the finite horizon optimal stationary policies is average cost optimal.
The ACOE with constant is the standard certificate of optimality for finite average cost models, and Proposition 6.5.1 is what allows any numerical solution of it to be trusted. Proposition 6.6.3 is the correctness theorem of the value iteration algorithm (VIA 6.6.4 of the book), and Proposition 6.6.6 removes its one extra hypothesis at the price of a model transformation. Chapter 8 of the book runs this algorithm on a sequence of finite truncations to compute optimal policies for countable-state queueing models, so these results are the base of the book's computational method.
All results in this mission are proved in the book; none has a machine-checked proof. Existing formalizations on the platform treat average reward models under a unichain hypothesis with a single action set type; this mission assumes only a constant minimum average cost (multichain models allowed) and uses the general policy class throughout.
The ACOE itself is not the obstacle; convergence of is. Theorem 6.4.2 bounds but does not make it converge, and Example 6.6.1 of the book (a two-state periodic chain) shows that without aperiodicity oscillates. The naive argument, passing to the limit in the finite horizon optimality equation, assumes the limits exist, which is exactly what is in question. Chain structure is the obstruction: a multichain optimal policy has several recurrent classes, and the Cesàro-type convergence that suffices for the ACOE itself is weaker than the pointwise convergence value iteration needs. The policy statement is also delicate, since the finite horizon minimizers need not converge.
S is finite ([Fintype S]); actions are a type Act with per-state nonempty Finset action sets. Costs are in ℝ≥0, transition probabilities in ℝ≥0∞, and all value functions are defined in [0,∞] as infima over all history-dependent randomized policies, then converted to ℝ (they are finite for finite ).min_a is Finset.inf' over . Limit points of policy sequences follow Definition B.1 (a subsequence agreeing eventually in every state). Finite horizon optimal policies are any minimizers of .The solution concept of von Neumann and Morgenstern — today usually called a stable set — was the first general answer to the question of what a rational outcome of a many-player cooperative game should be. It was introduced in Theory of Games and Economic Behavior (1944), and Chapter VI of that book states it exactly (§30) and then tests it on the smallest nontrivial case: the essential zero-sum three-person game (§32). The complete determination of all solutions of that game, (32:A)–(32:B) on p. 288, is the book's first full answer to "what are all the solutions of a given game?", and it is the result that made visible the two features every later discussion of stable sets has had to address: a game can have many solutions, and a solution can be an infinite set of imputations that discriminates against one player.
Stable sets remain an active topic in cooperative game theory: Lucas (1968) showed that some games have no stable set, and the literature on existence, uniqueness and structure (for example Shapley 1971 on convex games, whose core is the unique stable set) builds on the definitions formalized here.
A zero-sum -person game with players is described by its characteristic function , a real number for each set of players, satisfying (25:3:a)–(25:3:c):
An imputation is a vector with for each player and (30:1), (30:2). A set is effective for if (30:3). An imputation dominates , , if some nonempty set is effective for and for all (30:4). A solution is a set of imputations such that no element of dominates another element of (30:5:a) and every imputation outside is dominated by some element of (30:5:b).
Two characteristic functions are strategically equivalent if for constants with (27:1), (27:2). Every is strategically equivalent to exactly one reduced function (27:A); the game is inessential if and essential otherwise (27.3).
For three players, an essential game in reduced form with the unit chosen so that has
and its imputations are the points of the fundamental triangle , .
For the game (32:1), a set is a solution if and only if either
or, for some player and some with
is the set of all imputations with ((32:7), (32:7*), (32:7**), (32:A)). Both directions are part of the goal.
For general (§31): domination is irreflexive (31:K); an inessential game has exactly one imputation and an essential game infinitely many (31:I); solutions are never empty (31:J); in an essential game every imputation is dominated by one it does not dominate (31:L); an undominated imputation exists iff the game is inessential (31:M); a one-element solution exists iff the game is inessential, and it is then the only solution (31:P); strategic equivalence induces an isomorphism of imputations, effective sets, domination and solutions (31:Q).
For the three-person game (§32): domination is the coordinate condition (32:4) on two of the three players; two mutually undominated imputations agree in one coordinate (32:5); the set (32:6) is a solution (32:B); every set (32:7) with in the range (32:8) is a solution (32:A).
The goal is the first complete classification of the stable sets of a game. It shows that solutions are not unique and need not be finite: next to the symmetric three-point solution there is a one-parameter family, for each of the three players, of solutions that fix that player's payoff at and let the other two bargain freely. The book's interpretation of these "discriminatory" solutions (§33) as standards of behaviour is one of the lasting ideas of the theory. The general- results of §31 fix the trivial case completely: an inessential game has a unique, one-point solution, so every essential game has only solutions with at least two elements and an empty core. (31:Q) justifies working with reduced forms throughout the later chapters.
The results are proved in the book; none has a machine-checked proof on the platform as of this writing. The existing stable-set definitions on the platform concern feasible payoff vectors of a superadditive game, not imputations of a zero-sum game, so this mission also provides the book's definitions in the form every later chapter of the series (decomposition, simple games, general games) uses.
The "if" direction of the goal is a finite case analysis per set, but (30:5:b) must be checked for every imputation outside the set, with the dominating element chosen as a function of it. The "only if" direction is the substance: from an arbitrary solution — a possibly infinite, a priori unstructured subset of the triangle — one must derive that it is exactly one of the listed sets. The book's argument is geometric (Figures 54–60) and leans on pictures of dominated regions; the delicate points are the exclusion of the limiting position , where a single point of the triangle stays undominated, and the proof that a solution with two points on a horizontal line and one point off it must be exactly (32:6). The endpoint is included and must be handled; the endpoint is excluded and must be refuted.
Players are Fin n (the book's player is index ; for three players are 0, 1, 2), coalitions are Finset (Fin n), characteristic functions are Finset (Fin n) → ℝ, imputations are vectors Fin n → ℝ. The domination relation is defined on all vectors but every statement restricts it to imputations; solutions are sets of imputations and (30:5:b) quantifies over imputations only.
Standing hypotheses instantiated in the statements:
IsCharFunction v), the book's standing assumption for "a zero-sum -person game";Domination requires all three clauses of (30:4): dropping " not empty" makes every imputation dominate every other through and turns the goal into a statement about the empty solution; the definitions keep all three. The general- statements carry the characteristic-function hypotheses because without them a set function with no imputation has the empty set as a vacuous solution.
The dimension claim "an -dimensional continuum" in (31:I) is not formalized; only "infinitely many imputations" is. Contributions welcome: proofs of the milestones, a proof of the transfer of the goal to all essential three-person games through (31:Q), and reusable lemmas on domination via two-element coalitions.
Spare-parts inventory models for repairable items rest on Palm's theorem: if demands arrive as a Poisson process with constant rate and each demanded unit spends an independent, identically distributed resupply time with mean in the pipeline, the number of units in resupply is Poisson with mean in steady state. Stock levels, backorders and fill rates are all computed from that distribution.
Both assumptions fail in practice. Military flying programmes ramp up and down within weeks, repair shops close for periods, and commercial parts distribution centres see demand that varies by day of the week. Chapter 9 of Muckstadt's Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) extends Palm's theorem to a nonstationary Poisson demand process with time-dependent resupply-time distributions, gives the compound (multi-unit order) version, and uses the result to compute, at any time , the distribution of units in repair at the depot of a two-echelon system.
Timeline: Palm (1938) proved the stationary result for telephone traffic; Feeney and Sherbrooke (1966) extended it to compound Poisson demand; Hillestad and Carrillo (RAND, 1980) and Crawford (RAND, 1981) developed the time-dependent extensions, summarized by Carrillo (RAND, 1989). The chapter presents these results.
A single item is stocked at one location, and every demand is for one unit.
The mean of is
In the compound version (Section 9.2), orders arrive as above and each order is for units, with a time-stationary law . All units of an order share its resupply time, counts units demanded in , and is the -fold convolution of .
In the two-echelon version (Section 9.3), base has failure rate . A failure is repaired at the base with probability and at the depot otherwise. Depot repair of a failure occurring at time takes a deterministic time with for (no crossing). Write .
For every ,
This is an exact statement at each finite time, not a limit. With constant and it reduces to the finite-time step of Palm's theorem.
A plain supporting item states that is Poisson with mean , the factor the proof of Theorem 13 uses.
Theorem 13 gives the full distribution of the pipeline at every instant. Time-dependent expected backorders, , and fill rates follow from it, so stock levels can be planned against a surge or a repair outage without a steady-state approximation. Theorem 14 does the same for multi-unit orders. The depot result feeds the base-level convolution of Section 9.3.3, which in turn gives time-dependent performance measures for a two-echelon system.
These results are proved in the literature, and the chapter reproduces the proofs of Theorems 13 and 14. It cites Theorem 12 without proof ("similar to the one given in Chapter 3"). No machine-checked version of any of them is known, and neither Mathlib nor this platform has a Poisson process, stationary or not, a thinning theorem, or an order-statistics theorem. The formal content of this mission therefore includes the construction and the first distributional facts of the nonstationary Poisson process.
The algebra of the proof is a Poisson mixture of binomials and is short. The difficulty is Theorem 12 and its use. The obvious argument treats "the demands in " as independent draws from and assigns each an independent resupply time with law . Making this rigorous requires identifying the conditional joint law of the epochs given . The resupply time of the -th demand is not independent of its epoch: its law depends on the epoch. So it must be shown that, after conditioning, the marks attached to sorted epochs behave like marks attached to unsorted i.i.d. draws. The book's constant-rate argument (Chapter 3) uses the uniform density on the simplex. Here the density involves , which may vanish on intervals, and need not be invertible.
Service parts (spares for aircraft, machines, and networks) are typically managed item by item with a one-for-one replenishment policy, the policy: every unit withdrawn to meet a demand triggers an order for one replacement, so the inventory position stays at the stock level . A firm stocking thousands of such items at one location has to choose all the stock levels together, trading a budget on inventory investment against a service measure. Chapter 3 of Muckstadt, Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) sets up the three standard service measures (fill rate, ready rate, expected backorders), shows which of them have the convexity that optimization needs, and solves two multi-item stocking problems: minimum expected backorders under an investment budget, by Lagrangian relaxation justified by Everett's theorem, and maximum average fill rate, by a greedy marginal-analysis rule.
The Lagrangian method goes back to Everett (Operations Research 1963); the search for the multiplier in one-constraint problems of this kind is Fox and Landi (Operations Research 1970); the compound Poisson model is Feeney and Sherbrooke (Management Science 1966). The same separable Lagrangian structure underlies the multi-echelon METRIC-type models later in the book.
A single item is stocked at one location, demand not met from stock is backordered, and customer orders arrive as a Poisson process of rate . An order is for units with probability , where and the mean order size is finite (compound Poisson demand; simple Poisson demand is ). Resupply times have mean . The steady-state probability that units are in resupply is
where is the probability that orders total units. In this mission is the definition of the model, not a consequence of Palm's theorem. The mean lead-time demand is , and the book also writes .
For a stock level :
Forward differences are and ; discrete convexity means .
With items, unit costs and budget , Problem 4 (3.40) is
For a multiplier , the item-wise criterion defines as the least with , and .
For every , each exists and
for every vector of nonnegative integer stock levels. That is, is optimal for Problem 4 at budget . This is what the book asserts by combining Theorem 10 (p. 57, with the remark on p. 58) and the criterion of p. 61, and it is the basis of its bisection algorithm (p. 63). The goal fixes no numerical constant.
The goal reduces a coupled integer program over thousands of items to one scalar search: for a fixed multiplier each item is solved by a single scan of its distribution function, and each multiplier yields a point on the exact efficient frontier of expected backorders against investment. Milestone 8 does the same for fill rates on the region where they are concave, and milestone 1 explains why that region, , is imposed in practice. Milestone 4 is the identity that turns an investment budget into the constraint of Problem 4.
All results are proved in the book (Theorem 10 with a complete proof; the others by short derivations, the greedy optimality by a sketch). None of them is formalized, as far as the platform shows: there is no Everett-type Lagrangian sufficiency theorem, no compound Poisson backorder function, and no discrete marginal-analysis optimality result. The mission produces a reusable layer for later chapters: the compound Poisson steady-state law with its backorder function, and the Lagrangian machinery the book reuses for multi-echelon systems.
The algebra of first differences is elementary; the difficulties are elsewhere. is an infinite series whose convergence rests on the finiteness of the mean order size, and exchanging the difference with the sum, and identifying with , requires manipulating a doubly infinite sum over order counts and convolution powers. Existence of requires that the compound Poisson probabilities sum to one. For milestone 8 the obvious argument ("greedy is optimal for concave separable objectives") fails for knapsack constraints with unequal costs at arbitrary budgets; it holds only at the budgets the greedy run generates, and only on the region where every is concave; dropping the floor constraints makes it false.
Stock levels are natural numbers; probabilities, rates, costs and multipliers are reals. The compound Poisson law is a structure with fields , an order-size distribution with , , , and summable (the finite mean is added: without it is infinite). Expected on-hand inventory is the finite sum . Items are indexed by an arbitrary finite type (nonempty where a maximum over items is taken).
Pinnings and deviations, each stated in the item's Formalization Note:
A trivializing formalization is ruled out: the goal is stated for the book's own backorder function built from the compound Poisson law, not for an arbitrary convex function nor for a defined through its differences.
Welcome contributions: summability and normalization lemmas for the compound Poisson law, a general discrete Lagrangian lemma for separable objectives, and proofs of the milestones in any order.
Stochastic quasigradient (SQG) methods minimize an expectation over a constraint set when neither nor its gradient can be computed, only random vectors whose conditional mean is (close to) a subgradient. They are the workhorse of stochastic programming and, under the name stochastic gradient descent, of large-scale statistical learning. The classical convergence theory, going back to Robbins and Monro (1951) and to Ermoliev's quasi-Féjer analysis, asks the stepsizes to be chosen in advance with , , . Uryasev, in Chapter 18 of Numerical Techniques for Stochastic Optimization (Ermoliev and Wets, eds., 1988), points out that such programmed rules are slow in practice, and that practitioners want adaptive stepsizes computed on line from the observed directions.
Timeline:
Let be nonempty, convex and compact, its diameter, and convex on an open convex set , with subdifferential . The projection is the point of nearest to . On a probability space, the SQG method generates
from , where the direction is a stochastic quasigradient: with , a bias , and the -algebra induced by .
The adaptive stepsize rule of the chapter is, for fixed , and ,
The step grows when consecutive moves point the same way and shrinks otherwise. The weighted (Cesàro) averages are
The sequence is Cesàro convergent when converges to the solution set.
Chapter 17 (Pflug) uses the same method for over a closed convex , with from i.i.d. and stepsizes adapted to .
Under (18.15), (18.16) and (18.17), almost surely,
and if a.s., then and all accumulation points of are minimizers, almost surely.
Theorem 2 is a convergence guarantee for a stepsize rule that is computed from the run itself. It needs no square summability of the steps, and it tolerates a nonvanishing bias at a cost linear in the bias. This is the regime of practical SQG codes; §18.4–18.5 of the chapter discuss implementation and numerical experiments. Theorem 1 isolates the reason: Cesàro convergence needs only and . It also allows a stepsize that depends on the current direction, provided consecutive steps have ratio tending to .
The volume proves none of the probabilistic results in full. Theorem 1 of Chapter 18 is cited from Uryasev's earlier report. Theorem 2 has an outline proof that reduces it to Theorem 1. Chapter 17 gives a sketch through the Robbins–Siegmund lemma. None of these results is formalized. The mission produces machine-checked statements of all of them, with the misprints of the page resolved, and it separates the pathwise part of the Theorem 2 argument (steps 1 and 2, which are deterministic) from the martingale part (Theorem 1).
The obvious route to a.s. convergence is the quasi-Féjer or Robbins–Siegmund argument. It controls and needs , which is exactly what is not available here. The averaged analysis has to show that the martingale term is almost surely, and that is , when the stepsizes are themselves random. Under condition (2) of Theorem 1, is not even measurable with respect to the -algebra of the conditional expectation. So , and the standard decomposition breaks. For the adaptive rule, the stepsizes are coupled to the iterates through the exponent. Neither nor is given, and both must be derived path by path.
is EuclideanSpace ℝ (Fin n). Sequences are indexed from . Chapter 17 is shifted by one against the page: its , , become indices . Conditional expectations are Mathlib's condExp with respect to the history -algebras of the definition file. Every bound is written out as "for every , eventually ", or in (18.17) as a bound with . Expectations of squared norms are lower Lebesgue integrals. The deterministic proof steps (items 5 to 8) are stated for one sample path.
Readings of the page, each recorded in the item's Formalization Note:
No explicit constants replace an O(·) or an unspecified "C": every constant appears in the book's statements.
A trivializing formalization states Theorem 2 for arbitrary stepsizes satisfying (18.10)–(18.13), which is Theorem 1 again. Here the stepsizes are tied to the iterates by (18.5), and the of (18.17) is the of the rule.
Needed infrastructure: a Robbins–Siegmund almost-supermartingale lemma, which Mathlib does not have; a strong law for martingale differences with random weights (Kronecker's lemma in its stochastic form); nonexpansiveness of the projection onto a closed convex set; and nonemptiness of the subdifferential of a finite convex function on an open set. The first two are reusable across stochastic approximation. Contributions of any of the milestones, or of these lemmas as separate theorems, are welcome.
Decisions under uncertainty are often required to satisfy a constraint that depends on a random parameter , and requiring it for every possible is usually too conservative or infeasible. The scenario approach replaces the unknown distribution of by independent samples (scenarios) and enforces only the sampled constraints; its generalization theorem (Campi and Garatti, 2008) bounds the probability that the resulting decision violates a fresh constraint.
Enforcing all sampled constraints can still be costly: a few unusual scenarios may dominate the solution. A practitioner therefore often discards of the sampled constraints, optimally, greedily or at random, and re-solves. The question is what guarantee survives: the removed constraints were chosen by looking at the data, so the solution is biased towards points of higher risk. Campi and Garatti (2011) answered it with a bound that holds for every removal procedure. This mission formalizes that answer as it is presented in Chapter 3, Section 3.3 and Chapter 5, Section 5.3 of the textbook Introduction to the Scenario Approach (Campi and Garatti, SIAM/MOS 2018), together with its explicit corollary, Theorem 1.2. Applications include chance-constrained control, portfolio selection and prediction, where discarding scenarios trades a controlled amount of risk for a better cost.
A decision ranges over (in Lean, EuclideanSpace ℝ (Fin d)), with a closed convex domain and a linear cost . An uncertain parameter takes values in a measurable space with probability , and each determines a closed convex constraint set . The violation probability of a decision is
Given independent samples with joint law , the scenario program minimizes over . For a set of indexes, the program without the constraints in minimizes the same cost over ; its solution is written . A removal procedure selects, as a function of the whole sample, a set of indexes, and denotes the solution of the program without them. The procedure is required to output a solution that violates exactly the removed constraints (with probability one): a removed constraint that turns out to be satisfied is reinstated and another is removed. Two standing assumptions are used throughout: Assumption 3.4, that and every are convex and closed, and Assumption 3.6, that for every sample size and every sample the scenario program has exactly one solution.
For , under Assumptions 3.4 and 3.6, for every removal procedure and every ,
The bound depends on the problem only through , and on the removal procedure not at all. For it is Theorem 3.7.
Theorem 3.9 certifies every constraint-removal heuristic at once. Since the guarantee is the same for optimal, greedy and random removal, a user may pick the removal strategy purely for cost, and may inspect several values of before choosing, paying only a union bound over the values tried (Section 3.3). Theorem 1.2 turns the bound into an explicit rate: when is held fixed, the violation exceeds the empirical risk by a margin of order , only slightly worse than the rate for estimating the probability of a fixed event. The result also shows that the violation after removal concentrates around the target level, which is the basis of the book's comparison between sampling-and-discarding and simply using fewer scenarios (Example 3.10).
Theorem 3.9 is proved in the literature for general (Campi and Garatti, 2011); the textbook proves it for . To our knowledge no part of the scenario approach has a machine-checked proof. A formal development would supply the first verified version of the removal bound, a Lean treatment of solution maps of random convex programs, and reusable combinatorial and binomial-tail estimates.
The removed set is chosen after seeing the data, so the kept constraints are not an independent sample and Theorem 3.7 cannot be applied to directly. The argument must pass through all fixed index sets and account for the event that the removed constraints are violated; a plain union bound that ignores this event loses a factor and does not give (3.13). For a fixed index set, the probability that the removed scenarios are all violated involves the distribution of , which is only known to be dominated by a Beta law, so a stochastic-domination argument for the increasing function is needed. In general dimension the combinatorial constant comes from a sharper counting than the two-dimensional computation of Section 5.3, and that argument is in the cited paper rather than in the book.
Decisions live in EuclideanSpace ℝ (Fin d), samples of size are maps Fin m → Δ with law Measure.pi (fun _ => P) for a probability measure P, and the violation is the real number (P {δ | θ ∉ Θδ δ}).toReal. Events over samples are compared in ℝ≥0∞ with ENNReal.ofReal of the book's right-hand side. The removal procedure is an arbitrary map I : (Fin N → Δ) → Finset (Fin N) with (I ω).card = k, and θk is a map that, for every sample, solves the program without the constraints in I ω, and violates each of them with probability one. The following implicit hypotheses of the book are written as binders:
∀ᵐ ω ∂ℙ^N), the book's own hypothesis on p. 65, so (5.11) is an inclusion up to a null set as on the page; requiring the violation for every sample would be unsatisfiable for (on a sample with all equal a kept constraint coincides with a removed one) and would make the results vacuous;Theorem 1.2 is stated in the constraint formulation of Chapter 3, to which the book says it "straightforwardly generalizes" (p. 20), with the hypotheses of Theorem 3.9 from which Section 3.3.1 derives it. Eq. (5.14) and the closing display of Section 5.3 are stated for only, as in the book.
A trivializing formalization is excluded: the removal procedure is universally quantified, the solutions are exact minimizers rather than arbitrary feasible points, and the event is the strict ; a statement for one fixed rule, or with unconstrained, would be a different theorem.
A complete development needs: product measures and Fubini over Fin N → Δ, reindexing of the kept constraints as a sample of size , the Beta form of the binomial tail (the platform's binomial_upper_tail_eq_incomplete_beta is available), and stochastic domination for monotone integrands. Solution-map and violation infrastructure is shared with the sibling missions of this series. Contributions on any milestone, including the general- counting argument of the cited paper, are welcome.
The scenario approach turns an optimization problem under uncertainty into a finite, data-driven program: sample instances of the uncertain parameter, optimize against all of them, and certify how often the resulting design fails on a new instance. Its main guarantee (Theorem 3.7 of Campi and Garatti's Introduction to the Scenario Approach) bounds the probability of failure by a binomial tail in and in the number of optimization variables. To reach a failure level with confidence , the number of scenarios grows roughly like (Theorem 1.1 of the book). The product of and is what makes medium- and large-scale designs expensive: each scenario is one more constraint in the program that has to be solved.
FAST (Fast Algorithm for the Scenario Technique), introduced by Carè, Garatti and Campi in Operations Research 62 (2014), removes that product. It solves the program with a moderate number of scenarios and then, instead of re-optimizing, raises the returned cost level until it covers further scenarios. The book presents the algorithm and its guarantee, Theorem 8.5, in §8.3, and refers to the paper for the proof. This mission formalizes that guarantee.
Timeline:
Let be a measurable space carrying a probability measure , and let be a real loss of a decision under the uncertain parameter . As a standing assumption of the book, is convex for every .
Given scenarios drawn independently from , the scenario program (1.4) is
Its solution is and its optimal value . Assumption 3.6 requires that for every and every sample the solution exist and be unique. The pair has components, and is the number that enters every bound.
The risk (Definition 8.2) of a decision with cost level is
the probability that a new instance costs more than promised. It is the violation of the epigraphic constraint .
FAST takes independent scenarios. It solves (1.4) with the first of them, obtaining . In the detuning step it then sets
the smallest level that covers every scenario seen. The output is with .
For every ,
No relation between and is required. When the sum equals and the bound reads .
The first stage is an ordinary scenario program with scenarios. For ,
that is, is dominated by a distribution (recalled on p. 90).
For , makes the right-hand side of (8.5) at most (p. 95).
The result. Theorem 8.5 makes the guarantee of the scenario approach cheap to obtain. With (the book suggests ) and , the total number of scenarios is . This is additive in and rather than multiplicative, and the added scenarios cost only function evaluations, not a larger optimization. The price is suboptimality: is in general higher than the value a classical scenario program with the same confidence would return.
Formalizing it. The result is proved on paper, in the cited 2014 article; the book states it without proof. No part of the scenario theory has been machine-checked on this platform, as far as a search of the catalog shows. The mission produces a checked two-stage bound whose first stage is the loss-function form of Theorem 3.7, which is reusable by every mission of the series that works with program (1.4). The rule is an elementary but explicit sample-size certificate.
The obvious route treats the detuning step as a fresh scenario program with scenarios and applies Theorem 3.7 to it. That fails: is not the solution of that program, and Theorem 3.7 with scenarios gives a bound that is not of the product form (8.5). The level depends on all scenarios at once, including those that determined , and the map is monotone but need not be continuous, so the event is not a simple event about the new scenarios. Underneath the goal sits Theorem 3.7 itself, which is the main theorem of the book and whose proof occupies Chapter 5.
Lean representation:
EuclideanSpace ℝ (Fin n); the book's is written , never with natural-number subtraction.ω : Fin m → Δ with law Measure.pi (fun _ => P), and the same defines the risk. FAST draws one sample ω : Fin (N₁ + N₂) → Δ; its first stage is ω ∘ Fin.castAdd N₂.Finset.sup' over a nonempty index set. runs over all scenarios, not over the new ones only.(P {δ | c < ℓ ν δ}).toReal, with the strict inequality of Definition 8.2 and the strict event of (8.5). Probabilities of sample events are compared in ℝ≥0∞ through ENNReal.ofReal.νstar from samples to decisions, with the hypothesis that νstar ω₁ solves the program for every sample ω₁.Hypotheses the book leaves implicit, stated explicitly:
A formalization that bounds only the new scenarios is ruled out, because is defined as a maximum over all scenarios. So is one that takes as a free variable or drops Assumption 3.6: the goal is stated for the output of FAST as the book defines it.
A complete development needs the scenario program in loss form, product-measure conditioning on , and Theorem 3.7. The loss-form Theorem 3.7 is the reusable piece. Proofs of the milestones and of intermediate conditioning lemmas are welcome.
The 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. The question is how large a comparison constant is needed to make this inequality hold.
For every real , the optimal Hlawka constant for complex diagonal matrices is already proved in Lean. This mission asks whether that same constant works for all complex matrices, including rectangular ones. The statement is a conjecture. Accepted diagonal result
Audenaert and Kittaneh's Problem 7 asks for the best constant in the Schatten-norm setting, if one exists. Existence of some finite dimension-independent constant for every real is already settled by the project's Lean theorem. The task here is to establish the specified sharp candidate in the range . Audenaert–Kittaneh, §8.2, proved existence result
For a complex matrix with singular values , its Schatten norm is
There is no normalization by dimension. For three matrices of the same shape, define
Formal Schatten-norm definition
The shared cyclic candidate is
The fraction is the deficit ratio for the coordinate triple . For , its denominator is positive on the displayed interval and the supremum is attained. Cyclic definitions and attainment
The goal asks whether for every real and every triple of complex matrices of every finite shape. One constant for each exponent must work across all dimensions and triples. The endpoint 256, noninteger exponents, zero dimensions, singular and zero matrices, unequal norms and zero pair deficit are included.
Lean states the goal for complex-linear maps between any two finite-dimensional complex inner-product spaces, allowing different dimensions. No positivity, self-adjointness, commutativity or common diagonalization assumption is imposed.
The singular values determine a matrix's own norm. However, the separate singular-value lists of three matrices do not determine the norms of their pair sums and total sum. The diagonal theorem therefore does not supply the seven matrix norms needed in this inequality. Their relative directions matter as well.
The existing existence theorem supplies a constant, but does not identify it with . A proof here needs the exact cyclic constant. A proof only for even integer exponents or a restricted class of matrices would not settle this goal.
If the conjectured bound holds, it is automatically optimal uniformly over all finite matrix shapes: diagonal three-dimensional examples already require at least . Thus the missing step is that this constant works for arbitrary matrices. A counterexample would show that the diagonal constant is insufficient somewhere in the stated range. Cyclic lower bound, diagonal Schatten identity
Either outcome addresses this range of exponents; it would not settle the optimal general-matrix constant for every .
The foundation mission establishes the optimal diagonal constant for every real . The cutoff-90 mission has since extended the diagonal result in Lean to every real . The diagonal campaign invites contributors to lower that cutoff below 90.
This mission keeps and asks whether the same optimal constant works for arbitrary complex matrices, including rectangular ones. It can be pursued independently of improvements to the diagonal cutoff.
Its three linked milestones are already-proved background: existence, the sharp diagonal result, and the diagonal norm identity. The main general-matrix goal remains open. No complete proof is supplied for it.
79aa498bfcf7b22bd91d771fb32ec278e2d4704b.
Existence and diagonal librariesInterior-point methods are, together with the simplex method, the standard algorithms for linear programming, and the primal–dual path-following method is the form in which they are implemented in most solvers. Unlike the simplex method, it is a one-phase method: it can start from any point whose primal and dual variables are strictly positive, feasible or not, and drives infeasibility and complementarity to zero simultaneously. The question every user of such a method eventually asks is how fast these three measures of non-optimality decrease.
Chapter 18 of R. J. Vanderbei, Linear Programming: Foundations and Extensions (4th ed., Springer 2014, DOI 10.1007/978-1-4614-7630-6) defines the method from scratch (Fig. 18.1, p. 273) and proves a rate statement, Theorem 18.1 (pp. 277–279): as long as the step lengths stay bounded below and the iterates stay bounded, the primal and dual infeasibilities decay geometrically, and so does the complementarity, at a slower rate. This mission formalizes that theorem and the one-step identities and estimates it is built from. It is the fifth mission of a series on the book; the missions are independent of each other.
Let be a real matrix, , . The primal problem is to maximize subject to , ; the dual is to minimize subject to , . A primal–dual point is a quadruple with , ; it is strictly positive, , if every component is. Write for the diagonal matrices of and for the all-ones vector. The norms are and .
At a point the three measures of progress are the primal infeasibility , the dual infeasibility , and the complementarity . Fix parameters and . One iteration of the method, from a strictly positive point, sets , takes any solution of the Newton system
computes the step length
(with when all ratios vanish), and moves to . This is Fig. 18.1 with the shorter step (18.7) the book adopts for its analysis. Along a sequence of iterates, superscripts denote the quantities at the -th iterate, and is the step length computed there.
If , is real, and for all one has , , , then for all , with ,
The one-step identities for the infeasibilities, (18.8) and (18.9); the one-step complementarity estimate
under ; and the recursion (18.11). Two unnumbered statements complete the picture: every iteration has and keeps the point strictly positive, and at any strictly positive point the duality gap satisfies (§18.5.3).
Theorem 18.1 separates the convergence question for the path-following method into two parts: a rate statement that holds whenever steps stay long and iterates stay bounded, and the remaining question of when those two conditions hold. It also explains an effect seen in practice: the infeasibilities fall by the factor per iteration while the complementarity, and hence (by the duality-gap estimate) the gap , falls only by . The book stresses that the result is partial, because it does not show that the step lengths remain bounded away from zero; that requires modifications of the method and of the starting point that the book does not carry out.
All statements here are proved in the book. The mission's contribution is a machine-checked version, with the constant of the complementarity bound made explicit. Neither Mathlib nor the platform contains a formal proof of this theorem or a formalization of the infeasible-start primal–dual iteration it concerns; the platform's existing path-following result concerns a different, feasible-start short-step method in equality form.
The infeasibility identities are linear and follow from the first two Newton equations. The complementarity is where the Newton system linearizes a bilinear equation, so the new complementarity contains a second-order term that has no sign. Bounding it requires relating the size of the step to the size of the current iterate through the specific form of the step-length rule (18.7); the rule (18.6) of Fig. 18.1, with signed ratios, does not give such a bound. The multi-step estimate then couples two geometric sequences with different rates, and keeping the constant independent of the horizon is what makes the statement non-trivial.
Vectors are Fin n → ℝ and Fin m → ℝ, is a Matrix (Fin m) (Fin n) ℝ, and points and step directions are a structure PDPoint m n with fields x w y z. The sup-norm is ⨆ j, |v j| (the maximum; 0 for an empty vector). The step length is written with the explicit case when all ratios vanish, since Lean's r / 0 = 0 would otherwise give . An iteration is a relation between the current point, a step direction and the next point: the current point is strictly positive, the direction is some solution of the Newton system (uniqueness, which the book asserts under a full-rank assumption, is not assumed), and the next point is current direction. The hypotheses , (pp. 272–273) are stated in every theorem; is an arbitrary real number and a natural number. As in the book, the hypotheses of Theorem 18.1 range over , so the iteration from index is part of the data.
Explicit constants. The book's Theorem 18.1 asserts only "there exists a constant ". Because is fixed, that existential is satisfied trivially by , and a statement with would be empty. The goal therefore uses the constant the book's proof establishes (p. 279, last display): . Eq. (18.11) is stated with the book's written out.
The formalization needs only finite sums, dot products and matrix–vector products from Mathlib; the definitions of the iteration are reusable for other analyses of the same method (Chapters 19–22 of the book). Contributions are welcome for each milestone separately.
Interior-point methods solve linear programs by moving through the interior of the feasible region instead of along its edges, as the simplex method does. The methods used in practice are path-following methods: they track a curve, the central path, that runs through the interior of the feasible region and ends at an optimal solution. Before any such method can be analysed, the curve has to exist. This mission formalizes Chapter 17 of R. J. Vanderbei, Linear Programming: Foundations and Extensions (4th ed., Springer 2014), which defines the central path through the logarithmic barrier problem and proves that it exists exactly when the primal and the dual problem both have strictly positive feasible points.
The chapter's results have a short history. Barrier methods for nonlinear programming go back to Fiacco and McCormick (1968). Interest in interior-point methods for linear programming began with Karmarkar (1984), whose projective algorithm does not mention a central path; the connection between Karmarkar's method and the primal–dual central path was found by Megiddo (1989), with central points traced back to Huard (1967) and an extended study of the path by Bayer and Lagarias (1989). The chapter is the textbook entry point to this line of work and the foundation for the path-following algorithm of Chapter 18.
Let be a real matrix, and . The primal linear program is to maximize subject to , ; its dual is to minimize subject to , . With slack variables and they read (17.1)
For a vector , means that every component is strictly positive. The primal feasible region has nonempty interior when some satisfies with , ; the dual feasible region has nonempty interior when some satisfies with , .
For a parameter , the barrier function (17.7) is
and the barrier problem (17.2) is to maximize subject to , over the domain , where the logarithms are finite. A solution of the barrier problem is a point of that domain at which attains its maximum over the domain.
Writing for the diagonal matrices carrying and for the all-ones vector, the primal–dual central-path system (17.6) is
with . The last two equations say and for all and . The set of its solutions , , is the primal–dual central path.
The chapter also uses one fact from nonlinear programming: for the problem "maximize subject to , ", a critical point is a feasible with for some Lagrange multipliers (17.3), and is the Hessian of at .
For each fixed ,
Both directions are part of the goal. The statement fixes no constants and no rate; it asserts only when the barrier problem is solvable.
The corollary is stronger than the goal in one direction (it adds uniqueness and the dual variables) and weaker in another (it assumes boundedness).
The result itself. Theorem 17.2 gives an exact criterion for the barrier problem to be solvable for a fixed , and Corollary 17.3 turns it into the statement that the central path is a well-defined curve for all . Every path-following method, including the one analysed in Chapter 18 of the same book, targets points on this curve; without existence and uniqueness the "target" of an iteration is undefined. The system (17.6) is also the starting point of the primal–dual Newton step.
Formalizing it. These results are classical and proved in the book; none is formalized in the , form used here. The platform has the converse fact in the standard form , (a solution of the central-path conditions minimizes the barrier, Introduction to Linear Optimization), but not existence. A formal proof of Theorem 17.2 and Corollary 17.3 produces a reusable existence theorem for the central path that downstream missions on path-following and self-dual methods can import.
The "if" direction of Theorem 17.2 is an existence claim on a set that is neither closed nor bounded: the domain , is open, and the feasible region itself may be unbounded, so the obvious appeal to "a continuous function on a compact set attains its maximum" does not apply directly. The example "maximize subject to " (p. 264), whose barrier has no maximum, shows that the dual hypothesis cannot be dropped. The "only if" direction, which the book calls trivial and does not prove, needs first-order conditions at a maximizer over a relatively open set.
Theorem 17.1 needs a second-order Taylor expansion with a remainder that is uniformly along the constraint subspace, not along individual lines. Exercise 10.7 is a theorem of the alternative and is not a consequence of weak duality alone. Uniqueness in Corollary 17.3 requires the positivity of the solution: the equations , admit sign-flipped solutions.
Vectors are Fin n → ℝ and Fin m → ℝ; is a Matrix (Fin m) (Fin n) ℝ. The book's primal–dual pair in , form with slacks is used throughout; there are no explicit constants in this chapter.
Conventions committed to:
Real.log returns at nonpositive arguments and is never evaluated there.Bornology.IsBounded of the feasible set in (resp. ).Infrastructure a complete development needs: attainment of maxima on compact sets (IsCompact.exists_isMaxOn in Mathlib), first-order conditions on relatively open sets, a theorem of the alternative for Exercise 10.7, and concavity facts about the logarithm. A second-order sufficient condition under affine constraints is not in Mathlib and is reusable beyond linear programming. Proofs of any milestone, including the "only if" half of the goal separately, are welcome contributions.
The r-algorithm of N. Z. Shor is a variable-metric method for minimizing functions that are not differentiable everywhere, such as maxima of smooth functions, penalty functions and Lagrangian dual functions of integer and decomposition problems. It combines a subgradient step with a space dilation along the difference of two successive almost-gradients, and the book reports it competitive with the best variable-metric and conjugate-gradient methods on "gully"-shaped test problems (Shor 1985, §3.6, pp. 68–77). Its convergence theory is limited. Section 3.7 of Shor's book gives a convergence proof only for an idealized version with exact directional minimization, on a class of piecewise smooth functions, and the book itself calls a weakening of the assumptions and rate estimates desirable (p. 85). This mission formalizes that section.
Timeline. Shor and Zhurbenko introduced the r-algorithm in 1971 (Kibernetika, no. 3, 51–59). Shor analysed the convergence of its exact-line-search version in 1975 (Kibernetika, no. 4, 48–53). Section 3.7 of the 1979 Russian monograph, translated in 1985, gives that analysis for piecewise smooth functions. The book states on p. 85 that weaker assumptions and rate estimates would be desirable.
Let be -dimensional Euclidean space with inner product , . For a unit vector and the operator of space dilation is .
Widths. For a compact convex set and a unit vector , the width in direction is . The width is and the diameter is . With put (or when ) and .
The class . is partitioned into closed sets , each the closure of its interior, whose interiors are disjoint and homeomorphic to an open ball or open halfspace; is continuously differentiable on an open set containing ; and on . At a point , the set of almost-gradients is the set of gradients of the pieces with . For , is the closed convex hull of all , , together with the -balls around the elements of .
The -algorithm. Fix , . Start from , and a nonsingular . At iteration choose with ; set , , , , , and with such that does not increase along the step and some almost-gradient at makes a non-acute angle with in the transformed metric. The standing assumption is as (3.50).
Assume (3.50) and (3.52). If is an isolated local minimum, the component of containing also contains , and no other point of that component has linearly dependent , then
Theorem 3.13 is the only convergence theorem the book gives for the r-algorithm. Theorems 3.11 and 3.12 hold for any function of the class , convex or not, and say that iterates of the exact version cannot stall at a point where the local almost-gradients are linearly independent: linear dependence of is a generalized stationarity condition that includes . Lemmas 3.2 and 3.3 are statements about widths of convex bodies under linear maps and single dilations, and apply to any analysis of space-dilation methods, including the ellipsoid method.
All four results and the goal are proved in the book, the goal as a corollary without a written proof. None of them is formalized. The formalization adds a machine-checked definition of the class and of the algorithm as a relation on sequences covering every admissible choice of almost-gradients and stepsizes, a verified proof of the book's argument, and a check of the corollary step, which the book leaves to the reader.
The obvious argument for descent methods is that the function value drops by a fixed amount at every step unless the gradient is small. That argument fails here. The r-algorithm can make null steps, with while and change, and its steps are measured in a metric that degenerates as the dilations accumulate (). A small step does not certify near-stationarity, and a large accumulated dilation does not certify progress.
The difficulty is to relate the geometry of the transformed almost-gradient sets to the decay forced on . This needs width estimates for convex bodies under linear maps and single dilations, which Mathlib does not have. Theorem 3.12 also needs a uniform lower bound, near a compact level set, on the Gram determinants of the piece gradients, and the book's proof of it is only sketched. Theorem 3.13 is stated as a corollary with no proof at all. Deriving it requires showing that the iterates cannot leave the prescribed component of , and that their accumulation points reduce to .
EuclideanSpace ℝ (Fin n) with ; operators are continuous linear maps; is the adjoint. and are valued in , so is represented exactly. Widths are sInf/sSup of support values, equal to the book's minima and maxima on nonempty compact sets.The question of the largest area that can be moved around a corner has been studied since the late 1960s. Leo Moser posed it in 1966, and F. H. Hammersley gave the lower bound and the upper bound in 1968. Joseph Gerver constructed a shape of area approximately in 1992 and described four constants , , , satisfying four equations, from which the shape is built. Dan Romik rewrote those equations in exact form as equations (1)-(4) in 2018 and reported high-precision values of the constants. Jineon Baek proved in 2024 that Gerver's shape is optimal: no larger shape can be moved around the corner. The proof was autoformalized in Lean 4 by Dean Cureton and AI agents in 2026, as the repository deancureton/MovingSofa, building on Dawid Trela's formalization of Gerver's constants and motion, Jonathan Ho's Brunn-Minkowski development, the Jordan-curve developments of R. Kirov and the TauCeti project, and Google DeepMind's formal-conjectures statement.
Timeline: Moser poses the problem (1966); Hammersley gives the lower bound and the upper bound (1968); Gerver exhibits the shape and its differential equations (1992); Romik gives the exact equations and numerics (2018); Baek proves optimality (2024, arXiv:2411.19826); Cureton et al. complete a Lean 4 proof of optimality, existence and uniqueness of the constants, and movability of Gerver's shape (2026).
Work in the plane . The hallway is , the union of its horizontal and vertical sides. A moving sofa is a nonempty closed connected set in the horizontal side together with a continuous path of plane isometries indexed by the unit interval, starting at the identity, keeping the image of inside the hallway at all times, and ending with the image inside the vertical side. Motions take values in the full isometry group ; continuity together with forces the path to lie in the orientation-preserving component. The sofa constant is the supremum, in the extended nonnegative reals, of the areas over all moving sofas. The supremum is finite, at least , and attained.
Gerver's shape is defined from a rotation path. For constants , , , , let be the piecewise function with breakpoints , , , from Romik's Theorem 2, let and be its cosine and sine integrals, and let be the associated translation path. The sofa for those constants is the intersection over angles in of the correspondingly rotated and translated hallways, with the endpoints using the horizontal and vertical sides. The four equations ABphiThetaSpec cut out the constants. They have exactly one solution with and , . The same Lean development uses the identical notation as the formal statements, so prose and code read as one document.
For every , , , satisfying ABphiThetaSpec,
The goal leaves unfixed which solution of the spec is used; by uniqueness all choices give the same shape up to the proved identification, so this is the stable form of Baek's Theorem 1.1. It asserts that the supremum equals the area of Gerver's shape, hence that no moving sofa has larger area and that the supremum is attained.
The first is Gerver's Theorem 2 in Romik's equation form on the closed domain. The second says every such shape admits a hallway motion. Together they supply the constants and the witness that the supremum is attained. The live mission records a root sketch composing the upper-bound half (every moving sofa is bounded by Gerver's area) with the movability witness into the supremum equality.
The result itself closes a problem open since 1966. It identifies the maximum area, shows the maximum is attained by an explicit shape, and determines that shape from four equations whose solution is unique. Consequences include the numerical enclosure proved by interval arithmetic, the finiteness of the supremum, and the reduction of future improvements to the analysis of the functional on caps. Without it the exact maximum remains unknown.
Formalizing it adds a machine-checked proof that makes no classical area assumption: the Green-type curve-area identity and the Minkowski-type mixed-area facts quoted by the paper are proved, the paper's 11 proof gaps and 33 misprints are repaired, and the numerical certificate is kernel-checked. The hallway, motion, cap, convex-body, and surface-measure infrastructure is reusable for related isoperimetric and kinematic formalizations. Status honesty: the underlying paper proof is complete and has been formalized in the source repository; on this platform the three statements above are open targets awaiting proofs, and the uniqueness of the maximizer up to rigid motion remains open and is not part of this mission.
The obvious argument bounds the area of an arbitrary sofa by the area of a circumscribed cap, but caps need not satisfy the injectivity condition that makes the functional an upper bound, and need not be concave on the full space of caps. Maximizing sequences of polygons need not converge to a sofa, and limits need not be connected or attain the supremum. The naive idea of taking a supremum over all connected closed sets and extracting a convergent subsequence fails until compactness of motions, closedness of the moving-sofa predicate, and a balanced maximum with rotation angle are established. Each step fails for general sets and only holds after the polygon approximation and monotonization constructions.
Lean represents the plane as EuclideanSpace ℝ (Fin 2) with its standard orientation, hallway sides as explicit sets, motions as I → E(2) where E(2) is ℝ² ≃ᵃⁱ[ℝ] ℝ² with the topology induced from continuous maps, and area as MeasureSpace.volume. The supremum is in ℝ≥0∞. Statements target the c5ea003 (Lean v4.30.0) environment, an older supported revision against which the development was verified locally. The spec uses non-strict inequalities, which makes uniqueness stronger than the strict-inequality literature form. The functions , , , take the constants as explicit arguments rather than reading global chosen constants, so the definition bundle stays independent of the existence proof; given uniqueness this implies the source statements. Boundedness and measurability are not assumed; every moving sofa is proved compact in the source development. A submission that drops closedness or connectedness, that allows a discontinuous motion, or that hard-codes the numerical value instead of proving equality with the volume of the defined shape, does not satisfy the statements. Contributions welcome: direct proofs of the three targets, sharper enclosures of the volume, and reusable hallway and motion lemmas. Out of scope: uniqueness up to congruence, the certificate details beyond the stated lower bound, and the 20 unformalized numbered environments listed in the source NOTES.md that none of the three targets depends on.
FormalConjectures/Wikipedia/MovingSofa.lean at ddfbaf90. https://github.com/google-deepmind/formal-conjecturesBrocard's problem asks for all natural numbers such that is a perfect square. Henri Brocard raised the question in 1876 and again in 1885, and Srinivasa Ramanujan independently posed it in 1913 in the Journal of the Indian Mathematical Society. Only three solutions are known, and the problem is listed as Erdős problem #398 (erdosproblems.com/398). It is one of the simplest-looking Diophantine equations mixing a multiplicative object (the factorial) with an additive shift, and it is a standard test case for conjectures such as the abc conjecture.
No unconditional proof of finiteness is known.
For a natural number , the factorial is , with . A Brown number pair is a pair of natural numbers with
The three known pairs are , and , since , and .
For the conditional milestone, the radical of a natural number is the product of the distinct primes dividing . The abc conjecture asserts: for every there is such that for all positive integers with and ,
This says both that the three known pairs are solutions and that there are no others.
A resolution would settle a question open since 1876 and would be one of the rare complete solutions of a factorial Diophantine equation of this kind. The conditional finiteness result is a standard illustration of how the abc conjecture controls equations of the form .
For the formalization, the known-solutions milestone is a finite computation. The search-bound milestone is a large verified computation; a machine-checked certificate for it would be a reusable artifact. The conditional finiteness milestone formalizes a published argument that assumes the abc conjecture as a hypothesis. The goal itself is an open problem; none of these statements is known to have a machine-checked proof on this platform at the time of drafting.
Congruence obstructions cannot rule out large solutions: for every modulus and every one has , so is a square modulo . Local arguments alone therefore cannot close the problem. The known finiteness argument depends on the abc conjecture, which is itself unproved in the standard form used here. Computer searches only give lower bounds on any further solution.
ℕ); ranges over , so the sign of is not an issue. The factorial is Mathlib's Nat.factorial, with .Prop-valued definition used as a hypothesis in the conditional milestone; it is not asserted anywhere. The exponent is a real power.Brocard.A QMA verifier receives a quantum witness and checks it with a circuit generated efficiently from the input. An acceptance probability separated by an inverse-polynomial gap is enough to define the class, but applications often need the probability of a wrong answer to be exponentially small. Repeating the verifier on many supplied witness registers achieves this error reduction while allowing the witness to grow. Marriott and Watrous proved the stronger statement that the same error reduction can be obtained without increasing the number of witness qubits Quantum Arthur–Merlin Games, Section 3.
The existing Lean development verifies the copy-based theorem, including soundness for witnesses entangled across the copies, and constructs a uniform circuit family with polynomial resources. This mission asks for the separate witness-preserving theorem. The paper already proves that mathematical statement; the open work here is its formalization in the stated QMA circuit model.
At each input length , a verifier has witness qubits, a finite work register, a designated output wire, and a quantum circuit. A uniformly generated family has a polynomial-time classical procedure that emits the complete circuit description, including the witness and work-register sizes. On yes-instances, some normalized witness makes the verifier accept with probability at least . On no-instances, every normalized witness is accepted with probability at most . The thresholds satisfy and for a polynomial .
The existing formalization represents witnesses as complex amplitude functions on bit strings, requires normalization explicitly, and uses layered circuits over its specified finite gate set. It also represents efficiently available real thresholds by polynomial-time procedures that output dyadic approximations. These are part of the formal statement's interface and must be made visible to users of the mission.
For every polynomial error exponent and every source verifier satisfying the conditions above, construct a uniformly generated, well-formed, polynomial-resource verifier for the same language, with completeness at least and soundness at most , while keeping the witness count exactly at every input length:
This is the witness-preserving strong error-reduction result of Marriott and Watrous (Theorem 4). The existing copy-based result corresponds to the weaker QMA class inclusion in Theorem 3 and will be linked as a proved background result. The mission goal must state the witness-count equation explicitly so that a copy-based amplifier cannot satisfy it.
Witness-preserving amplification lets a QMA protocol demand much stronger reliability without asking the prover for a longer message. That matters whenever witness size is itself a resource being compared or bounded. The copy-based theorem shows that the QMA class is robust under error reduction, but does not establish this fixed-message guarantee.
Formalizing the stronger result would add a reusable account of a verifier that reuses one witness, proves soundness for every normalized input state, and compiles its behavior into an ordinary uniform circuit family. Those components can support later formalizations that reason about repeated quantum verification under a fixed witness budget.
The completed copy-based proof uses three independent verifier blocks in each amplification round and bounds arbitrary entangled witnesses across those blocks. Its circuit resource analysis therefore allows the witness count to grow. A witness-preserving argument cannot use that construction. It must analyze repeated verification on one register and establish exponentially small error without assuming the input witness has a special spectral form. The formal circuit model currently exposes final-output measurements; any additional measurement behavior used in the analysis must be justified in that model and shown implementable by a finite, uniformly generated circuit.
The central audit point is the exact witness-length equation. A theorem that merely returns another polynomial-size witness, or that changes the source verifier's witness definition, is a useful class-level result but does not prove this mission's target.
The goal is parameterized by input-length-dependent completeness and soundness thresholds with an inverse-polynomial gap, and by a polynomial target exponent. Every witness quantifier is over normalized states. The output verifier must satisfy the same well-formedness and polynomial-resource conditions as the completed copy-based development. The platform statement uses its existing ShiClassQMAU.UniformQMA circuit-family encoding, which includes the witness and ancilla counts separately. A final proof should be kernel checked with only Lean's standard logical axioms and should not assume an amplification transducer or an unproved measurement lemma.
The paper quantifies over the class poly of unary-time constructible functions. This proposal represents the gap denominator and target exponent as literal Polynomial ℕ values, matching the checked copy-based development. It therefore formalizes a polynomial-parameter instance of Theorem 4 rather than the paper's full function-class generality. The threshold functions are supplied by polynomial-time dyadic approximators in place of the paper's informal efficient-computation convention. These interface choices are explicit in the Lean goal and should not be read as a proof of the broader formulation.
The local copy-based proof is complete and audited, but it has not yet been transplanted to Prove2Me. Its publication is preparatory work for this mission, not evidence that the witness-preserving goal is already solved. The proposal should reference the published copy-based endpoint and include only a few substantial milestones, so each item is meaningful to audit.
For let denote the -th prime. Brocard's conjecture, named after Henri Brocard, asserts that for every there are at least four primes strictly between and (Wikipedia). It belongs to the family of "primes between consecutive squares" problems together with Legendre's conjecture, and it is a concrete, elementary-looking question about short-interval prime distribution that remains open.
Primes are listed in increasing order. In the Lean development the list is 0-indexed: Nat.nth Nat.Prime k is the -th prime counting from , so nth 0 = 2, nth 1 = 3, nth 2 = 5, and so on. For an index write n.nth Nat.Prime and (n+1).nth Nat.Prime, two consecutive primes. The quantity of interest is
Milestone (Ferreira): for all sufficiently large indices ,
Goal (Brocard's conjecture): the same inequality for every 0-indexed , i.e. for every pair of consecutive primes starting from .
A proof of the goal settles Brocard's conjecture outright. Given Ferreira's asymptotic result, the remaining work splits into making the threshold effective and closing the finite range below it, both of which would be new formal content; the milestone itself (formalizing Ferreira's analytic argument) is a substantial analytic-number-theory formalization project.
Unconditional results on primes in short intervals only reach exponents well above , while the interval has length about where can be small (e.g. twin primes), i.e. length on the order of the square root of its endpoint. Standard short-interval theorems therefore do not apply uniformly, and Legendre's conjecture — which would only give two primes here — is itself open.
Everything is stated with Mathlib's Nat.nth Nat.Prime, Finset.Ioo (open interval, endpoints excluded) and Finset.filter Nat.Prime, followed by Finset.card. The hypothesis 1 ≤ n in the goal is the 0-indexed form of the source's ""; it is necessary, since for index (primes ) the interval contains only the two primes . The milestone uses Filter.atTop ("for all sufficiently large "), with no explicit threshold. No custom definitions are required.
BrocardConjecture.lean.A central configuration of the Newtonian -body problem is a placement of point masses in which the gravitational acceleration of every body points toward the centre of mass and is proportional to its distance from it. Central configurations generate the only explicitly known solutions of the -body problem (the homographic, or self-similar, motions), they are the possible limiting shapes of total collisions, and they organise the topology of the integral manifolds. Counting them is therefore a basic question of celestial mechanics.
Timeline.
Fix bodies with masses ; body sits at . Write , and . A configuration with all is a central configuration (normalised so that the proportionality constant is ) when, for every ,
These equations are invariant under rotations of the plane; imposing removes this freedom, and a solution with this normalisation is a positive normalized central configuration (Definition 1 of the paper; Lean: PosNormalizedCC n m).
The proof works in the complex domain. Introducing unknowns (inverse distances) with turns the equations into the polynomial system (4) on :
A complex solution is a normalized central configuration (Lean: NormalizedCC n m), a real one if all are real (Lean: RealNormalizedCC n m). The potential is (Lean: potential n m).
There is a closed algebraic subset of codimension at least such that for all masses ,
The exceptional set is not made explicit; only its existence and dimension bound are asserted.
The same statement with all complex solutions of system (4) in place of the positive real ones.
For and every positive masses: finitely many positive (Theorem 1, Hampton–Moeckel) and even real (Theorem 5) normalized central configurations; finitely many complex ones unless the masses satisfy explicit polynomial relations (Theorem 3) or are all equal (Theorem 4).
Lemma 1 (a polynomial image of an affine variety is finite or cofinite), Lemma 2 (the potential takes finitely many values on the solution set), and the explicit mass vector .
The result. Theorem 2 is the first finiteness result for planar central configurations of five bodies, settling Smale's 6th problem for for generic masses; before it, no single 5-tuple of positive masses was known to have finitely many planar central configurations. Its four-body part gives a short proof of the Hampton–Moeckel theorem, including the real (not necessarily positive) solutions.
Formalizing it. The results are proved on paper; none of them is formalized. A formal development requires affine elimination theory (Chevalley's theorem on constructible images in the form of Lemma 1), a Sard-type argument on algebraic sets (Lemma 2), and the singular-sequence analysis of Sections 3–9, which is a long case analysis of limiting diagrams together with polynomial eliminations done by computer algebra in the paper.
Finiteness is not a local statement: nondegeneracy fails in general (Palmore), so no implicit-function argument applies, and a continuum of solutions would have to be excluded globally. In the complex domain continua genuinely exist for some masses (Roberts' continuum with a negative mass; its sign-modified version with positive masses solves system (4)), so any proof must use the positivity of the masses in an essential way, and the exceptional mass set of Theorem 2 cannot simply be dropped with the present method.
Fin n; the paper's bodies and are the indices 0 and 1, so the normalisation reads y 1 - y 0 = 0.NormalizedCC they are complex, as in Section 2 of the paper. Lemma 2 carries the paper's standing hypothesis that no nonempty subset of bodies has total mass zero (NoZeroSubMass).(x, y, δ); δ is a full n × n array constrained to be symmetric with zero diagonal, so it carries exactly the unknowns , . Finiteness of the solution set is unaffected by this encoding.massZeroLocus I of an ideal I of with ringKrullDim (ℝ[m] ⧸ I) ≤ 3. Taking is impossible (the quotient has dimension ), so the goal is not trivialised by an exceptional set equal to the whole mass space.Set.Finite of the solution set.Useful reusable infrastructure: finite-or-cofinite images of polynomial maps on affine varieties, and basic facts on central configurations (centre of mass, the identity ).
Two closed subgroups and of a profinite group are locally conjugate if, for every prime , a Sylow -subgroup of is conjugate in to a Sylow -subgroup of . Conjugate subgroups are always locally conjugate. The converse, which lets conjugacy be tested one prime at a time, fails in general. Deciding when it holds is a classical question about supplements of nilpotent normal subgroups.
A profinite group is a compact Hausdorff totally disconnected topological group. Equivalently, it can be described through compatible finite quotient groups. A pronilpotent group has nilpotent finite continuous quotients. A prosupersolvable group has supersolvable finite continuous quotients; a finite group is supersolvable when it admits a normal series with cyclic factors. These properties concern all finite continuous quotients, with no uniform bound on their orders or nilpotency classes.
A subgroup supplements a normal subgroup when . It complements when, in addition, . Two closed subgroups are locally conjugate when, for each prime , a Sylow -subgroup of one is conjugate in to a Sylow -subgroup of the other. For profinite groups, Sylow subgroups are maximal closed pro- subgroups. The conjugating element may depend on the prime. All subgroup notation in the paper carries closedness, as stipulated in §1.2.
The cohomological statements concern a profinite group acting continuously by automorphisms on a discrete group . With a left action, a continuous cocycle satisfies . Two cocycles are equivalent when for one fixed . Their quotient is the pointed set , whose distinguished point is the identity cocycle. Stable classes on a subgroup compare a cocycle with its conjugates after restriction to the relevant intersections. This matters when the subgroup itself is not normal. The definitions follow §§1–1.2.
The central conjugacy assertion is Theorem 1.1. For a closed normal pronilpotent subgroup of a profinite group , assume that is prosupersolvable or is pronilpotent. Then closed supplements of satisfy
Lemma 1.2 asserts, for finite nilpotent coefficients and its stated structural alternatives, a pointed bijection induced by simultaneous restriction:
The other numbered targets are Corollaries 1.3–1.4 and Propositions 2.1–2.3, 3.1–3.2, and 4.1–4.2. They retain the paper's distinctions between finite coefficients, locally finite discrete coefficients, and arbitrary closed pronilpotent subgroups. They also retain the normal-intersection condition in the semidirect-product inclusion and fixed-point results. The abelian conclusions impose no solvability assumption on the ambient profinite group.
Both counterexamples in §1 are targets. The quaternion example realizes in , has exactly two global cohomology classes and trivial Sylow cohomology, and exhibits locally conjugate complements that are not conjugate. The Heisenberg example uses of order , with the Heisenberg group of order , , and . Local containment holds while containment of a conjugate of fails.
The combined goal asserts all eleven numbered results and both counterexamples. Each assertion remains a separate milestone with the source's numbering or, for the unnumbered counterexamples, its section and page.
The conjugacy and containment theorems make precise when separate prime-wise witnesses can be replaced by one global witness. The fixed-point results similarly turn prime-wise fixed points, which can be different points, into a point fixed by the full subgroup. The counterexamples record the limits of these conclusions under weakened hypotheses. These are proved mathematical results of the preprint, rather than new conjectures.
A completed development would also provide reusable formal interfaces for continuous nonabelian first cohomology, stable classes, profinite Sylow and Hall conditions, and local subgroup relations. An earlier local Lean development supplies definitions and substantial proof material. The present draft statements are aligned to the arXiv version; their target proofs remain open in this proposal. Reusing earlier proofs requires checking their types against these interfaces and the pinned environment.
Local conjugators can vary with the prime, and there need not be one conjugator that works for all primes simultaneously. The quaternion example demonstrates this obstruction even in finite groups. Nonabelian cohomology is a pointed set, so the usual additive primary-decomposition language does not itself provide the needed assertion. The transition from finite groups to profinite groups also requires tracking topology, closedness, and continuity. The counterexamples and the finite-versus-profinite distinctions are part of the mathematical scope, not optional simplifications. See §§1–3.
All declarations use the namespace LocalConjugacy. Profinite ambient groups use Mathlib's ProfiniteGrp; subgroups, quotient groups, normality, complements, actions, fixed points, finite Sylow subgroups, nilpotence, and solvability use Mathlib structures or predicates. Custom definitions cover the continuous nonabelian quotient and the profinite local conditions absent from the pinned library interface. Conjugation is written on the left. This changes the notation for the conjugating element, not the conjugacy or inclusion assertion.
The fixed-point targets quantify over nonempty sets with no added topology and require closed stabilizers. Propositions 2.1–2.2 allow infinite locally finite discrete coefficients. Theorem 1.1 allows arbitrary closed pronilpotent . Finite special cases cannot replace these targets. Both counterexamples include explicit isomorphisms to the concrete groups named in the paper. Contributions may reuse the existing proof development, improve the reusable interfaces, or prove the targets directly while preserving these statements.
A scenario program replaces an uncertain optimization problem by its worst case over finitely many sampled instances. In its simplest form it reads
where is the cost of a decision when the uncertain parameter takes the value , and are independent draws from an unknown probability . The classical guarantee of the scenario approach (Campi and Garatti, 2008) bounds the probability that a new instance produces a cost above the optimal value , and it does so without any knowledge of .
That guarantee concerns a single number, . Two scenario programs with the same and the same optimal value can look very different at the solution: in one, most sampled costs lie just below ; in the other, they are widely scattered. The costs that do not determine the solution still carry information about how the cost of the chosen decision is distributed on future instances. Carè, Garatti and Campi (2015) showed that this information can be extracted with the same distribution-free character as the classical result, which is the subject of this mission. It is Chapter 8, §8.1 ("Probability box") of Campi and Garatti, Introduction to the Scenario Approach (SIAM/MOS 2018), the third mission of the series formalizing that book.
Timeline:
Let be a measurable space with a probability , and a cost that is convex in for every (a standing assumption of the book). For a sample of independent draws from , let be the solution of the program above and its optimal value.
Empirical costs (Definition 8.1). Sort the costs of the solution on the sampled scenarios in decreasing order, ; so .
Risk (Definition 8.2). For a decision and a level , . The risk of the -th empirical cost is , and .
Nondegeneracy (Definition 8.3). For every , with probability , . Costs with index below are excluded because several scenarios typically attain the maximum at .
Support constraints and full support (Definitions 5.1 and 5.4). In epigraph form, subject to , the constraint of scenario is a support constraint if removing it lowers the optimal value; the problem is fully supported if for every the program with scenarios has exactly support constraints with probability .
The ordered Dirichlet distribution with parameters is the law on with density .
Under nondegeneracy, for and all ,
This is an identity of joint distribution functions, not a bound, and it does not depend on or .
The result. The theorem controls the whole distribution function of the cost of the scenario solution on a new instance, not just one quantile of it. Discarding the extreme tails of the laws of yields, with a prescribed confidence , a region (the book's "probability box", Figure 8.2) that contains the entire cumulative distribution function of , computed from the sample alone. The first marginal recovers the classical Theorem 3.7, since makes the risk of at most .
Formalizing it. The theorem is proved in Carè, Garatti and Campi (2015); the book states it and gives no proof. No machine-checked version of the scenario approach, of its generalization theorem, or of ordered Dirichlet laws of risks is known to exist. A formalization would produce a checked proof of the distribution-free identity together with the combinatorial and measure-theoretic infrastructure (order statistics of sampled costs, laws of random risks) that the rest of scenario theory reuses. The milestones separate the classical beta bound, which is also the goal of the first mission of this series, from the new exact joint law.
The obvious attempt treats as the order statistics of the uniform variables . That works only for , when the decision space is a point and the costs are independent. For the decision is itself a function of the whole sample, so the sampled costs at are neither independent nor identically distributed, and the -th cost is tied to the scenarios that determine the solution. The factor and the constant encode exactly this dependence. Any argument must account for which scenarios are active at without assuming full support, since the theorem holds whether or not .
The decision space is EuclideanSpace ℝ (Fin n) and the book's is ; the sample is ω : Fin N → Δ with law Measure.pi (fun _ => P). Empirical costs are read from Tuple.sort with counted from ; risks are real numbers (P {δ | c < ℓ ν δ}).toReal. The right-hand side of the goal is a Lebesgue integral over the box intersected with the ordered simplex, stated for all real . The solution map is a hypothesis-constrained function, never an arbitrary map.
Implicit hypotheses of the book pinned down in the binders:
A statement in which the solution is an arbitrary measurable map, or in which the nondegeneracy or existence hypothesis is unsatisfiable, would make the goal vacuous; the hypotheses here are met, for example, by with a continuous law on , and for by any cost independent of with an atomless law.
A complete development needs: the scenario approach generalization theorem (reusable across this series), laws of order statistics of i.i.d. uniform variables, and the combinatorics of support sets of convex min-max programs. Proofs of the milestones, of the case of the goal, and of auxiliary facts about kthLargest are all welcome.
Quantum mechanics predicts probabilities, but it is notoriously quiet about what a probability is. Categorical quantum mechanics answers that by rewriting the finite-dimensional formalism in the language of dagger categories: a state is a morphism , an effect is a morphism , and the probability of an outcome is a scalar — an endomorphism of the tensor unit. On that translation the Born rule stops being an axiom and becomes a theorem about a complete, disjoint family of effects.
This mission formalizes that theorem, together with the two lemmas it rests on, in Lean 4 over Mathlib. It covers the dagger and measurement material of Chapter 2 of Reutter and Vicary's Categorical Quantum Mechanics.
Fix a monoidal dagger category with zero morphisms. The unit object carries a commutative monoid structure — the scalars. For a state and an effect , the probability that occurs on is the scalar
A family of effects is complete when the induced map satisfies , and disjoint when for . Both conditions are stated for a dagger biproduct of the unit objects.
This is the mission's goal. It fixes nothing beyond completeness and disjointness; the statement is exactly the categorical Born rule for a finite outcome set.
The Born rule is the point where the categorical and the Hilbert-space pictures are reconciled: the abstract statement specialises, in , to the usual . Proving it categorically means the rule is a consequence of the dagger-biproduct structure rather than an extra assumption, which is what makes the framework usable for quantum protocols — measurement, teleportation and the like are all built on complete disjoint families.
The supporting lemmas are reusable well beyond this mission: dagger biproducts are the categorical home of matrix calculus, and the isometry/unitary characterisations of disjointness and completeness are the standard toolkit for any later argument about measurements.
Moderate. The mathematics is elementary once the definitions are in place — the work is in bookkeeping: biproduct universal properties, the interaction of the dagger with the biproduct structure, and careful handling of the scalar monoid. The main intellectual step is realising that completeness alone, not equalizers, gives the second unitary identity.
Formalized here: dagger categories and their morphism classes (§2.3), dagger biproducts
(§2.3.3), and the scalar/state/effect vocabulary with the Born rule (§2.4.3). Mathlib has
no dagger-category theory at all, so the definitions are supplied from scratch as Lean
Definitions and are importable independently of this mission.
Not formalized: the Hilbert-space and relational models, the graphical calculus of §2.2, and the measurement/post-processing material after §2.4.3.
Two corrections to the source are made and documented in the formalization. The printed statement of Proposition 2.55 assumes completeness only, which is false; disjointness is required, as the book's own proof (which invokes Lemma 2.52) already assumes. And the book attributes the identity on to Lemma 2.52, whereas Lemma 2.52 only gives the identity on ; the identity on is Lemma 2.53. Lemma 2.53 is proved here without the book's equalizer hypothesis, so it is strictly stronger than the printed version.
CategoryTheory.Limits.Biproducts and CategoryTheory.Monoidal.Category
API, on which the definitions are built.Stochastic differential equations whose coefficients grow faster than linearly (for instance stochastic volatility models such as the 3/2-model) cannot be simulated with the classical explicit Euler–Maruyama scheme: Hutzenthaler, Jentzen and Kloeden showed that its moments diverge when the drift or diffusion grows superlinearly (Proc. R. Soc. A, 2011). Implicit schemes avoid the divergence but require solving a nonlinear equation at every step. Tamed Euler schemes keep the scheme explicit and damp the coefficients by a factor depending on the step size.
Theorem 3 is the target here; Theorems 1 and 2 are the targets of companion missions.
Fix a filtered probability space satisfying the usual conditions, a -dimensional Wiener martingale , a horizon , and exponents . For , is the Euclidean norm; for a matrix , is the Hilbert–Schmidt norm; is the scalar product. The coefficients are Borel functions and , and the SDE is
with an -measurable initial value . With , the scheme (2.2) is
and in this mission are the tamed coefficients of Model 2 with :
The conditions used are: A-2, local boundedness of on balls; A-4, the coercivity bound ; A-5, ; and A-6, the global monotonicity
together with the polynomial Lipschitz bound , with . The -condition asks and a moment exponent with and .
Under A-2, A-4–A-6 and the -condition, for every there is independent of with
The supremum is inside the expectation, which distinguishes it from Theorem 2.
Theorem 3 gives the optimal strong rate 1/2 for an explicit scheme, uniformly over the time interval, for SDEs whose diffusion coefficient may grow superlinearly. Uniform-in-time error bounds are what pathwise functionals need (running maxima, barrier options, hitting times), and via Borel–Cantelli they give the almost-sure rate of Corollary 1 in the paper. Lemma 5 is a general-purpose tool: a domination inequality of Lenglart type, used throughout stochastic analysis to pass from bounds at stopping times to bounds on running suprema.
The results are proved in the paper; to our knowledge none of them has been formalized. Formalizing them would produce the first machine-checked convergence rate of a numerical scheme for SDEs, and a Lean proof of a Lenglart-type inequality, which Mathlib does not currently contain.
The error is controlled by the monotonicity condition A-6, which is one-sided: it bounds from above but gives no Lipschitz bound on or with a constant independent of . The first idea, estimating directly by applying the Burkholder–Davis–Gundy inequality to the martingale part of the error equation, therefore does not close: it produces terms of the same order as the quantity being estimated, weighted by polynomial factors in and , and the argument that gives Theorem 2 controls only for fixed . Passing from fixed times to the supremum is what forces the loss from to in Theorem 3, and it is where Lemma 5 enters. On the formal side, the Itô integral against Brownian motion, Itô's formula for functions of multidimensional Itô processes and the Burkholder–Davis–Gundy inequality are not in Mathlib.
Processes are indexed by (ℝ≥0) with values in EuclideanSpace ℝ (Fin d); diffusion values live in EuclideanSpace ℝ (Fin d × Fin d₁), whose norm is the Hilbert–Schmidt norm. The stochastic integral is the Ethier–Kurtz platform relation EthierKurtz.HasBrownianItoIntegral, applied coordinatewise, with integrands cut off after . Solutions are hypotheses: the theorems apply to any solution of (2.1) and any family of solutions of (2.2) on one probability space with one and one ; existence is not claimed. Processes are required to be adapted to the filtration augmented by null sets (weaker than a complete filtration), the filtration is right-continuous, and nothing is required after . Expectations and suprema are computed in , so no statement holds through an integral defaulting to . Constants depend on everything except (and, in Theorem 3, may depend on ); only is used, and , follow the paper's convention.
Two hypotheses are added to the printed statements, both because the printed proofs need them:
Lemma 2 drops the dependence clause and asserts only finiteness. Lemma 5 assumes neither that is nondecreasing nor anything beyond the printed hypotheses.
A trivializing formalization is ruled out: the supremum sits inside a Lebesgue integral in , so the goal cannot hold because of a junk value, and the hypotheses are satisfiable (zero coefficients, constant solutions), which a sorry-free check confirms.
Needed infrastructure: Itô's formula for multidimensional Itô processes, the Burkholder–Davis–Gundy inequality (for Lemma 4), Gronwall's inequality in integral form, and stopping-time localisation for continuous adapted processes. Contributions to any of these are welcome, and all are reusable far beyond this mission. Lemma 5 is independent of the SDE part and can be attacked first.
Stochastic differential equations with superlinearly growing coefficients appear throughout applied probability: population models with cubic damping, Langevin dynamics with polynomial potentials, and stochastic volatility models such as the 3/2-model used for pricing VIX options, whose diffusion coefficient grows like . For such equations the classical explicit Euler–Maruyama method fails: Hutzenthaler, Jentzen and Kloeden (2011) proved that its -th moments diverge whenever a coefficient grows superlinearly, so it cannot converge in . Implicit methods converge (Higham–Mao–Stuart 2002) but cost a nonlinear solve per step.
The tamed Euler schemes are the explicit response.
This mission is the second of three on the paper. Mission I formalizes -convergence without a rate (Theorem 1), mission III the uniform-in-time rate (Theorem 3).
Fix a filtered probability space with right-continuous filtration, a horizon , dimensions , and a -dimensional Wiener martingale : a standard Brownian motion adapted to whose future increments are independent of . The coefficients are Borel maps and ; is the Euclidean norm, the Hilbert–Schmidt norm, the scalar product. The SDE is
with an -measurable initial value . For let and consider the scheme
whose coefficients are frozen at the last grid point, so that is computable step by step. The tamed coefficients of Model 2 are
The hypotheses, with constants :
Under A-2, A-4–A-6, the -condition and , there is a constant independent of with
The constant is existential and may depend on all data except .
Theorem 2 shows that an explicit scheme costing one coefficient evaluation per step attains the same strong order as the classical Euler method under global Lipschitz conditions. It does so for drift and diffusion coefficients that grow polynomially, and for moment orders that are small relative to and . Strong rates are what multilevel Monte Carlo needs: the variance of level corrections is controlled by the rate. When could be taken to be the statement specializes to the classical globally Lipschitz rate (Remark 6).
The result is proved on paper; it has no machine-checked proof. Stochastic integrals are not in Mathlib; this mission uses the Brownian Itô-integral relation published by the Ethier–Kurtz series on the platform. A formal proof would give the first verified strong convergence rate for any Euler-type scheme. Along the way it produces reusable moment bounds for tamed schemes and the control of one-step increments.
The obvious argument applies Itô's formula to and closes a Gronwall inequality. Two steps of it fail without taming. First, the error splits into the monotone part, handled by A-6, and cross terms such as multiplied by ; they are controlled only through moments of of order well above that are uniform in , which the untamed scheme lacks. Second, the taming itself introduces an error that must be shown to be in and not merely . The exponents in the -condition are exactly what the Hölder splittings of these two terms require.
EthierKurtz_HasBrownianItoIntegral, with the integrand cut off after .Feedback laws that damp vibrations in elastic structures are implemented by sensors and actuators, and a physical loop always reacts with some time delay : the damping force at time is computed from the velocity measured at time . Datko, Lagnese and Polis showed in 1986 that an arbitrarily small delay in a boundary feedback can destroy the stability of a one-dimensional wave equation (Datko–Lagnese–Polis, SIAM J. Control Optim. 24 (1986)), and Datko showed that such fragility is common to a broad class of feedback-stabilized hyperbolic systems (Datko, SIAM J. Control Optim. 26 (1988)). Delay-robustness is therefore a genuine question for every stabilizing feedback, not a technicality.
Nicaise and Pignotti (SIAM J. Control Optim. 45 (2006) 1561–1585) identified a simple sufficient condition in several space dimensions: if the feedback contains an undelayed velocity term with gain and a delayed one with gain , and , the energy still decays exponentially; if , instabilities appear for some delays. This mission formalizes the stability half for internal (distributed) damping, localized near the Neumann part of the boundary.
Timeline.
Let , , be a bounded open set with boundary of class , split as with and . Write for the outer unit normal, for the surface measure, for time derivatives and for the Laplacian in .
Geometric hypothesis (1.6)–(1.7): there are a function and with for all , , and on .
Damping coefficient. is an open neighbourhood of (in ), and satisfies
The system (1.12)–(1.16): for gains and delay ,
with on , on , initial data , , and history for .
The energy. Assume (1.8) and fix with (1.10). Then
The first summand is the standard energy ; the second accounts for the velocity history on the delay window.
There exist , depending on the data but not on the solution, such that every solution satisfies
The constants are left existential, as in the paper, so no later sharpening of rates invalidates the goal.
The result. Theorem 1.3 shows that a localized viscous damping acting only near the Neumann boundary keeps its exponential stabilizing effect when part of the feedback is delayed, provided the delayed gain is dominated by the undelayed one. Together with Theorem 1.4 of the same paper (instability for and suitable delays) it gives a sharp threshold in terms of the gains. The energy with its history term became the standard Lyapunov functional for delayed wave and plate equations in the literature that followed.
Formalizing it. The theorem is proved in the paper; no machine-checked proof of it, or of any exponential decay result for a multidimensional wave equation, is known to exist. A complete development would produce reusable Lean infrastructure: energy identities for the wave equation on domains via the divergence theorem, the delay-energy calculus, and an observability inequality for the wave equation with mixed boundary conditions. Each milestone has value on its own; Proposition 4.2 in particular is a classical control-theoretic result.
The energy estimates (milestones 1 and 2) are calculus once the divergence theorem is available. The central difficulty is observability. Energy dissipation alone gives only nonincreasing; exponential decay needs the energy at time to be controlled by the energy dissipated on (Proposition 4.3), and that needs the conservative wave equation to be observable from (Proposition 4.2). The observability inequality does not follow from energy identities: the paper relies on Carleman estimates of Lasiecka–Triggiani–Yao (1999) and a compactness–uniqueness argument, neither of which is available in Mathlib. The obvious attempt, a multiplier identity with alone, leaves boundary terms on that cannot be absorbed without a localization near and a lower-order compactness step.
EuclideanSpace ℝ (Fin n) with 1 ≤ n; solutions are real valued.Needed infrastructure: the divergence theorem on domains (assumed here as a structure field), differentiation under the integral sign for the energies, Carleman estimates or another route to observability for the mixed wave problem, and a compactness argument (Rellich). Contributions of any of these as standalone lemmas are welcome.
The 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. The question is how large a comparison constant is needed to make this inequality hold.
This mission establishes the best possible constant for complex diagonal matrices for every real . The result is proved in Lean. For each exponent, one constant works for every triple of diagonal matrices of the same size, across all finite sizes.
The constant comes from a simple family of three diagonal matrices, called the cyclic family. Varying one parameter determines the largest comparison constant these examples require. The theorem proves that this value also works for every other triple of diagonal matrices, however large. The goal theorem gives the exact formula and statement.
This is the foundation of the sharp diagonal Hlawka campaign. It supplies the shared definitions and supporting results for lowering the exponent cutoff while keeping the same formula. A later mission has now established the result in Lean for every real ; the campaign invites further improvements.
The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.
79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source library