Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Data brokers such as Acxiom, Nielsen and Oracle, and data generators such as Google and Facebook, sell processed consumer data to firms that use it to decide whom to target, whom to lend to, or which market to enter. The U.S. Federal Trade Commission's 2014 report on data brokers distinguishes two products: a marketing list, which carries contact information without which the buyer cannot act at all, and a data append, which enriches data the buyer already holds. Liang Guo's Selling Data to Marketers (Management Science, doi:10.1287/mnsc.2023.01350) asks how a seller should design a menu of data products of different informativeness when buyers differ in a privately known cost of acting.
The question belongs to the theory of optimal screening (Mussa and Rosen 1978; Maskin and Riley 1984), but with a twist: the buyer's marginal value of information is not a primitive. It is derived from the buyer's decision problem, so the direction of the single-crossing condition is itself an outcome of the model. This mission formalizes the paper's analysis of marketing lists in the base model with a binary value.
A marketer can take an action (target a consumer) at cost . The action's value is with prior probability and otherwise. The seller can provide a binary signal with , where the informativeness lies in an interval . The probability of the optimistic signal is , the posterior probability of after it is , and the posterior mean is ; are defined symmetrically. The paper assumes , so a marketer acts exactly after , and a marketer with cost who pays for a signal of informativeness gets
Serving a marketer at informativeness costs the seller , with and increasing.
There are two cost types, , with ; write , . Under the benchmark with observable cost, the seller extracts all surplus and chooses to maximize
whose maximizers are the efficient levels . With private costs the seller offers a menu with and maximizes subject to individual rationality and incentive compatibility , where . This is problem (6); its solutions are the optimal menus, with informativeness levels .
Under the regularity of described below,
The first claim is an equality of sets of maximizers; the inequalities compare every optimal menu with every efficient level.
obtained by making IR and IC bind. 5. The derivative of (7) in : .
In textbook screening the low type's allocation is distorted downward to reduce the high type's rent. Here the low type of the screening problem is the high-cost marketer, and its information can be distorted in either direction: the rent conceded to low-cost marketers falls with when and rises when . Proposition 2 therefore says that a seller of marketing lists may supply socially excessive information to some buyers, a possibility absent from the data-appends literature the paper compares against, where provision can only be insufficient. Proposition 1 isolates the mechanism: the prior decides whether information mainly prevents wasteful targeting or restores profitable targeting, and the cost of acting amplifies one or the other.
The result is proved in the paper; nothing in it has been machine-checked. The mission produces a checked version of the two-type screening reduction (including the verification that the constraints dropped in (7) hold at its solutions, which the paper asserts as standard) and of the comparative statics with set-valued optima, since is not assumed convex and optima need not be unique.
The derivative computations are routine once is simplified to . The work lies elsewhere. First, the reduction: "IR binds for the high-cost type and IC binds for the low-cost type" is the standard heuristic, but at a solution of (7) one still has to check the dropped constraint IC and the nonnegativity ; both depend on the ordering of and at the optimum, which in turn depends on the sign of . Second, strictness: comparative statics through increasing differences give only weak inequalities between maximizer sets. Upgrading to requires ruling out a common maximizer, which needs the optimum to be interior and differentiable there; the naive argument by first-order conditions fails at the corners . Third, as sets requires existence of optimal menus, hence attainment of the maximum of (7).
Everything is over . The model is a structure Model (values, prior, informativeness interval, selling cost) extended by Screening (type probability and the two costs); the standing assumptions , , , , increasing on (weakly), , , and for both types are fields. The posteriors are defined with the divisions printed in (2). Efficient levels and optimal menus are sets of maximizers, never chosen by Classical.choose or a first-order condition. Menus include .
The goal additionally assumes the part of footnote 5 (p. 7) that makes optima interior: continuous on , differentiable on , with right derivative and as . Convexity and twice differentiability, also in the footnote, are not assumed. The milestones carry no regularity beyond differentiability at the point considered (milestones 1, 5) and continuity for the optimality characterization in milestone 4.
The optimal menu is a maximizer of (6) under all four constraints, not a maximizer of (7): defining it through (7) would make half of the goal immediate and skip the reduction.
The development needs the algebra of the binary posterior, the two-type screening reduction, and a strict version of monotone comparative statics; Topkis's theorem on strictly increasing differences (Theorem 2.8.4) is already proved on the platform and referenced. Proofs of any milestone, and alternative arguments for the strict inequalities, are welcome.
Music streaming platforms collect a subscription fee from each user and pay part of the revenue to the artists whose content was played. The industry standard is the pro-rata method: the revenue pool is divided in proportion to each artist's total number of streams across all users. A competing method, the user-centric method, divides each user's own payment among the artists that user played, in proportion to that user's streams. SoundCloud adopted it in 2021 and Deezer has campaigned for it; the debate between the two methods is documented in the literature the paper cites, among others Dimont (2017), Haampland et al. (2022), Page and Safir (2018) and Meyn et al. (2023), listed below.
Bergantiños and Moreno-Ternero (arXiv:2310.11861, published in Management Science, 2025) put the debate on an axiomatic footing. Their Theorem 1 identifies the two basic principles every reasonable method in a large family satisfies, and isolates pro-rata and user-centric inside that family by one further principle each. This mission formalizes that theorem and the steps of its proof.
There are artists and a finite set of users, . A streaming problem records, for every artist and user , the number of times streamed content of . Each user pays , so the amount to share is . Write
A popularity index assigns to every problem a vector with positive sum, and artist is paid the reward
Since for every , an index is identified with its positive multiples. The pro-rata index is and the user-centric index is . A weight system assigns a weight to every user and every profile ; its weighted index is . Pro-rata is and user-centric is .
The axioms are:
Two further axioms of §3 compare the methods: reasonable lower bound (the artists played by a group of users receive at least ) and click-fraud-proofness (changing one user's streams moves no artist's reward by more than ).
For every popularity index :
Companions (§3, p. 13; Appendix, pp. 21–22): user-centric satisfies reasonable lower bound and click-fraud-proofness; with at least two artists, pro-rata satisfies neither.
Theorem 1 says that the choice between the two methods used in practice is a choice between two principles, and nothing else, once homogeneity and additivity are accepted: equal individual impact of similar users ("all streams count the same") gives pro-rata, and equal global impact of users ("all users count the same") gives user-centric. Part (a) describes the whole family of methods that respect the two basic axioms, which includes capped and hybrid schemes proposed in the industry (p. 10). The companion results show that the further axioms of §3 separate the two methods in favour of user-centric. The paper's further results, the core of the associated cooperative game (Theorem 2) and the core-selection characterization (Theorem 3), are separate missions of this series.
The result is proved in the paper; its proofs are in the appendix (pp. 18–22). No machine-checked version is known. A formalization fixes the model precisely, including the conventions the paper leaves implicit (the disjointness in additivity, nonempty user lists, the identification of indices up to a positive factor), and records exactly where two artists are needed.
The "if" directions are direct computations. The "only if" directions are a functional equation on indices: additivity reduces an index to its values on one-user problems, and homogeneity forces those values to be proportional to the profile, so the remaining freedom is one weight per user and profile. The work in (b) and (c) is to show that this weight is constant, using the extra axiom only on small auxiliary problems that contain users outside the given problem. The constant must be one number for all problems: a constant depending on the problem would make (b) and (c) much weaker, and is not what the paper proves.
Artists are Fin n, indexed from . Users are natural numbers, an infinite universe, and a problem is a finitely supported table ℕ →₀ (Fin n → ℕ) whose support is the user set ; every user of a problem therefore has a nonzero profile, which is the paper's standing assumption , and an index can only read the columns of users in . Streams are natural numbers. An index is a function from problems to Fin n → ℝ; it is a popularity index when it is nonnegative with positive sum on every problem with at least one user. The empty problem has nothing to share, and no positivity is demanded there; additivity forces the index to vanish on it. Additivity is stated for disjoint user sets: the printed axiom only says , which with would force and leave no index at all. "Is the pro-rata (user-centric) index" means "is a positive multiple of it, with one constant for all problems". Part (b) assumes at least two artists: with one artist the user-centric index satisfies its axioms and is not a multiple of pro-rata (every index then pays the whole to the single artist, so (b) holds at the level of rewards). Weights at the zero profile never enter a weighted index and are only required to be positive.
A formalization in which the positivity requirement applies to the empty problem, additivity allows overlapping user sets, or the constant in (b) or (c) depends on the problem is trivial or empty and is ruled out.
All objects are defined in one module, MusicStreaming.Axioms.Setting, on top of Mathlib's Finsupp and finite sums; nothing else is needed. Proofs of the milestones, alternative proofs of Theorem 1, and the verification that the definitions compute the paper's Example 1 are welcome.
Linear Cauchy–Riemann operators are the linearizations of the nonlinear Cauchy–Riemann equation for pseudoholomorphic curves. On the cylinder with the trivial bundle they take the form
where converges to loops of symmetric matrices as . These are the operators of Floer homology, of symplectic field theory and of contact homology. The dimension of their moduli spaces is the Fredholm index of , and the Riemann–Roch formula with punctures computes it from the Conley–Zehnder indices of the asymptotic operators :
This mission formalizes this formula, together with the Fredholm property of , following C. Wendl, Lectures on Symplectic Field Theory, Lectures 3–5, in the case of the cylinder (the sphere with one positive and one negative puncture). Mathlib has the notion of a Fredholm operator but no Sobolev spaces on cylinders, no Cauchy–Riemann operators and no Conley–Zehnder index.
If and the asymptotic operators are nondegenerate, then is Fredholm and (Wendl, Theorem 5.4 with Theorem 4.3, for the cylinder).
The result. The index formula is the dimension formula for moduli spaces of pseudoholomorphic cylinders: Floer trajectories in Hamiltonian Floer homology and holomorphic cylinders in symplectizations. It fixes the grading of these theories, and its sign conventions are those of the Conley–Zehnder index of the asymptotic orbits.
Formalizing it. The mission builds Sobolev spaces on the cylinder, the Fredholm theory of Cauchy–Riemann operators with cylindrical ends, and the Conley–Zehnder index of asymptotic operators. These are the analytic foundations of Floer theory and symplectic field theory and are reusable for transversality arguments and for the indices of other operators. Milestone 5 is a general statement about Banach spaces.
The operators act between infinite-dimensional spaces of functions on a non-compact domain, so finiteness of kernel and cokernel is a global statement that sees the behaviour at both ends. The Sobolev space is defined as a closure, and the operator acts on its elements through their weak derivatives. The Conley–Zehnder index is defined through a continuous argument of a normalized complex determinant along a path of symplectic matrices, extended to a normal form; the conventions (sign of , orientation of the cylinder, which end is positive) all enter the final formula. Several milestones are uniform estimates in which the constant is chosen before the function.
CauchyRiemannIndex. The definition module CauchyRiemannIndex_Setting defines the cylinder measure, W1p, crKernel, crRange, crIndex, IsFredholmCR, asymptotic operators through IsFundamentalSolution, IsNondegenerate and asymptoticCZIndex, and the Conley–Zehnder index czIndex of a symplectic path. The mission is standalone; czIndex and its auxiliary definitions repeat those of the ConleyZehnder mission word for word.EuclideanSpace ℝ (Fin n ⊕ Fin n), matrices are Matrix (Fin n ⊕ Fin n) (Fin n ⊕ Fin n) ℝ, and is Matrix.J. Maps on the cylinder are maps ℝ × ℝ → ℝ²ⁿ, periodic in the second variable, and is taken on the strip . is a closed subspace of Lp × Lp × Lp, consisting of triples .ℝ≥0∞ with and . Norms of smooth maps are eLpNorm in ℝ≥0∞; constants are in ℝ≥0.finrank ker - finrank (Lp ⧸ range) in ℤ; statements that use it also assert that both are finite-dimensional.ContDiff ℝ ∞ (, not analytic). The coefficient is only assumed continuous, with uniform convergence at the ends.Contributions welcome: general lemmas on Sobolev spaces of periodic functions, on Fredholm operators between Banach spaces, and on the Conley–Zehnder index.
To sell a stock short, an investor must first borrow it, and the owner who lends it charges a lending fee. Securities lending is a large market, and the fee varies across stocks: D'Avolio (2002) documents that shorting costs are positively related to the dispersion of investors' beliefs. Short-sale constraints have a long history in asset pricing (Miller 1977; Harrison and Kreps 1978; Jones and Lamont 2002), but most models either forbid short sales outright or take the fee as an exogenous parameter. Neither explains where the fee comes from, nor when a lending market is active at all.
Evgeniou, Hugonnier and Prieto build a dynamic general equilibrium model in which the fee is endogenous: two investors with logarithmic utility disagree about the expected return of a risky asset, and a lending agent, acting for the asset owners, sets the fee charged to short sellers to maximize the owners' fee revenue. Their §3 derives the equilibrium shorting cost in closed form at every state of the economy. This mission formalizes that derivation.
The economy has a riskless asset and two risky assets with strictly positive volatilities . Asset 1 can be shorted at a cost; asset 2 cannot be shorted at all. There are two investors, an optimist and a pessimist , with wealths . Each investor perceives market prices of risk (Sharpe ratios) , and the optimist is more optimistic about asset 1: , the disagreement .
A short position in asset 1 pays a shorting cost per dollar shorted, and a long position earns a lending yield . Both are measured per unit of volatility of asset 1: and . A position in asset 1 earns fees at the rate
with and . Investor chooses wealth fractions with to solve the mean-variance problem
which is what logarithmic utility reduces to at each instant. The lending agent's revenue per unit of volatility at fee is
An equilibrium at a state consists of these quantities such that: the no-dominance condition holds for both investors (equation (7)); each investor's portfolio is optimal; asset 1, in positive supply , clears; the lending market clears (fees paid by short sellers equal fees received by long holders); and is the least maximizer of over . The inactive set is and the active set is its complement.
At every equilibrium state,
Lending is active exactly where the pessimist perceives a strictly negative net Sharpe ratio on long positions, and there the lending agent charges half the Sharpe ratio the pessimist could earn by shorting absent frictions.
Two companion statements are also included: (18) (p. 20), that the pessimist is strictly short on , and the fee flow (p. 19).
The goal is the paper's description of the short market. It identifies the active set by a condition on one observable-in-principle quantity, the pessimist's net Sharpe ratio, and it gives the fee as a fixed fraction of the pessimist's frictionless Sharpe ratio. The rest of the paper rests on it: the one-asset closed forms of §4.1, the trading regions of §3.3, and the pricing results of Proposition 2 all start from (15)–(16). The fee-flow identity shows that the optimist captures a quarter of the pessimist's frictionless excess return, which is the upper bound Remark 1 attributes to any alternative fee-setting mechanism.
The result is proved in the paper, partly in the text and partly in Appendix A. Some steps are argued informally: (11) rests on the sentence "agents cannot be short simultaneously in equilibrium", and (14) on "substituting the optimal portfolios of Proposition 1 into the market clearing conditions". As far as is known, none of it has been machine-checked. A formalization makes each step explicit, including the degenerate states the text passes over. In checking the statements against each other, three printed slips were found and are corrected here (see Formalization scope).
The goal combines optimality, clearing and revenue maximization, and the obvious argument fails at its degenerate edge. On the inactive set the shorting cost equals the lending yield (). There Proposition 1's characterization of optimal portfolios no longer holds: portfolios that short asset 1 to buy asset 2 are also optimal. So the step "substitute the optimal portfolios" is not available, and (14) must be obtained from the clearing conditions directly in that case. Similarly the revenue maximizer is not unique on the inactive set; the shorting cost is pinned down only by the paper's selection of the least maximizer, and (16) is false for any other selection. Finally, (11) requires an argument that the two investors cannot both be short while asset 1 is in positive supply. This uses optimality of both portfolios, not just of one.
Everything is stated at one state of the paper's continuous-time economy, about real numbers. The continuous-time economy of §2 (Brownian filtrations, consumption streams, the dynamics of wealth) is the paper's motivation and is not formalized; the formalized statements are its instantaneous equilibrium conditions. The time index is dropped throughout, and the paper's "arbitrary process " in Proposition 1 becomes an arbitrary real number.
Conventions:
if … then … else 0.Corrected slips of the page, each disclosed in the item concerned:
The results (11), (13) and (14) are not built into the equilibrium predicate. With them assumed, the goal would reduce to a four-line computation; they are separate items to be proved. The definitions are short and self-contained, needing only real arithmetic from Mathlib. Proofs of the milestones, and proofs of the goal that use the milestones, 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 asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real , also holds for every real . This is an open problem: no proof is known, and the technique that reached 62 cannot go further. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three diagonal matrices. Because the cutoff-62 mission already covers every , the new work is the range from 50 to 62.
The cutoff came down from 256 to 62 across nine missions. The step from 90 to 80 used a weighted pair-curvature and confinement estimate introduced by moona3k, and further refinement pushed it from 80 through 70 to 62. The confinement method is now exhausted: at , every confinement radius whose tangent model stays positive already makes the budget-7 box factor larger than 1. Reaching 50 requires a fundamentally new idea. The goal theorem below gives the exact statement.
This is an entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 50 or lower also settles this mission.
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 libraryQuantum mechanics represents the states of a system by unit vectors (normed rays) of a complex Hilbert space and its observables by self-adjoint operators on . The most important observables — position, momentum, energy — are unbounded. A. Heathcote's paper Unbounded Operators and the Incompleteness of Quantum Mechanics (Philosophy of Science 57, 1990, 523–534) draws attention to a mathematical fact that is routinely glossed over in physical texts: an unbounded self-adjoint operator cannot be defined on all of , and there are concrete normalized wave functions on which the position and momentum operators do not act at all. The paper uses this to argue that the standard postulates of quantum mechanics are, in a precise sense, incomplete.
This mission isolates the mathematical content of that argument, which is a clean and checkable piece of functional analysis on .
Let be a complex Hilbert space. A (partially defined) linear operator has a domain ; it is bounded if there is with for all , and unbounded otherwise. It is self-adjoint if it equals its Hilbert adjoint, , which includes .
On :
There is a unit vector of , namely the class of , lying in neither domain:
The result. The goal shows that the two postulates "every normed ray is a state" and "observables are self-adjoint operators" force the existence of states on which the position operator (and, independently, the momentum operator) is undefined. Milestone 5 is what the paper uses to separate this phenomenon from the canonical commutation relations: the failure of is not explained by being "sharp in momentum", because is not even in . Milestone 6 records the physical reading: the mean position of this normalized state is infinite.
Formalizing it. The individual facts are standard and elementary; none of them is new. What the mission produces is a machine-checked version of the paper's argument stated against the actual space and Mathlib's notion of unbounded operators and adjoints, with the domain conventions made explicit.
The calculus is easy; the subtleties are in the bookkeeping. Elements of are almost-everywhere classes, so " is discontinuous at " does not by itself show : one must rule out every a.e.-modification of being absolutely continuous. Similarly, the Hellinger–Toeplitz argument gives but not density, which comes from the adjoint being a genuine operator.
H →ₗ.[ℂ] H; self-adjointness is IsSelfAdjoint with respect to the adjoint A†, over a complex complete inner product space.Lp ℂ 2 volume on ℝ; and are subsets of it. Integrals of non-negative quantities are Lebesgue integrals valued in , so "" is literal and not a junk value.This mission develops Chapter 7 of Quantum Algorithms and Learning Theory — Part II by Srinivasan Arunachalam. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
For a matrix of rank (the generator matrix of an linear code) and define the codeword state
For every rate there is a constant such that the following holds for all and all rank- matrices with : if a measurement (POVM ) on copies identifies from , for drawn uniformly from , with average success probability
then .
This improves the Holevo-type bound to the optimal for constant-rate codes, showing that codeword fingerprint states cannot be identified from few copies.
Formalization Note "" is read as a fixed rate , and the constant of may depend on only. Identifying the state means outputting , which is equivalent since is injective for rank . The code distance plays no role and is not a hypothesis.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 1 of Quantum algorithms for optimizers by Giacomo Nannicini. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
Let be a register made of a register of qubits followed by a register of qubits. Let be a pure state of , that is, a unit vector. Then there exist a finite index set , an orthonormal family of states of , an orthonormal family of states of , and nonnegative reals with , such that
This is the singular value decomposition rephrased for bipartite pure states. Classical simulation algorithms for quantum circuits use it.
Formalization Note The source leaves the index set unspecified; here it is Fin r for an existentially chosen r.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
Credit risk matters to insurer bond holdings, pension scheme fixed-income investment and counterparty guarantees. Merton's corporate debt model derives terminal shareholder and bondholder payoffs from limited liability and asset value. Jarrow–Lando–Turnbull introduces observable ratings with Markov state migrations and default, motivating a second, independently defined view of risky fixed-income valuation.
A firm has nonnegative terminal assets and a single promise of face-value debt. Creditors are paid no more than the promise and no more than available assets; equity gets the residual. Finite genuine probability masses attach to terminal asset scenarios and yield discounted debt and equity claim valuations. Separately, a three-state rating matrix contains two non-default ratings and a terminal default state, with nonnegative row probabilities and full row-sum constraints.
The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.
Strict asset deficit is equivalent to zero equity except for solvent zero-cashflow special cases.
A bond priced equally to risk-free debt has zero model spread.
Structural terminal solvency and an independent absorbing-rating transition system reconcile riskier defaultable debt prices, nonnegative credit value deductions and genuinely two-period probability conservation.
Structural terminal solvency and an independent absorbing-rating transition system reconcile riskier defaultable debt prices, nonnegative credit value deductions and genuinely two-period probability conservation.
As discussed in Merton's corporate-credit model, The mission connects terminal firm claims to an actual finite risk-neutral weighted value: equity plus debt exhaust firm assets, expected discounted defaultable debt is bounded above by its risk-free counterpart, and credit value deductions are nonnegative. The genuine two-step rating migration law preserves total probability mass. These independently defined results jointly give an actuarial foundation for pricing defaultable corporate securities and recognising credit exposures in asset-liability valuation.
It must be proved that the limited-liability payoffs partition total assets, with exact boundary conditions where assets equal or fall below face value. The pricing theorem must distinguish actual discounted expected creditor payments from assuming a closed-form Black–Scholes price; no lognormal risk-neutral firm distribution is postulated. Credit spreads require positive debt prices and maturities. A rating transition matrix must be proved stochastic under composition, and an absorbing default state is a model condition rather than automatically true for arbitrary matrices.
Limited liability and rating-migration probabilities are distinct mathematical constructs in this model. The complete diffusion-based Merton option value and continuous-time rating default models remain future mathematical research. The current target is nontrivial because it derives the bond valuation from limited-liability terminal payouts and an actual probability space, and the migration law from an independent finite transition kernel. Existing bond-present-value and state-reward missions are useful, but they do not identify shareholder and debt recovery claims. Its expected payoff and finite rating matrix infrastructure is reusable in asset-liability modelling and insurer counterparty credit valuation.
A firm's terminal assets must be partitioned consistently between equity and creditor payoffs. Above the promised debt face amount bondholders receive the promise and owners receive remaining assets. At the strict default threshold the owners' limited liability makes equity worthless and bondholders recover the remaining assets. The source values these payoffs using a proper finite risk-neutral scenario law, proving that discounted risky debt is no more valuable than the risk-free debt promise. The other branch builds a genuinely stochastic three-state rating transition matrix and derives two-step migration probabilities from matrix multiplication. Those observed or risk-neutral migration probabilities are not interchangeable without an additional measure-change argument. This is precise finite corporate credit mathematics; it is not a fabricated full closed-form structural diffusion model or a continuous-time default-intensity theory.
The new credit mission establishes exact one-period finite-state structural debt/equity payoff pricing and two-step rating probability conservation. It does not claim Merton's Black–Scholes closed-form equity value, stochastic diffusion replication, or the full continuous-time JLT risk-neutral generator model. The default-state absorbing property needs additional row restrictions and is not asserted for unrestricted transition matrices. Those are substantial extensions, and the current theorem bodies remain unproved.
These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.
Insurance economics prices risk using the utility of wealth rather than merely its variance. Pratt's seminal work derives risk aversion and the certainty-equivalent insurance premium, while Rothschild and Stiglitz connect comparative risk to probability order. Earlier actuarial entropic premium missions contain special finite retention objectives but do not derive an independently constructed expected wealth utility with premium indifference and finite stochastic dominance.
Losses are monetary outcomes on a genuinely finite scenario probability model, whose masses are nonnegative and sum to one. The exponential CARA wealth utility is strictly increasing and concave for positive aversion. The certainty-equivalent premium is constructed from the actual exponential moment of loss. Full insurance replaces the uncertain loss with a fixed premium and its utility is compared with the truly weighted uninsured outcome.
The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.
Utility of deterministic wealth equals its scenario expectation.
Risk-averse exponential expected utility demands at least the expected claim cost.
The actuarial insurer and policyholder indifference premium follows from genuinely averaged utility, with positive risk loading and a finite-scenario stochastic risk ordering.
The actuarial insurer and policyholder indifference premium follows from genuinely averaged utility, with positive risk loading and a finite-scenario stochastic risk ordering.
As discussed in Pratt's utility-risk treatment, The capstone proves a complete indifference premium identity, not merely its algebraic definition, and derives risk loading above expected loss from convexity of the exponential. A coupled stochastic order implies both the ordering of actual finite distribution functions and higher expected utility for increasing utility functions. The same ordering is related to excess-of-loss premiums through statewise monotonicity. These results supply core insurer and policyholder pricing foundations.
The logarithmic certainty equivalent requires strictly positive exponential moments and a nonzero risk-aversion parameter. The actual expected utility factorization must account for the sign of negative exponential utility. Risk loading requires Jensen's inequality or an equivalent discrete exponential-convexity argument, not the assertion that every risk is profitable to insure. The comparison of finite CDFs must reverse the inequality for higher wealth, while a higher loss severity raises stop-loss costs. Pathwise coupling is stronger than the entire stochastic-dominance order and is identified as such.
Certainty-equivalent premium and stochastic risk ordering are distinct mathematical constructs in this model. A future generalisation will derive second-order stochastic dominance via integrals of real CDFs and concave expected utility, not merely a pathwise coupling. The current project is nontrivial because the CARA indifference identity follows by differentiating and averaging the actual utility, and the insurer's risk loading is derived from Jensen's inequality. Existing specialised exponential risk-price examples provide a useful benchmark but do not replace these general sources. The premium and coupling functions are reusable for nonproportional reinsurance, risk classification and comparative risk analysis.
Under constant absolute risk aversion the negative exponential utility function is increasing and concave in wealth when risk aversion is positive, even though its numerical utility level is negative. A fair premium is not obtained by simply assuming a desired level of profit. The expected uninsured utility is calculated from true scenario probabilities, the utility with full insurance is calculated using a fixed premium and the resulting indifference equation is solved from the loss exponential moment. The log moment premium must then be compared against expected claim cost using convexity, and the sign of this loading depends on risk aversion. Finite distribution functions and expected excess claims are independently defined for comparison. The pathwise coupling order in the source is stronger than first-order stochastic dominance, so no false claim of characterising all stochastic orders is made. Second-order dominance requires a separate distribution-integral analysis.
This is a genuine finite-probability CARA model with exactly derived insured/uninsured premium indifference. The stochastic order is proven for explicit statewise couplings and thus yields a strong sufficient condition for first-order stochastic dominance, not a complete characterisation of arbitrary second-order stochastic dominance. General concave utility risk orders, mean-preserving spreads, Arrow–Pratt comparative aversion for all utility families, and infinite random variables are future developments. All proof obligations are open.
These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.
Mortality experience in joint-life assurance and pensions depends not only on whether someone died, but on which insured life survives and which survivor or joint reserve must then be held. Standard multiple-life actuarial valuations motivate last-survivor, reversionary and guaranteed pension benefits. Earlier actuarial missions XLV and XLVI treat basic reversionary annuities and single-life mortality profit separately; this connects them through a genuine four-outcome death-strain model.
Two members start alive and experience independent yearly survival outcomes. Exactly four mutually exclusive joint states follow: both survive, only the first survives, only the second survives, or neither survives. Their probabilities use product and complement survival factors. The year-end reserve and any benefits can differ for every one of these states. Opening reserves plus premiums earn the annual return before payment and the next state contingent reserve is recognized.
The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.
Each valid joint-life outcome has nonnegative mass.
Additional state-specific benefit claims add to expected death strain.
An exhaustive, correctly normalized two-life outcome model makes the mortality experience profit mean zero, retaining separate survivor reserves, death benefits and guaranteed payment conventions.
An exhaustive, correctly normalized two-life outcome model makes the mortality experience profit mean zero, retaining separate survivor reserves, death benefits and guaranteed payment conventions.
As discussed in Dickson, Hardy and Waters' multiple-life analysis, The capstone derives actual four-state normalization and reconciles joint mortality profit as expected death strain less observed state-specific death strain, whose expected result is zero under its own properly normalized law. The state-specific reserve functions distinguish the two possible remaining single-life liabilities rather than collapsing them into a single average. Limited-reversionary and certain guarantee payments are represented as separate conditional benefits.
Four disjoint probabilities must be normalized with exact endpoint treatment. Reserve releases after each death outcome may have opposite signs to death-benefit payments, so the state strain must include both payout and next-state reserve less the accumulated starting fund. Expected mortality profit cannot be asserted by defining it to have zero mean: it must follow from the actual weighted expectation of the observed strain. Independence is an explicit current assumption; arbitrary dependent lives need a separate four-state probability law.
Joint-life mortality profit and state-dependent death strain are distinct mathematical constructs in this model. A future mission could introduce dependent lifetimes and within-year order of deaths, then compute first-to-die and last-survivor benefit present values directly from the joint survival law. The present work is nontrivial because both survivor reserves and actual death claims differ across the four states, while the mean mortality profit emerges from their normalised probability distribution. Existing joint-life annuity and single-life profit missions do not establish this combination. The outcome-specific reserve and mortality gain functions are reusable for spouse's pensions, death-in-service benefits and multi-life experience analysis.
Four disjoint annual outcomes must be considered for a policy whose two insured lives begin the year alive. They are both alive, only the first alive, only the second alive and both dead. Each outcome has a separate year-end reserve and may have a different death or survivor benefit. Accordingly, its actual death strain includes the benefit paid plus the new reserve less accumulated beginning-year funds. Expected strain is a genuine probability-weighted average of those four observed strains. The mortality experience profit for any one realised outcome equals the expected strain less that outcome's actual strain. Its expectation must be shown to vanish under the normalised four-outcome probability distribution, rather than by assuming zero mean. This framework supplies an actuarial bridge from joint-life/reversionary benefits to experience profit analysis and guarantee-period pensions. Within-year timing and dependent life outcomes require additional formal work.
This is a complete one-year joint mortality-experience model with explicit separate survivor reserves, not a full continuous-time ordering of first and second deaths inside the same policy year. Guarantee-period timing is represented by a separate deterministic indicator input. Exact age differences, policy options, death-payment timing and dependence-copula extensions can build on these definitions later. All theorem statements remain unproved.
These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.
Panjer's original 1981 result derives the aggregate claims recursion from a special frequency probability law and arbitrary nonnegative-integer severity mass distribution, including claims worth zero. The original article and the Sundt–Jewell extension underpin the mission. Earlier actuarial mission LIV handles direct recurrence algebra, while LXXIII derives the Bernoulli first positive aggregate mass identity. This mission formalises a full positive-aggregate-severity recursion for a genuinely constructed compound law.
A claim count N has probability weights p_n supported on {0,...,m}, with no artificial truncation of an otherwise infinite count distribution. Independent severity masses f_j on nonnegative integer amounts admit a genuine n-fold convolution, with count-zero convolution equal to a unit atom at zero. Thus g_k=Σ_{n=0}^m p_n(f^{*n})k is defined independently of Panjer's formula. The count recursion p_n=(a+b/n)p{n−1} is assumed only for 1≤n≤m+1, including its boundary p_{m+1}=0, and p_n=0 above m. No conclusion about the aggregate g is assumed.
Write for the probability of exactly claims and for the probability that one claim has size . The frequency law is genuinely supported on ; an infinite Poisson distribution is not silently truncated. The empty portfolio has aggregate size zero, while denotes the distribution obtained by summing independent severities.
The first group constructs the aggregate probability directly from the frequency and severity laws:
It also proves the zero-severity convolution identities, nonnegative mass preservation, and finite frequency and severity generating-function relationships.
The count probabilities obey a Panjer recurrence with coefficients and . Crucially, the finite-support model includes the transition from to the compulsory zero probability at :
This makes the assumed count law compatible with the finite aggregate distribution. For a claim size that may equal zero, the aggregate zero atom involves every possible claim count:
The central target is the entire positive-aggregate-size Panjer recurrence, not merely its first positive atom. For every integer , the result is
The factor is essential because a positive number of claims may still produce aggregate size zero. Further targets establish properties of cumulative aggregate probabilities, capital exceedance tails and finite stop-loss expectations. Every aggregate probability is defined independently of the recurrence it is subsequently required to satisfy.
The original Panjer paper gives the classical aggregate-loss setting. The capstone derives (1-a f_0)g_k=Σ_{j=1}^k(a+bj/k) f_j g_{k-j} for every positive aggregate amount from the actual random sum, together with g_0=G_N(f_0). The generator gives a count-supported finite Panjer family; it does not claim an infinite Poisson/negative-binomial count law. The exact zero claim-size correction is essential even when count N is positive, because multiple claims may all have zero monetary size. The authoring graph also includes frequency PGFs, severity convolution, CDF/tail and stop-loss identities.
Existing actuarial probability and Panjer steps are established subject areas. Every formal result introduced in this mission is an open Lean theorem target; none has an accepted proof. A vacuous or trivial definition of the aggregate as the recurrence solution is explicitly ruled out. The proof must rearrange nested severity convolutions, differentiate coefficient identities or establish the equivalent frequency recursion, and manage the zero-severity term that multiplies g_k itself. The count-support cutoff must satisfy the Panjer multiplier at m+1 to avoid invalid boundary terms. The recurrence at k=0 is not defined due to division by k; zero aggregate mass follows separately from the frequency PGF. Because f_0 may be positive, truncating the count sum at arbitrary m with an infinite count law would be mathematically invalid; we avoid that by using a genuine finite count distribution.
This mission supplies a full k≥1 Panjer relation under an exact finite-support frequency model, not general infinite Poisson or geometric counts and not continuous claim severities. Positivity and mass normalisation require additional explicit probability conditions beyond the purely algebraic count recurrence, so the capstone is a valid algebraic identity even before imposing proper probability weights. All formal results remain Lean theorem targets without accepted proofs. The finite model is a reusable foundation for formal-power-series and analytic infinite-frequency cases.
These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.
The Yang–Mills functional measures the total curvature of a connection on a principal bundle. Its critical points, the Yang–Mills connections, are the non-abelian generalization of solutions of Maxwell's equations, and in four dimensions the most important among them are the self-dual and anti-self-dual connections (instantons), whose moduli spaces underlie Donaldson theory of smooth four-manifolds. A basic and frequently used fact, recorded as Proposition 3.1.1 in K. Uhlenbeck's lectures Equations of Gauge Theory (notes by L. Fredrickson, Temple University, 2012), is that instantons are not merely critical points: within a fixed topological class and with fixed boundary data they are absolute minimizers of the Yang–Mills energy. The same "energy identity" argument is the template the notes later apply to the Kapustin–Witten equations (Proposition 3.1.5).
Timeline of the ideas involved: Yang and Mills introduce the equations (1954); Belavin, Polyakov, Schwartz and Tyupkin observe the topological lower bound on the energy and its saturation by self-dual fields (1975); Atiyah, Hitchin and Singer study the deformation theory of instantons (1977–78); Donaldson uses the instanton moduli space in four-manifold topology (1983).
Work on the trivial principal -bundle over a closed box with the Euclidean metric. A connection is with , where each is a smooth map into the Lie algebra of traceless skew-Hermitian complex matrices. Its curvature is the -valued two-form with coefficients
The Hodge star on two-forms is , with the Levi-Civita symbol. A two-form is self-dual if and anti-self-dual if . The pointwise norm is , and the Yang–Mills functional on is
The Chern–Weil density is the coefficient of , and the Chern–Simons three-form is , with flux components .
If and are smooth -connections on that agree on , and is self-dual on all of or anti-self-dual on all of , then
The energy identity turns a second-order variational problem into a first-order one: any connection satisfying the first-order self-duality equation is automatically a Yang–Mills connection, and in fact a global minimizer in its class. This is the reason instanton moduli spaces are the natural objects of four-dimensional gauge theory, and it is the model for the corresponding minimization statements for the Kapustin–Witten equations treated later in the same notes. The result is classical and its proof is known; the remaining work is formal: a machine-checked development of the curvature, Hodge star, Chern–Simons transgression and the boundary integration on boxes, none of which are currently packaged in this form in Mathlib.
The algebraic identity of Lemma 3.1.2 is a finite computation. The substantive step is the transgression formula , a cancellation between derivative terms and cubic terms that depends on cyclicity of the trace and on the antisymmetry of , followed by Stokes' theorem on the box with correct face orientations. The naive approach of comparing and pointwise fails: the two connections agree only on the boundary, and only the integrated topological term is boundary-determined.
The general setting of the notes (a -bundle over a compact oriented Riemannian four-manifold with boundary, topological class ) is replaced by the trivial -bundle over a closed axis-parallel box in Euclidean , so the topological term is zero. Connections are smooth on all of (equivalently, smooth up to the boundary of the box) and every coefficient takes values in . Two-forms are stored as antisymmetric families of matrices; partial derivatives are taken entrywise; integrals are Lebesgue integrals over the box and over its faces. "Fixed boundary data" means at every point of . Self-duality is , matching in Section 2.2 of the notes.
Two sign/normalization corrections relative to the printed notes are made deliberately: Lemma 3.1.2 is stated with the sign obtained in its own proof on p. 32 ( rather than the printed , because on ), and the Chern–Simons form uses the standard coefficient in , i.e. , for which holds, instead of the printed .
A trivializing formalization would make the boundary condition or the self-duality hypothesis unsatisfiable; here the zero connection is self-dual and satisfies every hypothesis, and the statements are not vacuous.
Reusable infrastructure: Levi-Civita symbol and Hodge star on with matrix coefficients, curvature of matrix-valued connections, the Chern–Simons transgression, and Stokes' theorem for flux forms on boxes (Mathlib's divergence theorem on boxes is the natural tool). Contributions to any milestone are welcome.
How large can the order of a single permutation of objects be? The answer, Landau's function , is a basic invariant of the symmetric group : it is the maximum number of times a permutation can be iterated before it returns to the identity. Because the order of a permutation is the least common multiple of its cycle lengths, is also the largest least common multiple of the parts of a partition of , which ties the question to the distribution of prime numbers.
Timeline.
For a natural number , let be the group of all permutations of an -element set. The order of is the least with . Landau's function is
A partition of is a multiset of positive integers summing to . The prime counting function is the number of primes , the (offset) logarithmic integral is , and is its inverse on . Throughout, is the natural logarithm.
Landau's theorem pins down the growth rate of the largest element order in , which bounds, for example, how long any fixed shuffle of cards can be repeated before the deck returns to its starting order. The refined statements quantify the second-order behaviour and connect it to the error term in the prime number theorem; the criterion in milestone 7 is one of the known elementary reformulations of the Riemann hypothesis, and is included as a faithful statement of the source, not as an expected deliverable. The other results are proved in the literature; formalizing them requires building the partition/lcm description of element orders in and quantitative prime-counting estimates on top of Mathlib.
The order of a permutation is easy to compute from its cycle type, but maximizing an lcm over all partitions is a non-linear optimization: the optimum uses prime powers whose sizes are dictated by the distribution of primes, so even the leading-order asymptotics need Chebyshev-type or prime number theorem estimates, and the refined milestones need the prime number theorem with an explicit error term.
Equiv.Perm (Fin n); is the supremum of orderOf σ over the finite group (a natural number; ).Nat.Partition n; the lcm of a partition is the Multiset.lcm of its parts.Real.log (which returns at and is defined for negative input); all asymptotic statements are about , so the values at small are irrelevant there. The bounds in milestones 8–9 are stated for every and are true at .Nat.primeCounting ⌊x⌋₊; is the offset logarithmic integral ; is the least with , which for is the inverse function value. Replacing by the full integral changes the inverse by and does not affect any of the asymptotic statements.RiemannHypothesis.Contributions of reusable infrastructure (cycle-type lcm, prime-counting error terms, the logarithmic integral) are welcome.
Marginal utility is the change in utility (pleasure or satisfaction) that results from consuming one more unit of a good or service. It is the basic quantity of the marginalist theory of value, which explains prices and consumer choice by the additional satisfaction provided by each extra unit rather than by total usefulness. The law of diminishing marginal utility states that, other things being equal, the utility a consumer derives from additional units of a commodity goes on decreasing as the amount consumed increases; economists regard it as reflected in the concave shape of most utility functions.
Timeline. Gabriel Cramer (private letter, 1728) and Daniel Bernoulli (Specimen theoriae novae de mensura sortis, 1738) proposed that the desirability of money decreases as it accumulates, measuring it by the square root (Cramer) and the natural logarithm (Bernoulli), in order to resolve the St. Petersburg paradox. W. F. Lloyd (1833), N. W. Senior (1836), J. Dupuit (1844) and H. H. Gossen (1854) stated marginal-utility ideas with little contemporary influence. The theory entered the mainstream in the Marginal Revolution of Jevons (1862/1871), Menger (1871) and Walras (1874), and was consolidated by Marshall's Principles of Economics (1890), which treats utility as quantified. Ordinalist reformulations (Edgeworth 1881, Slutsky 1915, Hicks–Allen 1934) moved to indifference-curve analysis; cardinal utility returned with expected-utility theory (Ramsey 1926, von Neumann–Morgenstern 1944, Savage 1954), where diminishing marginal utility is linked to risk aversion.
A utility function of one quantified variable is a map , where is the quantity of a single good and every other variable is held fixed (ceteris paribus, "c.p."). The change in utility from state to state is
The marginal utility at is the limit of the ratio of the change in utility to the size of the change in ,
which mainstream neoclassical economics assumes to exist. The function has diminishing marginal utility on a set of quantities when
In the Lean development these are utilityChange, marginalUtility and HasDiminishingMarginalUtility in the namespace MarginalUtility.
For an open interval and with diminishing marginal utility on :
The first clause is the law as stated ("marginal utility goes on decreasing"); the second is its reading in terms of successive equal gains.
The law underlies the marginalist explanation of demand, the resolution of the water–diamond paradox, and, through the concavity of utility, the modelling of risk aversion in expected-utility theory. The concave-shape and satiation statements are the forms in which the law is used in consumer theory: under diminishing marginal utility, total utility is maximal exactly where marginal utility vanishes.
The mathematical content is classical single-variable calculus and is fully known. What this mission adds is a precise, machine-checked dictionary between the economic vocabulary ("marginal utility", "diminishing", "concave shape", "satiation") and standard analytic statements, on which later missions about consumer choice and risk aversion can build.
None of the statements is deep. The care required is in the hypotheses: the law is a statement about an open interval of quantities, marginal utility only makes sense where is differentiable, and mere (non-strict) concavity gives only non-strict decrease of successive gains. The source's verbal statements must be matched exactly in strength (strict versus non-strict inequalities) and in domain.
Utility is a function of one real quantity; the domain of interest is an open convex set (an open interval, possibly unbounded), passed as a hypothesis. Marginal utility is deriv U, which Lean sets to where is not differentiable; every statement that uses it assumes the needed differentiability. Diminishing marginal utility means and are differentiable on and on . A statement that only assumed without differentiability would be weaker than intended, because of the value- convention; the definition rules this out. Multivariate utility, ordinal utility and the qualitative assumptions listed in the source (identical units, constant tastes, and so on) are outside the scope of this mission. Proofs may use Mathlib's one-variable calculus and convexity libraries freely.
The second law of thermodynamics is a physical law based on universal empirical observation concerning heat and energy interconversions. Two of its classical statements are impossibility statements about machines. Rudolf Clausius (1854): "Heat can never pass from a colder to a warmer body without some other change, connected therewith, occurring at the same time." Lord Kelvin: "It is impossible for any system to operate in a thermodynamic cycle and deliver a net amount of energy by work to its surroundings while receiving energy by heat transfer from a single thermal reservoir." The Wikipedia article Second law of thermodynamics records that these two have been shown to be equivalent.
The law is not only prohibitive. Sadi Carnot's analysis of heat engines (1824) yields an upper bound on the efficiency of any engine running between two heat reservoirs, attained by reversible engines and strictly missed by irreversible ones, and — crucially — the same for all reversible engines whatever the working substance. That substance-independence is what makes a thermodynamic temperature possible: as the article puts it, "The second law allows a distinguished temperature scale, which defines an absolute, thermodynamic temperature, independent of the properties of any particular reference thermometric body."
This mission formalizes that chain: from the two impossibility statements, through Carnot's theorem, to the existence and uniqueness of the absolute temperature scale normalized by the Kelvin convention at the triple point of water.
A cyclically operating device is recorded by the heat it exchanges with thermal reservoirs over one complete cycle. Reservoirs are labelled by empirical temperature, an element of a linearly ordered type (: the reservoir at is colder). A cycle is a finitely supported function , where is the net heat absorbed by the device from the reservoir at (negative if rejected). Because the device returns to its initial state, the first law makes the net work delivered equal to the total heat absorbed:
The cycles that can actually be realized form a set , assumed to be a convex cone: the null cycle is realizable; two realizable devices can be run side by side, their heat exchanges adding; and a realizable device can be scaled by any factor . A cycle is reversible when and , and operates between and when it exchanges heat with no other reservoir. A Carnot engine between a hot and a cold is a reversible cycle operating between them with , and . The efficiency relative to the hot reservoir is .
In this language:
Assume is a convex cone satisfying the Clausius statement and admitting Carnot engines, and fix a reference reservoir . Then there is exactly one with
The content is that the left-hand ratio, a property of an engine, depends on the engine only through its two reservoirs, and does so as a ratio of numbers attached to the reservoirs. The normalization at is the Kelvin convention; as the article notes, "any reference temperature and any positive numerical value could be used".
for a convex cone admitting Carnot engines over at least two reservoir temperatures.
For and a Carnot engine between them, every realizable engine between the same two reservoirs satisfies , with strict inequality when is irreversible (); and any two Carnot engines between and have equal efficiency.
The goal makes explicit which features of the realizable processes are used when a textbook defines absolute temperature. The three hypotheses — convex cone, Clausius statement, existence of Carnot engines — are exactly what the derivation needs; the working substance, the equation of state, and the mechanism of a device never appear. Uniqueness is the part that is usually left implicit: the Kelvin normalization at one reservoir pins the scale completely.
The milestones follow the article's own order: equation (1) for the efficiency of an arbitrary engine; the equivalence of the Clausius and Kelvin statements; the three clauses of Carnot's theorem; the composition law for the reversible heat ratio across an intermediate reservoir; the conversion of that law into a scale; and the resulting Carnot efficiency .
The mathematics is elementary — convex cones in a space of finitely supported real functions, and one functional equation — but the bookkeeping is where faithfulness is won or lost. Carnot's theorem is proved by scaling a candidate engine against a reversed Carnot engine so that the composite does no net work, which makes the Clausius statement applicable; the equality case has to identify the candidate as a positive multiple of the Carnot engine before concluding that it is reversible. The composition law requires the intermediate reservoir to be exactly balanced, so that the composite is again a two-reservoir engine — the article's remark that "the heat flown from the engine 2 to the intermediate reservoir must be equal to the heat flown out from the reservoir to the engine 3". The functional equation must be solved without assuming the reference reservoir is the hottest or the coldest, so the scale is defined by below and by above it, and the composition law is applied in four different orderings.
The Einstein field equations (EFE) are the field equations of general relativity. They relate the curvature of spacetime, encoded in the metric , to its matter–energy content, encoded in the stress–energy tensor :
They were published by Einstein in 1915. A structural requirement on any such equation is that it be compatible with the local conservation of energy and momentum, . For the EFE this compatibility is automatic: the left-hand side is identically divergence-free by the contracted Bianchi identity, so the field equations force conservation of the right-hand side. This mission formalizes that implication together with the standard algebraic reformulations of the equations, following the Wikipedia article Einstein field equations (revision 1374672993).
Everything is written in one coordinate chart. A point is , where is the spacetime dimension (not fixed to ). A 2-tensor field is a matrix-valued function . A metric on an open set is a 2-tensor field whose components are on and which is symmetric and nondegenerate at each point of ; denotes the inverse matrix. Partial derivatives are coordinate (Fréchet) derivatives. Using the Misner–Thorne–Wheeler convention adopted by the source:
For a smooth nondegenerate symmetric metric on an open , constants , , any , and any such that the field equations hold on :
Conservation of is a consistency condition that any relativistic field equation for gravity has to satisfy; it is also the starting point for deriving the motion of matter (for dust, the geodesic equation) from the field equations alone. The trace-reversed and vacuum forms are the ones used in practice to study vacuum solutions such as Schwarzschild and Kerr, and Einstein manifolds in geometry.
All of these results are classical and fully proved in the literature. What is not yet available is a machine-checked development of the Levi-Civita curvature calculus in coordinates suitable for these statements: Mathlib currently has no Riemann or Ricci tensor of a pseudo-Riemannian metric. The mission produces that layer and the proofs on top of it.
The algebraic milestones (trace, trace reversal, vacuum form, vacuum energy) only need matrix algebra and the symmetry of ; without symmetry the identity fails, so symmetry is essential. The analytic core is the contracted Bianchi identity: it needs the symmetry of mixed second and third partial derivatives (Schwarz's theorem on an open set), derivatives of the matrix inverse , and lengthy index bookkeeping with sums over . Since all objects are total functions, every derivative step must be justified by differentiability on the open set , not taken for granted.
Fin D → ℝ; tensors are Matrix (Fin D) (Fin D) ℝ-valued functions; no manifold structure. is arbitrary, and no Lorentzian signature is imposed (the results hold for any nondegenerate symmetric metric, which includes the Lorentzian case).Multistage stochastic integer programs model sequential decisions under uncertainty in which some decisions are discrete: unit commitment in power systems, capacity expansion, production planning with setups. The standard decomposition methods for multistage stochastic linear programs, nested Benders decomposition and stochastic dual dynamic programming (SDDP), approximate each stage's expected cost-to-go function from below by finitely many affine cuts. This works because those functions are convex and polyhedral. With integer variables the cost-to-go functions are in general nonconvex, and no family of affine cuts can be exact at every evaluated state.
Zou, Ahmed and Sun (Math. Program. 175 (2019) 461–502) observe that the obstruction disappears when the state variables passed between stages are binary. Their Theorem 1 (p. 467) states that every real function of binary variables is represented exactly, at all binary points, by a convex polyhedral function on the unit cube. This is the structural fact on which their stochastic dual dynamic integer programming (SDDiP) algorithm rests: the cost-to-go function only ever needs to be evaluated at binary states, and there a convex piecewise linear under-approximation can be tight. Mixed integer states are reduced to binary ones by binary expansion (§5 of the paper).
Let and write for the binary points, the vectors each of whose coordinates is or , and for the unit cube. Let be a real valued function defined on .
For a set in a real vector space and , a convex underestimator of is a function that is convex on the convex hull and satisfies for every (Definition 3, p. 496). The largest convex underestimator of on , that is, a convex underestimator with on for every convex underestimator , is the convex lower envelope of . In this mission .
A function is convex piecewise linear with finitely many linear pieces on if there are and with for all .
The proof works with the polyhedron of affine minorants of ,
the function , and the linear program defining together with its dual
where lists the binary vectors.
has a convex lower envelope, and every convex lower envelope of satisfies
for some finite family of affine functions.
The result. Theorem 1 is what makes exact cutting-plane approximation possible for nonconvex value functions of binary states. In SDDiP, the expected cost-to-go function of each node is approximated from below by affine cuts; Theorem 1 guarantees that a convex polyhedral function exists that agrees with the true value function at every binary state, so a finite collection of valid cuts can be tight at every state the algorithm visits. Without it, the finite convergence of SDDiP to an optimal policy (Theorem 2 of the paper, with Lagrangian cuts from Theorem 3) would have no target to converge to. The statement fails for general finite sets in place of : on with , no convex underestimator reaches .
Formalizing it. The result is proved in the paper; to our knowledge it has no machine-checked proof. A formalization produces the identity , a finite-dimensional LP duality statement for the pair –, and a characterization of the convex lower envelope on the cube, each of independent use for later formalizations of binary and mixed integer programming (Lagrangian relaxations, convex closures, extended formulations).
Two steps carry the weight. The first is that the maximum defining is attained, with finitely many pieces coming from extreme points of the unbounded polyhedron : this needs LP duality and the existence of an optimal vertex for a pointed polyhedron, neither of which is a one-line consequence of Mathlib's convexity library. The second is the domination step. The printed argument handles interior points of the cube by writing a convex underestimator as a supremum of affine minorants, and binary points separately; the remaining boundary points of (for example when ) are covered by the paper's conclusion but not by those two cases, and require an argument that works on all of . Exactness at binary points uses that a binary point is not a nontrivial convex combination of other points of the cube.
Points of are Fin n → ℝ with the componentwise order; is Set.Icc 0 1, the binary points are the vectors with every coordinate or , and is the dot product. is a total function on of which only the values at binary points enter any statement. Convexity of an underestimator is required on , exactly as in Definition 3, not on all of ; the identification of this hull with is milestone 1, not a definition. The value is allowed and no hypothesis on is added.
The readings of informal words are: "the convex lower envelope" is a predicate (largest convex underestimator on ), so Theorem 1 asserts its existence and then its properties for every function satisfying it; "convex piecewise linear with a finite number of linear pieces" is "the maximum of finitely many affine functions on the cube"; "max" over is an attained maximum, stated with IsGreatest; "min" in is stated with IsLeast. The proof's function is a real supremum, used only after its attainment is proved.
The convex lower envelope is not defined as (or as the value of ): under that definition convexity and piecewise linearity would be unfoldings, and Theorem 1's content, that the largest convex underestimator of Definition 3 has this form and is exact at binary points, would be lost.
A complete development needs: convex hulls of finite sets in , LP duality for a finite system of inequalities, extreme points of polyhedra and attainment of linear maxima at them, and Jensen's inequality for finite convex combinations. The cube identity and the LP duality milestone are reusable beyond this mission. Proofs of individual milestones, alternative proofs of Theorem 1 that bypass LP duality, and generalizations of the definitions are welcome.
Algorithms for smooth constrained optimization stop when an approximate optimality test passes. The tests used in practice are sequential optimality conditions: properties of a sequence of iterates rather than of the limit point alone. Every local minimizer satisfies them, with or without a constraint qualification. The price is that a point passing such a test need not satisfy the Karush–Kuhn–Tucker (KKT) conditions. A strict constraint qualification for a sequential condition is a property of the constraints at under which implies KKT for every objective function. The weaker this property, the larger the class of problems on which the condition certifies KKT points.
The Strong Approximate KKT (SAKKT) condition of Haeser and Schuverdt (J. Optim. Theory Appl. 149(3), 2011) asks for approximate Lagrange multipliers whose inequality part vanishes on every constraint that is strictly satisfied at the current iterate. It strictly implies the Approximate KKT condition (AKKT). Haeser and Schuverdt also showed that SAKKT is equivalent to the Approximate Gradient Projection condition AGP(0) of Martínez and Svaiter (2003). Andreani, Martínez, Ramos and Silva (Optimization Online 5197, 2015; Math. Oper. Res. 43(3), 2018, doi:10.1287/moor.2017.0879) determined the weakest strict constraint qualification associated with each of AGP, CAKKT, LAGP and SAKKT. For AKKT the answer, the Cone Continuity Property, had been found earlier (Andreani et al. 2016). This mission formalizes the SAKKT case, Theorem 4.5 of the preprint.
Consider the nonlinear program
with and continuously differentiable on . The feasible set is , and is the set of active inequalities. The KKT condition holds at for if there are and , with for , such that .
The linearized cone is , and is the polar of a set . For a convex set , the normal cone is defined for and is empty for . is the Euclidean projection onto a nonempty closed convex set .
For a point , the linearized set consists of the with
It keeps the inequalities that are active or violated at and drops those strictly satisfied at .
A feasible satisfies SAKKT for if there are , and , with whenever , such that
It satisfies AGP(0) for if there is with . The outer limit of a set-valued map is the set of limits of sequences with (1.6). The point is SAKKT-regular (Definition 4.3) if
For continuously differentiable constraints and a feasible ,
The forward implication says SAKKT-regularity is a strict constraint qualification for SAKKT; the backward one says it is implied by every such qualification.
Theorem 4.5 describes exactly the constraint systems on which a SAKKT sequence converging to certifies a KKT point, for every objective. Any constraint qualification already known to make SAKKT imply KKT implies SAKKT-regularity; at a point that is not SAKKT-regular, some linear objective has a SAKKT sequence converging to a non-KKT point. Because SAKKT is stronger than AKKT and AGP, its regularity condition is weaker than theirs, and Section 5 of the paper places it in the hierarchy of constraint qualifications next to AGP-regularity and CAKKT-regularity. By Proposition 4.4, SAKKT-regularity reads geometrically: the cone generated by the gradients of the equality constraints and of the inequalities that are active or violated at varies outer semicontinuously as .
The paper's result is proved, and no part of it is formalized on the platform. The mission adds machine-checked statements of the characterization and of the polyhedral convex-analysis facts behind it: the projection characterization of normal cones, the description of normal cones of at perturbed points, and the identification of with .
The forward direction passes to the limit in normal cones of sets that change with : the set of rows kept depends on the sign of at the moving point, not on the active set at . Projections land at , while SAKKT-regularity speaks of normal cones at , so the normal vectors must be transported from to ; this is Proposition 4.4, a Farkas-type statement for the cone of active rows. Moving between SAKKT and AGP(0) requires the Haeser–Schuverdt equivalence, which the paper cites rather than proves. The backward direction must build an objective function and a sequential certificate from an arbitrary element of an outer limit, which needs existence and nonexpansiveness of projections onto every . Finally, and the KKT multipliers are linked by Farkas' lemma for a finitely generated cone.
EuclideanSpace ℝ (Fin n); indices are Fin m and Fin p; gradients are Mathlib's gradient.All objects are defined in the namespace StrictCQ.SAKKT. Proofs of milestones 1, 2, 4 and 5 are reusable convex analysis beyond this mission; contributions toward a proof of the Haeser–Schuverdt equivalence (milestone 3) are welcome independently of the goal.
Algorithms for smooth constrained optimization stop when an approximate optimality test passes. The tests used in practice are sequential optimality conditions: properties of a sequence of iterates rather than of the limit alone. Every local minimizer satisfies them, with or without a constraint qualification, which makes them natural stopping criteria. The price is that a point passing such a test need not satisfy the Karush–Kuhn–Tucker (KKT) conditions. A strict constraint qualification for a sequential condition is a property of the constraints at under which implies KKT for every objective function. The weaker this property, the more problems on which the stopping test is guaranteed to certify a KKT point.
The Approximate Gradient Projection (AGP) condition was introduced by Martínez and Svaiter (2003) and is the natural stopping criterion of inexact restoration methods. It is strictly stronger than the Approximate KKT condition (AKKT), and it does not require Lagrange multiplier estimates. Andreani, Martínez, Ramos and Silva (Optimization Online 5197, 2015; Math. Oper. Res. 43(3), 2018, doi:10.1287/moor.2017.0879) determined the weakest strict constraint qualification associated with AGP and with several other sequential conditions. For AKKT the answer had been found earlier: the Cone Continuity Property of Andreani, Martínez, Ramos and Silva (2016). This mission formalizes the AGP case, Theorem 4.2 of the preprint, together with its linear-constraint variant, Theorem 4.6.
Consider the nonlinear program
with and continuously differentiable on . The feasible set is , and is the set of active inequalities. The KKT condition holds at for if there are and , with for , such that .
The linearized cone is , and is the polar of a set . For a convex set , the normal cone is defined for and is empty for . denotes the Euclidean projection onto a closed convex set .
For and a point , the linearized set of (4.2) consists of the with
A feasible satisfies AGP() for if there is a sequence with
The outer limit of a set-valued map is the set of limits of sequences with (1.6). The point is AGP-regular (Definition 4.1) if
For continuously differentiable constraints and a feasible ,
The forward implication says AGP-regularity is a strict constraint qualification for AGP; the backward one says it is implied by every such qualification.
The same characterization for the Linear AGP condition (LAGP), in which the linear constraints are kept exact and the iterates stay in the set they define. LAGP-regularity (Definition 4.4) is outer semicontinuity of relative to . Two further items accompany it: Proposition 4.1, the explicit form of , and the equality appended to Definition 4.4.
Theorem 4.2 gives the exact boundary of the problems on which an AGP-based stopping test certifies KKT points. Any constraint qualification already known to make AGP imply KKT, for instance the Cone Continuity Property, implies AGP-regularity. Conversely, at a point that is not AGP-regular some objective function has an AGP sequence converging to a non-KKT point. In Section 5 of the paper the theorem places AGP-regularity in the hierarchy of constraint qualifications, with the regularity notions for CAKKT and SAKKT next to it.
The paper's result is proved, and no part of it is formalized on the platform. The mission adds machine-checked statements of the characterization and of the convex-analysis facts it rests on: the projection characterization of normal cones, nonexpansiveness, and the polyhedral normal cone of as the polar of the linearized cone. These facts are reusable for any sequential optimality condition built on projections.
The forward direction passes to the limit in normal cones of sets that vary with and are evaluated at perturbed points , which may lie outside . For finite the inclusion of in fails at such points. It holds only for large, through a continuity argument on the inactive constraints. The backward direction must manufacture an objective function and an AGP sequence from an arbitrary element of an outer limit, which requires existence of projections onto every . The identification of with needs the localization of a polyhedral normal cone, and the link between and KKT multipliers is Farkas' lemma for a finitely generated cone.
EuclideanSpace ℝ (Fin n); indices are Fin m and Fin p; gradients are Mathlib's gradient.All objects are defined in the namespace StrictCQ.AGP. Proofs of the convex-analysis milestones are reusable beyond this mission.
The shortest-path problem in a graph of convex sets (SPP in GCS), introduced by Marcucci, Umenberger, Parrilo and Tedrake (arXiv:2101.11565, SIAM J. Optim. 2024), asks for a path through a directed graph whose vertices carry convex sets, together with a point in each visited set, minimizing a sum of convex edge lengths. It models motion planning around obstacles, hybrid-system control and other problems that mix a discrete choice with continuous positions. The paper formulates it as a mixed-integer convex program whose only nonconvexity, before relaxation, is a family of bilinear equalities that couple the continuous positions with the flow variables .
Section 7 of the paper studies the convex relaxation used for these bilinear equalities in isolation. Products of valid inequalities linearized by are the idea behind the McCormick envelope (McCormick 1976) and the Reformulation-Linearization Technique of Sherali and Adams. This mission formalizes the paper's result that the relaxation is exact at every extreme point of the polytope , which is the property that makes the mixed-integer formulation exact at binary flows.
Fix and . Points of are written .
Always , and is convex.
Let be compact and convex, let be a polytope and let be an extreme point of . Then for all and ,
The result. In the paper's mixed-integer program each vertex contributes a bilinear set in which is the convex set at and is the polytope of flows on the edges at . Binary flows corresponding to a path are extreme points of these polytopes, so Lemma 7.4 says that replacing by loses nothing at the integer points of the program. This gives the paper's second, geometric proof that its mixed-integer convex formulation is exact (Theorem 5.7). By Remark 7.5 the lemma also extends a known property of the first-level Reformulation-Linearization Technique for bilinear programs with binary variables from polytopes to compact convex sets . Proposition 7.1 is what makes the relaxation finite: it replaces the infinitely many inequalities of by one perspective-cone constraint per facet of .
Formalizing it. The results are proved on paper; none of them has a machine-checked proof. The formalization also settles the exact hypotheses. Three statements of this section are false as printed (see Formalization scope), and the corrected versions are posed here with the counterexamples recorded. The perspective cone, the cone of valid inequalities and their duality (Lemma 4.9) are general convex-analysis facts that recur across conic and disjunctive programming.
The direction is one line, since . The converse at needs three ingredients that are each standard and none of which is in Mathlib in this form.
Proposition 7.1 as an equality needs an affine Farkas lemma, and its printed proof skips the case of the valid inequality .
is Fin n → ℝ, inner products are dotProduct, is Z *ᵥ c and is Matrix.vecMulVec x y. Triples are (x, y, Z) in (Fin n → ℝ) × (Fin m → ℝ) × Matrix (Fin n) (Fin m) ℝ. A polytope is given by a finite family (c i, d i) over a Fintype index and the hypothesis Bornology.IsBounded; extreme points are Mathlib's Set.extremePoints ℝ, never a predicate defined through active constraints. The dual cone uses the pairing on the product, not an inner product.
Hypotheses added relative to the page, each with a counterexample to the printed form:
Several hypotheses are dropped where they are not needed, which strengthens the statements: nonemptiness of throughout, and boundedness and finiteness in the inclusion of Proposition 7.1 and in the active-constraint milestone.
Trivializing formalizations ruled out: quantifies over all of and is not replaced by (7.3) in the goal; is never allowed to be merely closed in the goal; the hypotheses of the goal are satisfiable (, is checked in Lean).
A complete development needs the bipolar theorem for closed convex cones in , the closedness of the cone over a compact convex set, the active-constraint characterization of extreme points, and a finite affine Farkas lemma. All of these are reusable well beyond this mission and are welcome as separate contributions.
Practical algorithms for nonlinear programming do not stop at an exact Karush–Kuhn–Tucker (KKT) point; they stop when an approximate stationarity test passes. Sequential optimality conditions formalize what such tests certify: they are properties of a feasible point phrased through sequences and multiplier estimates, and every local minimizer satisfies them without any constraint qualification. The question that links them back to classical theory is which conditions on the constraints guarantee that a point satisfying a sequential condition is in fact a KKT point. Andreani, Martínez, Ramos and Silva call these strict constraint qualifications and ask, for each sequential condition, for the weakest one.
For the Approximate KKT condition (AKKT) the answer, the Cone Continuity Property, was given by Andreani, Martínez, Ramos and Silva in 2016 (SIAM J. Optim. 26(1)). Section 2 of the present paper treats the Scaled-AKKT condition, which divides the stationarity residual by the size of the multipliers. This scaling appears in the stopping criteria of practical codes and in complexity analyses of nonlinear programming methods. Scaled-AKKT is weaker than AKKT, and the paper uses it as the first, self-contained example of the analysis it then carries out for AGP, CAKKT and SAKKT.
Fix and continuously differentiable functions , , where carries the Euclidean inner product and norm . The feasible set is , and is fixed. An index is active when .
For an objective , the point satisfies KKT if there are and with , for inactive , and .
Scaled-AKKT holds at for if there are sequences , and with , such that for every , and
where is the supremum norm of a multiplier vector.
The Mangasarian–Fromovitz constraint qualification (MFCQ) holds at if are linearly independent and some satisfies for all and for all active . The cone of active gradients is
For a constraint system and a feasible ,
The forward implication says that (2.3) is a strict constraint qualification for Scaled-AKKT; the backward implication says that every strict constraint qualification for Scaled-AKKT implies (2.3).
The result separates Scaled-AKKT sharply from AKKT. For AKKT the weakest strict constraint qualification (the Cone Continuity Property) is implied by many classical conditions, including CPLD and RCPLD. For Scaled-AKKT it is essentially MFCQ, a much stronger requirement. A stopping test of the Scaled-AKKT type therefore certifies a KKT point only under MFCQ, apart from the degenerate case of a full active cone. The other sections of the paper characterize the weakest strict constraint qualifications for AGP, CAKKT and SAKKT, using the same "iff over all objectives" template that this mission formalizes in its simplest form.
The paper's argument is a half-page sketch. A formalization makes explicit several points it leaves implicit: the role of the in the scaling factor, the vanishing of inactive multipliers forced by the complementarity limit, and the theorem of the alternative that converts failure of MFCQ into a nonzero solution of (2.4). None of these results is formalized on Prove2Me or, to our knowledge, in Mathlib.
The forward direction splits on whether the multipliers stay bounded, and the unbounded case requires normalizing by and extracting a convergent subsequence. Along that subsequence one must check that the normalized multipliers have supremum norm exactly one, that the normalized objective gradient tends to zero, and that inactive multipliers tend to zero; only then does the limit contradict MFCQ. The backward direction needs a theorem of the alternative (Motzkin or Gordan type) for the active gradients, together with linear dependence of the equality gradients. The paper uses it without stating it. It also needs a vector with . The printed text chooses , which has the wrong sign for the objective ; milestone 6 is stated for every , so the sign issue does not propagate.
is EuclideanSpace ℝ (Fin n); the constraints are index families Fin m → E → ℝ and Fin p → E → ℝ; gradients are Mathlib's gradient. Multiplier vectors live in Fin m → ℝ and Fin p → ℝ, whose Mathlib norm is the supremum norm, while residuals use the Euclidean norm. Standing hypotheses: every , is (the paper's "continuous first-order derivatives"), every objective in the goal is , and is feasible. The objective is quantified inside the equivalence, so the left side of the goal depends on , , alone. "or" is inclusive. The cone condition is equality of the cone with all of , not with its linear span. KKT carries both the sign condition and complementarity. MFCQ is defined in its primal (direction) form; defining it as "no nonzero nonnegative null combination" would make milestones 4 and 5 hold by definition, and that reading is excluded. Milestone 2 omits the MFCQ hypothesis present in the paper's sentence because the bounded case does not use it.
A complete development needs subsequence extraction in finite-dimensional spaces, continuity of gradients of functions, and a theorem of the alternative for finitely many vectors. The last two are reusable beyond this mission. Proofs of individual milestones are welcome independently.
Multistage stochastic linear programs model decisions taken over time under uncertainty: reservoir releases in hydro-thermal scheduling, production and inventory plans, capacity expansion. Their standard solution method, stochastic dual dynamic programming (SDDP, Pereira and Pinto 1991), approximates each stage's cost-to-go function from below by cutting planes. This gives a lower bound on the optimal value and a candidate policy, but no guaranteed upper bound: in the risk-neutral case the policy's expected cost is estimated by Monte Carlo simulation.
Planners who are averse to risk replace the expectation in each stage by a coherent risk measure (Artzner, Delbaen, Eber and Heath 1999), nested stage by stage so that the resulting dynamic risk measure is time consistent (Ruszczyński and Shapiro 2006). Under such a nested objective, simulation no longer estimates the cost of a policy: the nested risk of a policy is not an average over sampled scenarios. Philpott, de Matos and Finardi (2013) address this by an inner approximation of the cost-to-go functions from above, built from convex combinations of finitely many points with known upper bounds. Their Proposition 5 shows that the optimal value of the resulting first-stage problem bounds the nested risk-adjusted cost of the policy defined by the inner approximation. This gives a deterministic upper bound that complements the SDDP lower bound, and they apply it to the Brazilian hydro-thermal system.
There are stages. The decision at stage is ; are matrices and . Stage 1 is deterministic: . For a random outcome ranges over a finite set , independently of earlier stages, and enters through the right-hand side . The feasible set of stage given the previous decision is
A coherent risk measure maps random costs to and is subadditive, monotone (), positively homogeneous and translation equivariant (). Larger is worse: these are costs. Each stage carries a one-step coherent risk measure on random costs over . It is extended to costs in by whenever some outcome has infinite cost.
For fix points and numbers . The inner approximation is the lower boundary of the convex hull of the pairs :
which is off the convex hull of the points, with . The policy's stage problem (13) and the first-stage problem (8) are
The numbers are upper bounds when for all and . A policy defined by the inner approximation, , takes at each state and outcome an action solving (13), and a first-stage action solving (8). The actual risk-adjusted cost of over stages is
with no future term at . The nested risk-adjusted cost of the policy is .
The bound holds for every , every family of coherent , every choice of points satisfying the upper-bound property, and every minimizing selection .
Proposition 3, the risk-neutral case . Proposition 4, the subgradient rule for given by its dual representation. The existence of a policy , which shows that the hypotheses of the goal can be met.
Proposition 5 makes the inner approximation a certificate. Any policy computed by minimizing against has nested risk-adjusted cost at most , a number obtained by solving one linear program. Together with the lower bound from outer approximation it brackets the risk-adjusted optimal value. The gap then measures the quality of a risk-averse SDDP policy without simulation, which the nested objective does not allow. The bound covers every coherent nesting used in practice, such as mixtures of expectation and CVaR.
The results are proved in the paper. None of them is machine-checked. A formalization adds a precise account of the infinite values the paper does not discuss: infeasible stages, points outside the convex hull, and the extension of to . It also pins down the exact form of the upper-bound hypothesis the induction needs.
The obvious reading of the hypothesis on p. 16, " is an upper bound on " with the true value function , does not support the induction. The policy does not act optimally, so its cost can exceed the true value, and the inductive step compares with the policy's own stage value , not with . The hypothesis that works bounds the risk-adjusted optimal value of the policy's stage problem (13) at the points, which is what the paper's Upper Bound Computation actually computes.
The second difficulty is infinite values, which the paper never discusses. A risk measure is defined on real random costs, yet stage problems can be infeasible, is off a convex hull, and a convex combination may put zero weight on a point whose bound is . Every inequality of the paper has to be re-read in , and the extended-real arithmetic must not silently produce a value the paper does not intend.
Vectors are Fin n → ℝ, all stages share and , and costs that may be infinite are EReal. Minima are EReal infima, on an empty set. Attainment of a minimum is never built into a definition: the policy is a selection with a minimizing property, required at every state where the stage problem is feasible. Stages are natural numbers. Points and bounds are indexed by the stage of the function they define, so pts s j is and qv s j is . Stagewise independence is built in: ranges over whatever happened before.
Standing assumptions made explicit in the statements:
The risk measures act on real random costs and are extended by when some outcome has infinite cost. In Proposition 4, is given by its dual representation (10); the representation theorem itself is not part of the mission. The existence statement adds solvability of and boundedness below of the last-stage program, without which (8) or the last stage has no solution.
The goal is not to be trivialized. Its hypotheses mention neither nor the induction claim; the policy must minimize at every feasible state, not only along visited states; and the statement is for general and general coherent , not the expectation. The bound is trivially true when and is informative when lies in the convex hull of the stage-1 points.
A complete development needs:
The first two are reusable for any SDDP-type development. Proofs of the milestones in any order are welcome.
Multistage stochastic programs model sequential decisions under uncertainty: hydro-thermal scheduling, inventory and capacity planning, portfolio management. The dominant solution methods, Stochastic Dual Dynamic Programming (SDDP, Pereira and Pinto 1991) and its relatives CUPPS and DOASA, never compute the Bellman (future-cost) functions of the problem. Instead they build outer approximations of them by cutting planes: affine minorants obtained from the optimal values and Lagrange multipliers of one-stage subproblems. Practitioners run these methods on very large problems, so the question of whether, and in what sense, the approximations converge is of direct practical relevance.
Earlier convergence proofs (Philpott and Guan 2008; Shapiro 2011) rely on linear stage problems, where only finitely many distinct cuts can be generated and convergence is finite. Girardeau, Leclère and Philpott (Math. Oper. Res. 2015) prove convergence for convex stage problems, where infinitely many distinct cuts may appear and finite termination is lost. This mission covers the first half of that paper: the deterministic multistage problem (§2), whose proof contains the whole scheme of the argument. The stochastic scenario-tree version is the companion mission of this series.
Fix a horizon . States lie in and controls in ; values are in . The data are state sets , control multifunctions , stage costs , linear dynamics , a final cost and an initial state . The problem (1) is
The Bellman functions are on and elsewhere, with .
Assumptions (H₁) require to be a convex multifunction with convex compact values; and to be convex, lower semicontinuous and proper; and to be finite and Lipschitz on . They also require extended relatively complete recourse (ERCR): for some , on the enlarged set (a -neighbourhood inside the affine hull of ) the cost is finite and some admissible control leads into .
The cutting-plane method keeps approximations , starting from and with . At iteration it runs forward from . At each stage it solves the one-stage problem with in place of , which gives a minimizer , the optimal value and a Lagrange multiplier of the constraint . It then adds the cut
and moves to . The approximate cost-to-go is .
For every run of the method and every ,
The first limit says the computed decisions become optimal for the true Bellman functions; the second says the cuts become exact at the visited states. Nothing is claimed away from the generated trajectories.
In the order the proof uses them:
Companion items state that runs exist under (H₁) and give Kelley's cutting-plane lemma (Lemma 2.1), the warm-up result of §2.
Theorem 2.1 is a convergence guarantee for cutting-plane decomposition of nonlinear convex multistage problems. It does not depend on finitely many dual extreme points, so it covers problems with nonlinear convex costs and convex control constraints. The result is the template for the stochastic Theorem 3.1, which covers SDDP, CUPPS and DOASA as special cases of a general node-selection scheme. Along the way the paper isolates ERCR, a constraint qualification that is exactly what bounds the Lagrange multipliers and makes the cuts uniformly Lipschitz.
The result is proved in the paper; as far as is known it has no machine-checked proof. This mission produces a Lean statement of the deterministic algorithm, with extended-real Bellman functions, cut validity, and multiplier selection as a predicate on runs. It also supplies the statements of the reusable lemmas: marginal-function convexity, the monotone-minorant lemma, Kelley's method. Formal proofs of the milestones, alternative arguments, and explicit Lipschitz constants are all open.
The naive argument, "the approximations increase and are bounded by , so they converge", only gives pointwise convergence of to some limit below . It does not show that the limit equals at the states actually visited, and the visited states change from iteration to iteration. The proof must control cuts computed at one state when they are evaluated at another. This needs a uniform bound on the multipliers . That bound comes from ERCR (moving a distance in every direction of the affine hull stays where the cost is finite), together with Lipschitz continuity of on a compact set lying inside the relative interior of its domain. Without ERCR the multipliers can be unbounded and the argument breaks. A second difficulty is the backward induction itself: the conclusion at stage uses both limits at stage , and passing from to needs a compactness argument (Lemma 5.2).
States are EuclideanSpace ℝ (Fin d) and controls EuclideanSpace ℝ (Fin p); costs and value functions are EReal-valued. Convexity of an extended-real function means convexity of its epigraph. Minima are EReal infima ( over an empty set), with attainment stated separately. is extended by outside .
The Lagrange multiplier condition is encoded by (12): lies in the direction space of and is a subgradient, on , of the stage optimal value at . A run is a predicate on : any minimizer and any multiplier are allowed. The paper's iteration is Lean's k + 1.
Standing assumptions added to (H₁), all used by the paper's proofs:
Deviations from the page:
Limits are Tendsto … (𝓝 0) in EReal. There, convergence to forces the differences to be eventually finite, so a value of cannot make a limit hold for free. The goal's hypotheses are exactly (H₁) and the run predicate. Statements that only assert the existence of a good run, or bound instead of the cuts, are not formalizations of Theorem 2.1.
A complete development needs:
All three are reusable well beyond this mission. Proofs of any milestone are welcome, as are proofs of the companion items.
A firm that sells differentiated products sets more than prices. It chooses quality levels (features, materials, reliability) and the ancillary services that come free with a product, such as a factory warranty or free maintenance for a fixed period. Wang, Ke and Cui (SSRN 3766191; Manufacturing & Service Operations Management, 2022, doi:10.1287/msom.2020.0947) study the joint choice of price, quality and service duration when consumers choose according to the multinomial logit (MNL) model.
A firm allowed to make more decisions can never earn less: it may always ignore the extra instruments. The question this mission formalizes is what happens to consumers. A natural guess is that every new instrument lets the firm extract more of the consumers' surplus. Section 2.3 of the paper (Proposition 5) shows that under MNL demand this guess is wrong: consumer surplus also rises, so more control is a "win–win". The welfare measure is the logit consumer surplus of Anderson, de Palma and Thisse (Discrete Choice Theory of Product Differentiation, MIT Press, 1992).
The mission is the sixth of a series on the paper; each mission defines its own copy of the model in its own namespace.
There are products . Product has a price , a quality level and a service duration , which must lie in a fixed interval . The parameters are: , the consumers' sensitivity to quality; , the utility of one unit of service time; , so that producing one unit at quality costs ; and , so that service costs per unit of time. The sign of is free: higher quality may make service cheaper (), dearer (), or leave it unchanged ().
A consumer buys product with the MNL choice probability
where the is the outside option of buying nothing. With market size one, the firm's profit is
and the bracket is the markup of product . Consumer surplus is
Three problems are compared, at the same pre-determined qualities and durations :
Section 5.1 adds the manufacturer's short-term problem (10): qualities are fixed, and the firm also chooses which products to offer.
For every maximizer of each of the three problems,
The inequalities are weak; equality holds, for instance, when the pre-determined are already optimal.
The result separates two effects that are usually conflated. More instruments raise profit; Proposition 5 says that under MNL demand the extra profit comes from serving more consumers (fewer choose the outside option), not from extracting more surplus from each. Proposition 8 states the corresponding structure for a firm whose product designs are already fixed: offer everything, use extreme service durations, and keep markups equal across products.
The paper proves these results; none is formalized. A machine-checked development produces the welfare comparison together with the price step of the MNL multi-product pricing problem (equal markups at every optimum, uniqueness of the optimal profit as a fixed point) as reusable statements, and pins down the boundary cases of Proposition 8 that the printed statement leaves implicit.
The ordering of profits is immediate from the nesting of feasible sets. The obstacle is translating it into consumer surplus: consumer surplus is not monotone in profit along arbitrary price vectors, and the argument needs that at every maximizer of each problem all markups are equal to , with the optimal profit. That requires a global optimality analysis of the multi-product MNL pricing problem: the profit is not concave in prices, and both the uniqueness of the fixed point and the characterization of all maximizers (not only a stationary point) must be established. Comparing values with defined as the optimal profit, without linking them to the maximizers, proves nothing about consumer surplus.
Fin N (0-based); is arbitrary and is allowed. The outside option is the in the denominator, not a product.A formalization in which the maximizers are given by the paper's closed-form prices, in which are defined as optimal values and only is compared, or in which there is a single product, would make the goal trivial or different and is ruled out.
Contributions are welcome on the MNL price step (equation (17)), which is reusable for any multi-product logit pricing model, and on the per-product separation of the duration choice in Proposition 8.