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?
Many convex programs impose inequalities valued in a vector space: componentwise inequalities, positive-semidefinite constraints, and families of ordered resource constraints are all instances of one cone order. Chapter 8 of David G. Luenberger's Optimization by Vector Space Methods develops a global theory for this setting. A perturbation of the constraint produces a convex value function, continuous linear functionals positive on the ordering cone become Lagrange multipliers, and a strict-feasibility condition yields an attained dual optimum. This mission formalizes the progression in §§8.2–8.6, culminating in the book's Lagrange Duality Theorem.
Let and be real normed spaces, let be a nonempty convex set, and let be a convex cone. The cone induces the relation
A continuous linear functional is dual-positive when for every . A map is cone-convex on when its value at a convex combination is below the corresponding convex combination of its values in this cone order. The primal program is
where is real-valued and convex on .
For a multiplier , the Lagrangian and its possibly infinite dual value are
The perturbed primal value replaces the zero right-hand side by . Lean represents and in EReal, so infeasible perturbations have value and objectives unbounded below can have value without arbitrary defaults.
Assume has nonempty interior, the primal value is finite, and there is a strictly feasible point with
Prove that a dual-positive exists and attains
If attains the primal infimum, also prove complementarity and that minimizes over .
Five source milestones delimit the reusable theory. A closed convex cone is recovered from all dual-positive inequalities (§8.2, Proposition 1). The finite-height epigraph of the extended perturbation value is convex, and that value is antitone in the cone order (§8.3, Propositions 1–2). A Lagrangian saddle point is sufficient for primal feasibility and optimality when the cone is closed (§8.4, Theorem 2). Finally, multipliers for two perturbed right-hand sides bound the change in optimal objective value from both sides (§8.5, Theorem 1). The root then states §8.6, Theorem 1 rather than duplicating the equivalent multiplier theorem from §8.3.
The capstone provides both equality of optimal values and an attained multiplier. It applies to a single vector inequality, so finite systems of scalar inequalities and matrix-cone constraints fit the same statement once their ordering cones are supplied. Complementarity and Lagrangian minimization turn a primal optimizer and multiplier into a certificate. The sensitivity milestone additionally gives quantitative information about how the optimum changes when the constraint right-hand side moves.
Formalization produces a reusable cone-order layer independent of coordinate choices. coneLE, dualPositive, and ConeConvexOn can support later Kuhn–Tucker, vector optimization, and conic programming developments. The EReal value functions preserve infeasibility and unboundedness, two cases that a real-valued sInf encoding would collapse. This is a formalization mission for a classical theorem, not a claim that the underlying duality result is open.
The theorem's strict-feasibility condition is load-bearing. Feasibility cannot replace interior feasibility, and nonempty interior of alone does not supply a Slater point. Equality constraints also cannot be converted into pairs of inequalities while retaining strict feasibility; Luenberger explicitly warns about this after the theorem.
The cone assumptions differ across milestones. The main strong-duality theorem does not require to be closed or pointed, whereas the bipolar and saddle-sufficiency statements require closedness. Using Mathlib's stronger ProperCone everywhere would silently add both topological and order hypotheses and shrink the theorem. Another tempting simplification is to make both value functions real. That loses the empty feasible set and unbounded dual subproblem, precisely the boundary cases used when comparing perturbations. The saddle inequalities must also have the correct orientation: the multiplier coordinate is maximized and the primal coordinate is minimized.
The mission uses ConvexCone ℝ Z with a custom induced relation; it deliberately does not assume a lattice order on . Multipliers are continuous linear maps . The root assumes a real finite optimum through IsGLB and a real witness , while lagrangeDualValue and perturbationValue retain EReal codomains. The strict condition is written as membership of in interior P, exactly matching .
No finite-dimensionality, reflexivity, completeness, closedness, or pointedness is added to the root. Closedness appears only where the source uses cone separation to recover primal feasibility. The sensitivity item assumes the two candidate points are feasible, their multipliers are dual-positive and complementary, and each point minimizes its shifted Lagrangian; these hypotheses spell out “solutions and corresponding multipliers” without relying on informal terminology.
Contributions may formalize cone separation, perturbation-value geometry, saddle certificates, or strong duality. Finite-dimensional orthant and positive-semidefinite specializations are useful corollaries but do not replace the general goal. Local multiplier rules, equality constraints, differentiable Kuhn–Tucker conditions, and Chapter 9's local theory remain outside this mission.
AI generated, I think it's correct
The matrix-multiplication exponent measures the asymptotic arithmetic cost of multiplying square matrices. A bound means that, over the field under consideration, matrices can be multiplied in field operations for every . Matrix multiplication is a central benchmark in algebraic complexity and a basic subroutine in linear algebra, graph algorithms, and symbolic computation.
The Coppersmith--Winograd tensor and the laser method produced the strongest bounds on for several decades. The 1990 tensor-square analysis gave . Later analyses of larger powers improved the numerical bound, but they organized their recursion through values assigned independently to constituent tensors. Duan, Wu, and Zhou identified a loss in that organization: several fine constituents that can coexist inside one coarse block may be counted as though they had to be selected independently. Their asymmetric-hashing framework partially compensates for this combination loss. The paper's full second-power specialization improves the best bound obtainable from the square of the Coppersmith--Winograd tensor to ; see Section 6.3 and its parameter Table 2 in Duan--Wu--Zhou.
This mission isolates that second-power result. It is smaller than the paper's record-setting eighth-power calculation, but it contains the genuinely new asymmetric-hashing and hole-repair mechanisms in their first complete form. It therefore provides a focused bridge from the existing formalization of the classical square analysis to later combination-loss methods.
For a field , the matrix-multiplication tensor
encodes multiplication of an matrix by a matrix. A restriction applies one linear map to each tensor leg, while a degeneration permits polynomial families of such maps and takes their first nonzero coefficient. A degeneration from the diagonal tensor gives a border-rank upper bound of .
The Coppersmith--Winograd tensor with parameter is
It has border rank at most . Its coordinate partition has six supported types, and the square has fifteen coarse constituent types with . A large tensor power contains many blocks with prescribed joint and marginal type distributions. The laser method retains blocks whose variables are disjoint and interprets their direct sum through Schönhage's asymptotic sum inequality.
Duan--Wu--Zhou refine this organization by also retaining a split distribution for the fine indices inside each coarse constituent. Coarse - and -blocks are made unique, while compatible coarse triples may initially share a -block. The resulting partially damaged constituent tensors are described as broken copies of a standard-form tensor. The formal target uses , the full Section 6 construction, and the paper's released second-power parameters.
For every field ,
The source reports the stronger numerical endpoint , so the displayed rational inequality has strict slack. The Lean declaration has exactly the same field quantification and uses exactly the same matMulExp definition as the existing Coppersmith--Winograd mission; only the theorem name and rational endpoint change.
The mission first isolates the available-block shuffling interface extracted from Definitions 5.3--5.5 and Claims 5.8--5.10, then formalizes the finite covering core of the Hole Lemma 5.6. The subsequent tensor realization by zeroing and identification, the multiple-copy Corollary 5.11, the compatibility-rate identity of Lemma 6.7, the probabilistic part of Claim 6.8, and the global restricted-splitting value inequality in Equation (25) remain visible structural leaves rather than being hidden inside scalar assumptions. The numerical milestone instantiates Equation (25) with the exact data of Section 6.3 and Table 2 and checks a strict value surplus at . The structural proof must also make explicit the conversion from the paper's six-symmetrized value to a direct HasTauValueAtLeast witness for the mode-symmetric CW square. The final bridge applies the existing tau-value/rank machinery and transfers the Strassen-preorder exponent bound to matMulExp.
The mathematical result gives the first improvement over the classical Coppersmith--Winograd number while continuing to use only the tensor square. It separates improvement of the tensor analysis from improvement obtained merely by moving to a much higher tensor power. The same standard-form and restricted-splitting language is then reused by the paper's higher-power algorithm, which reports .
For formalization, the mission adds reusable infrastructure for nested tensor partitions. Existing CW-square work records coarse support types and actual matrix-multiplication restrictions. This mission extends that layer with fine split distributions, compatibility between levels, broken-block bookkeeping, and repair of holes without replacing tensor statements by unverified scalar values. Those definitions are prerequisites for later asymmetric-hashing, complete-split, and more-asymmetry analyses.
The bound is known mathematically and was published at FOCS 2023. The open work is a machine-checked reconstruction. The underlying CW tensor, border-rank certificate, canonical tensor-square grading, Salem--Spencer sets, direct-sum tau-value notion, asymptotic sum inequality, and exponent equivalence already exist on Prove2Me. The new frontier is the cross-level combination-loss analysis and its exact numerical specialization.
The central difficulty is that coarse and fine decompositions cannot be optimized independently. Two coarse triples may share a -block, and a fine -block can be useful for one triple, compatible with several, or removed by a collision. Counting all locally valuable fine constituents therefore does not certify a direct sum. Conversely, requiring every coarse -block to be unique discards precisely the combinations that produce the improvement.
The Hole Lemma must also preserve the actual tensor. A broken copy lacks some fine variable blocks; combining several such copies is useful only when a degeneration covers every required block with controlled loss and does not duplicate monomials. On the numerical side, the same-marginal maximum-entropy term and restricted-splitting values must be bounded with certified real inequalities. Floating-point output from MATLAB is evidence for a witness, not a Lean proof.
The mission uses the existing TensorObj, MMObj, restriction, degeneration, asymptotic-rank, HasTauValueAtLeast, matMulExp_strassen, and matMulExp declarations in environment 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e. Top-level results quantify over an arbitrary field. Finite supports and block indices are represented by finite types; probability and split distributions are nonnegative real functions of total mass one; entropy and numerical optimization live in the reals.
The formalization is restricted to for the capstone, although generic definitions and source lemmas may quantify over levels and finite index types. A valid proof must connect scalar rate inequalities to witnessed restrictions or degenerations yielding direct sums of concrete matrix-multiplication tensors. A constant-valued surrogate for the restricted-splitting value, a hypothesis that already assumes the desired exponent bound, or a certificate definition containing its own conclusion is outside scope.
Contributions are welcome for standard-form tensor encodings, finite permutation arguments, hole repair, type and split counting, entropy maximization certificates, certified logarithm and power inequalities, and the final tau-value/rank assembly. Statements should identify the corresponding definition, lemma, claim, equation, or table in the source.
Convex duality converts an optimization problem over points into one over linear functionals. It supplies lower bounds, certificates of optimality, and alternative formulations whose geometry can be simpler than the primal problem. In §§7.8–7.12 of David G. Luenberger's Optimization by Vector Space Methods, this theory is developed for finite-valued convex and concave functions on convex subsets of a real normed space. The capstone is Fenchel duality with restricted domains and an attained continuous-linear-functional dual optimum. This mission preserves that functional-analytic setting rather than reducing the theorem to Euclidean space or silently extending the functions to the whole space.
Let be a real normed space, let be nonempty convex sets, let be convex on , and let be concave on . For a continuous linear functional , the restricted convex conjugate and restricted concave conjugate are
The convex conjugate is admitted into only when its defining set is bounded above; the concave conjugate is admitted into only when its defining set is bounded below. Because and are nonempty and the functions are real-valued, these predicates exactly exclude the unwanted infinite endpoint. The Lean definitions use real sSup and sInf, with boundedness carried explicitly by theorem hypotheses.
The restricted epigraph of is the set of satisfying and ; the restricted hypograph of reverses the scalar inequality. Luenberger's qualification requires a common point of the relative interiors of and , represented by Mathlib's intrinsicInterior, and also requires ordinary nonempty interior of at least one of these two graph sets.
Assume the finite primal value is the greatest lower bound of
Prove that some attains
If attains the primal infimum, also prove that attains both conjugate extrema at : and .
The mission records four source milestones. A local minimum of a convex function on its convex domain is global (§7.8, Proposition 1). Convexity of a restricted function is equivalent to convexity of its restricted epigraph (§7.8, Proposition 2). The finite-conjugate domain and the convex conjugate are convex (§7.10, Proposition 1). Finally, a closed restricted epigraph agrees pointwise on with the continuous-linear biconjugate (§7.10, Proposition 2). Together these statements expose the geometric and conjugacy interfaces on which the capstone depends without turning every paragraph of the chapter into a separate item.
The theorem gives an attained dual certificate in an arbitrary real normed space. Equality of primal and dual values eliminates a duality gap, while attainment produces a specific functional that can certify an optimal primal point through simultaneous conjugate equality. The biconjugate milestone is independently useful: it expresses a closed convex function as a supremum of continuous affine minorants on its domain.
Formalizing this material adds a restricted-domain conjugacy API that is not supplied by the existing project artifact named fenchelConjugate. That artifact accepts finite-valued functions on a Euclidean space and has no independent convex domain or concave conjugate. Reusing it here would erase hypotheses that are central to Luenberger's theorem. The new definitions remain small, but their exact boundedness contracts make them reusable for later separation, minimax, and Lagrange-duality missions. The theorem is classical; the mission asks for a checked development faithful to the 1969 source and the current Mathlib representation of continuous dual spaces.
The qualification is not the usual finite-dimensional slogan that relative interiors merely intersect. The source additionally demands that either the restricted epigraph or restricted hypograph have nonempty ordinary interior. Dropping that condition changes the theorem in infinite-dimensional spaces. Replacing intrinsicInterior by topological interior would also make valid lower-dimensional domains appear empty.
Extended values create another boundary. Real sSup and sInf are meaningful here only together with nonempty domains and the respective boundedness hypotheses. Treating their default values outside those hypotheses as genuine conjugates would admit false dual candidates. A finite-dimensional conjugate definition avoids neither issue and would prove only a special case. The biconjugate target must quantify over continuous linear functionals, not all algebraic linear maps, because closed epigraph separation is topological. Finally, the dual statement must include actual attainment; proving only equality with a supremum would omit a principal assertion of §7.12.
All primal functions are finite-valued real functions. Infinite conjugate values are represented by domain predicates—BddAbove for and BddBelow for —rather than by changing the public conjugate codomain. The primal finiteness assumption is encoded by a real number together with IsGLB, which simultaneously rules out an empty feasible intersection and an infimum of . Epigraph pairs are ordered as to match Mathlib conventions, although Luenberger prints the scalar coordinate first.
The ambient space is normed but is not assumed finite-dimensional, reflexive, or complete. Both and are explicitly nonempty. The main theorem keeps the common intrinsic-interior condition and the disjunctive ordinary-interior condition verbatim. Contributions may develop separation lemmas, boundedness facts for restricted conjugates, or direct proofs of the milestone statements. A whole-space Euclidean specialization is welcome only as a corollary, not as a replacement for the root. The minimax theorem of §7.13 and extended-real lower-semicontinuous variants are outside this mission.
Every full-dimensional convex body is sandwiched between an ellipsoid and its -fold dilation: shrinking the minimum-volume covering (Löwner–John) ellipsoid about its centre by the factor lands inside the body,
and the factor is tight on simplices. This rounding theorem underlies the ellipsoid method, John's theorem on the Banach–Mazur distance to the Euclidean ball, and much of modern convex geometry. The mission formalizes §8.4 of Boyd & Vandenberghe for polytopes , exactly as the book proves it: existence and uniqueness of the extremal ellipsoid, the KKT identities at the normalized optimum (, , ), the convex-combination step that produces the ball, and affine invariance.
A nonlocal game is played between a classical referee and two or more cooperating players who are not allowed to communicate during the game. In the two-player, one-round setting, the referee samples a pair of questions from a distribution , sends to Alice and to Bob, and receives answers and . The players win when a predicate accepts. Before the game begins they may agree on a strategy and share a resource, but after receiving their questions they are isolated from one another.
Nonlocal games occupy a useful interface between complexity theory and quantum information. From the perspective of complexity theory, they are the basic objects underlying multiprover interactive proofs: a verifier delegates a computation to separated provers and uses the consistency of their answers to distinguish valid from invalid claims. Classical two-prover games play a central role in the PCP theorem, hardness of approximation, and soundness amplification. Allowing the provers to share entanglement leads to the class and to a substantially richer theory. The theorem shows how dramatically entanglement changes this landscape: even estimating the entangled value of a nonlocal game can encode undecidable computation Ji--Natarajan--Vidick--Wright--Yuen 2020.
From the perspective of quantum information, nonlocal games are operational formulations of Bell experiments. A separation between classical and entangled values witnesses correlations that cannot be explained by a local hidden-variable model. The same framework supports self-testing, in which near-optimal behavior certifies the underlying state and measurements up to local equivalence, and device-independent cryptography, in which security or randomness is certified from observed input-output statistics rather than a trusted description of the devices. Representative references include Cleve--Høyer--Toner--Watrous 2004, Reichardt--Unger--Vazirani 2013, and Pironio et al. 2010. The survey of Palazuelos--Vidick 2016 describes further connections among nonlocal games, Bell inequalities, operator spaces, and quantum information.
Thus the value of a nonlocal game is simultaneously a complexity-theoretic soundness parameter and a quantitative measure of the power of nonclassical correlations. Understanding how this value changes under natural operations on games is important in both subjects.
We take the finite answer alphabets to be nonempty. In a classical strategy, Alice's answer depends only on , Bob's answer depends only on , and the players may coordinate using shared randomness. In a finite-dimensional entangled strategy, the players share a bipartite state and use POVM measurement operators
for their respective questions. The probability of producing answers on questions is
The supremum of the winning probability over all such finite-dimensional strategies is the entangled value . This optimization ranges over arbitrary local dimensions, shared states, and local measurements, which is one reason even apparently elementary questions about nonlocal games can be difficult.
For a positive integer , the repeated game consists of independently sampled copies of played simultaneously. Alice receives , Bob receives , and they answer with tuples and . They win only if
for every coordinate .
Parallel repetition is a basic method of soundness amplification. Starting from a game that dishonest players cannot win with certainty, the verifier repeats the test in the hope of driving the optimal success probability rapidly toward zero. The difficulty is that independence in the verifier's sampling does not force independence in the players' strategy. Alice may choose her entire answer tuple as a function of all her questions, Bob may do the same, and an entangled strategy may use a single state and joint measurements spanning all coordinates. In particular, one cannot obtain an upper bound on merely by analyzing the strategy that plays each coordinate independently.
For classical games, Raz's parallel repetition theorem gives exponential decay whenever the one-shot value is below one Raz 1998. Establishing the corresponding behavior for entangled games has been a long-running problem. A general polynomial bound was proved in Yuen 2016, implying for the first time that tends to zero for every finite two-player entangled game with .
The full exponential-decay theorem was recently settled by OpenAI. In Chapter 6 of Ten Advances in Mathematics and Theoretical Computer Science, OpenAI proves that for every finite two-player entangled game with , there is a constant such that
for every positive . OpenAI also released a Lean certificate for the result. This resolves the general quantum parallel-repetition conjecture, but it does not end the study of the problem. The proof introduces quantitative losses and a substantial technical apparatus, and there remains considerable value in finding alternative arguments, isolating the essential mechanism, improving the dependence on the one-shot gap and answer size, and producing shorter or more conceptual formal proofs.
This mission develops a reusable Lean framework for parallel repetition rather than formalizing only one paper. Its targets are organized by the strength of the asserted decay.
The main mission theorem is the fundamental asymptotic statement:
Equivalently, for every , all sufficiently large satisfy . This statement deliberately specifies no rate. It is a stable top-level theorem that can be recovered from any sufficiently strong quantitative bound.
A stronger target asks for game-dependent constants and such that
The abstract formulation avoids fixing a particular exponent or logarithmic correction. More refined formalizations can record explicit dependence on the gap , the answer alphabet, or other game parameters. Yuen's 2016 theorem is one important result at this level.
The exponential target asks for game-dependent constants such that
Following OpenAI's recent resolution, this target is now a theorem rather than an open conjecture. Within this mission it remains a central milestone: contributors may formalize the released argument in the mission's common interface, construct an independent proof, seek a more elegant or modular proof, or establish sharper quantitative variants.
These levels do not exhaust the project. The same framework can accommodate explicit finite- inequalities, stretched-exponential estimates, bounds for structured classes of games, improved parameter dependence, and reductions showing that one decay statement implies another.
The foundational Lean development represents a game by finite question sets , finite answer sets , a nonnegative normalized question distribution , and a Boolean verification predicate . The parallel-repetition theorems explicitly assume that and are nonempty. The development defines finite-dimensional entangled strategies using density matrices and POVM measurement operators, defines the repeated game on tuples, and takes the entangled value as a supremum over all finite-dimensional strategies. Repeated strategies are indexed by complete question tuples and are not required to factor coordinatewise.
A complete development will draw on formal libraries for finite probability, tensor products, positive semidefinite matrices, density matrices, POVMs, trace norms, fidelity, entropy, mutual information, and correlated sampling. These components should be formulated for reuse and should expose the dependence of each bound on the relevant game parameters.
The goal is both to verify parallel-repetition theorems and to build a dependable language for nonlocal games in Lean. Formalization forces distinctions that are easy to suppress on paper: whether constants depend on the game, whether a bound holds for all or only asymptotically, which strategy model is optimized over, and which hypotheses are needed for a particular rate. The mission welcomes reconstructions of known proofs as well as new, shorter, or conceptually different proofs.
Interior point methods solve linear programs by moving through the interior of the feasible set instead of along its edges — the approach that turned Karmarkar's 1984 breakthrough into today's practical large-scale solvers. This mission formalizes the primal path following algorithm of Chapter 9 of Bertsimas–Tsitsiklis. For the logarithmic barrier
replaces the constraint ; the minimizers of over trace the central path, characterized by the KKT conditions (9.17): , , , , (Lemma 9.5). The algorithm follows the path with one Newton step of the barrier problem per shrink , maintaining the proximity invariant
. The goal theorem is Theorem 9.7: with and a -close start, after iterations the algorithm reaches primal and dual feasible solutions with duality gap — the explicit form of the celebrated iteration bound. Alongside it we formalize the generic potential-reduction scheme (Theorem 9.4): any algorithm cutting by per step reaches gap within an explicit .
Can the feasibility of a system of linear inequalities be decided in a provably small number of iterations? The ellipsoid method — the algorithm with which Khachiyan showed in 1979 that linear programming is polynomially solvable — answers this with pure convex geometry. This mission formalizes Chapter 8 of Bertsimas–Tsitsiklis. An ellipsoid is
with symmetric positive definite. The geometric engine is Theorem 8.1: the half-ellipsoid is contained in the explicitly constructed ellipsoid ,
and the volume contracts:
. Two integer-data estimates make the contraction decisive: every extreme point of with entries bounded by has coordinates in (Lemma 8.2), and a full-dimensional bounded such polyhedron has (Lemma 8.4). The goal theorem is Theorem 8.2: started on a ball of volume at most containing , with a lower bound on when is nonempty, the ellipsoid method correctly decides whether is empty within iterations — the explicit iteration count behind the polynomial-time headline.
Why do network linear programs return integer answers for free? This mission formalizes the structural theory of the minimum cost network flow problem of Chapter 7 of Bertsimas & Tsitsiklis: a directed graph with external supplies , arc costs , and the node-arc incidence matrix — an matrix in which every column has exactly one (start node) and one (end node) — so that flow conservation reads , forcing the standing assumption . Because the rows of sum to zero, the book works with the truncated matrix of the first rows. The combinatorial heart is the correspondence between algebra and graph structure: a set of arcs forming a tree determines a unique tree solution of , off (Theorem 7.3); connectedness makes full-rank (Corollary 7.1); and a flow vector is a basic solution if and only if it is a tree solution (Theorem 7.4). The goal theorem is the integrality theorem (Theorem 7.5): for the uncapacitated problem on a connected graph, every basis matrix has an integer inverse (its determinant is by the tree/lower-triangular argument), integer supplies make every basic solution integer, and integer costs make every dual basic solution integer — whence integer optimal primal and dual solutions exist whenever the optimal cost is finite (Corollary 7.2). This is the fountainhead of combinatorial integrality in linear optimization, feeding the max-flow min-cut mission that follows.
How does the optimal cost of a linear program respond when the problem data change? Chapter 5 of Bertsimas-Tsitsiklis studies the standard form problem (rows of linearly independent) as the requirement vector and the cost vector vary. On the convex set of feasible right-hand sides, and under the standing assumption that the dual feasible set is nonempty, the optimal cost is finite and convex (Theorem 5.1) — indeed over the extreme points of the dual feasible set, a piecewise linear convex function whose breakpoints are exactly where the dual optimum is non-unique. The capstone (Theorem 5.2) identifies the generalized gradients of : if the primal at is feasible with finite optimal cost, then is an optimal solution of the dual if and only if is a subgradient of at (Definition 5.1: for all ) — the precise sense in which dual variables are marginal costs. Dually (Theorem 5.3), the set of cost vectors with finite optimal cost is convex, the optimal cost is concave on , and near any with a unique primal optimum , is linear with gradient . Local ranging (Section 5.1) and parametric programming (Section 5.5) are the procedural companions, folded into the design notes.
Every linear programming problem has a shadow. To the primal we associate the dual , whose variables price the primal constraints: one dual variable per primal constraint and one dual constraint per primal variable, with signs governed by the correspondence of Table 4.1. This mission formalizes §4.1–4.5 of Bertsimas–Tsitsiklis: the dual of a general-form linear program, the involution "the dual of the dual is the primal" (Theorem 4.1), and weak duality for any primal-feasible and dual-feasible (Theorem 4.3) with its two corollaries — an unbounded primal forces an infeasible dual (Corollary 4.1), and feasible with are automatically both optimal (Corollary 4.2). The goal theorem is strong duality (Theorem 4.4): if a linear programming problem has an optimal solution, so does its dual, and the respective optimal costs are equal — proved in the book by running the simplex method with the lexicographic pivoting rule of Mission IV on a standard-form transform. The statement is deliberately the book's attainment form: by Table 4.2 the primal and the dual can be simultaneously infeasible (Example 4.5), so an unguarded equality of optimal values is false. The mission closes with complementary slackness (Theorem 4.5): feasible and are simultaneously optimal if and only if for all and for all — the certificate structure behind the dual simplex method and every LP optimality check.
How does one actually solve a linear program? Chapter 2 showed that if a standard-form problem subject to , has an optimal solution, it has an optimal basic feasible solution; the simplex method searches among basic feasible solutions, moving along edges of the feasible set in cost-reducing directions. This mission formalizes the mathematics of Chapter 3 of Bertsimas–Tsitsiklis: feasible directions, the reduced costs
measuring the cost rate along the basic directions, the optimality conditions of Theorem 3.1 ( implies optimality, and conversely at nondegenerate optima), the basis change of Theorem 3.2, and the pivot iteration itself — encoded as a predicate relating a basis/BFS pair to its successor, so that every theorem covers every pivoting rule. The goal theorem is Theorem 3.3: if the feasible set is nonempty and every basic feasible solution is nondegenerate, the simplex method terminates after a finite number of iterations, ending either with an optimal basis and an associated optimal basic feasible solution, or with a direction satisfying , , certifying optimal cost . The secondary capstone, Theorem 3.4, removes the nondegeneracy assumption: under the lexicographic pivoting rule every tableau row other than the zeroth stays lexicographically positive, the zeroth row strictly increases lexicographically, and the simplex method terminates on every problem — the anticycling guarantee that also supplies the optimal-basis existence used by the strong duality theorem of Mission V.
Every linear programming problem asks to minimize a linear cost over a polyhedron — a set of the form , or in standard form . Chapter 2 of Bertsimas–Tsitsiklis develops the geometry of these feasible sets, and its central achievement is making the intuitive notion of a "corner point" rigorous. There are three natural candidates: the extreme point — a point of that cannot be written as a convex combination of two other points of (purely geometric, representation-independent); the vertex — the unique minimizer of some linear cost over (geometric, via supporting hyperplanes); and the basic feasible solution — a feasible point at which linearly independent constraints are active (algebraic, the object the simplex method actually computes with). This mission formalizes polyhedra, active constraints, vertices and basic (feasible) solutions, and proves the fundamental Theorem 2.3: for a nonempty polyhedron all three notions coincide. Around the capstone sit the supporting pillars: polyhedra are convex (Theorem 2.1), the characterization of points pinned down by linearly independent active constraints (Theorem 2.2), finiteness of the set of basic solutions (Corollary 2.1), and the basis-column characterization of basic solutions in standard form (Theorem 2.4) — the combinatorial engine behind the simplex method of Chapter 3 and the root of the entire series.
A continuous piecewise linear (CPWL) function is one assembled from finitely many flat pieces glued along flat seams. Every ReLU network computes such a function, and every such function is computed by some ReLU network. Questions about how deep a network must be are therefore questions about the internal structure of CPWL functions.
In 1993 Breiman built such functions from hinges: maxima of two affine maps. Sums of hinges approximate anything, but from two dimensions up they fail to represent most CPWL functions exactly. Wang and Sun (2005) widened the maxima, proving that every CPWL function on ℝⁿ is a signed sum of maxima of at most n+1 affine maps. Twenty years on it remains the workhorse structural fact, reducing any question about a network to a question about a single max gate and underpinning every known upper bound on the depth of exact representation.
That includes the newest one: at STOC 2026, Bakaev et al disproved the short standing conjecture that ⌈log₂(n+1)⌉ hidden layers are necessary, showing ⌈log₃(n−1)⌉+1 suffice. In this mission we deliver a machine-checked proof of the Wang and Sun theorem so future formalizations of network expressivity can invoke it rather than reprove it. Note that we take as given the lattice representation of Tarela and Martínez, independently proved by Ovchinnikov, which writes any CPWL function as a max of mins of its affine pieces. That is the one external ingredient the argument consumes, and our definition of CPWL builds it in.
How quickly does the empirical mean of independent random variables concentrate around the true mean? This question is the analytic engine of the entire theory of stochastic bandits: every optimistic algorithm (Explore-Then-Commit, UCB and its relatives) is calibrated by a tail bound on the sample mean. This mission formalizes the subgaussian framework of Chapter 5 of Lattimore–Szepesvári's Bandit Algorithms: a random variable is -subgaussian when for all , and the Cramér–Chernoff method converts this moment-generating-function control into the exponential tail . The goal theorem is the Hoeffding-type bound: the sample mean of independent -subgaussian deviations exceeds the true mean by with probability at most , together with its confidence form — the exact bound every UCB index is built from. These few lines of analysis are cited by every regret bound in the series.
Multi-agent reinforcement learning approximates a global value function by summing per-agent local value functions learned independently — a trick that works surprisingly well in practice (ride-hailing dispatch, restless bandits) but had no general theoretical justification. Chen and Peng (arXiv:2506.02385) explain why: they define a Markov entanglement measure for the joint transition dynamics of a multi-agent MDP, directly analogous to quantum entanglement of a two-party state, and show it controls exactly how much error this value-decomposition trick incurs. This mission formalizes their sharpest quantitative bound (Theorem 4): the error of decomposing the global Q-function into per-agent local Q-functions is controlled, entrywise, by the agent-wise total-variation measure of Markov entanglement.
A platform sourcing items from monopolistic sellers with private quality cannot tractably maximize its true profit: the bundle revenue is neither monotone, submodular, supermodular, subadditive, nor superadditive. Theorem 4.6 of Buying to Bundle: Optimal Sourcing from Monopolistic Sellers shows that the simple surrogate threshold mechanism — maximize the linearized objective — is profit-optimal up to a factor in large markets. Prove it: Bernoulli concentration for the bundle quality plus sub-exponential control of the dispersion gap (Lemma 4.5).
A Hadamard matrix is a square array of +1s and −1s whose rows are mutually orthogonal — equivalently, one whose determinant attains the absolute maximum that Jacques Hadamard proved in 1893 any ±1 matrix can reach. The story opens earlier, with James Joseph Sylvester's 1867 doubling construction producing such matrices in every power-of-two order; Hadamard himself added orders 12 and 20. The conjecture bearing his name asserts that a Hadamard matrix exists for every order divisible by four. Raymond Paley's 1933 construction from finite fields settled vast new families, and computer searches filled stubborn gaps — beginning with order 92 at JPL in 1962 and reaching order 428 only in 2005, after which 668 became the smallest order whose existence is still unknown. Far from a curiosity, these matrices are workhorses of applied mathematics, underpinning error-correcting codes (the Reed–Muller code that sharpened Mariner spacecraft imagery), spread-spectrum and CDMA signal design, optimal statistical designs of experiments, and coded-aperture spectroscopy. Settling the conjecture would close a 130-year-old gap where combinatorics, number theory, and design theory meet.
Show that every nonconstant complex polynomial has a complex root.
A complete formal proof of Fermats Last Theorem for exponent 5: for all positive natural numbers a,b,c, a^5 + b^5 != c^5. The proof follows the classical Legendre-Dirichlet approach (1825-1830): Case 1 (5 does not divide a,b,c) is dispatched by congruences, and Case 2 (5 divides one of them) uses infinite descent through the ring Z[zeta_5]. The open hard leaf is the Z[zeta_5] PID step (flt5_zeta5_ring_witnesses).
Nearly every measure of Boolean function complexity was known to be equivalent — except sensitivity. Proving the conjecture unified the whole picture.
A binomial option-pricing model is more than a numerical approximation: it is a finite complete market in which prices can be derived recursively from self-financing replication. At each node, the one-period stock-and-bank market fixes the value of the two possible continuation payments. Repeating this calculation yields the unique European replication price. When an option can be exercised early, the holder instead chooses between its immediate payment and continued exposure to the market. This creates a finite optimal-stopping problem whose value is determined by the Snell recursion.
This mission builds on Financial Derivatives I (payoff geometry, portfolios and put–call parity) and Financial Derivatives II (two-state arbitrage, unique replication and risk-neutral valuation). It proves the multi-period European and American/Bermudan results without introducing an unproved continuous-time stochastic integral or Black–Scholes formula.
The primary source is Paul Wilmott, Sam Howison and Jeff Dewynne, The Mathematics of Financial Derivatives (1995), Chapter 10, printed pp. 180–194. The European valuation is equation (10.16), printed p. 188; the American exercise recursion is equation (10.17), printed p. 191. The stock tree and related risk-neutral conventions appear in §§10.1–10.3, and the European/American algorithms in Figures 10.4 and 10.7. The dynamic-replication, finite stopping-policy and seller-superhedging equivalences below are rigorous extensions of the source's calculations, not verbatim propositions from the book. DOI.
Fix a finite number of periods ; an initial stock price ; constant up, down and bank-growth multipliers satisfying
The stock is dividend-free, with one-period outcomes and when its current value is . A current bank deposit becomes next period. Fractions, short stock positions and bank borrowing are allowed. There are no transaction costs or position constraints. The stronger assumption is important in a multi-period market: it keeps the stock strictly positive at every descendant node, so the FD-II two-state replication theorem is applicable everywhere.
The unique positive risk-neutral up and down weights are
These weights price next-period cashflows. They are derived from the stock and bank prices, and are not assertions about real-world stock-move frequencies. For next-period values , define
At current stock price , a one-period replicating portfolio contains
so and next period's stock and bank holdings deliver the prescribed child values. FD-II provides the exact one-period no-arbitrage and uniqueness justifications; this mission must prove that the assembled strategy remains self-financing across all dates and histories.
Model all terminal histories by a full binary payoff tree, allowing any signed and path-dependent payoff. At maturity the claim value equals its terminal payment . At earlier nodes the recursion is
Prove that this value equals the discounted sum of terminal payments under the product risk-neutral weights. Prove its linearity and monotonicity. Recursively construct an adapted stock/bank strategy that matches the continuation values at each child and rebalances without cash injection. Show that it replicates every terminal history and has the only possible initial cost. A European claim introduced as a separately traded security preserves no-arbitrage exactly when its quote equals that cost.
When the terminal payoff depends only on the final stock price, all histories with the same up count share a value. At time and after up moves,
Prove that the efficient -node recombining algorithm implements the same backward recursion as the full tree:
For path-dependent contracts, retaining the distinct histories is necessary. Recombining solely on the stock level would lose contractual information and is not asserted in that generality.
An exercise-reward tree assigns a real immediate payment at each node and records whether exercise is permitted there. Maturity exercise is mandatory; intermediate exercise is available at every date for an American contract and only at selected dates for a Bermudan contract. A stopping policy must use only the history known at the current node: it can stop when permitted or specify separate future decisions for the two child states.
At maturity the exercise value equals . At earlier nodes, let be the continuation value. The Snell recursion is
Prove, by finite backward induction, that every admissible stopping policy has discounted value no greater than , and construct a policy attaining by comparing exercise with continuation at each node. Thus is the finite optimal-stopping value, including ties, and allowing more exercise dates cannot decrease the holder's value. In particular, an American option with the same maturity payoff is worth at least its European counterpart.
As an independent financial theorem, construct a seller's adapted self-financing superhedge starting with the Snell value, and prove that no lower initial capital covers the payment for every admissible holder exercise policy. The holder's stopping policy is distinct from the writer's stock/bank trading strategy. For a put with immediate payment , the resulting recursion is the book's American-put algorithm. It also applies to calls, arbitrary finite exercise sets and signed rewards under the stated maturity convention.
The capstone, provisionally FinancialDerivatives.FD03.finiteBinomial_pricing_and_optimal_exercise, combines four genuinely proved statements:
The proof graph proceeds through market and stock positivity, one-step valuation, full-tree algebra, finite path sums, local hedge replication, recursive self-financing, recombining rows, exercise-policy upper bounds and attainment, and seller superhedging. Every parent must use the relevant actual accepted helpers, with no capstone conclusion packed into a definition or assumed as a hypothesis.
The time horizon may be zero, rates may be zero or negative as long as , and European claims may have negative payments. Stock positivity throughout the tree requires . At exercise-continuation ties either admissible decision is optimal. Strong no-arbitrage excludes and . Statements about American calls never being exercised early need separate dividend and interest assumptions and are not made unconditionally here.
Chapter 10's dividend-yield adjustments (§10.6, pp. 191–193) require distinguishing ex-dividend stock growth from total shareholder return; they are reserved for an explicit bridge to FD-08. CRR-to-Black–Scholes convergence is a separate advanced branch requiring precise asymptotics and a continuous-time pricing foundation. The book's numerical comparisons alone do not establish that theorem. The chapter's exercise connecting binomial and finite-difference methods is allocated to the later numerical-analysis missions.
The mission will reuse published, verified Prove2Me and pinned-Mathlib statements. Its natural-language descriptions, Lean declarations, source ledger, milestone ordering and independent read-backs will be audited before the owner confirms and submits a Draft. A Draft or a locally prepared Lean snippet is not evidence that a definition compiles or a theorem has been proved.
Every component mission transcribed one layer of Bitcoin Core's validation: the subsidy schedule, compact targets and retargeting, the merkle root, the ledger accounting, median time past and the header rules, the activation heights and flag exceptions, serialization and hashing, the Script interpreter, the signature layer, the SegWit and Taproot dispatch. None of them is a consensus rule on its own. The rule is the way AcceptBlockHeader, CheckBlock, ContextualCheckBlock and ConnectBlock combine them — in which order the tests run, which ledger each transaction sees, where the fees and sigop costs accumulate, what the clock may reject, which historical blocks are exempt, and what state results. This mission writes that composition down, as the executable of the umbrella contract, states the declarative and independently, and proves the two contract theorems. (validation.cpp, tx_verify.cpp, chainparams.cpp)
A chain state is the list of validated headers from the genesis to the tip together with the UTXO set (a ledger of coins: output, creation height, coinbase flag). The genesis state holds the genesis header and an empty ledger, as the source never adds the genesis coinbase. A candidate block is offered with the local clock ; the outcome is accept S' undo, invalid, futureTime (BLOCK_TIME_FUTURE, a temporary rejection) or missingPrev (the block does not build on the tip).
Header path (AcceptBlockHeader): proof of work, the parent lookup, then ContextualCheckBlockHeader in source order — nBits against GetNextWorkRequired (the period's first block supplied from the chain), the median-time-past floor, the two-hour ceiling against the clock, the BIP34/66/65 version floors. CheckBlock: merkle root and mutation, size and count limits, exactly one coinbase first, CheckTransaction for every transaction, the legacy sigop bound. ContextualCheckBlock: IsFinalTx against the lock-time cutoff (median time past once CSV is active), the BIP34 height push in the coinbase, CheckWitnessMalleation (the commitment in the last qualifying coinbase output, the 32-byte nonce, or no witness at all), the weight limit. ConnectBlock: the genesis shortcut, the BIP30 scan with IsBIP30Repeat and the BIP34 shortcut, GetBlockScriptFlags with the two exception blocks, and the loop — CheckTxInputs, the fee range, SequenceLocks, GetTransactionSigOpCost against 80,000, CheckInputScripts through the complete VerifyScript (Taproot branch included), UpdateCoins — then the coinbase bound against GetBlockSubsidy. DisconnectBlock spends the block's outputs back and restores the inputs from the undo data in reverse, with the clean flag and the two unspendable-coinbase exceptions.
Every layer below is the published mission's function: coreSubsidy, nextWorkRequired, checkProofOfWork, computeMerkleRoot, medianTimePast, versionOutdated, blockScriptFlags, lockTimeFlags, sequenceLocks, verifyScriptFull. Nothing is re-transcribed.
is a predicate, not a program: a header predicate in the PoW mission's specTarget form with the parent, difficulty, time floor, clock ceiling and version floors; a block predicate; a contextual predicate; and a ledger predicate that quantifies over the transactions in sequence — each spends existing, mature coins of valid value, the inputs cover the outputs, the BIP68 specification satisfiesBIP68 holds, every input script verifies, the fees and sigop costs stay within their bounds, BIP30 freshness holds where the scan applies, and the coinbase is bounded by the fees plus the specification subsidy. extends the headers and folds UpdateCoins over the transactions.
genesis_checkBlock): the mainnet genesis block passes CheckBlock, by kernel evaluation.acceptHeader_iff), time classification (futureTime_iff, validate_clock, futureTime_transient): the future-time rejection is exactly characterized, transient, and the only clock dependence.checkTransaction_iff, checkBlock_iff, contextualCheck_iff, checkTxInputs_iff, sequenceLocks_iff, connectLoop_iff, connectBlock_iff): each Boolean stage equals its predicate, the BIP68 one through the published fold_acceptance.bip30_history): exactly when the BIP30 scan is skipped.connectBlock_apply, apply_spec, reachable_wellFormed, work_increases): the resulting ledger is the fold, reachable states are well formed, chain work strictly increases.disconnect_connect): the undo data restores the previous ledger, cleanly.acceptance): .With the component missions, the umbrella's two contract theorems are now Lean theorems about a concrete, source-linked rendering of the pinned mainnet rules, with no parameter left abstract: hashes are SHA-256d, signatures are secp256k1 ECDSA and BIP340 Schnorr, scripts run through the full interpreter, and the historical exceptions are the source's. The definitions were exercised on the real chain: the genesis block, blocks 1–170 as the header chain, and block 170 — the first transaction between two users — validates end to end against the ledger holding block 9's coinbase, is rejected when its signature is altered or the spent coinbase is immature, is classified futureTime at an early clock, and disconnects back to the original ledger cleanly.
What remains outside: the proof-of-work hardness and signature unforgeability (computational assumptions, not functional correctness), the on-disk and networking layers, and a reorganization across multiple blocks, which is the disconnect theorem applied in sequence.
The loop breaks at the first failing transaction and threads four accumulators; its characterization needs the fee total and sigop cost to be non-negative so that running-range tests collapse to the final bound, which in turn needs the block predicate's non-negative outputs — the hypotheses on connectLoop_iff and connectBlock_iff. CheckTxInputs uses nSpendHeight - coin.nHeight with natural subtraction, which happens to agree with the specification form for every coin height. The future-time test sits in the middle of the header chain, so classifying it requires the four earlier tests to pass. DisconnectBlock restores inputs in reverse and spends outputs by exact match, so the identity needs the txids distinct, the outputs fresh and every ledger coin spendable with a positive height — which is where reachability and the BIP30 scan enter.
Policy is off; fJustCheck is false; assumed-valid shortcuts are not modeled (scripts are always checked). The chain is linear: a header whose parent is not the tip is the missingPrev outcome, as BLOCK_MISSING_PREV is not a validity verdict. Block hashes and byte orders are those of the serialization mission. No Mathlib is required; the development imports only Std.
validation.cpp, consensus/tx_verify.cpp, consensus/tx_check.cpp, coins.cpp, kernel/chainparams.cpp at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48. SourceUK defined benefit pensions may combine salary-related benefits, guaranteed minimum pensions (GMP), underpins, different increase promises, survivor entitlements and payment guarantees. Applying a minimum at retirement can produce different payments from applying it to each later instalment. Likewise, a guarantee payable to an estate cannot automatically extinguish a legally protected survivor benefit. These distinctions affect the expected present value and administration of a scheme's promises. Standard life-contingency methods are developed by Dickson, Hardy and Waters (2020), https://doi.org/10.1017/9781108784184, and Promislow (2015), https://www.wiley.com/en-us/Fundamentals+of+Actuarial+Mathematics%2C+3rd+Edition-p-9781118782460.
The main contract has a finite horizon of calendar-month instalments indexed by . A valid date mapping supplies each instalment's actual Gregorian date. Consecutive mapped dates must follow the next calendar month, using a fixed original payment-day anchor and clamping that day at month end when necessary. A member's actual date of death is represented separately for each mortality scenario, within the interval after their last alive instalment and before the next scheduled instalment.
A finite joint scenario law , with , indexes award information , the member's final alive period , and the survivor's final alive period . The horizon terminal state represents survival to the horizon. No independence among these variables is assumed. A payment due at date has discount factor , and the expected present value is
The first ordinary pension tranche offers award-date amounts and . An automatic award-date underpin fixes and retains the selected alternative's own subsequent increase schedule and linked survivor entitlement. A payment-date floor, , is a different promise because it may switch the winning alternative later. A second tranche has a separate increase schedule. Monthly amounts and weekly statutory rates use explicitly different units.
For ordinary non-GMP benefits, a scheduled annual limited price indexation rate with floor and cap , , is , where is the relevant price index movement. In this illustrative contract, a first scheduled increase within a year of retirement uses the complete-month fraction of the capped annual rate. Later increases occur on scheduled annual dates. Statutory and contractual rounding, index lookbacks and component eligibility remain distinct.
Prove that for the same joint law, with a strict example. Distinguish the exercise-date information available to a decision-maker from later mortality or inflation outcomes. Formalise floors, caps, compounding, separately scheduled first increases, and both member and survivor indexation paths.
The scheme's statutory pre-1988 GMP has no scheme increase under section 109 of the Pension Schemes Act 1993. Qualifying post-1988 GMP receives the full relevant increase on 6 April following the payable date, then on subsequent eligible 6 April dates, without ordinary first-increase pro-rating. Pre-commencement GMP revaluation is a different process. See sections 109–110: https://www.legislation.gov.uk/ukpga/1993/48/section/109.
For eligible cases under section 87(1) or 87(2), let be the weekly relevant sum, the GMP increase since cessation after the specifically applicable pre-1985 transfer-credit growth disregard, the appropriate addition and the later earnings addition. The conditional protected weekly aggregate is
The later earnings term applies only where the scheme provides qualifying post-cessation employment-related accrual under section 87(4)(d). Eligibility separately excludes employment left before 1 January 1985 and employment ceasing to be contracted-out before that date, as provided in section 87(7). For survivors, section 87(2) uses the prescribed half-member-GMP cessation baseline and the actual member death date. The relevant sum, statutory assumptions for the later earnings addition, dates, transfers and special-case entitlement are externally certified scheme/member inputs. The section 87(3)(a) complete-substitute case, sections 91–92 special circumstances and transitional provisions require separate assessment. See https://www.legislation.gov.uk/ukpga/1993/48/section/87.
A statutory survivor GMP entitlement uses a separately certified payable date no earlier than member death; annual 6 April increases are measured from that date. This entitlement is kept separate from the contractual survivor amount. The comparator with an estate guarantee can displace only scheme-permitted survivor amounts above the protected statutory floor. A positive top-up meets any higher applicable certified statutory minimum without adding the entire GMP a second time.
Pensions Act 1995 section 53 permits certain excess pension increases in one tax year to be credited towards specified statutory increases in the immediately following tax year, subject to eligibility and allocation restrictions. Pension-credit-attributable pensions are excluded by subsection (3A). Distinguish actual increments after certified credits from the full deemed statutory increase. A generic credit arithmetic definition does not determine statutory eligibility: https://www.legislation.gov.uk/ukpga/1995/26/section/53.
Establish finite joint-law cashflow valuation identities, member/survivor payment boundaries and the distinction between parallel estate-plus-survivor payments and a scheme-permitted replacement arrangement. Show that tranche-by-tranche floors can exceed an underpin applied to the aggregate pension.
Reconcile the scenario-by-scenario and separately assembled expected present values of a two-tranche monthly pension with option-linked survivor benefits, scheduled ordinary increases, statutory GMP protections and conditional section 87 floors. Prove that the original award exceeds either first-tranche award, both member and survivor payment-level minima are met and the difference between parallel and replacement guarantees equals only the contractually displaceable survivor surplus. The independent section 53 results are supporting work, rather than an assumed automatic offset within the integrated root.
The formalisation permits scheme rules and certified statutory inputs to be translated into explicit cashflows, with benefit eligibility, date boundaries and unit conversions inspectable. It also provides reusable finite-state valuation and option identities. The underlying life-contingent valuation identities are already established in Dickson, Hardy and Waters (2020). The combined contractual synthesis is an original derived formalisation target. Its present Lean theorem statements have no accepted machine-checked proofs and are not claimed to occur verbatim in those textbooks.
The maximum operator does not commute with expectation or with aggregation over heterogeneous benefit streams. Award-date decisions must respect their information sets. GMP dates and ordinary increase dates use different event rules; death may occur between payments. Where estate guarantees overlap survivor payments, the amount displaced depends on the precise pension promise and protection of statutory benefits. A simple interchange of finite sums proves a valuation reconciliation only after each contingent entitlement has been defined correctly.
The Lean development uses finite scenarios, nominal instalment amounts, explicit Gregorian dates, a monthly payment calendar, death-date intervals, deterministic increase schedules and certified legal inputs. Its finite two-life indicators and expectation arithmetic reuse the published Actuarial Mathematics CII definitions ActuarialJointD.alive, onlyY, mass and expect via small award-state, retirement and censoring adapters. These are imported from public CII modules at the matching pinned Mathlib revision; the adapted definitions are checked by a separate Lean compatibility proof before reliance in the integrated capstone. The section 87 protections model specified ordinary cases and exclude stated historical circumstances; they do not determine universal legal entitlement. Section 53 credits are a separate conditional component. Special statutory cases, GMP equalisation, conversions, insurer-specific administration and arbitrary exercise-time information are outside the integrated capstone. The finite identities do not require member and survivor independence. Five additional open F theorem targets extend the proved CII annuity and guarantee identities. They include bounded survivor-state equivalence and award-indexed and actual F survivor valuation identities. Their methods have compiled in a private exact-revision Lean check. Neither automatically establishes the integrated scheme promise, because death-fixed survivor amounts, scheduled increases and statutory minima require separate hypotheses. All principal theorem statements remain open proof obligations until independently accepted by the remote verifier.
The fourth mission in the financial-derivatives series follows the Cambridge chapter by Paul Wilmott, Sam Howison and Jeff Dewynne, The Mathematics of Financial Derivatives (1995), Chapter 11, Exotic and Path-dependent Options, printed pp. 197–205. In particular, §§11.2–11.4 introduce compound options (options on options), chooser options and barrier options. Chapter 12 gives the fuller treatment of barrier valuation; Chapters 13–15 develop more advanced path-dependent models. This mission establishes exact finite-market identities underpinning the Chapter 11 examples. Its capstone is a derived rigorous formulation of simple-chooser pricing, rather than a claim that the book states it in this formal notation.
The preceding FD-03 mission models a strictly arbitrage-free, dividend-free repeated binomial market as a full binary tree. FD-04 will reuse its definitions for market parameters, the stock tree, the European payoff tree and backward-induction valuation. As of 27 October 2026, FD-03 is in review and its definitions have not yet been confirmed as publicly importable. The corresponding paper mathematics is established, while the new Lean declarations and the unaccepted FD-03 theorems remain open formalisation work. Basic real algebra and finite structures already exist in Mathlib. No unproved FD-03 theorem is treated as an axiom.
Let the stock start at , with up multiplier , down multiplier , and gross per-period bank factor such that . Trading is frictionless, the stock has no dividends, and the same binomial parameters remain fixed at every node. Write for the FD-03 backward-induction price of a European payoff after steps when the stock begins at . The arithmetic discount factor over periods is , which is meaningful even when .
For any strike and stock price , put
Strikes are normally nonnegative for actual option contracts. The core equalities hold for signed , making the Lean theorem more general without changing the financial interpretation. All contracts settle in the same currency. Valuations are time-zero values; a payoff computed at the choice date still needs to be discounted back to time zero.
The principal target is an exact simple chooser option pricing formula. Supporting targets cover payoff-level put–call parity, recursive valuation, a finite two-stage valuation identity, compound exercise values and complementary barrier contracts. Each target must have a non-vacuous Lean statement whose conclusion follows from earlier definitions and accepted theorems.
A simple chooser permits the holder to choose, after periods, between a European call and European put with the same strike , common final expiry a further periods later, and the same underlying stock. At the choice date the two option values are
The chooser pays the more valuable of these two options at that date, so its time-zero price is
The put–call parity lemma for the remaining periods is
Hence the choice-date payoff decomposes as
Risk-neutral linearity and the two-stage valuation identity then yield the root goal:
Here expires at final maturity, whereas the added European put expires at the choice date with discounted strike . The result covers , , ties at the choice date and negative interest rates compatible with . It assumes identical call and put strikes, expiry and exercise conventions. A general chooser with different strikes or expiries has a different decomposition.
The formal root is FinancialDerivatives.FD04.simpleChooser_pricing_identity. It directly asserts the boxed equality for the concrete FD-03 valuation operator, rather than introducing the equality as a hypothesis or hiding it in a definition.
A call-on-call has choice/exercise time after steps, underlying call strike , underlying expiry another steps later, and compound strike . Its exercise payoff at stock price is . Define the corresponding time-zero binomial valuation and prove basic positivity, zero-strike reduction (when the underlying call value is nonnegative), and monotonicity as the compound strike increases. Proving a Black–Scholes/Geske closed form requires continuous-time assumptions and is outside this discrete foundational mission.
A discretely monitored upper barrier is touched if at least one observed stock price satisfies . The observation sequence must state explicitly whether spot and maturity are included. On any common path, for terminal call payoff , define the knock-in payoff as when touched and zero otherwise, and define the knock-out payoff with the complementary trigger. Their sum is always the ordinary call payoff. There is no rebate, and the in/out contracts share identical monitoring and terminal settlement rules. This is a payoff identity; the full valuation and diffusion barrier PDE are reserved for later missions.
Rubinstein's original chooser-option discussion (1991) demonstrates why a chooser can be decomposed into a longer-dated call and a shorter-dated put. This makes the pricing calculation auditable and supplies a compositional theorem for subsequent missions. The compound and barrier branches supply independent contract primitives. Future continuous-time models can reuse the payoff-level decomposition while replacing the finite backward recursion with an appropriate discounted conditional expectation. Cox, Ross and Rubinstein (1979) provides the foundational arbitrage-based binomial valuation framework.
The hard formal steps derive put–call parity from the concrete repeated-binomial recursion, show that two-stage valuation equals pricing directly over the combined horizon, and establish additivity of European prices for arbitrary terminal history trees. The depths n, m and n+m require structural induction and precise indexed-tree rewriting. The main theorem cannot be established by assuming the chooser formula, assuming put–call parity, or defining the chooser price to be its intended decomposition.
Zero-step horizons, ties at choice, and negative rates consistent with positive gross growth are included. All chooser options here have identical call and put strikes, expiry dates and exercise conventions. Monitoring for barrier contracts is an explicitly supplied sequence of stock observations; touching the level counts as a hit and zero rebates are required for in/out parity. Continuous-monitoring diffusion barrier pricing and Geske compound-option closed forms belong to later missions.
Wilmott, P., Howison, S. and Dewynne, J. (1995), The Mathematics of Financial Derivatives: A Student Introduction, Cambridge University Press, Chapter 11, pp. 197–205, especially §§11.2–11.4. Cambridge chapter. Book DOI.
Rubinstein, M. (1991), Chooser Options, University of California, Berkeley research manuscript, 6 February 1991. University-hosted PDF. Original same-strike chooser decomposition.
Cox, J. C., Ross, S. A. and Rubinstein, M. (1979), Option pricing: A simplified approach, Journal of Financial Economics, 7(3), pp. 229–263. DOI. Finite binomial arbitrage-pricing foundation.
Since block 709,632 (BIP341 activation, November 2021) every version-1 witness program with a 32-byte payload is a Taproot output. Spending it means either a key-path spend — one Schnorr signature by the output key — or a script-path spend that reveals a leaf script together with a control block proving that the leaf is committed to by the output key, and then runs the leaf under the Tapscript rules of BIP342. Both paths are evaluated by the version-1 branch of VerifyWitnessProgram, which the published VerifyScript mission left as a parameter (TaprootHandler). This mission supplies that parameter from the source and closes the script-validation layer. (VerifyWitnessProgram, BIP341, BIP342)
The transcription covers the tagged hashes (TapLeaf, TapBranch, TapTweak, TapSighash), the merkle path of a control block, the key tweak check through the x-only tweak-add of libsecp256k1, the BIP341 signature hash with all its hash types and the annex, CheckSchnorrSignature, and the Tapscript interpreter rules: the OP_SUCCESSx scan, MINIMALIF as consensus, OP_CHECKSIGADD, the ban on OP_CHECKMULTISIG, the validation-weight budget, OP_CODESEPARATOR positions, and the absence of an operation count.
Key path. The witness, after removing an annex (a final element starting with 0x50 when at least two elements are present), is a single element: a 64-byte BIP340 signature under SIGHASH_DEFAULT, or 65 bytes whose last byte is a non-zero hash type. The message is the BIP341 signature hash computed from the transaction, the spent outputs, the input index, the hash type and the annex; the key is the 32-byte program itself.
Script path. The last element is the control block (33 + 32k bytes, k ≤ 128); the one before it is the leaf script; the control byte's low bit is the parity of the output key and its other bits the leaf version. VerifyTaprootCommitment recomputes the merkle root from the leaf hash and the path nodes, hashes it with the internal key into the tweak, and checks that the internal key plus tweak·G has the output key's x-coordinate and the stated parity. Leaf version 0xc0 runs the script under Tapscript with the weight budget |serialized witness| + 50; other leaf versions succeed (upgrade hook).
Tapscript. Builds on the published Script mission's interpreter: each non-signature opcode is the same execOp; OP_CHECKSIG, OP_CHECKSIGVERIFY and OP_CHECKSIGADD go through EvalChecksigTapscript (an empty signature is a clean false, 32-byte keys are checked with BIP340, other key lengths are upgradable and succeed, each passed signature costs 50 weight); OP_IF/OP_NOTIF require [] or [1]; OP_CHECKMULTISIG(VERIFY) fail; OP_SUCCESSx anywhere in the script makes it succeed before execution.
tapbranch_comm) and merkle paths (merkleRoot_base, merkleRoot_snoc): the merkle root is a left fold of the symmetric branch hash along the control block's nodes.opsuccess_accepts, checkmultisig_rejected, minimalif_rejects, sigops_budget, checksig_empty): the five BIP342 rules that differ from legacy script, as universal statements about the transcription.sighash_type_invalid, sighash_single_missing).keypath_handler, keypath_annex, checkSchnorr_iff) culminating in the goal, keypath_correct: a key-path spend verifies iff the witness is a BIP340 signature by the output key of the BIP341 hash under the encoded hash type.scriptpath_commitment): a verifying script-path spend carries a valid commitment of the revealed leaf to the output key.With the Script, Signature and VerifyScript missions, the goal theorem reduces the acceptance of a Taproot key-path spend to one BIP340 verification of one BIP341 hash, for every flag set, transaction and amount. verifyScriptFull is the complete VerifyScript of the source, with no parameter left: every output type that has ever been spendable on mainnet now has its validation rule transcribed in Lean. The script-path theorem fixes the commitment structure that the Tapscript execution sits behind; the Tapscript rule theorems make the BIP342 differences from legacy script facts about the definitions.
Policy flags (DISCOURAGE_*) are off, as in block validation. The definitions were checked by evaluation against the full BIP341 wallet test vectors (script trees, tweaks, control blocks, key-path signature hashes and signatures) and the BIP340 vectors.
CheckSchnorrSignature distinguishes three signature lengths and reads the hash type from the last byte: the characterization needs the 65-byte case decomposed as body ++ [b] with dropLast/getLast? reasoning, and the converse direction must rule out a 64-byte body being presented as a 65-byte signature. The merkle step theorem requires the chunking of a control block to commute with appending a node, an induction over the node count with the natural-number division (length − 33)/32. The annex is detected by getLast? on the raw witness but popped by dropLast; the script-path theorem threads the witness through two pops in CScriptWitness order (last element on top) before reaching the commitment check.
The handler is instantiated for the spent outputs of the transaction (needed by the BIP341 hash); the context is the VerifyScript mission's Ctx. Tapscript opcode positions and OP_CODESEPARATOR are tracked here (the Tapscript sighash commits to the position). No Mathlib is required; the development imports only Std.
A trivializing formalization would define the key path as "a Schnorr signature verifies"; here taprootHandler is the source's control flow, and the key-path statement is a theorem about it.
VerifyWitnessProgram, ExecuteWitnessScript, EvalScript, EvalChecksigTapscript, SignatureHashSchnorr, VerifyTaprootCommitment, src/script/interpreter.cpp; XOnlyPubKey::CheckTapTweak, src/pubkey.cpp; secp256k1_xonly_pubkey_tweak_add_check, src/secp256k1, at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48. Source