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?
A life table summarises the survival of a cohort as ages advance, as developed in Promislow's life-table treatment. It provides an essential common language for life assurance, retirement pensions, annuities and reserves. A credible mathematical foundation must make precise when cohort counts define conditional probabilities, how death counts exhaust an assumed closed population, and why commutation-function ratios give the same values as discounted contractual payments. The classical notation is widely understood by actuaries but can conceal assumptions at terminal ages, when there are no remaining lives, and at fractional-year payment times. This formalisation specifies those assumptions so that later results can safely reuse them.
Consider an integer-age cohort with a finite terminal age, nonnegative numbers alive and nonincreasing numbers alive at successive ages. At the terminal age the remaining cohort is zero. Annual deaths are the change in cohort size over each year. Conditional survival starts only from an age with positive numbers alive. The model also has a strictly positive annual discount factor; when the corresponding effective interest rate is nonnegative, that factor is at most one. A due annuity pays on the integer anniversaries at which the insured life is alive. An annual death assurance pays at the end of the year of death. All financial amounts in the principal identities are per unit benefit, valued at the attained age of the insured life.
The opening group establishes that successive survivor and decrement counts conserve population mass. Multi-year survival, conditional and deferred mortality must be derived from original counts and remain coherent under time shifts. A zero survivor count is an explicit boundary of the probability model. Curtate lifetime moments are obtained from the annual death distribution and its tail probabilities. Continuous survival and hazard relationships form an additional interface requiring a genuine measurable lifetime law. They cannot be inferred from the table's integer-age observations without an interpolation assumption.
The next group distinguishes age at selection from time since selection and attained age. Ultimate mortality applies only after the selection period. Within a year, uniform distribution of deaths, constant force and Balducci interpolation share the annual survival endpoints but generally disagree between those endpoints. Each conditional fractional formula needs the corresponding survival denominator to be positive. These are alternative models, so the choice of interpolation must remain explicit.
The commutation columns are defined from the same original survivor counts and a fixed annual discount factor. Discounted survivors and year-end deaths create the first-order columns. Their finite forward sums create the second-order columns, and sums of those forward sums create the increasing-benefit columns. In particular, for survivors the discounted payments begin at the valuation anniversary, whereas for deaths the benefit is payable on the next anniversary. The finite terminal convention is essential for the last year's assurance payment and the last available annuity instalment.
The principal goal is the finite-cohort valuation reconciliation. Starting independently from annual numbers alive and numbers dying, it shows that total deaths exhaust the living cohort, actual survival-contingent payments agree with the annuity commutation ratio, actual annual death payments agree with the assurance commutation ratio, and the commutation sums satisfy their backward recursions. It also establishes the capital identity expressing unit present value as annual death assurance plus the discount loss on an annuity due. No commutation recurrence or present-value equivalence is assumed as an input.
At a valid attained age, the annuity and assurance are independently valued from the original cohort:
As in the classical actuarial notation, the resulting interfaces separate cohort mass from conditional probability and separate mortality from the economic discounting basis. This allows a later actuarial mission to combine them only where the required regularity and positivity assumptions are available. The commutation functions supply a transparent independent valuation route alongside direct finite cashflow sums. Their ratios remain useful as a reference calculation even when production models value very large pension populations by member-level cashflow projection. Higher-order commutation functions are also the natural algebraic representation of benefits that increase by one unit at each subsequent anniversary.
This foundation is reusable across future mortality and valuation missions. A foundational namespace is particularly important where related existing missions already use different local definitions. The present work provides a compatibility design and a proposed canonical public vocabulary. Publishing an older equivalent definition does not automatically establish a safe imported interface: exact source, revision, visibility, and declaration signatures must match. The programme therefore retains existing mission objects and develops explicit crosswalks, rather than silently replacing earlier results.
The mathematical difficulty centres on conditioning, index shifts and independent routes to the same financial result. At an age with no survivors, a formal programming language may return a totalised value for division by zero even though no conditional mortality probability exists. A common off-by-one error values a death at the beginning of its year or includes a due annuity payment after the terminal age. Another error confuses discounting to time zero with discounting to the current valuation age. Select mortality requires careful handling of attained age at the exact selection-duration boundary. Continuous lifetime hazard and moment formulas additionally need probability, measurability and integrability assumptions that finite cohort counts alone cannot supply.
The double-sum commutation identities require a finite discrete summation argument and must use published survivor and assurance conventions consistently. The goal compares separate original definitions of payment cashflows, the population exit distribution, and commutation columns under one valid finite life table. The capstone is nonvacuous: a positive starting cohort and positive discount factor exclude empty-cohort substitutions and make its conditional cashflows meaningful. Its assumptions impose cohort validity and positive discounting; they do not contain the desired present-value identities as hypotheses.
The initial formalisation supplies a canonical finite discrete cohort and annual cashflow basis. The continuous-law, hazard, select and fractional-age results are separately specified mathematical interfaces and are admitted into the formal theorem inventory only when remote declaration checks establish valid Lean signatures. For nonnegative effective interest the annual discount is in the interval from zero excluded to one included. More general deterministic term structures and stochastic discount factors require separate cashflow definitions. Joint-life and competing-decrement extensions must identify any independence or mutually exclusive decrement assumptions explicitly.
No assertion is made about mortality being stationary across calendar years or about the validity of a specific mortality table for a real population. The terminal-age assumption imposes certain death before the finite horizon. It is unsuitable without modification for a lifetime distribution with unbounded support. A lifetime with an atom at an integer boundary requires separate weak and strict survival events; interpreting a one-year death count as the hazard at the death instant is unjustified without further assumptions. Open formal statements remain proof obligations, and passing a declaration check would establish only well-formed Lean, not the mathematical truth of the intended result.
The finite-cohort valuation targets also include independently defined one-year and multi-year mortality probabilities, temporary and deferred annuities, term and endowment assurances, pure endowments, annuities in arrears and increasing finite-term cashflows. The expanded candidate graph has 26 definitions and 48 open theorem obligations in a coherent reconciliation programme. New results require independently derived cashflow-to-commutation identities.
Related proposals LII (commutation functions and finite-term benefits) and LXII (fractional-duration valuation) are in review, not public importable dependencies. Existing published life-table theorems in XLV must be reused where signatures match. The fractional-age and continuous-law interfaces require separate hypotheses. All research targets remain provisional until their exact published-name overlap checks, authoritative declaration elaboration and dependency links are validated. No private diagnostic is counted as a proved theorem.
The increasing-insurance commutation column requires the relative-duration or absolute-age convention to be declared explicitly. Annual UDD includes certain year-end death, but constant-force and Balducci interpolation require annual death probability strictly below one.
Near thermodynamic equilibrium, flows of extensive quantities (heat, matter, charge) depend linearly on the thermodynamic forces (gradients of the conjugate intensive variables). Some of the coefficients in these linear laws describe cross effects: a temperature gradient driving an electric current (Seebeck effect), a voltage driving a heat flow (Peltier effect), a temperature gradient driving diffusion (Soret effect) and its converse (Dufour effect). In 1931 Lars Onsager showed that, as a consequence of the time-reversibility of microscopic dynamics, the matrix of these coefficients is symmetric (Onsager 1931). These reciprocal relations were confirmed experimentally across many classes of irreversible processes (Miller 1960), and Onsager received the 1968 Nobel Prize in Chemistry for them.
This mission formalizes the abstract, finite-dimensional version of Onsager's principle as presented by Landau and Lifshitz (Statistical Physics, Part 1, 1975) and reproduced in the Wikipedia article Onsager reciprocal relations, sections "Abstract formulation" and "Proof".
Let be the fluctuations of thermodynamic quantities from their equilibrium values. For small fluctuations the entropy is quadratic, and Boltzmann's formula gives the Gaussian fluctuation distribution
where is a positive definite symmetric real matrix and summation over repeated indices is understood. Write for the average of with respect to .
The thermodynamic conjugate quantities are . In the quasi-stationary regime the fluctuations relax according to for a real matrix , so that with the kinetic coefficients
The mean value at time of a fluctuation which takes the value at is , and . The time correlation is .
If fluctuations are symmetric under time reversal,
then the kinetic coefficients are symmetric:
The symmetry is the mathematical content of the reciprocal relations: it reduces the number of independent transport coefficients from to and yields the equality of measurable cross-coefficients such as the Peltier and Seebeck coefficients. Together with the positive semi-definiteness of the coefficient matrix (from non-negative entropy production), it is the basic structural input of linear irreversible thermodynamics.
The result is classical and its proof is standard in physics textbooks; this mission produces a machine-checked version of the finite-dimensional argument, including the Gaussian moment identity and the differentiation of the time-correlation function under the integral sign. No machine-checked formalization of this statement is known to the proposer.
The algebraic core is short, but the formal argument needs analytic input that the textbook treats as routine: Gaussian integrals over for a general positive definite (integrability of polynomial moments against and the value of the second moments), differentiation of a parameter-dependent integral involving a matrix exponential, and the passage from an identity valid for to an identity between derivatives at the boundary point , where only a one-sided derivative is available from the hypothesis.
Vectors are functions Fin n → ℝ with Lebesgue measure; matrices are Matrix (Fin n) (Fin n) ℝ, and β.PosDef (which includes symmetry) is assumed in every theorem. The average is the ratio of Bochner integrals, so the normalizing constant cancels. The mean relaxation is the matrix exponential . The time-reversal hypothesis is assumed only for . The entropy and Boltzmann's constant are not modelled; is the primitive datum, as in the source's statement of the principle. The hypothesis is non-vacuous (e.g. satisfies it), and the conclusion concerns , not .
All definitions are collected in Definitions.Def_OnsagerReciprocal_basic (namespace OnsagerReciprocal). Reusable Gaussian-moment lemmas for positive definite quadratic forms are welcome contributions.
In 1913 Albert Einstein and the mathematician Marcel Grossmann published the Entwurf ("outline") of a generalized theory of relativity and a theory of gravitation. It is the first theory in which the gravitational field is described by the ten components of a space-time metric, , and in which Ricci and Levi-Civita's absolute differential calculus (Grossmann's mathematical part) is brought into physics. Its gravitational field equations were superseded by the generally covariant field equations of November 1915, but the framework of the Entwurf — metric as gravitational potential, the energy-momentum law of matter in a gravitational field, a stress-energy expression for the gravitational field itself — carried over to general relativity.
The physical part (Part I, by Einstein) derives the field equations from one requirement: the energy-momentum law must hold for matter and gravitational field together. The derivation runs through an explicit differential identity, eq. (12), whose rewritten form (12a) yields the field equations (18) and the total conservation law (19). This mission formalizes that chain of statements.
Timeline.
All objects live in one coordinate chart, , with the time coordinate. The fundamental tensor is a symmetric matrix field with negative determinant ; is the reciprocal (contravariant) tensor, the inverse matrix, and is the density factor. All sums run over .
A material process is described by its contravariant stress-energy tensor (for incoherent dust, ). Its energy-momentum law in the gravitational field is eq. (10):
The second sum is the momentum (for , the energy) transferred per unit volume from the gravitational field to matter.
The gravitational field carries its own stress-energy tensor , eq. (13):
and the field equations involve the second-order operator of eq. (15),
The Entwurf field equations (18) read , with a constant. Lowering indices with gives the covariant objects , (eq. (14)) and the operator (eq. (16)).
If the energy-momentum law (10) and the field equations (18) hold, then for
The result itself. Eq. (19) is the property Einstein required of any relativistic theory of gravitation: the energy of the gravitational field acts as a source in the same way as every other form of energy, and matter together with field obeys conservation laws of divergence form. Identity (12a) is what makes this work for the Entwurf operator ; together with the matter law (10), the field equations (18) and the gravitational stress-energy are fixed by it.
Formalizing it. These statements are proved in the source by explicit computation, and the steps (12) → (12a) and the covariant forms (20)–(22) are given without the intermediate algebra. A machine-checked development provides the full index computations: derivatives of and in terms of those of , the contractions in (12a) and (12b), and the lowering identities linking to and to . A search of the platform library found no existing formalization of these statements.
There is no conceptual obstacle, but the identities are long. Identity (12a) involves second derivatives of , the derivative of , and contractions over up to six indices. The source gives only the final form of (12) and says the identity is obtained "nach dem angedeuteten Verfahren"; the intermediate algebra, and the analytic facts behind it (differentiability of matrix inversion and of under the standing assumptions), are not written out. A naive expansion of all sums produces thousands of terms.
The first law of thermodynamics is the form the law of conservation of energy takes for thermodynamic processes. For a closed system (no transfer of matter) it is usually written, in the sign convention of Clausius, as
where is the heat supplied to the system, is the work done by the system on its surroundings, and is the internal energy. Heat and work describe a process and depend on the path; the internal energy is a property of the state, and its change depends only on the initial and final states.
The Wikipedia article First law of thermodynamics (revision oldid=1366986255) describes two ways of reaching this statement. In the original "thermodynamic approach" (Clausius 1850, Rankine), heat, defined by calorimetry, and work are primitive notions. In the "mechanical approach" (Bryan 1907, Carathéodory 1909, Born 1921), only adiabatic work is primitive. The law then asserts that adiabatic work is independent of the path, and that this work defines a state function , fixed up to an additive constant. Heat becomes a derived quantity, the residual . This mission formalizes the logical core of the mechanical approach.
A closed system has a set of states. A process has an initial state , a final state , a net work done by the system on its surroundings, and a label recording whether it is adiabatic (carried out inside an adiabatic enclosure, so that energy is transferred only as work). A set of processes stands for the processes that can actually be carried out. It is assumed to satisfy:
A function is an internal energy for if for every adiabatic . For a given , the heat supplied in a process is the residual
Under assumptions 1 to 4,
This is the article's statement: "For all adiabatic processes between two specified states of a closed system of any nature, the net work done is the same regardless the details of the process, and determines a state function called internal energy, ", together with its remark that the internal energy "is defined only up to an arbitrary additive constant of integration".
The goal makes precise the step in the mechanical approach where internal energy is defined from adiabatic work instead of being postulated. It shows which properties of the set of realizable processes are needed for the definition to make sense. Once exists, the familiar consequences follow at once: the Clausius equation for every process, the heat-free character of adiabatic processes, for adynamic processes, the equality of work and heat over a cycle, and the impossibility of perpetual motion of the first kind. Milestones 5 to 10 record these.
The mathematics is elementary and the results are classical. The value of the formalization is that it states exactly the hypotheses under which "path-independent adiabatic work defines a state function" holds. The article itself notes the gaps: experimental evidence for independence from the order of stages is thin (Bailyn), and Münster observes that one cannot always go adiabatically in both directions between two states. Assumption 4 therefore asks only for one direction.
The only non-routine step is existence when accessibility holds in just one direction per state. One defines or , depending on which link exists. Showing that this choice is consistent, and that it gives for an arbitrary adiabatic process , requires splitting into four cases according to how and are linked to . In some of these cases the composite process is an adiabatic cycle, which must be compared with a null process. Without null processes, or without closure under composition, the naive definition is not well-defined.
The Black–Scholes model (Black and Scholes, 1973; Merton, 1973) is the reference model for pricing European options. Its closed-form price, the Black–Scholes formula, is quoted daily by options markets, its partial derivatives (the Greeks) are the standard risk measures that trading desks limit and hedge, and the Black–Scholes equation is the prototype of the parabolic pricing PDEs that are solved numerically when no closed form exists. Merton and Scholes received the 1997 Nobel Memorial Prize in Economic Sciences for this work.
Timeline. Bachelier (1900) first applied Brownian motion to option pricing. In the 1960s Sprenkle, Boness, Samuelson and Merton refined the theory. Black and Scholes found the risk-neutral hedging argument in 1968 and published the formula in The Pricing of Options and Corporate Liabilities (Journal of Political Economy, 1973); Merton's paper of the same year extended the mathematical framework and coined the name.
Fix a strike , an expiry , a constant risk-free rate and a constant volatility . At time the time to maturity is and the spot price of the (non-dividend-paying) stock is . Let
be the standard normal distribution and density functions, and set
The Black–Scholes call and put prices are
In the alternative (Black '76) parametrisation one uses the discount factor and the forward price , with , and . Under the risk-neutral measure the terminal price is with standard normal.
On the domain the call price is and satisfies
together with the boundary and terminal conditions as , as , and as .
The result. The goal is the statement that ties the model's two faces together: the closed-form price is a classical solution of the pricing PDE with the payoff as terminal datum. The Greeks are what hedging strategies are built from (delta hedging is the core of the model's replication argument), put–call parity is the basic no-arbitrage relation, and the risk-neutral and binary-option identities are the probabilistic reading of the two terms in the formula.
Formalizing it. All results here are classical and proved in textbooks (e.g. Hull, Options, Futures, and Other Derivatives). The work is formalization: building a reusable, machine-checked library for the normal distribution function, the Black–Scholes price and its sensitivities, and Gaussian expectations of log-normal payoffs, on top of Mathlib's real analysis and its Gaussian measure gaussianReal.
Each identity is elementary on paper, but the calculus is long: every Greek requires differentiating through a logarithm, a square root and a quotient, and the simplifications rest on the identity . The limits in the goal need Gaussian tail estimates (e.g. as , where grows while decays). The risk-neutral identities require computing Gaussian integrals over half-lines with an exponential weight, i.e. a change of variables shifting the mean of the normal distribution.
All objects are real-valued and deterministic: is defined by the integral formula above (a Lebesgue integral over ), by its closed form, and prices by the formulas, as functions of with parameters . Partial derivatives are stated with HasDerivAt (genuine differentiability plus the value), except in the goal's PDE, where deriv is used together with an explicit clause on the open domain. Each theorem carries the standing assumptions , , , where they are needed; the parity identities hold without them and are stated unconditionally. At and the formula is undefined in the source, so the boundary and terminal conditions are stated as one-sided limits rather than values. Risk-neutral expectations are integrals against the standard Gaussian gaussianReal 0 1 of an explicit log-normal terminal price; no stochastic calculus (Itô integrals, SDEs, Girsanov, Feynman–Kac) is required or formalized. The dividend-paying extensions, American options and the perpetual put are out of scope; binary options are formalized for the non-dividend case .
Contributions of reusable lemmas (derivative of , symmetry , limits of at , Gaussian half-line integrals) are welcome.
The units of a ring of algebraic integers control much of the arithmetic of a number field. They decide when two generators of the same principal ideal differ, they enter the analytic class number formula through the regulator, and for real quadratic fields they are the solutions of Pell's equation . Dirichlet's unit theorem (Dirichlet, 1846) determines the structure of this unit group completely: it is finitely generated, and its rank is computed from the way the field embeds into and . With the finiteness of the class group, it is one of the two basic finiteness theorems of algebraic number theory and appears in every introductory text on the subject.
This mission follows the account of the theorem, the regulator and its standard examples given in the Wikipedia article Dirichlet's unit theorem (https://en.wikipedia.org/wiki/Dirichlet%27s_unit_theorem).
A number field is a field containing with finite dimension as a -vector space. Its ring of integers consists of the elements of that are roots of monic polynomials with integer coefficients, and its unit group is the group of invertible elements of .
The field has exactly field embeddings . Let be the number of embeddings with image in , and the number of pairs of complex-conjugate non-real embeddings, so that . Equivalently, and count the real and complex infinite places of , i.e. the absolute values . Write for a real place and for a complex place.
The rank of an abelian group is the largest number of elements that are independent over . For this is the largest number of multiplicatively independent units. Units of finite order are exactly the roots of unity in .
Put . If generate modulo roots of unity, the matrix has every row summing to . The absolute value of the determinant of the square matrix left after deleting any one column is the regulator of .
The result itself. The unit theorem gives . This is the input for the analytic class number formula, where the regulator appears next to the class number. It also yields the finiteness of solutions of norm-form and -unit problems and the structure of solutions of Pell's equation. It is the model for Hasse and Chevalley's -unit theorem and for Leopoldt's conjecture on -adic regulators.
Formalizing it. The theorem itself is classical and has already been formalized: Mathlib contains the unit group's rank, a system of fundamental units and a regulator in its NumberField.Units development. This mission adds the surrounding statements of the source article as explicit, independently checkable targets. These are the alternative descriptions of the signature, the rank in quadratic fields and in extensions, the unit theorem for non-maximal orders, the well-definedness of the regulator in the generator-free form given in the article, and the worked examples. The examples involve explicit numerical regulator values that are not in the library.
The upper bound on the rank follows by showing that the logarithmic image of the units is discrete. The hard part is the lower bound: one must produce independent units. This requires constructing units of prescribed size at the infinite places. The obvious approach of writing down units explicitly does not work in general. The standard route uses Minkowski's geometry of numbers. The examples carry their own difficulty: showing that given units are fundamental and pinning a regulator to four decimal places takes certified bounds, not just exhibiting units. The statement for orders requires passing between and through a finite-index argument.
Statements are in Lean 4 over Mathlib, in the namespace DirichletUnitTheorem. They use Mathlib's notions directly: NumberField, 𝓞 K, InfinitePlace, nrRealPlaces/nrComplexPlaces for /, InfinitePlace.mult for , IsTotallyReal/IsTotallyComplex for real/imaginary quadratic fields, and NumberField.Units.regulator for the regulator in the example milestones. The rank is Module.rank ℤ of the additive version of the unit group. This is a cardinal, so finite generation and the rank are stated separately. An order is a subring of of finite additive index. Approximate numerical values from the source are encoded as open intervals.
Units of finite order are written with IsOfFinOrder, so no statement depends on a particular torsion API. The goal is not trivialized by the truncated subtraction in , because always holds.
Welcome contributions include proofs that bridge to the existing Mathlib development, certified numerical bounds for regulators, and the order and extension statements, which are reusable beyond this mission.
Supply and demand is the basic model of price determination in a perfectly competitive market: holding everything else fixed, the price of a good adjusts until the quantity buyers want equals the quantity sellers offer. The model is the standard first chapter of microeconomics, it underlies partial-equilibrium policy analysis (taxes, subsidies, price controls), and it is applied to labour markets (with the wage as the price) and money markets (with the interest rate as the price). See the Wikipedia article, which is the source of this mission.
Timeline. Demand curves were first drawn by Cournot (1838); supply curves were added by Fleeming Jenkin (1870), who also drew the first comparative-statics diagrams of a curve shift; Marshall's Principles of Economics (1890) popularised the "Marshallian cross". Qualitative versions of the comparative-statics law are much older: Ibn Taymiyyah (14th century) wrote that "if desire for goods increases while its availability decreases, its price rises".
Prices and quantities are real numbers. A supply curve is a function giving the quantity supplied at each price, and a demand curve is a function giving the quantity demanded. A set of admissible prices is fixed (for example all reals, or the positive reals). Supply is upward-sloping: is strictly increasing on . Demand is downward-sloping (the law of demand): is strictly decreasing on .
A pair is a market equilibrium of , written , when
i.e. the market clears at price with quantity transacted.
An increase in demand (a right shift of the demand curve) from to means for every admissible price ; an increase in supply from to means for every admissible price.
The market curve of finitely many individual curves , , is their horizontal sum . The point elasticity of a curve at is . The article's example curves are and (supply) and and (demand).
For upward-sloping supply and downward-sloping demand on , with equilibria at admissible prices:
The corresponding statements for decreases (left shifts) are the same statements with the indices exchanged.
The comparative-statics laws are the qualitative predictions that make the supply-and-demand model usable: they say in which direction price and quantity move after a change in a non-price determinant (tastes, incomes, input costs, technology). The simultaneous-shift law is the precise form of the qualitative statement quoted above, and it also records what the model does not predict (the direction of the quantity change is left open).
These results are classical and elementary. The point of this mission is a clean, reusable formal vocabulary for partial-equilibrium market models (equilibrium, curve shifts, market curves, elasticity) on which later missions about taxes, surplus, and elasticity can build.
The mathematics is elementary; the care is in the modelling. Two traps: assuming the equilibria exist and lie in the admissible price set is necessary (the article's linear supply curve is negative for , and the isoelastic curves are only meaningful for ); and the law of demand or of supply cannot be dropped, since for an upward-sloping demand curve (Veblen or Giffen goods, discussed in the article) the comparative-statics conclusions can fail.
All curves are total functions ; slope assumptions are imposed only on the admissible set , an arbitrary set of reals, and every equilibrium price is assumed to lie in . Strict monotonicity is used for both supply and demand, as in the article's figures and its law of demand. Existence of an equilibrium is not asserted; the statements are about given equilibria. Real powers and are Mathlib's Real.rpow, and statements about them are restricted to . The point elasticity uses Mathlib's deriv.
The definitions live in a single definition file, SupplyDemand_Model, in the namespace SupplyDemand, shared by all statements.
Comparative advantage is the principle that two parties can both gain from trade even when one of them is more productive at producing every good. It is usually credited to David Ricardo's On the Principles of Political Economy and Taxation (1817), with earlier formulations in an anonymous 1814 pamphlet and in Robert Torrens' Essay on the External Corn Trade (1815). It is widely described as one of the most powerful yet counter-intuitive insights in economics, and it underlies the standard argument that trade patterns are driven by relative, not absolute, productivity.
A short timeline of the two-country, two-good theory:
The Ricardian model has two countries, Home and Foreign, and two goods, cloth and wine. Labour is the only factor of production; it moves freely between sectors inside a country but not between countries. Home has a labour force ; producing one unit of cloth takes units of labour and one unit of wine takes . Foreign's data are written with a prime: , , .
Home has a comparative advantage in cloth when its opportunity cost of cloth in terms of wine is lower than Foreign's:
which is the same as saying that Home is relatively more productive in cloth, . Nothing is assumed about absolute productivity.
In autarky a country can produce and consume any bundle with . Under free trade both goods sell at world prices ; the wage in the cloth sector is and in the wine sector , and workers move to the sector with the higher wage. A country that produces only cloth and trades at the world relative price can consume any bundle with ; a country that produces only wine can consume any bundle with .
If Home has a comparative advantage in cloth and the world relative price lies between the two autarky prices,
then Home's autarky set is contained in its consumption set when it specializes in cloth, and Foreign's autarky set is contained in its consumption set when it specializes in wine. When the corresponding inequality is strict, the inclusion is strict: the country can consume bundles it could not produce itself.
The result is the textbook form of the classical argument for specialization and trade: the gain does not depend on either country being absolutely more productive, only on a difference in relative labour costs. The price-bound milestone says where world prices can settle, and the terms-of-trade milestone says that both countries gain exactly at prices between their opportunity costs. Ricardo's numbers make the general statements concrete.
These are classical results with elementary proofs. The value of the mission is a reusable, precisely stated Ricardian model — definitions of countries, autarky sets, trade consumption sets and competitive outputs — on which later missions in this series (many goods, many countries, the Dornbusch–Fischer–Samuelson continuum, Haberler's production possibility curves) can build.
There is no deep obstacle; the work is in stating the model faithfully. The obvious shortcut is to compare autarky and trade only at the two corner bundles, or to drop the wage-based description of who produces what and simply assume each country specializes. The milestones instead derive specialization from the wage comparison, so the five-case relative-supply statement has to cover the boundary prices where workers are indifferent and output is not unique.
All quantities are real numbers. A country is a structure carrying , , and proofs that all three are positive, so no unit labour requirement can be zero. Prices are explicit arguments with positivity hypotheses wherever they are divided by. Bundles are pairs . A competitive output is a bundle with full employment (, ) in which a sector produces only if its wage is at least the other sector's wage. Relative demand is not modelled as a function; the price bound is stated for any competitive outputs whose world cloth and world wine supplies are both strictly positive (finite, nonzero relative supply, as market clearing with a finite positive relative demand requires). The comparative-advantage hypothesis is kept in the goal as the section's standing assumption, although the price-bound hypotheses imply its non-strict form.
Contributions welcome: proofs of the milestones and the goal, and follow-up missions extending the model to many goods or many countries.
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.
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.
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.Online stochastic matching models display advertising and similar allocation problems in which requests arrive one at a time and must be served immediately. A bipartite graph links a set of advertisers to a set of impression types; requests arrive, each of a type drawn independently with , and each request must be assigned at once and irrevocably to an unmatched interested advertiser, or dropped. Performance is measured by the competitive ratio , where OPT is the maximum matching of the realized graph.
Without distributional knowledge the best possible ratio is (Karp, Vazirani and Vazirani, 1990). Knowing the type distribution allows more:
This mission concerns the analytic core of Theorem 3, the general-rates bound.
For an advertiser , let be the LP flow into . Its neighbours , which include a dummy advertiser with , are indexed by . For each neighbour, is the expected number of random lists , and is the neighbour's flow, so that . Write and .
Claim 2 of the paper introduces the functions
where is the probability that is matched through a list headed by . The per-advertiser bracket is
and the reduced function of three variables is
In Lean these are h, g, bracket f x y and R f β s in RandomListsMatching.GeneralRates.
For , any and reals with , and ,
The paper bounds below by (p. 15), so this inequality is the whole of what Theorem 3's numerical constant rests on.
The result. Theorem 3 gives for online stochastic matching with general (non-integral) arrival rates, improving the of Manshadi et al. The probabilistic half of its proof reduces matching probabilities to the closed forms and ; the paper then states that "in the remaining part of the section, we only use algebraic manipulations and the following properties of functions and ". That remaining part, posed here, is an exact real inequality, and it is where the constant is decided.
Formalizing it. The paper proves Claim 3 in one line ("can be easily verified by taking first and second order partial derivatives") and Claim 4 by a grid computation over cubes of side , with no recorded error analysis. A machine-checked proof replaces both. It also settles the regime of the constant: Claim 4 as printed, with the constraint "for ", is false, and the bound holds in the limit form stated here. None of these statements has a formal proof anywhere, to the extent of the search made for this mission.
The margin is small. The minimum of over the feasible region is about , attained near on the boundary ; the margin over is under . Any argument that loses a constant factor in the estimates of , or replaces by a rational bound that is not tight to five digits, fails. The bound is a three-variable statement with the minimum on a boundary face, so a one-variable monotonicity argument does not settle it.
The second difficulty is the function itself. Its two-case definition is continuous but the quotient form has a removable singularity at , which is exactly the end of the interval on which Claim 3 asserts convexity and concavity. Derivative computations that are routine away from the diagonal need care there.
The natural first idea for the goal, to apply Claim 4 directly to the bracket, does not type-check: the bracket depends on the whole family , and the reduction to three variables through the chord and cross-sum bounds is a separate step.
Real.exp 1, is Real.log 2, and is the exact rational (0.706 : ℝ).Fin k, and is allowed.MonotoneOn, AntitoneOn); convexity is ConvexOn ℝ (Set.Icc 0 y). The derivative in (5) is deriv (fun t => h y t) 0, the derivative in the second argument; the page's is a slip.A complete development needs the derivative calculus of on , including the diagonal, and certified interval bounds for and . The latter is reusable well beyond this mission. Proofs of Claim 3 or Claim 4 alone are welcome contributions.