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?
Zipf's law is the empirical observation that when a set of measured values is sorted in decreasing order, the value of the -th entry is often approximately inversely proportional to . Its best-known instance is word frequency in natural language: in the Brown Corpus the most frequent word, "the", accounts for nearly of all word occurrences, the second, "of", for slightly over , and so on. The same rank–size relation has been reported for city populations (Auerbach 1913), firm sizes (Axtell 2001), and many other data sets; it is named after the linguist George Kingsley Zipf (1932, 1935, 1949) and remains a central concept of quantitative linguistics (Piantadosi 2014).
In mathematical statistics the law is formalized as the Zipf distribution, a family of discrete probability distributions whose rank–frequency relation is an inverse power law, together with its relatives: the zeta distribution (Lotka's law), the Zipf–Mandelbrot law and the Yule–Simon distribution. Several generative explanations — random typing (Miller 1957, Li 1992) and preferential attachment — produce power laws by provable mechanisms.
Timeline of the results formalized here:
For a real exponent and an integer , the generalized harmonic number is
The Zipf distribution on elements with exponent assigns to the element of rank the probability
The classical Zipf law is . The source lists the parameter range , .
The Riemann zeta function is for . The Hurwitz zeta function is . The Zipf–Mandelbrot law on ranks with shift and exponent is with . The Yule–Simon distribution with parameter is , .
For :
That is, the generalized Zipf distribution extends to infinitely many items exactly when , in which case the normalizing constant becomes Riemann's zeta function.
The goal pins down exactly when "Zipf's law with infinitely many items" makes sense, and identifies the resulting distribution (the zeta distribution) with Riemann's zeta function. The milestones are the infobox facts that statisticians use when fitting Zipf models (CDF, mean, variance, entropy, mode), the log–log diagnostic used to test data against the law, two of the related laws the source lists (Zipf–Mandelbrot, Yule–Simon), one of the generative explanations (random typing), and the stated link to Benford's law.
The results are classical; the work is formalizing them. Most milestones are finite algebra about ; the goal, the Yule–Simon tail, the random-typing bound and the Benford connection need analysis.
The finite identities are routine once the support conventions are fixed. The analytic content is concentrated in four places. The goal needs the -series test and the identification of the limit with Mathlib's complex riemannZeta, which is defined by analytic continuation rather than by the series. The Yule–Simon tail needs the asymptotics . The random-typing bound requires controlling the rank of a word through the number of strictly shorter words, uniformly over every rank order compatible with the probabilities. The Benford connection requires comparing the harmonic sums over each block of integers with a fixed leading digit with , with an error that is negligible against .
Real.rpow); .zipfPMF N s k is defined for every natural and is outside the support . Statements that need a nonempty support assume .riemannZeta s of the real partial sums viewed as complex numbers, and divergence as Tendsto … atTop atTop. The source's parameter range is kept as a hypothesis.Benford's law (also the Newcomb–Benford law, or first-digit law) is the observation that in many real-life collections of numbers the leading significant digit is small far more often than a uniform guess would suggest: the digit leads about of the time and the digit less than of the time. Simon Newcomb noticed in 1881 that the early pages of logarithm tables were more worn than the later ones and proposed that digit leads with probability (Newcomb 1881); Frank Benford rediscovered the law in 1938 and tested it on 20,229 observations from 20 domains (Benford 1938). The law is used today as a screening statistic in forensic accounting, election forensics and the detection of fabricated scientific data.
Beyond empirical data, many classical integer sequences satisfy the law exactly, in the asymptotic sense: the powers of , the powers of any integer with irrational, the Fibonacci numbers and the factorials. These are theorems, and they are the core of this mission.
Timeline of the mathematical results formalized here:
Fix an integer base . Every real can be written uniquely as with significand and . The leading digit of is . Equivalently, with the fractional part,
More generally, the integer formed by the first significant digits is , and the -th significant digit is that integer for reduced modulo .
The Benford probabilities are
A real sequence satisfies Benford's law in base if for every digit
A positive random variable satisfies the strong form of the law if is uniformly distributed on .
For every natural number such that is irrational, the sequence satisfies Benford's law in base :
The goal is the cleanest instance of the mechanism behind Benford's law: a sequence obeys the law exactly when the fractional parts of its base- logarithms are equidistributed modulo , and for those fractional parts are the multiples reduced modulo . The milestones cover the rest of the mathematical content of the article: the definition and normalization of the law, the derivation from a log-uniform significand, the generalization to several leading digits and to the -th digit, scale invariance, the continuous-time exponential case, and the negative results for and .
All of these results are classical and proved in the literature cited above; the work here is formalizing the known proofs. Related entries already on the platform (a leading-digit / fractional-part characterization and an equidistribution-based Benford criterion, stated with different definitions) may be reusable by solvers.
The goal and milestones 5–7 reduce to equidistribution of a sequence modulo . For and Fibonacci numbers this is Weyl's equidistribution theorem for irrational rotations (Fibonacci additionally needs Binet's formula and an error term that vanishes). Factorials are harder: is not a linear sequence, and the classical proof combines Stirling's formula with an equidistribution criterion for sequences whose differences vary slowly. The scale-invariance theorem requires a Fourier-analytic argument on the circle . The negative results require showing that a counting ratio oscillates, which needs explicit lower and upper estimates along two subsequences.
Real.logb takes , so negative numbers get the leading digit of their absolute value, and the junk value occurs. Every statement either restricts to positive (or nonzero) inputs or only uses positive sequences.Reusable infrastructure: leading-digit and significand API, equidistribution of modulo (Weyl), Benford criteria via equidistribution. Contributions toward a general "equidistributed Benford" lemma are welcome.
Why is general relativity not a renormalizable quantum field theory? The textbook answer is perturbative: Newton's constant has negative mass dimension, so the gravitational coupling is irrelevant and loop divergences cannot be absorbed into finitely many counterterms. That argument can in principle be evaded (Weinberg's asymptotic safety). Shomer's note (arXiv:0709.3555), following Banks and Aharony–Banks, gives a non-perturbative, thermodynamic argument instead: the very-high-energy spectrum of any renormalizable -dimensional QFT is that of a -dimensional conformal field theory (CFT), whereas the high-energy spectrum of gravity is dominated by black holes, whose Bekenstein–Hawking entropy grows with energy in a way no CFT can match.
For every spacetime dimension , every and every CFT datum ,
Here means bounded above and below by positive multiples of each other for all large ; this is how the paper's "" is read.
Eq. (29) (the elimination of ), Eq. (30), Eq. (32) exactly, footnote 26 (exponent comparison), Eq. (34) asymptotically, the AdS mismatch with a -dimensional CFT, and the AdS match with a -dimensional CFT.
The goal is the precise mathematical content of the paper's one-line argument: once the black-hole entropy formula and the CFT scaling law are fixed, their large-energy growth exponents are incompatible. The physics inputs (that a renormalizable QFT flows to a CFT in the UV, that black holes dominate the gravitational density of states, the Bekenstein–Hawking formula) are modelling assumptions, encoded as definitions; the mission formalizes the asymptotic analysis that turns them into a contradiction, not the physics itself.
Mathematically elementary but fiddly: the horizon radius is defined implicitly as the largest positive zero of , so one must solve (exactly in flat space, asymptotically in AdS, where ), handle real powers, and compare asymptotic classes with distinct exponents.
All statements live in namespace GravityNonRenorm and import one definition file. The unit-sphere volume is the closed form . Horizon radii are sSup of the set of positive zeros of (junk value when that set is empty, e.g. for ); all claims are asymptotic as or assume , so the junk value is never used. Dimensions are natural numbers; for flat-space statements, for AdS, for CFT statements.
Fick's laws of diffusion, posited by Adolf Fick in 1855, are the basic constitutive and evolution laws for the transport of mass by diffusion. The first law states that the diffusive flux is proportional to minus the concentration gradient, ; the second law is the resulting evolution equation for the concentration,
They are the standard model for diffusion in solids, liquids and gases (in the absence of bulk flow), and are used to model transport in foods, neurons, biopolymers, pharmaceuticals, porous soils, nuclear materials and semiconductor doping. Mathematically, the second law is the heat equation with the thermal diffusivity replaced by the diffusion coefficient .
This mission formalizes the mathematical content of the Wikipedia article Fick's laws of diffusion: the derivation of the second law from the first, the steady state, the fundamental solution, the error-function solutions for a constant source, and the mean-squared-displacement law.
A concentration is a real function of position and time ; a flux is a real function . The diffusion coefficient is a constant . For the diffusion kernel is
and in space dimensions
The complementary error function is .
For , solves for , has for every , and satisfies
for every bounded continuous and every .
The fundamental solution is what makes the second law usable: the solution of the one-dimensional diffusion problem with bounded continuous initial data is the convolution of the data with , and the erfc profiles and diffusion length quoted throughout applications are derived from it. The mean-squared-displacement law connects the macroscopic diffusion coefficient to the microscopic Brownian motion of particles.
All statements are classical and proved in the literature; the task here is to formalize them. Mathlib provides the Gaussian integral but has no error function and no development of the one-dimensional diffusion equation, so the mission also produces reusable infrastructure (erfc and its derivative and limits, Gaussian moments in , the approximate-identity property).
The individual computations are routine on paper; the formal difficulty lies in rigor that the article leaves implicit: differentiating the kernel in both variables only on , justifying limits of parameter-dependent integrals as (dominated convergence for the point-source property), computing the second moment of an -dimensional Gaussian on Euclidean space, and building erfc from scratch, including its derivative and its limits at .
All objects are real-valued; derivatives are Mathlib's deriv (which is at non-differentiable points), integrals are Lebesgue integrals, and limits as use the right-neighbourhood filter. Every statement about the kernel or erfc profiles assumes and evaluates the PDE only at , so junk values of square root and division never matter. The steady-state milestone assumes regularity, without which deriv would admit non-smooth "solutions" such as . is EuclideanSpace ℝ (Fin n). Physical parts of the article (Stokes–Einstein relation, Maxwell–Stefan, sorption kinetics, approximations) are out of scope.
Okun's law is an empirically observed relationship between unemployment and losses in a country's production, named after Arthur M. Okun, who proposed it in 1962 (Okun 1962). It appears in two standard forms. The gap version relates the output gap to the unemployment gap; the difference (or growth-rate) version relates year-to-year changes in output to year-to-year changes in unemployment. Macroeconomics textbooks (Abel & Bernanke 2005) present the gap version and then derive the difference version from it by a short chain of algebraic manipulations followed by two approximations. The empirical validity of the law is disputed and is not the subject of this mission; the subject is the internal mathematics of the derivation.
Time is discrete: years are indexed by . All quantities are real-valued time series:
For a series write for its annual change and for its growth rate from year to year . The gap version of Okun's law in year is
The source's final formula is , where is the growth rate of full-employment output. The goal states the derivation exactly: if the gap version holds in years and (with positive , , ), the natural rate does not change () and potential output grows at rate (), then
The last term is precisely the error made by the source's approximation .
The derivation is the textbook justification for using the difference form, which is the version actually estimated by regression. Making every step exact shows exactly which hypotheses (positivity of output, the gap law in two consecutive years with the same coefficient, a constant natural rate) and which approximation (the factor ) the difference form rests on, and gives the size of the neglected term. The result is elementary and known; what the mission adds is a machine-checked, approximation-free account of the derivation.
The algebra is elementary. The care required is in bookkeeping: the source uses "" in two places and silently assumes all denominators are nonzero. A faithful statement must replace each "" either by an explicit hypothesis or by an explicit remainder term, and must state the positivity assumptions that make the divisions meaningful.
Series are functions ; ; the growth rate is (Lean's real division returns when dividing by , so positivity hypotheses on , , are stated explicitly wherever a division by them occurs). The gap law is a predicate on one year with a fixed coefficient ; all statements use the gap law in exactly the two years and with the same . The source's approximations and are taken as exact hypotheses, and the approximation is replaced by an explicit remainder term, so the goal is an exact identity rather than a vague approximation. The shared definitions live in one definition file (OkunsLaw_defs).
Gresham's law is the monetary principle usually summarised as "bad money drives out good": when two kinds of coin circulate side by side and the law obliges everyone to accept both at the same face value, the coin whose metal is worth more tends to vanish from circulation, while the debased coin stays in use. The principle was named in 1857–58 by Henry Dunning Macleod after Sir Thomas Gresham, who explained to Elizabeth I in 1558 why the English coinage had deteriorated after the Great Debasements of Henry VIII and Edward VI. It appears much earlier in Aristophanes' The Frogs (405 BC), in Nicole Oresme's treatise on money (c. 1350–1357), in a 1472 Venetian report ("the bad money will chase out the good"), and in Copernicus' Monetae cudendae ratio (1519/1528), whence the alternative name Gresham–Copernicus law. The source of this mission is the Wikipedia article.
Modern instances quoted by the article include the disappearance of 90% silver U.S. half dollars after the Coinage Act of 1965, the 2007 U.S. ban on melting one- and five-cent coins, and Britain's drift to a de facto gold standard after Isaac Newton fixed the guinea at 21 shillings in 1717. The article also records the reverse phenomenon, Thiers' law (named by Peter Bernholz): without effective legal tender laws, good money drives out bad money once the bad money becomes nearly worthless.
A coin is described by two real numbers: its face value , the nominal value at which legal tender law requires it to be accepted, and its melt value , the market value of the metal it contains (its intrinsic or commodity value). "Good money" has a melt value close to its face value; "bad money" has a melt value considerably below its face value while being accepted at the same face value.
A holder owns a finite wallet of coins, indexed by a type , with face values and melt values . Legal tender at equal value means that all coins of the wallet carry the same face value. Because creditors must accept coins at face value, a set is a legal payment of a debt when . The holder "prefers to save the intrinsically more valuable money": a legal payment is optimal when no other legal payment of the same debt leaves the holder with more intrinsic value, i.e.
Without legal tender law, a seller values coins only by their metal, and accepts at market value a set of coins for a price exactly when .
For the 1717 episode, the home legal rate is shillings per guinea and abroad the gold of one guinea costs the silver of shillings. One arbitrage round turns shillings into the gold of guineas abroad, which is coined at home and exchanged back at the legal rate for shillings.
If the wallet is split into good coins and bad coins, every bad coin has strictly smaller melt value than every good coin, and all coins carry the same face value, then in any optimal payment
a good coin is handed over only once every bad coin has been handed over. Equivalently, as long as the holder retains a bad coin, no good coin circulates.
The goal is the decision-theoretic core of the article's "Theory" section: legal tender laws act as a price control fixing the exchange ratio of coins with different intrinsic content, and a holder who keeps the more valuable coins therefore pays with the less valuable ones. The milestones isolate the article's worked example (sixpences and pennies), the exact optimality condition behind it, the reverse regime (Thiers' law, and Mundell's reformulation "bad money drives out good if they exchange for the same price"), and the bimetallic arbitrage that drained silver from Britain after 1717.
The statements are elementary; the value of the mission is a precise, checked account of which hypotheses carry the law — equal face value enforced by law, and a strict ranking of intrinsic values — so that the informal statement becomes an exact theorem with its conditions visible.
The obvious argument is a single swap: exchange a paid good coin for a retained bad coin. The swap keeps the payment legal only because all coins carry the same face value; with unequal face values it changes the amount paid and the argument fails. The exchange characterization also needs positive face values: with zero face values every subset is a payment of , and the condition "paid coins are no more valuable than retained ones" no longer implies optimality.
Face and melt values are real numbers; wallets are finite sets (Finset) of indices, so distinct coins with identical values are distinct elements. Payments must match the debt exactly (no change is modelled inside a single payment; the shopkeeper giving change is another payer facing the same problem). Optimality compares retained intrinsic value among legal payments of the same debt from the same wallet. The arbitrage round ignores transport and minting costs. Melting, hoarding and export are not modelled as separate actions; the formal content is the payment choice, the market-value acceptance rule, and the arbitrage round.
The goal is not vacuous: optimal payments exist for every attainable debt (the wallet is finite), and the hypotheses are satisfiable, e.g. by one good and one bad coin of face value and melt values and .
All declarations live in the namespace GreshamLaw, in one definition file GreshamLaw_Model.
Say's law, or the law of markets, is the classical claim that production is the source of demand. Jean-Baptiste Say wrote in his Treatise on Political Economy (1803) that "a product is no sooner created, than it, from that instant, affords a market for other products to the full extent of its own value". The doctrine was restated by James Mill ("the production of commodities creates ... a market for the commodities produced") and David Ricardo ("demand depends only on supply"), and it was a key element of the framework of macroeconomics from the mid-19th century until the 1930s.
Its best-known consequence is that a general glut — a widespread excess of supply over demand for all goods at once — cannot occur: if one good remains unsold, some other good must be in short supply. This claim was disputed from the start. Thomas Malthus reported evidence of general gluts; John Stuart Mill argued that during a general glut there is excess demand for money, and rescued the no-glut principle by counting money as one of the commodities. During the Great Depression, Keynes argued that Say's law is simply not true, and Keynesian, post-Keynesian and Marxian critics locate its failure in the hoarding of money. Krugman called it "at best, a useless tautology when individuals have the option of accumulating money rather than purchasing real goods and services".
The debate turns on an accounting fact that is easy to state and easy to misstate: what exactly follows from budget constraints alone, and what changes when money can be held rather than spent. This mission pins that down formally.
Fix a finite set of agents and a finite set of goods. A price vector is . Agent brings the bundle to market (his supply) and plans to buy the bundle (his demand). The market value of a bundle is
and the aggregate excess demand for good is .
With at least one good, strictly positive prices and Say's budget principle,
The goal and milestones 1–2 isolate the content of Say's law as the article's "modern way of expressing" it: in a pure barter setting the budget constraints alone force gluts and shortages to cancel in value. Milestones 3–5 make the classical and Keynesian objections precise: once money can be held, the same constraints identify a general glut with an excess demand for money (Mill), and they no longer exclude a general glut (Keynes, Krugman, Marx's C–M–C critique). Together they separate what is an accounting identity from what is a behavioural assumption (no hoarding), which is the point at issue in the historical debate. The results are classical; the contribution here is a machine-checked, assumption-explicit statement of each.
The mathematics is elementary; the difficulty is entirely in stating the claims faithfully. The informal phrase "supply creates its own demand" is ambiguous between an identity about values and a claim about quantities of each good, and it silently requires positive prices and a nonempty set of goods — without them "every good is in excess supply" can hold vacuously or with no value consequence. The monetary results must keep money out of the set of goods, so that "an excess of all other commodities" means what Mill meant.
Goods and agents are finite types; quantities, prices and money balances are real numbers with no sign restriction (supplies and demands may be read as gross amounts or as net trades). Positivity of prices and nonemptiness of the set of goods (or agents) are explicit hypotheses exactly where they are needed. Prices are taken as given; no utility maximisation, equilibrium existence, price adjustment or dynamics is modelled, so statements about full employment, persistence of depressions or the speed of price adjustment are out of scope. The definition file SaysLaw_Model is shared by every statement.
The BCS theory of Bardeen, Cooper and Schrieffer (1957) is the microscopic theory of conventional superconductivity in metals; its authors received the 1972 Nobel Prize in Physics. Its most quoted quantitative predictions are universal numbers: in the weak-coupling limit the zero-temperature energy gap and the transition temperature are related by , the gap closes as , and the specific heat jumps by at . These numbers are what experiments compare against, and they follow from a single scalar integral equation, the BCS gap equation. This mission formalizes that mathematical core, following the section Erfolge der BCS-Theorie of the German Wikipedia article BCS-Theorie.
Timeline (as summarized in the source):
Fix the Boltzmann constant , the Debye energy (called hbarOmegaD in Lean) and the dimensionless coupling (called coupling), where is the attractive pairing potential and is half the electronic density of states at the Fermi energy. With the quasiparticle energy define
The zero-temperature gap is the positive solution of ; the critical temperature is the positive solution of ; and for the gap is the positive solution of . The Fermi–Dirac function is , and .
with the Euler–Mascheroni constant. The source writes ; both equalities are weak-coupling asymptotics, so the goal is stated as a limit at fixed , .
The universal ratios are the standard quantitative test that separates weak-coupling (BCS-like) superconductors from strong-coupling ones; deviations from and are used to diagnose strong electron–phonon coupling. Mathematically, each statement is an assertion about a parameter-dependent integral equation and its asymptotics as , with the Euler–Mascheroni constant and arising from the asymptotics of and from a Sommerfeld-type expansion near . These results are classical in the physics literature; the mission aims at a machine-checked derivation of the textbook constants from the gap equation, together with reusable lemmas on monotone parameter-dependent integrals.
The statements reduce to an explicit antiderivative. The finite-temperature statements do not: and are defined only implicitly, so the asymptotics require a uniform expansion . The near- and specific-heat statements additionally concern the behaviour of at the boundary point , where itself is not differentiable, and the evaluation of the resulting coefficient in the limit .
sSup) of the corresponding positive solution sets, so they equal when no positive solution exists; existence and uniqueness are separate milestones. In particular for .riemannZeta 3.Dynamic stochastic general equilibrium (DSGE) models are the standard framework used by central banks and fiscal authorities for policy analysis and forecasting (Wikipedia overview). The models used for monetary-policy analysis are built from three interrelated blocks — demand, supply and a monetary-policy rule — that jointly determine output, inflation and the nominal interest rate. The canonical small-scale instance is the three-equation New Keynesian model (Woodford 2003; Galí 2008; Clarida, Galí and Gertler 1999).
A basic question about such a model is whether it pins down a unique equilibrium path at all. If many bounded paths solve the model, the model makes no definite prediction and expectations can become self-fulfilling. The answer for the three-equation model is the Taylor principle: the interest-rate rule must respond to inflation strongly enough.
Timeline. Blanchard and Kahn (1980) gave the eigenvalue-counting criterion for existence and uniqueness of bounded solutions of linear rational-expectations models. Kydland and Prescott (1982) started the real-business-cycle/DSGE programme. Rotemberg and Woodford (1997) introduced the New Keynesian DSGE framework. Bullard and Mitra (2002) derived the explicit determinacy condition for the model with a contemporaneous Taylor rule, presented in textbook form by Galí (2008, Ch. 3).
Time is discrete, . All variables are deviations from the zero-inflation steady state: is the output gap, inflation, and the nominal interest rate. The parameters are (inverse elasticity of intertemporal substitution), (discount factor), (slope of the Phillips curve), and the policy coefficients .
A triple of real sequences is an equilibrium if for every
The demand equation is the log-linearised consumption Euler equation, which equates marginal utility of consumption today with discounted marginal utility tomorrow. The model is determinate if the zero path is its only equilibrium in which , and all stay bounded.
For , , , :
The result itself. The Taylor principle is the standard criterion for whether an interest-rate rule yields a well-defined equilibrium in New Keynesian models, and it is the first property checked when a policy rule is proposed. The determinacy region it describes is the starting point for the analysis of optimal policy and of learnability (Bullard and Mitra 2002).
Formalizing it. The result is classical and proved on paper. This mission formalizes the known argument. The mission produces a reusable Lean definition of the basic New Keynesian model, a general lemma on bounded orbits of linear recursions (which applies to any linear rational-expectations model with only forward-looking variables), and a formal Schur–Cohn criterion for real quadratics.
The economic content is elementary, but the obvious argument skips the hardest step. Textbook treatments state "determinacy holds iff both eigenvalues lie outside the unit circle" without proof, and the equivalence between "no nonzero bounded solution" and an eigenvalue condition has to be established for real sequences while the eigenvalues may be complex. In particular the converse direction needs a real bounded solution built from a complex eigenvector, and the boundary case of eigenvalues on the unit circle must come out on the non-determinate side. The parameter translation also has to handle complex-conjugate eigenvalues, not only real ones.
DSGE. Contributions of general linear-recursion and polynomial-root lemmas are welcome.The Titius–Bode law is an empirical rule, published in the eighteenth century by J. D. Titius and J. E. Bode, for the semi-major axes of the planets: in units in which the Earth's semi-major axis is , the planets lie near with . It anticipated the positions of Uranus (1781) and Ceres (1801), failed for Neptune (1846), and has since become a standard example of how a numerical pattern can fit data without a physical mechanism. Dermott's law (S. F. Dermott, 1968) is the analogous power law for the orbital periods of the major satellites of Jupiter, Saturn and Uranus.
Much of the debate about such rules is quantitative rather than physical. The Wikipedia article on the law records, in a footnote to its data table, the observation that because consecutive predicted distances roughly double, an arbitrary planet may be found within to of one of the predicted positions. In other words, the agreement of any single body with the rule at that level carries no information. This mission formalizes that observation and the elementary arithmetic of the law as stated in the source.
Timeline (as recorded in the source). Gregory (1702, 1715) and Wolff (1723–24) give the sequence ; Titius (1766) and Bode (1772) publish the rule; Uranus (1781) and Ceres (1801) fit it; Neptune (1846) does not; Blagg (1913) and Richardson (1945) replace the ratio by about ; Dermott (1968) proposes the period law for satellite systems; Nieto (1970, 1972) reviews the subject.
For a formal exponent put . The Titius–Bode distance in astronomical units is
so , , , . The same numbers appear in three other guises in the source: the original form (Earth ), the form (Earth ), and the canonical form for . The relative deviation of an observed value from a predicted value is , which the source reports as a percentage.
Dermott's law models the period of the -th satellite as . Kepler's third law makes the semi-major axis proportional to the power of the period, .
Every distance of at least au lies within to of some Titius–Bode position. The lower limit is exactly where the statement begins to hold: below it no predicted position is close enough. The source says "an arbitrary planet"; the formal statement makes the range explicit.
The goal makes precise why a fit of a single body to the Titius–Bode rule within tens of percent is weak evidence: the predicted positions are spaced so that the whole half-line is covered by such bands. The resonance milestone gives the corresponding figures for a period commensurability, and the Dermott milestone connects period power laws to Titius–Bode-type distance laws, as the source asserts.
All results are elementary and none is open. The value of the mission is a checked, unambiguous record of the arithmetic claims in the source, including one place where the source's formulas disagree: the "recursive form" with does not reproduce the canonical form index-for-index but is shifted by one (milestone 2). No machine-checked version of these statements is known to exist on the platform.
There is no deep obstacle. The covering argument needs care in two places: the first step of the rule () is not a doubling, and the generic doubling lemma must locate the first term that exceeds without assuming monotonicity. The resonance milestone requires certified numerical bounds on the irrational numbers and that are tight enough to fix the second decimal place of a percentage.
Distances, periods and deviations are real numbers. The exponent set is encoded as the natural numbers with a bottom element adjoined, and is defined to be . The relative deviation is the plain quotient ; every statement only evaluates it at positive . Percent figures from the source (, ) are stated as "within percentage points", i.e. correct to the two decimals printed. Kepler's law enters only as the hypothesis with ; no orbital mechanics is formalized. The doubling lemma is stated for an arbitrary real sequence and is reusable for any Titius–Bode-type rule.
Trivializing encodings are ruled out: the goal is not stated for an empty or bounded range of , the predicted set is the full image of the rule, and the deviation band is the one printed in the source.
The Hartree-Fock method approximates the ground state of an interacting many-electron system by the best single Slater determinant. It is the starting point of essentially all of quantum chemistry and of mean-field theories in condensed-matter physics: post-Hartree-Fock methods (configuration interaction, coupled cluster, perturbation theory) expand around it, and its orbital energies are the standard first estimate of ionization and excitation energies. E. Koch's lecture notes Mean-Field Theory: Hartree-Fock and BCS (Jülich Autumn School on Correlated Electrons, 2016) derive the method entirely within second quantization: Slater determinants are products of creation operators acting on a vacuum, variations are generated by one-body unitaries , and the stationarity condition becomes an algebraic statement about matrix elements. The central result of the Hartree-Fock section is the Brillouin theorem: a Slater determinant is stationary exactly when the Hamiltonian does not couple it to its single excitations.
Timeline of the ideas involved: Hartree introduces the self-consistent field (1928); Fock and Slater add exchange through antisymmetrized wave functions (1930); Koopmans relates orbital energies to ionization energies (1934); Brillouin formulates the single-excitation condition (1934); Thouless gives the representation of Slater determinants by exponentials of one-body operators (1960).
Fix orthonormal reference orbitals ; an orbital is a coefficient vector with . The Fock space has orthonormal basis , (the set of occupied orbitals). The creation operator maps to if and to otherwise; the annihilation operator is its adjoint, and for a general orbital . The vacuum is .
The Slater determinant of orbitals is . A one-body operator with matrix is . For a hermitian the operators map Slater determinants to Slater determinants, and the energy functional along such a variation is
For the concrete Hamiltonian of Sec. 3.2,
the Fock matrix of the determinant with occupied reference orbitals is , with diagonal entries the orbital energies .
For a hermitian and orthonormal ,
It asserts no specific Hamiltonian, no particle number and no basis choice; it is the basis-independent form of the source's condition (63).
The milestone list follows the source's own steps: the anticommutation relations (15); the overlap formula (7)/(46); the action of , on a determinant (42); the one-body density matrix (43) and Wick's theorem (45); the transformation of vacuum and creators under (57), (59); the first-order variation (61)–(62). For the two-body Hamiltonian it adds the Fock-matrix form of the Brillouin condition (64), the Hartree-Fock energy, Koopmans' theorem (66) and the electron-hole excitation energy (67).
The Brillouin theorem turns the nonlinear variational problem over all Slater determinants into a condition on finitely many matrix elements; for a two-body Hamiltonian it says that the occupied–virtual block of the Fock matrix vanishes, which is the self-consistency condition solved by every Hartree-Fock code. Koopmans' theorem and the particle-hole formula give the physical interpretation of the orbital energies.
All results are classical and proved in the source and in standard textbooks. What this mission adds is a machine-checked account of second quantization on a finite orbital basis: the anticommutation relations, determinant overlaps and Wick's theorem for Slater determinants are reusable for any later formalization of configuration interaction, coupled cluster or BCS theory.
The source's arguments are short manipulations of operator identities, but each hides bookkeeping that is easy to get wrong: fermionic signs when operators are reordered, the identification of Slater determinants with ordered products of creators, and the Laplace expansion behind Wick's theorem. The variational step requires differentiating a matrix exponential on Fock space and identifying the derivative with a commutator. The direction from the Brillouin condition back to stationarity needs the hermiticity of and a decomposition of an arbitrary hermitian into occupied–occupied, virtual–virtual and occupied–virtual blocks; the first two blocks act on only by a scalar. The Fock-matrix milestones additionally need the exchange symmetry of two-body matrix elements stated in Sec. 2.3.2; without it the stated formulas fail.
Fock space over orbitals is represented concretely: vectors are functions on Finset (Fin K) and operators are complex matrices indexed by Finset (Fin K). Creators carry the sign , so ordered products of creators of increasing orbitals give . All quantities are complex; the exponential is NormedSpace.exp; stationarity is HasDerivAt … 0 0 for a function . Orthonormality of the occupied orbitals is an explicit hypothesis wherever the source assumes it. The source works with a possibly infinite orbital basis; here the basis is finite, as in the variational setting of its Sec. 3.
The equivalence in the goal cannot be satisfied vacuously: hermiticity of and orthonormality of the orbitals are both satisfiable, and both sides quantify over all admissible , respectively all occupied and virtual orbitals.
Two printed formulas are not taken verbatim: Eq. (60) lacks the minus sign in the exponent and is omitted, and Eq. (61) prints the first-order commutator in the opposite order; the milestone records the correct derivative , which leaves (62) unchanged.
Contributions welcome: a general API for products of creation and annihilation operators in this model (sign lemmas, normal ordering), which all milestones share.
The zeroth law of thermodynamics is the principle that makes temperature a meaningful notion. In the formulation of Fowler and Guggenheim, and in the standard textbooks of Guggenheim, Buchdahl and Bailyn, it states: if two systems are both in thermal equilibrium with a third system, then they are in thermal equilibrium with each other. It was named by R. H. Fowler in the 1930s, after the first, second and third laws were already established, because it is logically prior to them: it is what justifies the use of thermometers and the assignment of a single "temperature" to each equilibrated system.
Mathematically, the content of the law is a statement about a binary relation. Together with the convention that each system is in equilibrium with itself, it turns thermal equilibrium into an equivalence relation, and an equivalence relation is exactly what is needed to "tag" every system with a label (an empirical temperature) so that two systems are in equilibrium precisely when their labels agree. This mission formalizes that chain of reasoning as presented in the Wikipedia article Zeroth law of thermodynamics.
Let be a set (a type) whose elements are thermodynamic systems, each in its own state of internal equilibrium, and let be a binary relation on ; reads " is in thermal equilibrium with ". No further structure is assumed.
This is the "existence of temperature" postulate of Fowler and Guggenheim: the condition for thermal equilibrium is equality of a single-valued function of the state. The labelling set is left arbitrary, as in the source ("the labeling may be quite arbitrary").
The result is the logical foundation of thermometry: it is what allows any one system to serve as a thermometer for all others, and it underlies every empirical temperature scale and, via the second law, the absolute scale. The statements here are elementary and are known; the value of the mission is a clean, reusable formal vocabulary for thermal equilibrium (the two Euclidean forms of the law and the notion of an empirical temperature) on which formalizations of later parts of axiomatic thermodynamics can build.
None of the steps is deep. The point that needs care is that the zeroth law alone does not give an equivalence relation: reflexivity is an additional convention, and the source stresses that a reflexive and transitive relation is not automatically symmetric. Each milestone therefore states its reflexivity hypothesis explicitly.
Systems form an arbitrary type S (possibly empty), and thermal equilibrium is an arbitrary relation TE : S → S → Prop. Equivalence relations are Lean's Equivalence; partitions use Mathlib's Setoid.IsPartition. The labelling type of an empirical temperature lives in the same universe as S. The richer structure of real-valued temperature (ordering into "hotter" and "colder", continuity) is explicitly not part of the zeroth law according to the source and is out of scope. Definitions ZerothLaw, ZerothLawPlanck, IsEmpiricalTemperature are shared by all statements, in the namespace ZerothLawThermo.
The conservation of momentum, of mechanical energy and of mass are the three bookkeeping laws on which elementary Newtonian mechanics and continuum mechanics rest. In Newtonian mechanics each of them is not an extra postulate but a theorem: momentum conservation follows from Newton's second and third laws, conservation of mechanical energy follows from Newton's second law when the forces are derived from a potential, and conservation of total mass in a fluid follows from the continuity equation. This mission asks for machine-checked proofs of these classical derivations, in the form in which they appear in the encyclopedia articles Momentum, Conservation of energy and Conservation of mass.
Historically, Huygens (1669) listed both the total momentum and the total vis viva as invariants of collisions; Leibniz (1676–1689) promoted the vis viva; the distinction between elastic and inelastic collisions and the general principle of energy conservation were clarified only in the 19th century. Lomonosov (1756) and Lavoisier (1773) established conservation of mass in chemical reactions; its continuum form is the continuity equation of fluid dynamics.
All motion takes place in Euclidean space (any dimension ; is the physical case), with the standard inner product and norm .
The goal theorem is the conservation of both total momentum and total mechanical energy for an isolated -body system interacting through symmetric pair potentials, along any collision-free trajectory:
Milestones:
These are the textbook consequences of Newton's laws used throughout mechanics, astronomy and engineering: momentum conservation determines the outcome of collisions and explosions, energy conservation gives first integrals that reduce equations of motion, and mass conservation is the first of the Euler equations of fluid dynamics. The results themselves are classical and fully known; the work in this mission is formalization. The platform already contains specialised instances (for example a two-body centre-of-mass statement and energy conservation in the Kepler problem); this mission states the general -body, arbitrary-dimension versions and the continuum mass law, which can be reused by later mechanics missions.
The algebraic milestones (collisions) are elementary. The analytic ones require care: energy conservation needs the chain rule for and for the norm , which is differentiable only away from collisions; the work–energy theorem needs the fundamental theorem of calculus for a continuous integrand; mass conservation needs differentiation under the integral sign and the vanishing of the integral of the divergence of a compactly supported vector field, a form of the divergence theorem that must be assembled from one-dimensional integration by parts.
EuclideanSpace ℝ (Fin d); time is ℝ; trajectories are defined for all times, and derivatives are given explicitly through HasDerivAt hypotheses (, ) rather than through deriv.deriv / fderiv, the density and the velocity field are jointly in , and the density vanishes outside a fixed ball for all times. The integral is the Lebesgue integral on .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. Their linear (continuous) counterparts are routinely solved by nested decomposition methods such as stochastic dual dynamic programming (SDDP; Pereira and Pinto, 1991), which approximate each node's expected cost-to-go function from below by a maximum of linear cuts. With integer variables the cost-to-go functions are no longer convex, and cuts from linear programming duality are in general not exact at the points where they are generated.
Zou, Ahmed and Sun (Math. Program. 175 (2019) 461–502) restrict the state variables passed between stages to be binary and introduce a local copy of the parent's state at every node. Dualizing only the copy constraint gives a class of cuts, the Lagrangian cuts, which the authors call "one of the major results of the paper" (p. 478). Their Theorem 3 shows that these cuts are valid (they never overestimate the true value function) and tight (they reproduce the current approximate value at the binary state where they are generated). Together with finiteness, these are the sufficient conditions of the paper's Definition 2 under which SND and SDDiP find an optimal solution in finitely many iterations with probability one (Theorem 2 of the paper, the subject of a companion mission).
Fix a node of the scenario tree and an iteration of the algorithm. The node has:
The approximate expected cost-to-go (3.2) is
and the updated forward problem (3.1) at a parent state has value
Let and let add a variable that dominates every aggregated cut. The Lagrangian function and Lagrangian dual (4.3)–(4.4) are
An optimal and define the Lagrangian cut . Given true value functions of the children and , the true nodal value (2.3) is .
For binary and optimal for :
and, if the children's cuts are valid for on and there,
The paper's statement for the whole collection of cuts of an iteration follows by applying this at every sampled node from the last stage backwards, exactly as its proof does by induction.
Tightness at binary states is what separates Lagrangian cuts from the cuts of continuous relaxations or of a direct Lagrangian relaxation of the constraints coupling stages: the paper's Example 2 shows a direct relaxation whose cut is not tight even at a binary state, and Example 1 shows that with a non-binary state the duality gap is positive. With valid, tight and finite cuts, SND and SDDiP become exact algorithms for multistage stochastic integer programs with binary states, and through binarization they approximate problems with general mixed-integer states.
The result is proved in the paper; no machine-checked proof of it is known. Formalizing it requires a Lean statement of Geoffrion's theorem for this nodal problem (Lagrangian duality equals optimization over the convex hull of a mixed integer set), which is of independent use for integer programming, and the binary-face fact for sets inside the unit cube.
The validity half is weak duality and is short. The difficulty is in tightness. Step (4.5) is a strong duality statement for a nonconvex set: it needs that the convex hull of is a polyhedron, which follows only because is compact and mixed integer polyhedral (so is a finite union of polytopes), and then linear programming duality with attainment over that polyhedron. Neither the polyhedrality of convex hulls of finite unions of polytopes with a common recession direction nor finite-dimensional LP strong duality in the needed form is readily available in Mathlib. A tempting shortcut, Lagrangian duality from convex analysis with a Slater point, does not apply: a binary lies on the boundary of the projection of onto , so the constraint qualification fails and polyhedrality is genuinely needed.
States, copies and multipliers are vectors in (Fin d → ℝ); a state is binary when each coordinate is or . Points of are tuples (z, x, y, θ). Assumption (A1) is three fields of the node structure (nonempty, compact, mixed integer polyhedral after concatenating coordinates). Cuts are indexed by Fin i and children by Fin nC; probabilities are only required to be nonnegative. A last-stage node is nC = 0 with L = 0. The constraint (2.1c) is kept in and folded into in (2.3) and (3.1), as in the paper.
Readings of informal words:
sInf of the set of objective values, and every theorem states the minimum as an attained least element (IsLeast) or as a lower bound over all feasible points, so no junk value of sInf on an empty or unbounded set is used. The hypothesis makes a genuine minimum.A trivializing formalization is ruled out: is the primal value of the forward problem (3.1) with from (3.2) and is never defined through the dual, and validity is required at every binary , not only at .
A complete development needs: polyhedrality of convex hulls of bounded mixed integer sets, LP strong duality with attainment (or Geoffrion's theorem directly), Carathéodory-type reasoning in product spaces, and the fact that a binary point which is a positive convex combination of points of equals each of them. The first two are reusable well beyond this mission. Proofs of individual milestones are welcome independently; the validity milestones are accessible first.
An agent whose preferences change over time cannot simply optimize once: a plan that is optimal today may be abandoned tomorrow by the agent's own "future selves". This is time inconsistency, and its standard source is non-exponential discounting, studied since Strotz (1955). The usual response, going back to Strotz and made rigorous in continuous time by Ekeland and Lazrak (2006), is to look for an equilibrium strategy: a strategy from which no future self wants to deviate. In continuous time "no incentive to deviate" is encoded through a first-order condition, which Huang and Zhou call a weak equilibrium.
Björk, Khapko and Murgoci (2017, Remark 3.5) observed that this first-order condition need not express the absence of an incentive to deviate: it only says that a derivative vanishes or is nonnegative, and a stationary point need not be a maximum. Huang and Zhou (Math. Oper. Res. 46(2), 2021; read here as arXiv:1809.09243v3) introduce a strong equilibrium, which requires the agent's payoff to be no better after any short deviation, and study the two notions for continuous-time Markov chains with controlled generators. This mission formalizes their main example (Example 4.3): a concrete two-state model in which a weak equilibrium fails to be strong, so that an agent in one state strictly gains from deviating on every short interval.
The state space is . A generator is a matrix whose -th row lies in . Admissible rows form sets , and the control space is . A payoff function gives the payment rate at time difference in state when row is in force. The expected payoff of using from state is
The concatenation uses on and afterwards. A generator is a weak equilibrium if for all , , and a strong equilibrium if for all there is with for every .
The paper's first-order and second-order quantities are
with the payoff computed with the time derivative in place of .
In the two-state model of §4, , , every generator is with , and , with the pseudo-exponential discount . Example 4.3 takes , , , , and for , for .
The statement is fully explicit and has no hypotheses.
Remark 4.1: for , , for all small . And (4.13): the equation has a unique solution , and is a strong equilibrium.
The example shows that the weak equilibrium concept, the standard one in the time-inconsistency literature since Ekeland and Lazrak, admits strategies that an agent would abandon: Remark 4.1 exhibits a deviation that strictly increases the payoff on every short interval. Together with (4.13), it shows that in one and the same model a weak-but-not-strong equilibrium and a strong equilibrium coexist, so the choice of equilibrium concept changes which strategies are predicted. The example is the paper's justification for introducing strong equilibria.
The result is proved in the paper, through the first-order characterization (Theorem 3.1), the second-order test (Proposition 3.3, resting on the second-order expansion Lemma 3.2) and explicit computations in the two-state model. None of it has been machine-checked. A formal proof would provide checked versions of Theorem 3.1 and Proposition 3.3 for finite-state chains, reusable for any other example, and an independent check of the arithmetic of Example 4.3, where the source contains at least one misprinted formula.
Both conjuncts of the goal concern the small- behaviour of , an integral of products of matrix exponentials. Weakness reduces to a first-order comparison by Theorem 3.1, but its proof needs the expansion (3.6) with an remainder controlled uniformly enough to pass under the integral over . Failure of strong equilibrium cannot be read off the first-order term: at the maximizer of is not unique, every ties at first order, and the decision moves to the second-order coefficient of Lemma 3.2, whose derivation needs a second-order expansion of the concatenated payoff. The regularity hypotheses of Lemma 3.2 and of (3.3) must also be verified for the example's discount function.
States are Fin N; the paper's state is index , so in the two-state model state 1 is 0 : Fin 2 and state 2 is 1 : Fin 2. Expectations are written through the transition matrices (NormedSpace.exp (t • Q)) and Fubini, exactly as the paper computes on p. 23; no Markov process is constructed. Payoffs are Bochner integrals over . The weak-equilibrium condition is written as "for every , eventually as the quotient is ", which is without a real-valued liminf. The norm in (2.3) is the sup norm, equivalent to the paper's Euclidean norm because (2.3) quantifies over every .
Standing assumptions: , continuity of in (2.2) and the integrability condition (2.3). Theorem 3.1 adds the shift bound (3.3)–(3.5); Proposition 3.3 assumes the conditions of Lemma 3.2, with the derivative tied to . The closed forms (4.3)–(4.4) assume (the page allows , but with a zero rate the payoff integral diverges); the algebraic identities (4.5)–(4.8) keep the page's ; Example 4.3 has , . Statement (4.11) gives and the argmax; the page's case formula for contains a misprint and is not used.
No trivializing reading is available: the goal has no hypotheses, is built from and the concatenation uses before and after , so neither conjunct holds by a junk value. Integrability of every payoff follows from (2.3) and is never assumed.
Theorem 3.1 and the second-order package are also drafted in the companion mission on existence of equilibria; they are restated here in the sub-namespace StrongWeakEq.TwoState. The goal needs the verification of (2.3), (3.3) and the Lemma 3.2 conditions for the example (convexity of gives (3.15)), the closed forms of for two-state generators, and the expansions of the paper. Contributions of proofs of the general results (Theorem 3.1, Proposition 3.3) are welcome independently of the example.
In a prophet inequality a gambler sees the realizations of independent nonnegative random variables one at a time and must decide irrevocably, at each step, whether to stop and keep the current value. Her performance is compared with that of a prophet who sees everything in advance and takes the maximum. The ratio between the two is the standard benchmark for online selection, and through the correspondence between threshold stopping rules and posted prices it governs the efficiency of sequential posted-price mechanisms in algorithmic mechanism design.
The constant depends on the order in which the values arrive. In adversarial order the best guarantee is (Krengel and Sucheston; Samuel-Cahn). For independent and identically distributed values it is about (Hill and Kertz 1982 gave the upper bound; Correa, Foncea, Hoeksma, Oosterwijk and Vredeveld 2017 proved it tight). The prophet secretary problem sits between these two: the distributions may differ, but the values arrive in a uniformly random order.
Timeline.
Before this bound no separation between the prophet secretary problem and the i.i.d. prophet inequality was known.
An instance with variables is a family of laws on . The values are independent. A permutation of , uniform and independent of the values, fixes the arrival order: at time the gambler sees which variable arrives and its value .
A strategy decides at each time whether to stop. The decision may use the observed history and an independent seed , uniform on , and must depend on them measurably. These are the randomized stopping times of the gambler's information. The gambler knows the distributions, so a strategy may be chosen after the instance. The reward is : the value at the first stop, and if she never stops. The value of a strategy is , and the prophet's value is .
A strategy guarantees if on every instance.
The §5 instance has variables, for and . Each of equals with probability and otherwise, and . For , the time- rule accepts a value whenever one appears, and accepts exactly when it arrives at time or later.
For every there is an instance with on which every strategy satisfies
The instance comes first and all strategies second. This is what "no strategy can guarantee more than " means once strategies may depend on the distributions. Universally quantifying a fixed strategy first would describe a weaker gambler.
At the ratio of milestones 4 and 1 tends to .
The bound shows that random order with non-identical distributions is strictly harder for the gambler than i.i.d. values: the constant cannot exceed , which is below . It improves the bound of Azar, Chiplunkar and Kaplan and extends it from deterministic distribution-insensitive algorithms to all strategies, including randomized ones that know the distributions. With the guarantee of the same paper, it brackets the optimal prophet secretary constant in . Later work raised the lower end, but the exact value is still open.
The result is proved in the paper. It is not formalized anywhere we know of, and no prophet secretary statement exists on the platform. Formalizing it means writing down a general model of randomized stopping strategies in random order, which other random-order results can reuse. The heart of the proof is a dynamic-programming argument that is easy to state informally and has never been machine-checked. The finite- bound of milestone 4, with an explicit constant in place of , is also a welcome contribution.
Computing the value of one good strategy on the §5 instance is routine (milestone 3). The goal, though, quantifies over every strategy, including randomized ones that observe identities and the whole history. The paper's sentence "Solving the dynamic programming, the algorithm picks the value if and only if it appears at time or later" carries the whole reduction. It requires:
Bounding a few natural strategies does not suffice. The asymptotic analysis must also be made uniform in the strategy, so that a single constant in works for all of them.
Fin (n+1), and is Fin.last n.Measure.pi μ.volume.restrict (Icc 0 1)).ENNReal.ofReal of the reward, so no integrability hypotheses appear.Strategy N) is the class of all measurable decision rules on the full observed history plus an independent seed, and it is quantified after the instance. Restricting it to threshold rules, time- rules or deterministic rules would make the goal a different, weaker theorem; that restriction is ruled out. The class is nonempty, and its measurability requirement is satisfiable: jRule carries its proof.Reusable infrastructure includes the random-order stopping model, the reward of the first stop, and the dynamic-programming reduction for a single deterministic variable. Contributions are welcome on any milestone, and on an explicit in milestone 4.
An agent that interacts repeatedly with an unknown Markov decision process must trade exploration against exploitation. The dominant design principle for provably efficient reinforcement learning has been optimism in the face of uncertainty: UCRL2 (Jaksch, Ortner & Auer, 2010) and REGAL (Bartlett & Tewari, 2009) build confidence sets around the unknown model and act according to the most favourable model in them. Computing that optimistic policy can be expensive, and confidence sets built separately for every state–action pair can be loose.
Posterior sampling for reinforcement learning (PSRL), proposed by Strens (2000), replaces optimism by randomization: at the start of each episode it samples one MDP from the posterior distribution and follows the optimal policy of that sample. It is the reinforcement-learning analogue of Thompson sampling for bandits. Osband, Russo & Van Roy (2013) gave the first regret guarantee for PSRL, and with it the first regret guarantee for an RL algorithm not based on optimism. Their argument transfers the Bayesian-regret analysis of Thompson sampling by Russo & Van Roy (2014) from bandits to MDPs.
Timeline:
A finite-horizon MDP has states, actions and horizon . Choosing action in state yields a reward drawn from a distribution on , with mean , and moves the state to with probability . Every episode starts from a state drawn from the initial distribution . A policy maps a state and a step to an action, and its value is the expected total mean reward from step on,
A policy is optimal for if it maximizes for every and ; denotes a fixed choice of optimal policy for each .
The true MDP is random with prior . In episode , PSRL samples from the posterior given the history of all earlier states, actions and rewards, and follows for steps. With , the regret of episode and the cumulative regret are
In Lean, MDPs are indexed by a parameter in a measurable space (MDPFamily), the value is value F θ π j with 0-based steps, and the run is the structure PSRLRun.
There is an absolute constant such that, for all , every prior , every measurable optimal-policy selector, every PSRL run with and every ,
This is the paper's statement. It does not fix the constant, which the paper's appendix computes with errors.
Theorem 1 holds for every prior, with no assumption on the MDP class beyond finiteness and bounded rewards. It shows that a single posterior sample per episode, rather than an optimistic search over a confidence set, already achieves the rate of the optimistic algorithms. The reduction it rests on (Lemma 1 and Theorem 2) applies to any problem in which the agent can sample from the posterior.
The theorem has a paper proof but, as far as is known, no machine-checked proof. A formalization adds three things. First, an exact model of the episodic Bayesian setting, with posterior sampling stated as a conditional law. Second, corrected versions of two steps: the factor in (8), which the page's argument does not justify as printed, and the square-root sum of Appendix B, which is false as printed. Third, reusable pieces: a path-defined finite-horizon value with its dynamic programming equation, a conditional-expectation form of the posterior-sampling identity, and deterministic counting lemmas for visit counts.
The proof combines three kinds of argument, each with its own obstacle in Lean.
Model. States and actions are Fin S and Fin A. Steps and episodes are 0-based: Lean step j is the paper's step , and Lean episode k is the paper's episode , with . MDPs are a measurable family over a parameter space Θ: transition rows satisfy the published IsTransitionKernel, and reward laws are Markov kernels supported on . The initial distribution is fixed. The value is defined from the state laws along the trajectory, not by the Bellman recursion.
The run. PSRLRun consists of measurable random elements on a probability space. Posterior sampling, the reset from , rewards and transitions are stated as conditional expectations of indicators. Three assumptions the paper leaves implicit are made explicit:
The optimal-policy selector is any measurable map that is optimal at every step.
Constants and corrections. is one absolute constant, quantified before every other object; a constant that depends on , , , the prior or would make the goal trivial, because the regret is at most . Milestone 7 uses the factor , which the page's chain proves, where the page prints , and milestone 9 uses where the page prints the false bound ; both corrections are disclosed in the statements.
Ruled out. The value is not defined by the recursion, which would make Lemma 2 definitional. Measurability is required, so the expectations are not junk zeros. The posterior-sampling clause concerns indicators of only, so it does not already contain Lemma 1.
Needed infrastructure. Conditional expectations with respect to -algebras generated by random elements; finite-horizon Markov chain laws; Weissman's inequality and Hoeffding's inequality at random sample sizes; elementary bounds on . The counting milestones (8, 9) and Lemma 2 are self-contained and a good place to start. Proofs of the conditioning steps (milestones 1, 2, 4) are reusable for any posterior-sampling analysis.
Value-at-Risk (VaR) is the regulatory risk measure for banking and insurance capital: it is the quantile of a loss distribution at a fixed tail probability. Two questions arise when several agents use it. First, risk sharing: if an aggregate loss is split among agents , each measuring its share with its own risk measure, what is the smallest total risk the group can achieve and which split achieves it? Second, model uncertainty: an agent rarely knows the distribution of a loss exactly, and a common response is to evaluate the worst case over all distributions close to an estimate, here in the sense of the Wasserstein distance used in distributionally robust optimization (Esfahani and Kuhn, 2018).
F. Liu, T. Mao, R. Wang and L. Wei, Inf-Convolution, Optimal Allocations, and Model Uncertainty for Tail Risk Measures (Mathematics of Operations Research, 2022; the version used here is the authors' SSRN copy 3490348 of January 16, 2022, ssrn.com/abstract=3490348), combine the two questions. When each agent uses a Wasserstein-robust VaR and the split must be comonotonic (every share increases with the total, the usual requirement in insurance), their Theorem 6 gives the optimal total risk in closed form and shows that one agent should carry the entire loss.
Fix an atomless probability space : every event of positive probability contains an event of strictly smaller positive probability. A random variable is a loss, with distribution function . The domain is , the essentially bounded measurable random variables.
For the left and right Value-at-Risk are
so a small looks far into the tail of the loss. selects one of the two.
The Wasserstein metric of order between and with quantile functions and is
and the robust version of a risk measure at radius is
Two random variables are comonotonic if for all in an event of probability one. The comonotonic allocations of among agents are
and the constrained inf-convolution of is . An allocation attaining the infimum is optimal.
Let and .
(i) If and , then
(ii) If and , then
In either case is an optimal comonotonic allocation.
The theorem is one of the few explicit solutions of a risk-sharing problem with model uncertainty and non-convex agents. Without uncertainty, the inf-convolution of VaRs is a VaR at the summed level (Theorem 1 of the same paper), and its optimal allocations split the tail of the loss across agents. Under Wasserstein uncertainty and a comonotonicity constraint the structure changes: the optimum concentrates the whole loss on the agent least sensitive to uncertainty when the levels agree, or least sensitive to risk when the radii agree, and the remaining agents hold only cash. In particular the equal split , optimal for identical convex risk measures, is in general not optimal here. Proposition 4(iii) is independently useful: it computes the worst-case VaR over a one-dimensional Wasserstein ball of any order and shows that left and right VaR coincide after robustification.
The results are proved in the paper. As far as is known, none of them has a machine-checked proof; this mission produces the first formal statements and, eventually, proofs. The quantile-based Wasserstein metric, the robust risk measure and the comonotonic inf-convolution are reusable objects for further work on robust risk measures.
The upper bound is a direct computation with one explicit allocation. The lower bound is the hard part. VaR is not convex, so the duality arguments that solve the inf-convolution of convex risk measures do not apply, and the robust VaR is not a distortion risk measure to which the Expected Shortfall formula of Proposition 4(ii) applies. The paper itself notes (p. 30) that the inf-convolution of robust VaRs over all allocations is hard to compute because VaR lacks convexity, and obtains only two-sided bounds there, which are generally not sharp. The explicit formula of Theorem 6 depends on the comonotonicity constraint, on the order , and on the agents sharing either the level or the radius; the paper states it only under these assumptions, and the ordering of the radii or levels is necessary for the identity as written, since it singles out the agent who carries the loss. For Proposition 4(iii), the supremum over the ball is a supremum over distributions, and identifying it with a real number requires realising worst-case distributions as random variables on the given space, which is where atomlessness is used.
Random variables are functions ; is the set of measurable, almost surely bounded functions, with no quotient. The probability measure is atomless in the splitting sense. The quantile function is , and the Wasserstein integral is the interval integral over ; for its integrand is bounded and monotone on , so the integral is the paper's. The supremum in the robust measure ranges over only, as in the paper. It is a real supremum: the set is nonempty since it contains , and for VaR its boundedness from above is part of the statement of Proposition 4(iii), so no junk value enters. Allocation constraints hold pointwise. The constrained inf-convolution is valued in the extended reals. The agents are indexed by Fin (m+1), so ; the orderings of the radii and of the levels are hypotheses, since without them the identities fail. Theorem 6 is stated for order ; Proposition 4(iii) for every real . The single implicit hypothesis made explicit is in (41), which keeps the VaR level in .
A formalization in which the robust supremum ranges over all measurable functions, or over an unbounded set where the real supremum is , would make the identities trivial or false; both are excluded by the definitions above.
The development needs: quantile functions of bounded random variables and their monotonicity; the existence on an atomless space of a random variable with a prescribed quantile function; comonotonic additivity of VaR; and the interval-integral calculus for monotone integrands. Contributions of general lemmas on quantile functions and on one-dimensional Wasserstein distances are welcome and reusable beyond this mission.
Data-driven control asks for a controller computed directly from measured trajectories of an unknown system, without first identifying a model. When the measurements are corrupted by noise, many systems explain the same data, and a controller is acceptable only if it works for all of them. Van Waarde, Camlibel, Eising and Trentelman (arXiv:2203.12959) model the noise by a quadratic matrix inequality (QMI). The set of systems consistent with the data is then itself the solution set of a QMI, and the design question becomes whether one QMI implies another. Their Theorem 5.1 gives a necessary and sufficient linear matrix inequality (LMI) for the existence of a common stabilizing controller, with no rank or Slater-type assumption on the data. It improves van Waarde, Camlibel, Mesbahi, IEEE TAC 2022, Thm. 14, which needed a generalized Slater condition.
The LMI of Theorem 5.1 has size and unknowns. Section 5.2 of the paper removes the controller variable: Theorem 5.3 gives an LMI of size in the Lyapunov matrix and one scalar , and then writes a stabilizing controller as a closed-form expression in and the data. This mission formalizes that reduction and the Section 3 results on QMI solution sets that it rests on.
All matrices are real. is the set of symmetric matrices, () means symmetric positive semidefinite (definite), and is the Moore–Penrose pseudo-inverse. For , partitioned with of size and of size ,
and is the same set with . The generalized Schur complement is , and is the class of with , and . For , and .
Data. An unknown system produces and ; and are the first and last columns of . The noise matrix is unknown but satisfies for a given . The consistent systems are
The data are informative for quadratic stabilization if there are and with for all .
With and : the data are informative if and only if some , satisfy
and then
stabilizes every . Under and the same holds with strict inequalities, , and . The goal states all four parts.
Theorem 5.3 separates the computation of a Lyapunov matrix from the computation of the controller. The LMI drops from size to and loses the entries of . A controller then follows from by one explicit formula, with no second optimization. The noise class covers energy bounds, bounds on individual samples, noise confined to a known subspace, and exact data, so the result applies where earlier conditions requiring or a Slater point fail.
The Section 3 results are general facts about QMIs: an explicit parameterization of all solutions, also when the solution set is unbounded, and the identification of the image of a solution set under a linear map. They are reusable wherever QMIs appear in robust control: Petersen's lemma, the elimination lemma, dissipativity analysis.
All results are proved in the paper, with the exception of the proof of Theorem 3.5, which is only described as similar to that of Theorem 3.4. None is formalized. The work here is the formal development: a pseudo-inverse calculus for real matrices, generalized Schur complements, matrix square roots in the Loewner order, and the block-matrix identities of Section 5.
The QMI reformulation of the stabilization problem is short. The difficulty lies in degenerate matrices. is typically singular, so every step works with pseudo-inverses, kernel inclusions and generalized Schur complements, and identities that are routine for invertible blocks need range conditions. The closed-form gain (5.10) comes from a block pseudo-inverse formula for a positive semidefinite matrix whose blocks may all be singular, and checking it requires tracking which ranges contain which. The strict statements need a separate argument: a strict inequality does not pass to without full column rank of , which is why Theorem 3.5 and Corollary 3.7 assume it.
The first idea, to eliminate from (5.5) by completing the square, runs into the same singular blocks: the minimizing involves pseudo-inverses of data-dependent matrices whose ranges are not controlled by the LMI alone.
Lean conventions:
PosSemidef (which includes symmetry); is PosDef.A⁻¹, which returns on singular matrices, appears only in (5.11a) and in , where the matrices are invertible.CFC.sqrt in the Loewner order. Kernel inclusions are stated on vectors. Full column rank of is rank W = p.The statements of Theorems 5.1 and 5.3 carry the hypothesis that the data were generated by some , i.e. ; the paper assumes this when it says the data are generated by (2.1) with noise model (2.3). Without it, informativity holds vacuously and the equivalences fail. "Stabilizing gain" is asserted with the of the LMI: the Lyapunov inequality and for every . Corollaries 3.6 and 3.7 print the hypothesis , which is dimensionally impossible; it is read as . The printed dimensions in Lemma A.2 are corrected to those its formula requires.
A formalization in which Σ may be empty, or in which is replaced by the total inverse, would make the goal vacuous or false. Both are ruled out above.
Theorem 5.1 is restated here as a milestone. It is also the goal of the companion mission IV, and solvers may prove it there.
Reusable infrastructure is welcome as separate contributions: uniqueness and the basic identities of the matrix pseudo-inverse; the generalized Schur complement criterion for positive semidefiniteness of a block matrix; Douglas-type factorization (Lemma A.1); square roots of positive semidefinite matrices commuting with pseudo-inverses.
Stochastic dual dynamic programming (SDDP) and its relatives are the standard algorithms for multistage stochastic programs: hydro-thermal scheduling, energy storage and long-horizon capacity planning are solved with them in industry. They approximate each future cost function from below by a maximum of affine cuts, compute new cuts only at a few randomly chosen nodes of the scenario tree, and use the current approximations to simulate decisions forward. Whether such sampled cutting-plane schemes converge, and in what sense, decides whether their bounds can be trusted.
This mission formalizes the stochastic part (§3) of the 2015 paper. Mission 1 of the series covers its deterministic part (§2).
A finite scenario tree has nodes , root , parent map , children , leaves , and node probabilities with and . Every node carries a control multifunction , a cost and linear dynamics ; every node carries a compact convex stock set ; leaves carry final costs . The future cost functions are defined backwards by (20):
Assumptions ask for convex, lower semicontinuous, proper costs, convex compact-valued convex multifunctions , Lipschitz final costs, and an extended relatively complete recourse condition: feasibility and finite cost on a -neighbourhood of every .
The algorithm keeps approximations , starting from . At iteration it simulates the whole tree with , producing stocks and controls . Cuts are computed at the selected nodes by solving the stage problems (21) at their children and averaging optimal values and Lagrange multipliers with weights . Every approximation is then updated by (22), . The selections form a random process. It is τ-admissible (Definition 1) when, inside each block of iterations, cuts are computed backwards along the tree, and when the block indicators are i.i.d. in , independent of the past, and equal to with positive probability.
Under and a τ-admissible selection process, almost surely, for every non-leaf node and every node respectively,
The decisions become optimal for the true problem and the approximations become exact at the visited stocks. Nothing is claimed about exactness elsewhere in the state space.
The theorem covers in one statement CUPPS (1-admissible), DOASA and SDDP (-admissible), and many other sampling schemes, for stage problems that are convex rather than linear and for scenario trees without stagewise independence. It shows that the lower bound produced by these methods converges to the optimal value along the simulated trajectories.
The result is proved on paper. It is not formalized anywhere: no proof assistant library contains SDDP-type algorithms for convex stage problems. This mission makes the algorithm, the τ-admissibility notion and the convergence statement precise. Formalizing them corrects slips of the printed statements: the lower-bound property holds on the affine hull of only, the boundedness of the cut slopes concerns finite cuts only, and the theorem's two limits concern different node sets. The rest of the work is the formalization of the published proof.
The deterministic argument (mission 1) shows exactness at stage from exactness at stage along the whole iteration sequence. In the stochastic case a node is updated only at the random iterations at which it is selected, while its stock moves at every iteration. Exactness along the selected iterations (32) does not transfer to the others: a selection rule that updated a node only when its stock lay in a given region would leave the approximation inexact elsewhere. The proof has to show that the iterations at which the approximation is still -inexact are, by independence, selected with positive frequency. This requires the event " is -inexact" to be measurable with respect to the past selections, so the algorithm's choices among multiple minimisers and multipliers must be deterministic (footnote 6). It also requires the optional-skipping Lemma 5.4 and the strong law of large numbers. The first idea of conditioning on the stocks directly fails because the stocks depend on all past selections.
EuclideanSpace ℝ (Fin d), controls in EuclideanSpace ℝ (Fin p). Costs and value functions take values in EReal; convexity is epigraph convexity; off ; the initial approximation is . Limits are EReal limits, so convergence to forces the differences to be finite eventually.StochasticProg.Multistage.Tree (a finite rooted tree with stages) is referenced; leaves, ascendents and node probabilities are defined on it. Costs are indexed by the child node as in (19a) and (20).Vc k is the paper's .Bool-valued maps on a probability space; Definition 1 (i) holds on every path; (ii) is per node, i.i.d. in and independent of , with no independence across nodes.run_exists shows that runs exist for every selection path, and a sanity check shows and τ-admissibility are satisfiable, so the goal is not vacuous. Its conclusion mentions none of the proof's auxiliary objects.EReal-valued convex functions, are welcome.In distributed optimization a network of agents minimizes a sum of private functions while each agent talks only to its neighbours. Applications include federated and decentralized learning, sensor networks and multi-robot systems, where the data cannot be pooled at one site. Many of these networks are directed (communication links are one-way, for instance because transmission powers differ) and time-varying (links come and go). On such networks no doubly stochastic mixing matrix is available in general, and plain averaging drifts toward a weighted average instead of the true one. The push-sum protocol corrects this drift by carrying an auxiliary weight at every agent (Kempe, Dobra & Gehrke 2003; Nedić & Olshevsky 2015).
Y. Sun, A. Daneshmand and G. Scutari (arXiv:1905.02637v2) analyse SONATA, a gradient-tracking method in which each agent solves a strongly convex surrogate of its local problem instead of taking a gradient step, for composite problems (a convex, possibly nonsmooth regulariser and a convex constraint set). They prove linear convergence on undirected graphs (their Theorem 3.9, the companion mission of this series) and, in Section 4, for a push-sum version over time-varying digraphs (Theorem 4.5). This mission formalizes the second result.
Timeline. Gradient tracking with push-sum over time-varying digraphs appears in NEXT/SONATA (Di Lorenzo & Scutari 2016; Scutari & Sun 2019), where convergence was proved without rates for nonconvex problems. Linear rates for smooth unconstrained strongly convex problems over time-varying digraphs were obtained for Push-DIGing (Nedić, Olshevsky & Shi 2017). Sun, Daneshmand and Scutari (2019, revised 2020) extend the linear rate to the composite, constrained setting with surrogates, and require only the average , not every , to be strongly convex.
Problem (P). Agent holds ; the agents solve
Assumption A: is nonempty, closed and convex; each is twice differentiable on an open set and convex; on with ; is convex on . is the solution and .
Surrogates (Assumption C). Each agent has , on , with , -Lipschitz and -strongly convex on . Constants satisfy on (15); , .
Network (Assumption B′). At time the digraph has edge set ; is a link from to . There is an integer such that the union of the edge sets over every window is strongly connected.
Weights (Assumption E). is column stochastic, , if and for other .
Algorithm 3. From , , , each agent computes
then , and .
The analysis uses the weighted gap , the tracking error , and the consensus errors , measured against the -weighted averages.
If , there is such that for every , every run and every agent ,
The goal is qualitative: neither nor the rate is fixed, so it survives any improvement of the constants.
In attack order: the weighted tracking identity (74) and its consequence ; the bounds (p. 29); the per-agent descent inequality (Lemma I.1); the lower bound on the weighted step length (Lemma I.2); the tracking-error bound (Lemma I.3); the contraction (Proposition 4.1); the bound of by and (Proposition 4.3).
Theorem 4.5 gives a linear rate for distributed composite and constrained optimization over time-varying directed networks. Two features matter: the individual need not be strongly convex, and the surrogates cover proximal-gradient steps, DANE-type local solves and mirror-descent steps under one analysis. The rate depends on the surrogate-mismatch constants , which is the mechanism by which the paper shows that local computation helps when the are similar.
The result is proved in the paper; the proof of Theorem 4.5 refers to the undirected argument, and several of its supporting statements (Propositions 4.1 and 4.3) have their proofs omitted or relegated to the supplement, with consensus estimates quoted from Scutari & Sun (2019). To our knowledge none of it is machine-checked. A formalization produces a checked proof of the directed result together with reusable statements about push-sum weights over -strongly connected digraphs.
The obvious argument is to repeat the undirected proof with weighted averages. Two steps fail. First, the -weighted average is not the minimiser of , so consensus errors measured against it lose a constant (the 8 in Lemma I.3 instead of 4), and every passage between weighted and unweighted sums needs the bounds , which rest on a product-of-matrices argument over windows of length . Second, the matrices change with , so there is no single contraction factor; geometric decay of the consensus errors holds only over windows, and the coupling between the optimality gap, the consensus errors and the step lengths must be closed by a small-gain argument whose constants are uniform over the run. The step-size threshold must not depend on the starting point.
Points are EuclideanSpace ℝ (Fin d); stacked vectors are Fin m → ℝ^d with the Euclidean norm , never Lean's sup norm. The Hessian is the derivative of the gradient, and Loewner bounds are quadratic-form inequalities. Time is 0-based. A run is a relational predicate: is some minimizer of the subproblem, whose existence the paper takes for granted; is assumed to exist. The divisions by appear as in the paper and are genuine, since Assumption E keeps the weights positive. is convex on and locally convex on (positive semidefinite Hessian; need not be convex), , and are parameters: the statements hold for every valid choice. The graph sequence, , and the matrices come before ; the starting point and the run come after . The bounds on are stated for (the printed is at ), and positivity of is claimed only when or .
The following do not count as a formalization of the goal: an unsatisfiable run predicate (a sorry-free verification file exhibits a run satisfying every hypothesis), a chosen after the run, the bounds or a contraction factor assumed in place of Assumptions B′ and E, and dropping the normalisation.
Not posed: the explicit rate (Theorem III.1), the complexity corollaries, and the consensus estimates Lemma 4.2 and Proposition 4.4, whose constants come from Scutari & Sun (2019) (as printed, is negative). A complete development needs Taylor expansions with integral remainder along segments, first-order optimality for composite problems on convex sets, and products of column-stochastic matrices over strongly connected windows; the last is reusable for any push-sum method. Contributions to any milestone, and to the missing consensus estimates as auxiliary lemmas, are welcome.
Finsler's lemma (P. Finsler, 1937) states that for symmetric matrices , the quadratic form is positive on every nonzero with if and only if for some real . Together with the S-lemma of Yakubovich it is one of the basic tools for converting a statement about all vectors satisfying a quadratic constraint into a single linear matrix inequality (LMI) in a multiplier, which can then be checked by semidefinite programming. Both results are used throughout robust control, where uncertainty is described by quadratic constraints.
In data-driven control the unknown object is a matrix, not a vector: the system matrices consistent with noisy measurements form a set of the form
and a controller has to work for every element of such a set. H. J. van Waarde, M. K. Camlibel, J. Eising and H. L. Trentelman (arXiv:2203.12959, SIAM J. Control Optim. 2023) develop matrix-valued versions of the S-lemma and of Finsler's lemma for exactly this purpose. Their matrix S-lemma (Theorem 4.7) requires a Slater-type condition: must have a positive eigenvalue. This mission concerns the complementary case in which has no positive eigenvalue, where the inequality defining degenerates into an equality and a Finsler-type statement is needed.
All matrices are real. For a symmetric matrix , () means positive semidefinite (definite); means . is the Moore–Penrose pseudo-inverse, the unique matrix with , and , symmetric.
Fix integers and . A symmetric matrix is partitioned as
with of size and of size , and likewise . For write , and define
The generalized Schur complement is , and the class consists of the symmetric with , and . For , the condition is equivalent to having no positive eigenvalue; then . Finally, set
First, if for some , then . Second, if , and , then
A companion item formalizes Example 4.9 (p. 13): for and all hypotheses except the one on hold, the inclusion holds, and no works.
The theorem turns an inclusion between two sets of matrices, a statement quantified over infinitely many , into feasibility of a scalar-multiplier LMI. In the paper it is one of four matrix S-lemma variants (Theorems 4.7, 4.8, 4.10, 4.11) that together cover the cases arising in data-based control: whether the data-consistent set has a Slater point, and whether the conclusion is non-strict or strict. Theorem 4.8 is the variant for noise models whose quadratic description has no interior, for instance exact equality constraints on the noise. Example 4.9 shows that the kernel hypothesis on is genuinely needed, so the statement marks the boundary of when the lossless reduction holds.
The paper gives a complete proof. No machine-checked proof of this theorem, of the matrix S-lemma, or of Finsler's lemma in matrix form is known to exist, in Lean or elsewhere. Formalizing it produces reusable infrastructure: the Moore–Penrose pseudo-inverse of real matrices with its Penrose identities, the generalized Schur complement criterion for positive semidefiniteness of a block matrix, and congruence manipulations of block matrices, none of which is currently in Mathlib in this form.
The "if" direction is a one-line computation. For the "only if" direction the classical vector Finsler lemma is not directly applicable: it concerns vectors with , while the hypothesis here only controls matrices with , which is a much smaller family when , and the conclusion is non-strict. The natural first idea, applying the vector S-lemma, fails because has no positive eigenvalue, so its Slater condition is violated. Instead one must exploit the structure of : the pseudo-inverse appears because and are typically singular, and every manipulation must track kernels and ranges exactly.
The blocks are indexed by arbitrary finite types ι (size ) and κ (size ); a matrix in is Matrix (ι ⊕ κ) (ι ⊕ κ) ℝ, its blocks are toBlocks₁₁ etc., and is Matrix κ ι ℝ. is Mathlib's PosSemidef, which includes symmetry. The pseudo-inverse is defined by Hilbert's choice among matrices satisfying the four Penrose conditions; since such a matrix exists and is unique, this is the pseudo-inverse and not a junk value. Kernel inclusions are stated with matrix–vector products.
One hypothesis is added and disclosed: (Nonempty ι) in the second statement of Theorem 4.8 and in the milestones that need it. The proof picks a nonzero vector of , and at the equivalence is false (, , ). The first statement keeps a real multiplier of any sign; the second requires , as printed. The hypothesis together with makes nonempty, so the inclusion is never vacuous; a formalization in which could be empty, or in which were replaced by the inverse (which is on singular blocks in Lean), would not be this theorem.
Needed infrastructure: existence and uniqueness of the Moore–Penrose pseudo-inverse (needed to work with the definition at all), symmetry of for symmetric , the generalized Schur complement criterion for , and positive semidefiniteness under congruence by an invertible matrix. These lemmas are reusable beyond this mission and contributions of them are welcome, as are proofs of the companion Example 4.9.
Many planning problems combine a discrete choice with a continuous one. A robot moving through a cluttered room chooses which free regions to traverse and where exactly to cross between them; a vehicle chooses a sequence of operating modes and a trajectory within each mode. Marcucci, Umenberger, Parrilo and Tedrake (arXiv:2101.11565, SIAM J. Optim. 2024, doi:10.1137/22M1523790) abstract this as the shortest-path problem in a graph of convex sets (SPP in GCS): a shortest-path problem in which each vertex is not a point but a convex set, and the length of an edge depends on where in its two sets the path enters and leaves. The paper shows that the problem is NP-hard even in simple cases, and then gives a mixed-integer convex formulation that is exact and whose convex relaxation is strong in practice. That formulation underlies the GCS motion planners developed later by the same group.
A graph of convex sets consists of a finite directed graph , a source vertex , a target vertex , a nonempty compact convex set for each vertex , and for each edge an edge length , which is proper, closed and convex. No symmetry or triangle inequality is assumed. An - path is a sequence of distinct vertices with , and ; is the set of its edges. The SPP in GCS (2.1) is
The perspective of a set is the closed cone (Definition 4.1). The perspective of a function is , the function whose epigraph is the perspective of the epigraph of (Definition 4.4). For it equals .
With and the edges entering and leaving , the MICP (5.5) has a flow and two vectors per edge:
Its optimal value is . The paper derives (5.5) from a biconvex program (5.2), the shortest-path LP (5.1) together with vertex positions and the bilinear constraints , . Lemma 5.4 turns every valid linear inequality on the flows at a vertex into a valid perspective constraint.
Under the standing assumptions of §2 and the assumption of p. 7 that no edge enters and no edge leaves ,
Both sides are infima in the extended reals and equal when there is no - path.
A companion item states the recovery part of Theorem 5.7 (second and third sentences): an optimal MICP solution yields an optimal path and optimal positions , .
Theorem 5.7 is what makes (5.5) usable: it says that the mixed-integer program, whose only nonconvexity is , solves the SPP in GCS exactly. The SPP in GCS is NP-hard by Theorem 3.1, so exactness is the most one can ask of a polynomial-size formulation, and dropping integrality gives a convex program whose value is a lower bound for branch and bound. The perspective construction of Lemma 5.4 is a general recipe, closely related to the reformulation-linearization technique, for convexifying products of flows and positions.
On the formal side, the paper's proof is half a page and leaves several points to the reader: why the integer flows decompose into a path and cycles, why the closure in the perspective cone disappears for compact sets, and why the perspective function vanishes at the origin. A machine-checked proof makes these steps explicit. The result has not been formalized before, and the mission also produces reusable statements about perspectives of sets and functions in extended-real arithmetic and about the decomposition of unit - flows with degree bounds.
The inequality is the routine half: a path and its positions give a feasible point of (5.5) of the same cost. The other half requires reading a path out of an arbitrary feasible point. Integer flows satisfying (5.5b)–(5.5d) need not be a path: they may also contain disjoint cycles, and the degree constraint (5.5c) is what prevents a cycle from sharing a vertex with the path (Example 5.10 shows the value drops without it). The cost of a cycle must be shown to be nonnegative, and the perspective constraints must be shown to collapse to on zero-flow edges. That step uses compactness of . For unbounded sets the zero slice of is the recession cone, and the argument fails. The cost at zero flow is , defined by a closure, and its value uses properness and convexity of , not just the formula .
Fin n → ℝ. Edge lengths and all optimal values are EReal; optimal values are infima (⨅/sInf), equal to on an empty feasible set. Attainment is not assumed.E : Finset (V × V) over a finite vertex type, a source, a target, sets X v and lengths ℓ e. The standing assumptions of §2 (; nonempty, compact, convex; proper closed convex) are the predicate IsGCS. The assumption of p. 7 is the separate predicate NoInSNoOutT, a hypothesis of the goal, of the path-and-cycles milestone and of the recovery item.A linear set of the projective line is the set of points spanned by the nonzero vectors of an -subspace . The extremal ones, the maximum scattered linear sets, are given by scattered polynomials over , and each such also gives an -linear maximum rank-distance (MRD) code of minimum distance (Sheekey, Adv. Math. Commun. 10, 2016). Rank-distance codes are used in network coding, and linear sets appear in the study of semifields, blocking sets and two-intersection sets.
Linear sets and codes are classified up to equivalence: two linear sets are the same object if a collineation of the line, an element of , maps one onto the other. The question is therefore not only whether new scattered polynomials exist but how many inequivalent linear sets they produce.
Let be an odd prime, , , , , and let be the finite field of order . Its subfield is .
A -polynomial is a map with (qpoly). It is scattered (IsScatteredPoly) if for all , forces with .
The graph of is (graph). A point of is the set of all -multiples of a nonzero (point), and the linear set of is the point set
For a field automorphism and an invertible matrix over , the map ( acting on coordinates, act) is an element of ; with it is in . Two subsets are GL- or ΓL-equivalent (GLEquiv, GammaLEquiv) if such a map sends onto . Two point sets are PGL- or PΓL-equivalent (PGLEquiv, PGammaLEquiv) if the induced map on points, , sends one onto the other.
The family. For ,
(hSet), and . For and , is scattered and is a maximum scattered linear set (Theorem 3.1).
For , the number of -classes met by the sets , , satisfies
It is stated as: some of at least that size has pairwise -inequivalent . The goal fixes the paper's constants; the proof on p. 26 in fact counts classes exactly in terms of class sizes, so a sharper bound is a natural follow-up.
The result. Theorem 5.1 shows that maximum scattered linear sets of , and hence -linear MRD codes, exist in numbers exponential in up to equivalence, whereas each previously known infinite family yields at most times a function of classes (Table 1, p. 3). Remark 5.4 draws the consequence that the family is new. Its intermediate results, the classification of the - and -equivalences between the (Theorem 4.2) and the reduction of -equivalence to sets of quotients, are the standard tools for any later classification of this family.
Formalizing it. The theorem has a complete published proof; none of it is machine-checked. The platform has no action of or on the projective line, no linear sets of as point sets, and no coefficient identities for -polynomials defining the same linear set. The mission produces these, then the class counts. Lemma 2.2 is a result of an earlier paper (Csajbók–Marino–Polverino 2018) cited without proof, so formalizing it means formalizing part of that paper too.
Equality of two linear sets is equality of sets of points, which says nothing directly about the polynomials: different -polynomials can define the same linear set (all with do). The obvious idea, that -equivalent linear sets come from -equivalent subspaces , fails in general (p. 3), so the count cannot be read off Theorem 4.2. The step that needs the restriction is the comparison of coefficients in the -polynomial identities, which for is open (Remark 5.5). A second difficulty is bookkeeping: the exponents , , the negative powers of and the case split on must all be tracked through every identity.
CharP F p, p prime, Odd p (" odd"), q = p ^ r with 0 < r, and Fintype.card F = q ^ (2 * t). is the exponent of , as in Theorem 5.1, so . Lemma 2.2, (37) and the step are stated for general and Fintype.card F = q ^ n, without " odd", as printed.x ^ q ^ i; negative powers of are field quotients (h / h ^ q ^ (t+1) for ), exact since on . Natural-number subtractions , , , , are exact in the stated ranges.Fin 2 → F; points are sets of scalar multiples; linear sets are sets of points. Equivalences are stated as images of sets under with a unit and a ring automorphism.A risk sharing problem distributes an aggregate random loss among agents, each of whom evaluates its share with a risk measure . The smallest achievable aggregate risk is the inf-convolution , and allocations that attain it are optimal. In insurance and in regulated banking the allocation is often required to be comonotonic: every share moves in the same direction as the total loss. This is the no-sabotage, or no-moral-hazard, condition of the insurance literature (Huberman, Mayers and Smith 1983; Carlier and Dana 2003). For risk measures that respect convex order, comonotonic allocations lose nothing (the comonotone improvement of Carlier, Dana and Galichon 2012). For the risk measures most used in practice, Value-at-Risk and its relatives, this is not true, so the comonotonic problem has to be studied in its own right.
Liu, Mao, Wang and Wei (2022) study inf-convolutions of tail risk measures, the risk measures that depend only on the distribution of a loss beyond a fixed quantile. Value-at-Risk, Expected Shortfall and Range-Value-at-Risk are all of this kind. Their Theorem 3 shows that the unconstrained inf-convolution of tail risk measures is again a tail risk measure, with tail parameter the sum of the individual ones. Theorem 4, the subject of this mission, treats the comonotonic constraint, and the tail parameter becomes the maximum.
Fix an atomless probability space : every event of positive probability contains an event of strictly smaller positive probability. Random variables are real measurable functions on , and a positive value is a loss. The distribution function of is , and its left-continuous inverse is for . A quantile uniform of is a random variable, uniform on , with almost surely.
For the tail of beyond its -quantile is . Its distribution function is
A risk measure is a -tail risk measure if whenever and have the same distribution (Definition 1). A -generator of such a is a law-invariant risk measure with for all .
Two random variables are comonotonic, , if on an event of probability one, for all . The comonotonic allocations of and the constrained inf-convolution are
Let be an -tail risk measure, , , let , and let be an -generator of . Then for every and every quantile uniform of ,
and is an -tail risk measure.
Theorem 4 gives an explicit formula for comonotonic risk sharing among tail risk measures. The optimal comonotonic aggregate risk of is computed from the tail alone, by sharing the tail among the generators. As a consequence the constrained inf-convolution depends on only through its distribution beyond the -quantile, with the largest individual tail parameter. Compared with Theorem 3, where the unconstrained tail parameter is , the comonotonic constraint keeps the aggregate as tail-focused as the least tail-focused agent. For a regulator this means that comonotonic sharing among, for instance, Expected Shortfall agents at different levels produces a measure that still ignores the body of the loss distribution beyond a known level.
The result is proved in the paper, through Lemma 2, in Appendix B. No machine-checked proof of it is known. Formalizing it requires the comonotonic additivity of quantiles and the explicit construction of comonotonic allocations from quantile functions and a quantile uniform. Both are reusable well beyond this paper: they underlie comonotonic risk measures, distortion risk measures and the comonotone-improvement literature.
The theorem looks like a change of variables, and the proof in the paper is short. The work is in Lemma 2. Part (a) needs the comonotonic additivity of the left quantile function, on for comonotonic with sum , and has to produce an allocation whose sum equals the tail everywhere, not only almost everywhere. Part (b) runs the other way. A comonotonic allocation of the tail has to be extended below the -quantile, where the tail carries no information, without breaking comonotonicity with or the sum constraint. The extension needs each component of the tail allocation to be bounded below. That bound is a consequence of comonotonicity and of the tail being bounded below, not a hypothesis.
Equalities in law between tails are a second source of friction. The tail is defined through a quantile uniform, which is not unique, and the statements must hold for every choice.
The probability space is atomless in the classical sense (an explicit predicate, stronger than Mathlib's NoAtoms). The domain of every risk measure is , all measurable real functions. The paper allows any convex cone containing that is closed under equality in law and under taking tails; fixing is a disclosed specialization. Individual risk measures and generators are real valued; is valued in the extended reals. The sum constraint of an allocation is pointwise on . Equality in law of tails, , is encoded by (6) as equality of and , and the law of is written through (6) as well. Quantile uniforms are quantified over, never chosen, and the generator relation is required for every quantile uniform. The maximum is the supremum over the finite index set, with agents. The existence of generators (Liu and Wang 2021, Proposition 3.1) is cited by the paper and enters as a hypothesis. Part (iii) of Theorem 4, which needs the comonotone-improvement theorem, is out of scope.
A real-valued infimum for would return on an empty or unbounded-below set and make the identity of (i) partly vacuous; the extended-real infimum and the nonemptiness of (one agent takes everything) rule this out.
A complete development needs the left quantile function and its comonotonic additivity, the existence of a quantile uniform on an atomless space (Föllmer and Schied 2016, Lemma A.32), the distribution of the tail (6), and the measurability of composed with a random variable. All of these are reusable, and contributions of any of them are welcome.