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?
Mass dimension one (MDO) fermionic fields — spin-1/2 fields built from eigenspinors of charge conjugation (historically called Elko) — have canonical mass dimension one instead of 3/2 and admit only very few couplings to Standard Model particles. This makes them natural dark-matter candidates. In an Einstein–Cartan framework with torsion, the homogeneous part of such a field obeys equations that closely resemble scalar-field cosmology but carry an extra spin–gravity coupling factor .
S. H. Pereira, M. E. S. Alves and T. M. Guimarães (Eur. Phys. J. C 79 (2019) 543) propose that a single MDO field drives the whole cosmic history: inflation, reheating, dark matter and dark energy. The analytic backbone of that claim is Section 3 of the paper: once the field has rolled to the bottom of a symmetry-breaking potential, its gravitational coupling to baryons behaves exactly like cold dark matter and its residual potential energy behaves exactly like a cosmological constant.
Work in units with , on a flat FLRW background with scale factor and Hubble function . The MDO field is with a normalised Minkowski spinor; only the real function enters. Other matter has energy density and pressure . Writing , the model is governed by
(Eqs. (5)–(7), (9)), with MDO energy density and pressure given by Eqs. (10)–(11). The potential is with and , .
If on a late-time interval the field is frozen at , the only other matter is pressureless baryonic matter , and the Friedmann equation (5) holds, then with , ,
where , and (Eq. (24)).
The goal is the statement that makes the MDO field a unified dark sector at late times: the background expansion is indistinguishable from CDM, the dark-matter density is fixed by and the baryon density rather than by an incomplete decay of the inflaton, and the dark-energy density is fixed by . Equations (12)–(16) are the reusable structural fact that the torsionful MDO system is equivalent in form to a torsion-free two-fluid model. The milestones collect the algebraic and differential identities the paper uses without proof.
Formalizing these makes the derivations machine-checked and isolates exactly which hypotheses (frozen field, pressureless baryons, Friedmann equation) the CDM form depends on. The paper's numerical results for inflation (about 71 e-folds, Figs. 1–3) and the reheating discussion (Sect. 5) are numerical or qualitative and are outside the scope of this mission.
The algebra is elementary but error-prone: and themselves contain and , so the equivalences (15)–(16) are fixed-point identities rather than substitutions. Eq. (14) requires differentiating , which involves , and , so differentiability bookkeeping is the main formal cost. The dilution law requires a mean-value argument on an interval, not a pointwise computation.
All quantities are real functions of cosmic time; time derivatives are Mathlib's deriv, and each theorem carries the differentiability hypotheses it needs. Late-time statements are posed on an open half-line , since a matter-filled expanding universe cannot have for all real . The frozen-field regime is encoded exactly as on that half-line, and the field equation (7) is not assumed there (the paper itself only uses Eqs. (12)/(15) in this regime, and (7) with and varying would be overdetermined). Lean's Real.sqrt returns on negative inputs; in Eq. (21) this gives when , which is the correct minimiser in that regime. Definitions live in a single shared file under the namespace MDOUnifiedCosmology.
The Friedmann spacetimes (FLRW spacetimes) are the explicit, spatially homogeneous and isotropic solutions of Einstein's field equations on which standard Big Bang cosmology is built. Under a pressureless (dust, ) equation of state they form a family indexed by a curvature parameter : the critical spacetime , the underdense spacetimes and the overdense spacetimes . The current CDM model fits supernova data with the critical Friedmann spacetime plus a cosmological constant (dark energy).
Alexander, Temple and Vogler (arXiv:2510.14228) study how stable the pressureless Friedmann spacetimes are under smooth, spherically symmetric (radial) perturbations near the Big Bang. They write the Einstein–Euler equations in self-similar variables , , a formulation introduced by Smoller, Temple and Vogler (Proc. R. Soc. A, 2017). In these variables the critical Friedmann spacetime is a time-independent solution. They argue that the instability of this rest point causes underdense perturbations to accelerate away from Friedmann spacetimes at intermediate times, and they propose this as a mechanism for the observed acceleration that needs no cosmological constant.
This mission formalizes the dynamical-systems core of that paper: the STV ODE of orders and , its rest points and eigenvalues, the exact Friedmann trajectory, and the order-2 instability theorem.
Expand a solution that is smooth at the centre of symmetry in even powers of : (density) and (velocity). Collecting like powers of gives, at each order , a closed system , the STV ODE of order . At order , in the unknowns :
At order , in , the system adds
The system is autonomous in log-time . Its rest points include the Minkowski point , resp. , and the critical Friedmann point , resp. . The , Friedmann spacetime with parameter is given in parametric form by and explicit functions of (equations (2.41), (2.43)).
Fix . Let be the set of solutions of the order-2 STV ODE on that tend to as , tend to as , and agree exactly with the Friedmann spacetime at leading order, i.e. . Then
So the Friedmann spacetime is one member of a one-parameter family of trajectories from to . All members agree with it at leading order, and the others differ from it at order 2.
The result. At order every relevant trajectory is a Friedmann spacetime. Order is the first order where the instability of (the second positive eigenvalue ) produces trajectories that agree with a Friedmann spacetime as and as but differ from it in between. The paper reads this as an acceleration away from Friedmann spacetimes without dark energy. The extra eigenvalue is why some perturbations do not have a self-similar Big Bang.
Formalizing it. The paper is an announcement: most claims are justified by eigenvalue computations and appeals to standard ODE theory (Hartman–Grobman, decay at degenerate nodes). A machine-checked proof of the order-2 statements would turn these appeals into explicit arguments for a concrete polynomial system. None of these results is known to have been formalized.
The eigenvalue milestones are finite computations. The trajectory milestones (Theorem 5) need hyperbolic-function identities and limits at , where numerators and denominators both vanish to high order. The goal is harder because it is global. Linearizing at only describes trajectories near . One must also show that every member of the family exists for all time and reaches , and that nothing outside the family belongs to . Theorem 7 needs sharp decay rates at a rest point whose Jacobian is not diagonalizable, which is where the logarithm comes from.
Fin 2 → ℝ or Fin 4 → ℝ, with coordinates ordered and .fderiv). Norms on are sup norms.Completeness of a normed or metric space is the property behind most existence theorems in analysis: limits of approximations, fixed points, integrals. Many of the spaces that matter in analysis and in the theory of distributions are not metrizable, though: the space of test functions, weak-star duals, and spaces of operators with the strong or weak operator topology. For such topological vector spaces the right replacement for sequences is nets, and the plain notion "every Cauchy net converges" turns out to be too strong. Weak-star duals of infinite-dimensional Fréchet spaces, for example, never satisfy it.
Paul Garrett's lecture notes Completeness and quasi-completeness (PDF) argue that the right general notion is quasi-completeness: every bounded Cauchy net converges. They show that it holds for Hilbert, Banach, Fréchet and LF-spaces, for their weak-star duals, and for spaces of continuous linear maps with the topology of pointwise convergence. In the notes, one stated purpose is to justify Gelfand–Pettis integrals of compactly supported continuous functions with values in such spaces, for instance distribution-valued functions.
The results are classical. Boundedness in strict inductive limits goes back to Dieudonné and Schwartz, and the incompleteness of weak duals to Grothendieck (1950). See Bourbaki, Topological Vector Spaces, III.5, and Schaefer, Topological Vector Spaces.
All vector spaces are over or and all topological vector spaces are Hausdorff. A set in a topological vector space is bounded if every neighbourhood of absorbs it. A net is a map from a directed partially ordered set. It is Cauchy if for every neighbourhood of there is with for all . is complete if every Cauchy net converges, and quasi-complete if every bounded Cauchy net converges.
A Fréchet space is a locally convex, metrizable, complete topological vector space. A locally convex space is the strict colimit of a chain of subspaces if , each is closed in , and the topology of is the finest locally convex topology inducing the given topology on every . Concretely, a balanced convex set is a neighbourhood of in as soon as every trace is a neighbourhood of in . An LF-space is a strict colimit of Fréchet spaces; is the standard example.
For topological vector spaces , write for the continuous linear maps with the topology given by the seminorms , for and a convex balanced neighbourhood of in . When is locally convex this is the topology of pointwise convergence. A set of linear maps is equicontinuous if for every neighbourhood of in there is a neighbourhood of in with for all .
Theorem 4.1.1 makes the strong-operator and weak-operator topologies on bounded operators between Hilbert spaces quasi-complete, and does the same for operators out of test-function spaces. Combined with quasi-completeness of weak-star duals of LF-spaces (Remark 5.0.3), it is what lets vector-valued integration and Cauchy–Goursat-type complex analysis be applied to families of distributions and operators. Banach–Steinhaus for LF-spaces (Theorem 3.0.1) and the Dieudonné–Schwartz description of bounded sets (Proposition 2.1.1) are among the most frequently used facts about distributions.
Mathlib has the Banach–Steinhaus theorem for Banach spaces and barrelled spaces, the topology of pointwise convergence on continuous linear maps, weak duals, and the test-function space . It has no general theory of strict inductive limits and no quasi-completeness results of this kind. This mission formalizes that layer: the results are proved on paper, not yet formalized.
The obvious argument for Theorem 4.1.1 takes pointwise limits. That gives a linear map, but continuity of the limit is the real issue: it needs equicontinuity of a merely pointwise-bounded net of operators, which is a Baire-category statement and fails for general domains. For LF domains the Baire argument does not apply directly, because an LF-space is never metrizable when the chain is strictly increasing. The argument has to pass through the steps , which needs the description of bounded and equicontinuous sets in a strict colimit. That description depends on each being closed in and uses Hahn–Banach separation.
Definitions (namespace GarrettFA, shared by any later missions on these notes):
IsQuasiComplete 𝕜 E and IsNetComplete E follow the notes literally, with nets indexed by directed partial orders. The index type is taken in the universe of E, which is no restriction because Cauchy nets correspond to Cauchy filters.IsEquicontinuousSet S encodes equicontinuity at as in §2.2.IsStrictColimit 𝕜 F is a predicate on a chain F : ℕ → Submodule 𝕜 V and the given topology on V, and IsLFSpace and IsFrechetSpace are built from it. The steps carry the subspace topology from . By the Dieudonné–Schwartz theorem this is the same as giving the steps their own topologies, so the class of spaces is the source's.IsInitTopology 𝕜 V says that the topology of is . Its existence is a separate theorem item, which rules out a vacuous predicate.Local convexity is real local convexity (LocallyConvexSpace ℝ, with IsScalarTower ℝ 𝕜), as in Mathlib's distribution theory. is Mathlib's X →Lₚₜ[𝕜] Y. Its topology is the source's -topology because is locally convex.
Two statements of the notes are corrected. Theorem 3.0.1 is stated there for arbitrary linear maps; it needs continuous ones, since a single discontinuous functional is pointwise bounded but not equicontinuous. Corollary 5.0.2 claims incompleteness of weak duals of all infinite-dimensional LF-spaces. That fails for the LF-space of Example 1.3.1, whose topology is the finest locally convex one, so its weak dual is complete. The LF statement is therefore made for LF-spaces with an infinite-dimensional step. Proposition 1.3.5 is built into the formalization, where the steps are subspaces of .
Contributions of reusable infrastructure on strict inductive limits and barrelled spaces are welcome.
An Euler system is a family of cohomology classes, indexed by abelian extensions of a base field, whose members are tied together by norm relations whose correction factors look like the Euler factors of an -function. Euler systems were introduced by Kolyvagin (Kolyvagin 1990), building on Thaine's work on cyclotomic fields (Thaine 1988), and they are one of the main tools for bounding Selmer groups and ideal class groups: Kolyvagin used them to prove finiteness of some Tate–Shafarevich groups, and Rubin used them for a new proof of the main conjecture of Iwasawa theory (Rubin 2000).
The simplest Euler system, and the model for all others, is the cyclotomic Euler system of cyclotomic units . Kolyvagin used it to give an elementary proof of the Gras conjecture. This mission formalizes the two defining relations of this system as stated in the Wikipedia article Euler system.
Timeline (as summarized in the source): Thaine (1988) annihilators of class groups of real abelian fields; Kolyvagin (1988, 1990) Heegner-point and general Euler systems; Kato (2004) Euler system of Beilinson elements; Rubin (2000) monograph Euler Systems; Mazur–Rubin (2004) Kolyvagin systems.
For every square-free positive integer fix a primitive -th root of unity , chosen compatibly: whenever are coprime. Put
For a prime , the Frobenius is the automorphism of with . The norm is the field norm of the extension , and a prime of lies above if it is a prime ideal of the ring of integers containing .
For square-free and a prime :
The two relations are exactly the axioms that later, more abstract Euler systems (Gauss sums, elliptic units, Heegner points, Kato's elements) are modelled on; the cyclotomic case is where the Euler-system machinery for class groups of abelian fields starts. Both relations are classical and proved; what remains is formalizing them. Mathlib provides cyclotomic fields, primitive roots of unity, field norms and rings of integers; the mission builds the relations on top of these and provides a reusable definition layer for cyclotomic units.
The norm relation requires identifying the Galois group of with — which uses the irreducibility of the -th cyclotomic polynomial over for — and then computing the norm as a product over conjugates inside , transported along the intermediate-field coercions. The congruence relation requires working in the ring of integers of a subfield of and showing that lies in every prime above . Neither is conceptually deep, but both involve substantial bookkeeping between subfields of , abstract cyclotomic extensions, and rings of integers.
All fields are subfields of : is IntermediateField.adjoin ℚ {ζ n}, and over is IntermediateField.adjoin (ℚ(ζ_n)) {ζ (n*l)}. The norm is Algebra.norm; is written as ; is any -algebra automorphism of with . Roots of unity are required to be primitive. Two deviations from the literal text of the source, both forced: the norm's base field is (the source's is a typo), and the norm relation assumes (for , ). The existence milestone rules out a vacuous reading of the compatibility hypothesis. Welcome contributions: lemmas on Galois groups of compositums of cyclotomic fields inside , and on primes above in .
In centralized labour markets such as the US National Resident Matching Program, doctors are assigned to hospital residency positions by a mechanism that produces a stable matching. There are more positions than doctors, so some hospitals end up with empty positions; these are typically rural hospitals, which are less sought after than urban ones. This raised the question of whether a different mechanism could help these hospitals (Roth 1986). The rural hospitals theorem answers this negatively, provided all preferences are strict.
Timeline.
A market has a finite set of doctors and a finite set of hospitals; hospital has positions. Every doctor strictly ranks the hospitals together with the option of staying unmatched, and every hospital strictly ranks the doctors together with the option of leaving a position empty. An assignment sends each doctor to a hospital or to nothing; is the set of doctors at . It is a matching if for every .
A matching is stable if (i) no doctor is placed at a hospital she ranks below staying unmatched, and no hospital holds a doctor it ranks below an empty position, and (ii) there is no blocking pair : a doctor who prefers to her assignment, while finds acceptable and either has an empty position or prefers to one of its current doctors.
For any two stable matchings :
The result itself. Changing the matching mechanism, as long as it outputs stable matchings, cannot give under-subscribed hospitals more doctors or different doctors, and cannot change which doctors are employed. Hence policy aimed at rural hospitals must change preferences, capacities, or abandon stability, not merely switch between stable mechanisms.
Formalizing it. The theorem is classical and proved in the cited papers; this mission asks for a machine-checked proof in Lean 4 with Mathlib, for the general many-to-one model with capacities and acceptability, together with the one-position special case.
Comparing two stable matchings one agent at a time does not work: a single doctor moving between hospitals says nothing about how many positions each hospital fills, and the statements concern every agent of the market simultaneously. Stability of both matchings has to be used at once, and Part 2 is strictly stronger than Part 1 (equal numbers of doctors at an under-filled hospital do not imply equal sets of doctors). The existence of a stable matching is not needed for these statements.
Doctors and hospitals are finite types D, H. Preferences are injective rank functions on Option H (for a doctor) and Option D (for a hospital), smaller rank meaning more preferred and none meaning unmatched or an empty position; injectivity encodes strictness. Hospital preferences over groups are responsive. Capacities are natural numbers and may be zero. An assignment is μ : D → Option H. Stability is Market.IsStable: capacity constraints, individual rationality, and no blocking pair. All statements quantify over arbitrary stable matchings, so they are not vacuous: stable matchings exist in every such market (Gale–Shapley), though existence is not part of this mission.
Contributions welcome: proofs of the milestones, an existence theorem for stable matchings in this model, and lemmas about stable matchings reusable in other matching missions.
Cantor's continuum problem asks for the value of , the cardinality of the power set of an infinite cardinal . For regular cardinals ZFC says almost nothing: by Easton's theorem (1970) the function on regular cardinals can be essentially any non-decreasing function with . For singular cardinals the picture is different, and the singular cardinals hypothesis (SCH) is the natural statement of "GCH-like behaviour at singular cardinals". It arose from the question whether the least cardinal at which GCH fails can be singular.
Timeline.
All cardinals live in one universe. For a cardinal , is its successor cardinal and its cofinality (the cofinality of the initial ordinal of ). A cardinal is singular if it is infinite and , and a strong limit if and for all .
A normal measure on is a nonprincipal -complete ultrafilter on under which every regressive function is constant on a measure-one set; is measurable if it is uncountable and carries one. is strongly compact if it is uncountable and every proper -complete filter on any set extends to a -complete ultrafilter. The proper forcing axiom (PFA) asserts that for every proper poset and every dense subsets of there is a filter meeting all of them.
SCH itself is independent of ZFC, so it cannot be a goal; the goal is the ZFC theorem that SCH can only first fail at countable cofinality.
JechSetTheory.silver).JechSetTheory.sch_of_sch_cof_aleph0).The goal locates the first possible failure of SCH: any model of SCH must have a counterexample of countable cofinality, which is why Prikry-type forcing (which adds an -sequence) is the standard tool for producing failures, and why is the canonical test case. Milestones 1, 7, 8 and 10 show that very different hypotheses (GCH, large cardinals, forcing axioms) all imply SCH, while milestone 9 shows PFA does so without GCH.
These results are classical and have complete published proofs (Jech, Set Theory, Chapters 8, 20, 24, 31). Silver's theorem is already machine-checked on this platform; the rest, including the stationary-set form of Silver's theorem needed for the goal, are not yet formalized here.
The naive attempt at the goal, "apply Silver's theorem at the least counterexample", fails: Silver's theorem as stated needs GCH at all infinite cardinals below , but SCH below says nothing about regular cardinals or non-strong-limits. The proof needs the stronger, stationary-set version of Silver's theorem (Galvin–Hajnal style), applied to the stationary set of singular strong limits of countable cofinality below . Scott's and Solovay's theorems need ultrapower arguments, and PFA SCH needs reflection and covering-type combinatorics; none of these exist in Mathlib.
Cardinal.{u}; singularity is Cardinal.IsSingular, strong limit is Cardinal.IsStrongLimit, cofinality is κ.ord.cof, successor is Order.succ κ. The second form reuses the published predicate JechSetTheory.SCHAt.Ordinal.{u} containing the ordinals below ; completeness quantifies over index types of universe u. "Proper filter" in the definition of strong compactness is Filter.NeBot; without it no cardinal would be strongly compact and Solovay's theorem would be vacuous.Def_JechStationary), ultrapowers by normal measures, Fodor's lemma, Galvin–Hajnal bounds.The stable matching problem asks for a pairing between two equally sized groups in which no two participants would both rather be matched with each other than with their assigned partners. It was posed and solved by Gale and Shapley in 1962 in the context of college admissions and marriage (Gale–Shapley 1962). Their deferred acceptance algorithm underlies centralized clearinghouses such as the assignment of graduating medical students to hospital residencies, and the theory of stable allocations was recognized by the 2012 Nobel Memorial Prize in Economic Sciences awarded to Shapley and Roth.
Timeline of the results targeted here:
Fix . There are men and women, both indexed by . Each man ranks all women strictly: is the position of in 's list, position being most preferred; symmetrically each woman has . Both are bijections. A matching is a bijection from men to women. A pair blocks if and ; is stable if no pair blocks it.
The Gale–Shapley algorithm runs in rounds. A state records, for every man, how many women he has proposed to so far, and for every woman, her current provisional fiancé (if any). In each round every unengaged man proposes to the most preferred woman he has not yet proposed to, and every woman keeps the most preferred among her current fiancé and this round's suitors, rejecting the others. The Gale–Shapley outcome is the matching read off from the state after rounds.
This contains termination (all men are engaged after rounds), the fact that the final engagements form a bijection, and stability.
Existence of stable matchings is the foundation of two-sided matching theory, and the algorithmic proof is constructive. Man-optimality and woman-pessimality show that the proposing side is systematically favored, which is the reason the choice of proposing side matters in practice, as in the 1995 redesign of the residency match. The incentive results (milestones 5–8) explain why participants on the proposing side can safely report their true preferences while the receiving side cannot, and the lattice structure underlies efficient algorithms for enumerating and optimizing over stable matchings.
All results in this mission are classical and proved in the literature. The work here is formalization: a precise model of the round-based algorithm, machine-checked proofs of its correctness and optimality, and the incentive properties, which are usually argued informally.
The goal requires reasoning about an iterated state transformer rather than an abstract existence statement. The step that is usually waved away is the invariant that an unengaged man still has a woman left to propose to, which is what makes the bound and the bijectivity of the final engagements work. Man-optimality needs the invariant that no man is ever rejected by a woman who is his partner in some stable matching, which is not visible from the output alone. Group strategy-proofness is substantially harder than individual truthfulness: the known proofs go through a "blocking lemma" about matchings that are weakly preferred by all men.
Men and women are Fin n; preferences are strict total orders given as rank bijections Fin n ≃ Fin n; matchings are bijections Fin n ≃ Fin n. The algorithm is the round-based version described in the source: all unengaged men propose simultaneously in each round. The algorithm's output is fixed as the state after exactly rounds; termination within that bound is itself a milestone, so a wrong bound would make the goal false rather than vacuous. The case is included and is trivial. Incentive results compare Gale–Shapley outcomes of two instances that differ only in the lists of the deviating participants, with gains measured by the deviators' true lists.
The definitions are reusable for further missions on the same article (rural hospitals theorem, hospitals/residents problem). Contributions welcome: invariants of the algorithm, the blocking lemma, and alternative proofs of existence.
The secretary problem is the standard example of an optimal stopping problem with partial information. It is also known as the marriage problem, the sultan's dowry problem, the fussy suitor problem, the googol game and the best choice problem. It is studied in applied probability, statistics and decision theory. Its solution is often called the 37% rule: a simple rule picks the single best of applicants with probability about , whether there are 100 or 100 million applicants (Wikipedia: Secretary problem). The problem is a standard example of the exploration–exploitation dilemma.
Timeline (as recounted in the Wikipedia article's History section, following Ferguson 1989):
There is a single position and there are applicants, where is known. If seen together, the applicants can be ranked from best to worst with no ties. They are interviewed one at a time in a uniformly random order: each of the orders is equally likely. Right after each interview the applicant is either accepted, which ends the process, or rejected for good. The decision may depend only on the relative ranks of the applicants interviewed so far. The objective is to maximize the probability of selecting the best applicant of the whole group.
An order is a permutation of . The applicant interviewed at time has quality , where larger means better. The relative rank of the applicant interviewed at time is the number of applicants interviewed before time who are worse than them. A stopping rule maps the list of relative ranks observed so far to "accept" or "reject". Its success probability is the fraction of the orders on which the applicant accepted by is the overall best. A rule that never accepts anyone fails. The optimal success probability is
A candidate is an applicant who is better than every applicant interviewed before them. The cutoff rule with cutoff rejects the first applicants and then accepts the first candidate after that point.
The result. The 37% rule is the classical result of optimal stopping. It shows that a fixed fraction of the best possible success probability survives as the number of options grows without bound, and that a simple threshold policy achieves it. The structure of its solution has three parts: optimal rules may be taken to be threshold rules, there is an exact formula in terms of the records of a uniformly random permutation, and a limit turns a harmonic sum into an integral. This structure recurs throughout the best-choice literature, including the prophet-secretary and multi-choice secretary problems.
Formalizing it. The result has been proved since the late 1950s and early 1960s. The remaining work is to formalize the known proof: a model of rank-based stopping rules over uniformly random permutations, the exact success probability of cutoff rules, the optimality of cutoff rules among all rank-based rules, and the asymptotics.
The success probability of a fixed cutoff rule and the calculus limit are elementary. The central step is the optimality of cutoff rules (Milestone 3). A stopping rule may depend arbitrarily on the whole history of relative ranks, and one has to show that no such rule beats the best cutoff rule. Evaluating cutoff rules alone does not prove the goal, because is a supremum over all rank-based rules. A second, smaller difficulty is that the limit statements need control of the harmonic sums along a varying cutoff , not only along a fixed ratio.
Equiv.Perm (Fin n) with uniform weights. successProb n s is the ratio (number of winning permutations) / in .List ℕ → Bool, applied to the list of relative ranks observed so far. Through the length of the list it also knows the current time. It never sees absolute qualities. Randomized rules are not modelled. A randomized rule is a mixture of deterministic ones, so it cannot do better.optimalProb n is the real supremum of successProb n s over all such rules. The values lie in , so the supremum is the usual least upper bound.Fin n). Cutoffs are 1-based, as in the article: cutoffRule r accepts at time exactly when and the current applicant is a candidate.Real.exp (-1).All declarations live in the namespace ClassicalSecretary. Reusable contributions are welcome, in particular facts about records of uniformly random permutations (independence of relative ranks, the probability that position is a record) and a backward-induction principle for finite-horizon stopping problems.
In a spatially flat Friedmann–Lemaître–Robertson–Walker (FLRW) universe the expansion is described by the Hubble parameter . A long-standing line of work treats the vacuum energy density not as a constant but as a quantity that decays as particles are created out of the vacuum in the expanding spacetime. If total energy is conserved, a time-varying vacuum density must be accompanied by particle production, and conversely the creation rate fixes how depends on .
S. Carneiro's 2012 paper (DOI 10.1142/S2010194512008173) applies this idea at both ends of cosmic history. At late times, creation of ultra-light non-relativistic dark particles gives a vacuum density , the law expected for the QCD vacuum condensate in a low-energy expanding spacetime. At early times, creation of relativistic particles gives and an inflationary solution with constant slow-roll parameter. The paper also recalls a non-singular model in which drives a transition from a de Sitter phase to a radiation phase.
Units are . All quantities are real functions of cosmological time on an open time interval :
The total density and pressure are and . The equations used are:
The slow-roll parameter is , and the matter fraction is . In the equivalent scalar-field description, is regarded as a function of a field , and the field equations are and , with the derivative with respect to .
If , and with , then on any time interval where ,
for an integration constant .
Eq. (17) is the paper's central claim that particle creation with backreaction produces inflation with constant , and so with a scale-invariant spectrum and spectral index . Eqs. (10)–(11) give the late-time decaying-vacuum law behind the paper's concordance model, and Eqs. (4)–(5) give the non-singular de Sitter-to-radiation transition. These derivations have not been machine-checked before. A formal development makes explicit the regularity assumptions and side conditions the paper leaves implicit, such as , , and the non-degeneracy condition in Eq. (10).
Most steps are short calculations, but each one hides analytic content. Deriving relations between functions from equations between derivatives (Eqs. (10), (16), (17), (23)) needs the fact that a function with zero derivative on a connected open set is constant. Eq. (5) defines implicitly, so the existence, differentiability and asymptotics of the inverse function must be established. Eq. (24) requires showing that the sign in cannot switch, even though is not assumed continuous.
Functions are maps , time derivatives are Mathlib's deriv, and differentiability is assumed at every point of the time interval . The interval is an open, preconnected subset of , because the solutions of the paper generally exist only on a half-line: for example, vanishes at a finite time. A statement assuming a global-in-time solution would be vacuous. Constants of integration are existentially quantified. The integration constant enters only through , and Lean's convention makes this the same as an arbitrary real constant. The numerical and observational parts of the paper (data fits, ) and the perturbation analysis (Eqs. (19)–(20)) are out of scope.
The cosmological constant problem is the mismatch between the vacuum energy density predicted by quantum field theory in flat space–time and the small value of the cosmological term inferred from observations (Weinberg 1989). One line of work replaces the constant by a decaying vacuum: a time-dependent cosmological term that falls as the universe expands, while the energy it loses is transferred to matter so that total energy is conserved.
S. Carneiro's essay From de Sitter to de Sitter: a non-singular inflationary universe driven by vacuum (Int. J. Mod. Phys. D 15 (2006) 2241–2247, honorable mention in the 2006 Gravity Research Foundation essay competition) derives such a law from a semi-classical argument, , and studies the cosmologies it produces. In the early-time regime it finds a universe with no initial singularity: an eternal quasi-de Sitter phase at the Planck scale, followed by a fast transition to a radiation era. In the late-time regime it finds a dust era that tends again to a de Sitter universe. The calculations in the paper are explicit closed-form computations, which makes them a good target for a complete machine-checked development.
All quantities are in Planck units, and space is flat. The expansion is described by the Hubble parameter of a scale factor . The cosmic fluid has total energy density and total pressure , where are the matter density and pressure and is the vacuum term. The Friedmann equation is and the conservation equation is
Radiation has and dust has . The relative energy densities are and , and the deceleration parameter is .
The vacuum term comes from a massless scalar field obeying . For slowly varying this has the damped radial plane-wave solution , with and given by explicit square-root formulas (Eqs. (7)–(8)), and energy density . Shifting the cutoff of the thermally regularized vacuum integral by and subtracting the flat-space value gives the vacuum term . In the mission's Lean development these objects are waveNumber, dampingRate, planeWave, vacuumTerm, dustScaleFactor and decelerationParameter, all in the namespace CarneiroDeSitter.
With radiation and , the evolution equation is (Eq. (12)). The goal asserts that it has a solution defined for all times, given implicitly by Eq. (13):
The goal is the paper's central claim: under the stated vacuum law the universe has existed for an infinite past, in a quasi-de Sitter phase with , and leaves it through a transition in which and fall towards zero, producing radiation. The milestones cover the steps the paper uses to reach it (the vacuum law, the evolution equation and its integration) and the late-time picture (the dust solution and its de Sitter limit, which the paper links to the Eddington–Dirac large-number relation ).
The results are proved by hand calculation in the paper. The same evolution equation and implicit solution reappear in Carneiro's later paper Cosmological Concordance Model with Particle Creation (2012), whose statements are also on the platform (namespace CarneiroParticleCreation); this mission formalizes the 2006 paper, its vacuum law and its late-time dust solution. Formalizing them produces a verified account of which statements are exact identities and which are approximations. Where the paper writes "", the milestones state the exact identity or asymptotic equivalence behind it.
The algebraic milestones (5, 7) are routine. The goal concerns a function known only implicitly: the solution is the inverse of on , and its existence on the whole line, its differentiability and its end behaviour all have to be established for an inverse function, not read off a formula. Milestone 6 is a uniqueness statement on all of , so it cannot be checked by substitution. Milestones 1 and 10 are improper integrals whose values involve and , and they need integrability arguments near and . Milestones 2, 3, 8 and 9 involve derivatives of complex exponentials, square roots and real powers, where Lean's conventions for and at non-positive arguments must be handled.
Real.artanh, the real power is Real.rpow, is Asymptotics.IsEquivalent, and is written as .Contributions are welcome on all milestones. The inverse-function and Bose-integral arguments can be reused outside this mission.
Noetherian schemes are the standard finiteness condition of algebraic geometry. Almost every scheme met in practice is Noetherian: affine and projective varieties over a field, schemes of finite type over , and many moduli spaces. Many basic theorems about schemes (finiteness of irreducible components, quasi-compactness of morphisms, good behaviour of coherent sheaves and their cohomology) are proved under a Noetherian hypothesis, so the notion appears in the hypotheses of a large part of the literature, starting with Hartshorne's Algebraic Geometry, Chapter II, and the Stacks Project.
This mission formalizes the foundational statements in the Wikipedia article "Noetherian scheme": the definition and its equivalent forms, the basic topological and ring-theoretic consequences, the stability of the notion under morphisms of finite type, and the standard non-examples.
A scheme is a locally ringed space that is locally isomorphic to spectra of commutative rings. For an open subset write for its ring of sections. An open subset is an open affine if for a commutative ring ; then .
NoetherianScheme.IsLocallyNoetherianScheme).NoetherianScheme.IsNoetherianScheme).A topological space is a Noetherian space if every descending chain of closed subsets stabilizes. A morphism is quasi-compact if preimages of quasi-compact opens are quasi-compact, locally of finite type if it is given locally by finitely generated algebras, and of finite type if it is both.
This combines the article's statements that a scheme is Noetherian iff it is locally Noetherian and compact, and that every open affine of a locally Noetherian scheme has a Noetherian ring of sections. It shows the definition does not depend on the chosen cover.
The goal is what makes the notion usable: it allows checking Noetherianity on any affine cover and using it on every affine open. Milestones 1–5 and 7–8 are the facts invoked whenever a Noetherian hypothesis is used. Milestones 9–10 are the source of most examples, since they show that every scheme of finite type over a field or over is Noetherian. Milestones 6, 11 and 12 show the limits of the notion: Noetherianity is not a topological property, and natural rings in number theory (adeles, rings of integers of infinite extensions) fall outside it, even in dimension one.
Mathlib already contains its own versions of several of these facts, phrased through AlgebraicGeometry.IsLocallyNoetherian and AlgebraicGeometry.IsNoetherian, which take "every open affine has Noetherian sections" as the definition. The statements here use the source's cover-based definition, so connecting the two is part of the work.
The central point of the goal is that a cover-based condition must be transferred to an arbitrary open affine , which in general is not one of the covering opens and is not covered by finitely many standard opens of a single covering affine. The obvious argument (intersect with the cover) produces opens that are not affine, or are affine in different rings, so a local-to-global argument for the property "Noetherian" on affine opens is needed. The non-examples (milestones 6, 11, 12) each require building or analysing a specific non-Noetherian ring that Mathlib does not yet study from this angle.
AlgebraicGeometry.Scheme in a fixed universe u. Open affines are X.affineOpens; rings of sections are Γ(X, U); local rings are stalks X.presheaf.stalk x.CompactSpace on the underlying space (quasi-compact, no Hausdorff condition).LocallyOfFiniteType f together with QuasiCompact f.NumberField.AdeleRing (𝓞 K) K. The field is any field of characteristic zero with IsCyclotomicExtension {n | 0 < n} ℚ K; such fields exist (for example inside an algebraic closure of ), so the hypothesis is not vacuous.IsNoetherian as the definition would make the goal close to a restatement; the definitions here deliberately follow the source.Uncertain financial returns affect funded pensions, DC saving and endowment adequacy. A single investment rate selected once and held fixed for the full projection is fundamentally different from a genuinely independent sequence of annual investment returns. The former produces expected powers of a single random variable while the latter factorises independent annual gross-return moments. These distinctions underpin the financial risk assumptions in stochastic finance models. Existing actuarial missions cover discounted deterministic cashflows but not these stochastic accumulation and contributions.
Annual gross returns equal one plus their annual net investment returns. A finite probability space has actual scenario masses with total one, so expectation and variance are weighted finite sums. The fixed-rate accumulation raises the same scenario gross factor to the investment horizon. For independent years the model explicitly constructs a product joint mass p(a)q(b) and verifies the first and second product moments. A real pension fund receives a contribution at the beginning of the year before earning its realised gross return.
The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.
A finite discrete fixed-rate model begins at a sure one.
Actual joint product probability laws establish two independent annual accumulation moments.
The independent-return pension accumulation recursions reconcile first and second fund moments including contribution cross terms.
The independent-return pension accumulation recursions reconcile first and second fund moments including contribution cross terms.
As discussed in Shreve's stochastic-finance treatment, The capstones distinguish random fixed returns from actually independent annual returns without presupposing a target identity. For the latter, the true two-year joint probability law factorises the expected growth and its second moment. Under subsequent iid moment factorisation, a multi-year first and second return moment model yields an exact variance recursion. The fund valuation then derives consistent one-step mean, second-moment and variance formulae with contributions, including the cross-term from previously accumulated assets. The model is useful for genuine stochastic saving, actuarial adequacy and projected pension risk.
It is mathematically false in general that expected compound returns equal the power of the expected rate for a fixed but random interest assumption. Genuine product probability weights, not a definition of independence as the desired conclusion, support the two-year factorisation. For a regular savings fund, the contribution is invested with the previous fund, so the second moment includes a cross term twice the contribution times the prior expected fund. The variance has to be derived from the two independently defined moments with positive gross-return second-moment bounds. All signs and independence restrictions should be preserved at every step.
Fixed stochastic-rate model and independent annual returns are distinct mathematical constructs in this model. A future substantial probability model could construct fully independent n-year return families and an exact savings accumulation probability distribution, rather than stopping at the two-year product law. The present source has nontrivial results because it independently calculates both moments of an actual joint scenario distribution and reconciles the cross terms in the savings fund variance. Existing stochastic insurance claims calculations alone do not provide an investment growth scenario model. This finite product model and fund recursion are reusable for defined contribution pensions, insurance asset adequacy testing and later cashflow simulations.
For a random interest rate sampled once at issue and held fixed, the expected n-year accumulation is an expectation of a random power, not generally a power of the expected return. If annual investment returns instead vary independently, the gross growth factors are multiplied across years and their expected product factorises. This mission proves the two-year factorisation from genuine independent finite product-state probability masses, without taking independence to mean the target moment identity by definition. For regular savings, contribution timing matters because a beginning-of-period contribution earns that period's return. The second-moment recursion must therefore contain the mixed term twice the contribution times the previous expected fund. These identities provide an actuarial basis for testing pension fund accumulation and capital adequacy, but do not justify a normal or lognormal fund distribution merely from calculated means and variances.
The principal independence derivation is from an actual finite two-year product scenario model, while the general n-year variance is stated as an explicit algebraic moment-factorisation law. Deriving n-way stochastic independence under a full probability measure, lognormal approximate fund distribution and path-dependent contributions remains work for subsequent substantial probability theory. No normal approximation or lognormality is assumed from mean and variance alone. These open theorem targets are not accepted proofs.
These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.
Unit-linked life and pension policies require careful accounting for where gross premiums go, which underlying fund units are purchased and which charges are received by the insurer. The FCA's unit-linked review identifies allocation, management, surrender and other policy charges as distinct insurer cashflows. Earlier actuarial missions XLVI and LXIX already formalise simple unit funds and guarantees, but lack explicit offer/bid unit pricing and a fully reconciled insurer non-unit profit signature.
A policyholder pays a gross premium, of which an allocation percentage is invested at the offer price and the remainder is retained by the insurer. Unit-holders value their existing holdings using the bid price. Management and fixed administration charges reduce fund assets; a guaranteed minimum death benefit creates an insurer mortality risk above the unit-linked fund. The insurer's non-unit account collects charges and premium differences and separately pays expenses, commissions and mortality guarantee strain.
The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.
Cancelling no more units than held retains a nonnegative unit account.
A nonnegative surrender charge cannot increase the positive fund value.
Actual unit premium allocation and bid-offer cost reconcile with the insurer's separate death guarantee obligations and complete non-unit cashflow profit account.
Actual unit premium allocation and bid-offer cost reconcile with the insurer's separate death guarantee obligations and complete non-unit cashflow profit account.
As discussed in the FCA's unit-linked review, The target reconciles every gross premium unit purchase and retained amount; it values immediate bid-offer spread costs, decomposes guaranteed death benefits into the invested fund plus net insurer amount at risk, and establishes an independent non-unit profit cashflow balance. Additional supporting theorems make the risk discount present value additive across the profit signature, with correct timing of beginning-year premium allocations and end-year fund costs. This provides an exact starting point for insurance policy profit testing and the analysis of charge sensitivity.
Bid and offer prices cannot be interchanged: a unit bought at offer is valued at bid and a positive spread produces a real cost even with unchanged market prices. A premium allocation percentage is not identical to the percentage of bid value created. Death insurance cost is the excess guaranteed benefit above the fund, rather than the total benefit, because fund assets already cover the remainder. The non-unit income and the actual expenses/commission/insurance risk must be kept separate rather than silently netted inside fund performance. The proof must impose suitable positivity on offer prices and fund values.
Bid-offer spread and non-unit profit signature are distinct mathematical constructs in this model. A future extension will include surrender probabilities, partial withdrawal, guaranteed annuity options and stochastic policyholder behaviour, together with a non-unit reserve liability under the prospective profit-testing basis. The current identities are nontrivial because they distinguish bid-valued units bought at an offer price, actual management charges, underlying expenses and the top-up death cost. Existing unit account and zeroisation missions do not include all these separate components in one coherent insurer profit signature. The explicit fund and charge functions are reusable for product pricing sensitivities, reserve testing and financial reporting.
Insurance premiums credited to unit-linked funds are converted into units at the offer price, but the policyholder's fund is valued using the bid price. A positive spread therefore creates an immediate difference even when financial markets have not moved. Management fees and policy administration charges reduce the unit fund, whereas amounts charged to policyholders generate insurer non-unit income and are not synonymous with the actual expenses incurred. A guaranteed death benefit creates mortality cost only on the positive excess above the linked fund value; it would double-count fund assets to charge the full guaranteed amount as non-unit insurer cost. The non-unit profit signature then recognises unallocated premiums, spreads and management and administration charges less commission, expenses, additional death cover and any guarantee cost. Future cashflows are discounted year by year. These identities form a precise accounting model, not a regulatory determination of fair consumer value.
The mission develops one-period unit accounting and finite annual expected profit signatures. It is not a market conduct or compliance assessment of a particular insurer. Fund return and projected mortality are explicit model inputs and do not assert a complete stochastic-policy profit distribution. Complex paid-up terms, partial surrender and non-unit reserve zeroisation have related earlier mission infrastructure and require further integration. Every Lean theorem remains open.
These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.
General-insurance reserving methods must distinguish development of claim payments from changes in their price level. The IFoA inflation reserving guidance distinguishes implicit and explicit inflation adjustments. Its earlier claims reserving report identifies inflation and average cost per claim methods alongside standard chain ladder. Earlier actuarial missions LIII and LIX cover volume chain ladder and reserve variances but not these two methods.
Incremental claims are paid in calendar years determined by accident year plus development year. A strictly positive index converts nominal claims into a constant valuation-year price level before applying development factors. The projected real future claim payment is then reinflated to its expected future calendar-year cost. Separately, an average cost per claim development triangle and a count triangle project ultimate claim frequency and mean severity.
The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.
A price index remains positive for growth greater than minus one.
Sufficient projected ultimate value gives nonnegative outstanding reserve.
The inflation-adjusted chain-ladder projection and the independently developed average-cost claim reserve both reconcile nominal cashflows, real development and ultimate claims without treating the projection as an observed fact.
The inflation-adjusted chain-ladder projection and the independently developed average-cost claim reserve both reconcile nominal cashflows, real development and ultimate claims without treating the projection as an observed fact.
As discussed in the IFoA claims-reserving literature, The target establishes exact no-loss conversion between nominal and real claims, proper telescoping between incremental and cumulative triangles, the composition of real development factors, and the multiplication of projected ultimate claim numbers by projected average severity. It then reconciles both ultimate and outstanding amounts in an independent combined capstone. A payment-year inflation assumption is distinguishable from a development-year link factor, which guards against projecting historical calendar-year inflation twice.
The proof must preserve accident-year, development-year and calendar-year indexing and impose positivity on every ratio's index, claim count and growth denominator before invoking any reconstruction identity. The dollar value of a claim that has already been paid must never be reinflated as if it were a future payment. Volume development and average-cost development use different denominators and cannot be conflated in a single grossing-up factor without an additional model assumption. The capstone reconciles separately constructed projections rather than defining reserves by the desired equality.
Historical inflation adjustment and claim-development factors are distinct mathematical constructs in this model. A future extension could integrate stochastic calendar-year inflation factors, accident-year trends, and parameter-estimation uncertainty into a single insurer liability distribution. The current exact algebraic target is nontrivial because it reconstructs nominal cashflows after applying conversion and development operations to independently constructed real and count-based projections. Known chain-ladder methods do not eliminate the need to prove that the resulting factors and projected reserve components reconcile. The finite triangle definitions and their transformations are reusable for other claims reserving methods, including tail development and multiple accident years.
A loss development triangle involves three separate notions of time: accident-year origin, settlement development lag and payment calendar year. Past inflation must be removed according to the actual payment year before development is extrapolated. Only after the real-valued development has been projected should future expected payment-year inflation be reinstated, and only once. A claim volume development factor does not represent a price inflation rate. The average-cost-per-claim method separately projects ultimate claim numbers and average claim sizes, then multiplies them. This decomposition distinguishes frequency development from claim inflation and severity development. The actuarial motivation is substantial, as long-tailed insured losses can have irregular calendar-year price patterns. The mathematical statements in this source are exact projection identities, not claims that past development patterns predict future claim payments without residual risk.
This is a mathematically exact deterministic claims triangle and projected cashflow formalisation, not a claim that chain-ladder assumptions hold for a particular line of business or that the selected inflation index is statistically correct. The index rate and link factors are model inputs, and the full stochastic process/reserve estimation error remains covered only in related Mack mission LIX. Interactions of separate inflation by payment type and stochastic calendar effects are future research problems. All Lean theorem bodies are open.
These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.
The Cramér–Lundberg model describes insurer capital invested in premium revenue while discrete random claims are paid at unpredictable arrival times. The model's classical adjustment coefficient and ruin probability are treated in risk theory and in modern ruin-probability bounds. Earlier mission LXXVIII derives a candidate ruin formula satisfying a renewal equation, but does not model the actual first-passage event. This mission supplies genuine stochastic first passage and measurable ruin events with an explicit stopped exponential-moment route to a rigorous bound.
Let W_j and Y_j be random waiting times and severities on a measurable probability space. At n-th claim arrival, cumulative elapsed time is the sum of W_0 through W_{n−1}, aggregate paid claims are the corresponding sum of Y_j, and the surplus is initial capital plus premium rate c times elapsed time minus claims. Ruin means surplus strictly less than zero and is only tested at claim boundaries, where a positive continuous premium slope allows a crossing to occur. The first-hit event excludes every earlier ruin, and its union over n is ultimate ruin.
The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.
Larger capital cannot create pathwise ruin.
Observation of more arrivals can only increase probability of ruin.
The actual stochastic first-passage event and stopped exponential moment condition derive a nonvacuous ultimate Lundberg capital bound.
The actual stochastic first-passage event and stopped exponential moment condition derive a nonvacuous ultimate Lundberg capital bound.
The mission establishes a real measured probability of ultimate ruin, monotonicity under capital and arrival horizon, and a disjoint partition by the first claim causing ruin. It then uses a stopped exponential loss process and an explicit moment upper bound to derive a Lundberg inequality for finite and ultimate ruin probabilities. The auxiliary stopped expectation condition is an independent martingale-style hypothesis, not an assumption of the desired probability bound. This helps distinguish authentic probability claims from an explicit exponential candidate whose equation has been verified. The risk-theory literature motivates the exponential-capital tail.
Nontrivial probability analysis is required to link a finite first-passage indicator to a stopped exponential transform. The first-hit sum cannot count multiple ruin dates on the same path, and the no-ruin terminal term must appear exactly once. Strict ruin, equality at zero and an observed negative surplus require distinct treatment. The finite-horizon inequality then uses measurability, positivity of exponential loss and a moment expectation hypothesis. Passing to ultimate ruin requires the countable union of nested ruin events and probability measure continuity, without assuming the theorem's conclusion.
Existing actuarial theory establishes the analytical principle, whereas the formal work here must prove the stated identities in Lean using the true distribution and event definitions. Some prior mission targets describe finite distributions or a candidate valuation, but they do not establish these stronger infinite-support or measured first-passage results. The boundary assumptions are part of each mathematical statement and cannot be replaced by a tautological definition. A complete proof requires independent source lemmas, explicit handling of the limiting case and verification of every transformation before concluding the capstone.
The pathwise event uses a strict negative surplus, not failure on equality at zero. The first-passage index is a disjoint union of finite-arrival failure events, and the increasing union gives ultimate ruin. A conditional moment hypothesis provides a nontrivial route to an exponential capital inequality. It is not the same assertion as the inequality on the ultimate ruin probability. The model does not claim to establish the Poisson arrival distribution or full independence of exponential severities from this conditional input. Those must be proved in a later, more elaborate stochastic source model.
The capstone proves the conditional stopped-moment Lundberg inequality for an actual measurable first-passage event, not yet the complete exponential-claims distributional identification. Independent exponential waiting times and independent claim severities supply the classical route to the stopped moment hypothesis but are not themselves constructed or verified in this graph. A future mission should derive that moment condition from fully specified iid waiting and severity distributions and prove uniqueness of the exact ruin probability. The pathwise framework is reusable for continuous-time embedding, overshoot losses, first-passage service tables and capital assessment. All Lean proof obligations remain open.
These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.
Continuous-time multi-state life insurance uses a generator of competing decrement intensities and prospective reserves for status-dependent benefits. The time-dependent state equations appear in multi-state insurance research; Promislow (2015), Chapter 19, provides actuarial fundamentals. The existing LXXVI mission constructs general conservative generator rows but only solves the stationary alive/dead reserve. This mission adds time-varying competing risks and derives a genuine contingent-payment reserve from its cashflows.
Three mutually exclusive states consist of active insurance, termination by cause one and termination by cause two. The latter are absorbing. The common exit intensity is a nonstationary force λ(t)=a+bt with cumulative hazard H(t)=at+bt²/2. A fixed proportion p of the exit force belongs to the first cause; 1−p belongs to the second. Nonnegative a, b and future dates and p in the unit interval make the transition probabilities stochastic. The model admits two distinct termination payments, one for each cause, and a separately specified maturity endowment.
The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.
Generator no-exit diagonal is minus total force.
Forward cause-two flow equals complementary hazard share times active membership.
A genuinely nonstationary three-state absorbing model conserves probability and its independently integral-defined prospective liability obeys the cause-contingent Thiele equation.
A genuinely nonstationary three-state absorbing model conserves probability and its independently integral-defined prospective liability obeys the cause-contingent Thiele equation.
The prospective reserve is an independently defined sum of a terminal-survival present value and a bona fide interval integral of the time-discounted, competing-exit claim intensity. The capstone proves its terminal boundary and differentiates it to obtain a nonstationary, three-status Thiele ODE, with an explicit cause-mix death strain. The result includes complete Chapman–Kolmogorov composition and transition normalisation for two absorbing exits. Research on multi-state actuarial equations explains how these equations fit into the broader general reserve framework.
The proof must establish a nontrivial inhomogeneous probability structure, not simply define reserve cashflows by the desired ODE. The cumulative-force derivative must be combined with the exponential survival chain rule, and the transition matrix must be composed across different calendar intervals. The integral of discounted cause-specific benefits must then be differentiated with a moving lower endpoint and a valuation-date-dependent exponential factor. Several steps rely on genuine interval integral differentiation and the finite-timestamp boundary conventions; no closed-form fixed-intensity substitution is assumed.
The model imposes fixed cause allocation while the total force changes with time. It therefore admits a genuine conditional transition matrix with two absorbing states. This provides a nonstationary counterexample to treating all transition intensities as constant; forcing an arbitrary time-dependent kernel to satisfy the desired generator equation by assumption would be vacuous. The interval-integral benefit value is independently defined before differentiating it. Its terminal boundary depends on the maturity payment, and no death benefit is payable at maturity beyond the contractual endpoint. The formalisation does not assume a general matrix-exponential formula for time-dependent noncommuting generators.
The mission establishes a nonstationary three-state absorbing competing-decrement model, not an arbitrary intercommunicating time-dependent finite-state generator or a semi-Markov duration-reset model. This restriction is important because its exact transition matrix and reserve integrals can be constructed without assuming the answer. Later actuarial missions can reuse the resulting conditional survivor functions and Thiele equation as a basis for disability recovery and wider inter-state transfers. Lean statements are open research targets, not accepted formal proofs, and the mathematical identity must be obtained from the originally defined valuation.
These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.
Actual insurer mortality and withdrawal observations are censored and may differ systematically with explanatory covariates. Cox's original 1972 proportional-hazards paper treats an arbitrary baseline hazard combined with covariate-relative-risk multipliers and constructs a conditional partial likelihood. Existing actuarial missions cover lifetimes, Kaplan–Meier/Greenwood and mortality graduation, but not regression risk-set estimation.
A life with scalar covariate z and regression parameter beta has hazard λ0(t) exp(beta z). The cumulative baseline hazard determines the survival function. At each distinct observed failure time there is a finite nonempty at-risk set, including the life that died, and censoring removes deaths that are not observed without treating them as failures. This mission assumes no tied failures in its conditional likelihood graph; more general Efron and Breslow ties require a separate coherent treatment.
The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.
A zero covariate reduces to baseline survival.
A censored observation must not simultaneously be a failure contribution.
Cox covariates alter baseline hazard multiplicatively, survival stays within probability bounds, and the nontrivial risk-set score is derived as the derivative of the conditional partial likelihood.
Cox covariates alter baseline hazard multiplicatively, survival stays within probability bounds, and the nontrivial risk-set score is derived as the derivative of the conditional partial likelihood.
The mission formally separates a common arbitrary baseline hazard from the relative hazard of each observed insured life. The partial likelihood uses event-specific risk sets, not a single fixed cohort denominator, and the model derives the true conditional event probabilities and analytic score from the independently defined likelihood. As in the original Cox model, the mathematical outcome provides essential foundations for credible, covariate-sensitive life contingent predictions and statistical mortality investigations.
The risk sets must remain nonempty and include observed failures when interpreting their shares as probabilities. Finite products with changing risk sets combine with a log-likelihood that is differentiated using an exponential weighted denominator. The central theorem must obtain the score from a derivative and must not define score equality as a model axiom. Positive covariate multipliers and boundary survival values are derived separately. The model does not assert a numerical maximum likelihood estimator exists without concavity or identifiability conditions.
The conditional partial likelihood is based on one observed failure at a time. Each event has its own finite risk set. A life censored before the event time is excluded from that later set, but an individual censored after the time remains exposed at that instant. Censoring patterns therefore change the risk sets, even though the baseline force drops out of the conditional event ratio. With a scalar coefficient, this model is an actuarially meaningful specialisation of the Cox regression formulation. The score derivative is substantive because its risk-weighted average contains the current coefficient in both the numerator and denominator. The numerator and denominator must each be differentiated, the denominator must remain strictly positive and the log derivative must not assume the target identity. Only after these facts have been proved can the formula for the score be justified. Extending the analysis to a score vector and information matrix would involve covariance matrices weighted by dynamic risk sets, and the nonnegativity of observed information is not a pointwise algebraic identity without proper hypotheses. Reusable consequences of this foundation include estimation with life-assurance underwriting covariates, statistical investigation of pensioner mortality, cause-specific decrements and a later treatment of time-dependent covariates. This graph deliberately treats distinct failure times rather than asserting a tied-events formula that has not yet been formally justified; Efron and Breslow corrections motivate future work, not assumptions of the current model.
The model treats a single scalar covariate and untied observed failures. It neither assumes a parametric distribution for the baseline mortality force nor confuses censored lives with observed deaths. It does not prove martingale asymptotics, proportional-hazard diagnostics, time-varying regression coefficients or Efron tied-event corrections. These are legitimate larger follow-on missions. Its theorem statements and source are unproved formal targets.
These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.
Panjer recursions allow compound claim distributions to be computed without enumerating many severity convolutions. The original Panjer paper and the Sundt–Jewell family extension establish the actuarial context. The previous LXXVII mission covers finite-support frequency distributions with zero claim amounts. Here the claim count ranges over all nonnegative integers, so correct series convergence and coefficient interchange become new formal obligations.
Let N be Poisson with claim count intensity λ≥0 or geometric with parameter q in [0,1). Independently distributed claim severities are nonnegative integer valued, with pmf f_j and possibly f_0>0. For each claim count n, the distribution f^{*n} is formed using genuine convolution; the empty portfolio assigns mass one to zero. The compound mass g_k is defined as the infinite sum of p_n times the n-fold convolution coefficient, independently of any Panjer formula.
The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.
True infinite aggregate mass is nonnegative.
Compound Poisson zero mass comes from thinning.
The genuinely infinite Poisson and geometric aggregates obey their independently derived corrected Panjer laws.
The genuinely infinite Poisson and geometric aggregates obey their independently derived corrected Panjer laws.
The capstone derives both infinite frequency families' entire positive-aggregate recurrence. For Poisson frequency the kernel includes a severity-size factor λj/k; for geometric frequency it contains an essential zero-claim correction 1−qf_0. The zero aggregate mass itself is the count PGF evaluated at severity f_0, not merely the probability of having no claims. The 1981 ASTIN literature underpins these equations, while a countably supported Lean formalisation makes their analytic conditions explicit.
Unlike the finite claim count in LXXVII, an infinite frequency model requires genuine convergence before double series may be rearranged. Proving the Poisson and geometric frequency normalisations is distinct from proving convergence of the actual aggregate pmf. At a fixed amount k a finite inner convolution remains, but summation over the count n is infinite. The nontrivial step is justifying probability-generating function composition and extracting the correct severity coefficients without assuming the desired recurrence or silently truncating Poisson claims. Special cases with all claim sizes zero are included.
Existing actuarial theory establishes the analytical principle, whereas the formal work here must prove the stated identities in Lean using the true distribution and event definitions. Some prior mission targets describe finite distributions or a candidate valuation, but they do not establish these stronger infinite-support or measured first-passage results. The boundary assumptions are part of each mathematical statement and cannot be replaced by a tautological definition. A complete proof requires independent source lemmas, explicit handling of the limiting case and verification of every transformation before concluding the capstone.
The generating-function series is defined from the probability mass of each count; the count law is genuinely infinite, not a finite upper cutoff with a hidden tail. In particular, the positive Panjer recursion cannot be used to define its own aggregate coefficients: the aggregate mass must first be constructed from convolution powers and the count weights. At claim size zero, the event of positive frequency with all zero-valued claims contributes to the true aggregate zero probability. Geometric count and Poisson count require distinct coefficient functions, even though they share the same actuarial notation for the severity distribution.
This mission addresses actual infinite Poisson and geometric count laws, with arbitrary properly normalised discrete severities. It does not cover noninteger-shape negative-binomial frequency, complex-domain analytic continuation or continuous claim sizes. The formal target makes probability nonnegativity and summed severity mass explicit, and all Lean proofs remain open. The resulting count/compound transforms can be reused in later collective-risk, stop-loss and capital modelling applications. It deliberately excludes vacuous proof strategies that define the aggregate distribution as the recurrence answer.
These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.
Actuarial claim counts and average costs depend on policy exposure, customer characteristics and risk-factor selection. The foundational Nelder–Wedderburn GLM formulation derives exponential-family maximum likelihood through a predictor and link, including Poisson count and Gamma response examples. Existing actuarial missions cover finite exposures and rating relativities, but not a unified log-likelihood score, information and deviance calculation.
An exposed group contributes E positive insured person-years. The count predictor η produces expected claims μ=E exp η, so log exposure is a compulsory offset rather than a fitted regression coefficient. The model defines observed claims per exposure, the Poisson log-likelihood up to a response-only factorial constant, its scalar score, expected information and saturated deviance. A separate Gamma mean and variance model describes positive insurance severity.
The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.
Nonnegative frequency and severity produce nonnegative pure premium.
Poisson log-likelihood attains a global maximum at the fitted canonical count for strictly positive observations.
A genuine positive-exposure Poisson GLM has the correct canonical offset, score and Fisher derivative, nonnegative saturated deviance and consistent severity-loaded insurance premium.
A genuine positive-exposure Poisson GLM has the correct canonical offset, score and Fisher derivative, nonnegative saturated deviance and consistent severity-loaded insurance premium.
Following Nelder–Wedderburn, the capstone derives the Poisson model's canonical offset, identifies the score as a genuine derivative of the log-likelihood, and proves that its derivative is negative Fisher information. A nonnegative deviance measures disagreement with saturated data and integrates with multiplication of expected frequency and severity to obtain the insurer's pure premium. This is the mathematical basis for estimating tariff frequency relativities and verifying model fit.
A real-valued logarithm is not automatically the log of a positive expected count: exposure positivity must be explicit. Count zero is handled with a separate non-log-deviance expression, avoiding undefined logarithmic ratios. The score and information identities must follow by differentiation rather than by an assumed GLM normal equation. It is a nontrivial analytic task: a vacuous definition of a zero score would not establish any likelihood derivative. The deviance inequality uses the logarithmic convexity inequality and requires positive expected and observed claims, while the finite exposure boundary avoids any mistaken claim of an informative zero-exposure observation.
The Poisson GLM score is the derivative of a log-likelihood rather than an arbitrary residual statistic. The exposure offset shifts the logarithm of expected claim counts, so changing exposed policy-years modifies the fitted expected count without changing the per-exposure class rate. This is a defining issue in insurance rating where two policyholders with the same expected annual frequency can have different months insured. The score derivative gives the negative Fisher information, leading to the familiar concavity of the scalar canonical log-likelihood under positive exposures. Identifying a maximum-likelihood estimate, however, also requires adequate observed data and a nondegenerate model: at zero observed claims, the MLE can be approached only as the predicted rate tends to zero, not necessarily at a finite linear predictor. The scaled deviance measures disagreement with saturated data; it is nonnegative by the logarithmic inequality when observed and fitted counts are strictly positive. The zero-count case has to be handled by a limiting convention outside the positive-count formula. This is actuarially material in sparse claim classes and high-frequency policy segments. Gamma severity uses a different conditional variance function, so its dispersion and positivity conditions are not inherited directly from the Poisson count model. This graph is a reusable foundation for multivariate tariff construction, fitted pure premiums, exposure offsets and later iterative weighted regression algorithms. Its source model follows Nelder and Wedderburn while making every claim-count positivity hypothesis explicit.
This is the scalar Poisson frequency and Gamma severity foundation, not a full numerical fitting algorithm or a general matrix-valued IRLS solver. The categorical design matrix, multivariate coefficient normal equations, dispersion estimation, residual-based diagnostics and parameter-inference asymptotics are reserved for follow-on missions. There is no assertion that positive claims always exist or that every rate model is identifiable. All Lean proof statements remain open.
These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.
Extreme insurance severity and catastrophe accumulation require models whose tails are not dictated by a Gaussian or ordinary exponential claim law. The NIST generalized Pareto reference provides a tail model for excess claim payments over a high threshold, while NIST maximum-type Gumbel models describe maxima of repeated extreme events. Existing actuarial risk missions cover limited stop-loss expectations and tail risk measures, but not the extreme-value distribution families themselves.
For positive shape ξ and scale σ, an exceedance amount x≥0 has GPD survival (1+ξx/σ) to the power minus one over shape. The distribution has an explicit actuarial claim density, hazard and percentile quantile. Its upper excess distribution retains the same shape while the scale increases linearly with the threshold. For ξ below one the conditional tail expectation is finite and can be expressed in terms of its loss quantile. A separate positive-shape GEV and maximum-type Gumbel distribution model extreme maxima.
The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.
The GPD density is minus the actual survival derivative.
GPD tail expectation follows the actuarial excess-loss identity.
An actual positive-shape GPD combines a valid percentile inverse, threshold-stable excess distribution and coherent expected shortfall, alongside a genuine extreme-maximum CDF.
An actual positive-shape GPD combines a valid percentile inverse, threshold-stable excess distribution and coherent expected shortfall, alongside a genuine extreme-maximum CDF.
The capstone connects the actual GPD distribution function, quantile inversion, excess-threshold stability and analytical expected shortfall. These are independent mathematical constructions, not labels attached to the target identities. This is a foundation for setting catastrophe attachment points, deriving economic capital quantiles and analysing sensitivity of retained high losses as severity tail shape changes. The extreme-value literature also explains why the GP exceedance approximation complements the family of limiting extreme maxima.
Power-law transformations are valid only where the base and denominators are strictly positive. Shape ξ=0 is a separate exponential limit and must not be quietly substituted into a nonzero-shape power expression. Valid quantile inversion needs a probability below one, a positive scale and a positive shape. The conditional excess calculation requires exact cancellation of two power-law tails with different scales. The expected-shortfall identity needs the finite-mean restriction ξ<1, while finite variance needs ξ<1/2. The maximum CDF uses nonnegative integer powers and genuine probability bounds.
The generalised Pareto excess distribution is most naturally expressed as an actual conditional survival function above a high loss threshold. Its threshold stability property says that when the threshold rises, the shape remains fixed and the excess scale changes linearly. The proof must use the quotient of two survival probabilities and factor the two scale-dependent power-law terms. A mere definition of the updated scale would not establish the identity. This gives an analytic foundation for excess-of-loss reinsurance attachment and severity tail risk. The capital quantile inverts the GPD CDF using a real power; the definition is meaningful only with the probability strictly below one and a positive scale and shape. Expected shortfall requires stronger tail integrability than a simple high quantile. A positive shape at or above one produces a distribution with infinite mean, so a finite closed-form conditional tail expectation must be restricted to shape below one. A finite second moment requires shape below one half. These parameter boundaries are central to actuarial capital stress testing. Maximum-type Gumbel and GEV distributions arise from the theory of sample extremes and use distinct parameterisations from the excess-loss distribution. The GEV expression implemented here is intentionally limited to the valid positive-shape support and does not assert the universal asymptotic convergence theorem. The NIST severity model supplies the distributional formula, and the NIST Gumbel model supplies the maximum-type reference. The resulting identities can be reused in future high-quantile capital and retention-optimisation missions without assuming that all insurance losses follow the Pareto family.
The mission formalises positive-shape heavy-tailed GPD and GEV and ordinary maximum-type Gumbel models. It does not claim the full three-regime extreme-value convergence theorem or derive the Pickands–Balkema–de Haan asymptotic result from arbitrary parent claims. The zero-shape GPD limit and bounded negative-shape Weibull branch are future extensions. The tail expected value is a defined closed-form functional; a further probability-integration theorem would be needed to prove equality with a conditional expectation integral. Lean theorem statements remain open.
These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.
As shown in crop insurance dependence studies, insurance risks share systemic mortality, climate, market and catastrophe drivers, so their aggregate extremes cannot always be modelled as independent. Copulas combine marginal loss distributions with their dependence structure. Actuarial empirical studies demonstrate that lower and upper joint-tail dependence can materially change high-quantile capital estimates. Existing Prove2Me missions cover risk measures and finite dependent lifetimes, but not copula margins, rectangle probability conditions or insurance co-exceedance.
A bivariate copula is a two-dimensional distribution function with uniform margins. Its cumulative joint probability on any rectangle must be nonnegative, so mere pointwise bounds are not sufficient to define a valid copula. The model independently defines product independence, comonotonic and countermonotonic Fréchet couplings, an FGM dependent family, and convex mixtures of copulas, with explicit parameter restrictions.
The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.
Two exchangeable uniform loss lines have symmetric FGM dependence.
All valid bivariate uniform joint risks satisfy the upper Fréchet bound.
FGM joint insurance dependence obeys genuine copula axioms, universally valid Fréchet limits and an exact analytic capital tail correction.
FGM joint insurance dependence obeys genuine copula axioms, universally valid Fréchet limits and an exact analytic capital tail correction.
As the crop insurance dependence study demonstrates, the capstone proves a genuinely bivariate dependence family has uniform margins and nonnegative rectangle masses, satisfies universal Fréchet bounds, and produces the exact difference between two-line capital exceedance probability and the independent baseline. The function used in the tail calculation is constructed independently of the conclusion and must meet the full two-increasing criterion. The mathematics isolates dependence risk from marginal expected losses and supports subsequent high-quantile capital analysis.
The two-increasing property is a nontrivial rectangular inequality, not a claim that a function happens to take values in the unit interval. The FGM copula must satisfy this criterion for its full allowed parameter range, and the Fréchet bounds must be proved for any separately certified copula. Tail co-exceedance combines survival complements and the joint cumulative distribution without assuming independence. Correct parameter and threshold restrictions are crucial.
The Fréchet–Hoeffding bounds arise from nonnegative masses of carefully chosen rectangles within the unit square and the uniform marginal constraints. Their proof uses the full two-increasing property, not merely pointwise nonnegativity of the joint CDF. It is possible to construct a function that has plausible one-dimensional boundaries but produces a negative rectangle mass, so boundary checks alone do not establish a copula. Convex mixtures preserve the genuine constraints because rectangle probability is linear in the dependence function and mixture weights are nonnegative. The FGM dependence family supplies a parameterised example where the entire copula proof is nontrivial yet algebraically accessible. Its parameter range must be restricted to preserve all rectangle masses. The joint exceedance probability then follows from inclusion-exclusion: capital thresholds correspond to upper tails of the marginal uniform transforms. This is an important distinction from simply computing the probability that at least one line exceeds its threshold. The same margins can coexist with different joint capital requirements, so portfolio dependence cannot generally be recovered from marginal loss expectations. This development is reusable when analysing risk aggregation and diversification under copula uncertainty. The crop-insurance dependence study illustrates the sensitivity of high-quantile risk to the dependence family. Gaussian, Clayton and Gumbel copulas require careful domain, monotonicity and tail-limit results and should be additional substantial targets rather than names appended to an unverified bivariate function.
This is the complete bivariate Fréchet/independence/FGM finite-copula foundation. The full Sklar representation theorem for arbitrary marginal distributions and Gaussian, Clayton and Gumbel parameter families require substantial measure-theoretic and analytic extensions and remain future work. The real-valued percentage thresholds must lie in the unit interval; conditional ratios are claimed only away from zero denominators. Theorem statements remain open.
These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.
Defined benefit funding involves a mathematical choice about when benefits are recognised and how contributions relate to prospective projected payroll. The IFoA's historical GN26 distinguishes entry-age, attained-age and aggregate methods. Existing actuarial missions cover projected/current unit credit and prospective reserve cashflows; they do not derive the wider standard contribution rate and exact actuarial surplus decomposition in the same theorem graph. This mission formalises the distinct valuation equations rather than repeating the projected unit method.
Write B for actuarial present value of total prospective benefits, P for the present value of projected future earnings, A for fund assets and L for accrued actuarial liability. An entry-age rate is calibrated when the member joins; an attained-age rate covers the total projected benefits net of the accrued projected-unit liability; the aggregate rate credits assets directly. Deficit payments are discounted over an explicit recovery annuity, and current assets and liabilities each evolve by actual monetary cashflows and assumption changes.
The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.
Annual attained normal cost equals rate times current pensionable earnings.
Under the mathematical total-function convention, zero payroll cannot define a useful rate; the model therefore makes no recovery claim at that boundary.
The three genuinely distinct DB funding methods reconcile projected liabilities while deficit contributions and complete one-year experience movements reconcile surplus.
The three genuinely distinct DB funding methods reconcile projected liabilities while deficit contributions and complete one-year experience movements reconcile surplus.
The capstone reconciles entry-age funding, attained-age future-service financing, aggregate funding and modified deficit contribution rates with an exact opening-to-closing surplus movement. In particular, the attained-age rate is derived from future-service value and the aggregate rate is derived from total prospective benefits less existing assets. The objective respects the OECD comparison of pension funding methods and does not conflate entry-age accrued liability with projected-unit accrued benefits.
The mathematical work must keep different cost allocations separate and exclude undefined zero-payroll or zero-amortisation denominators wherever contribution recovery is claimed. It must distinguish the actuarial liability from fund assets and preserve the signs of benefit outgo, administration expenses, interest unwind and changes in assumptions. The surplus capstone combines several independently defined rollforwards and excludes artificial circular definitions of a fully funded position.
The normal cost and accrued liability need different interpretations across the three prospective methods. For the entry-age model, future contributions use a rate calibrated on original entrant benefits and entrant payroll, whereas the current accrued liability subtracts the value of future payments at that inherited rate. For attained age, a separate projected unit past-service valuation is the liability, so only future-service benefits enter the prospective contribution rate. These two normal rates cannot be asserted equal without assumptions on salary progression, cohort service and entrance dates. The aggregate method deliberately credits existing scheme assets against all projected benefits when calculating a single funding rate, rather than reporting the past-service liability and deficit as distinct parts. The difference has real consequences for an open or closed scheme in surplus. This distinction is discussed in the IFoA terminology. The experience surplus reconciliation treats actuarial assets, cash contributions, actual investment gain, pensions paid and expense outgo separately from unwinding accrued liabilities, service cost, liability benefit releases and assumption changes. An investment gain and an investment assumption revision are not the same cashflow and must not be silently combined. The capstone derives both sides from the separately defined asset and liability rolls, so it does not assume their equality through the definition of surplus. These equations provide reusable inputs for later pension funding projections, deficit-recovery schedules, capital adequacy and sensitivity analysis. The chosen real-valued model does not itself make an actuarial statement about prudence, solvency regulations or a chosen best-estimate basis.
This is a precise real-valued funding reconciliation, not an assertion that a particular funding method is appropriate for a specific pension scheme. Discounted future benefits and payroll are model inputs, not a new probabilistic pension cashflow engine, and no universal claim of a positive contribution rate is made when assets exceed liabilities. The model's zero-denominator branches are mathematical total-function conventions only; normal recovery assertions require nonzero annuity and payroll inputs. Existing projected unit, early/late factors and cohort service models are reused conceptually without duplicating their theorem graphs. The statements remain open proof obligations.
These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.
Dependent competing risks arise when more than one cause can terminate a pension or insurance status, and when a single event can terminate several lives simultaneously. A traditional independent-life calculation can materially understate the probability of joint survival and misunderstand the probability of simultaneous failure. Promislow's account of minimum failure times, competing causes, common shock and multi-state modelling is the conceptual guide. The Marshall–Olkin model is an independently published stochastic model of linked exponential lifetimes. This mission formalises the actual underlying failure events and their resulting actuarial benefits; its proposed Lean theorem declarations are new mathematical targets, not claims of already accepted proofs. The book is S. David Promislow, Fundamentals of Actuarial Mathematics, Third Edition (2015), chapters 11, 17 and 19. The independently published supporting research reference is available here.
On a measurable outcome space Ω with probability measure μ, take three real-valued primitive failure times U, V and Z. U and V represent idiosyncratic risks for the two lives; Z is a common shock. The observed times are T₁=min(U,Z) and T₂=min(V,Z). An earliest Z causes both observed lives to fail together, even when U,V and Z have no primitive ties. Survival means strictly exceeding a stated duration. Failure by a horizon includes equality with that endpoint. For probabilistic interpretation, primitive times should be nonnegative and measurable. Pairwise independence is inadequate to justify multiplying three primitive survivor probabilities, so the joint product identity requires suitable mutual independence assumptions. Full parametric expressions require independent primitive exponential waiting times.
The central actuarial model can be written
The first block uses the actual probability measure of lifetime events. It distinguishes first idiosyncratic cause, second idiosyncratic cause, common-shock cause and primitive ties. The probabilities of the strict first-cause events add to one only if ties have zero probability. A positive common-shock event still produces a genuine observed joint-failure atom. Conditional survival and the monotonicity of joint survival at increasing deadlines are not inferred from deterministic symbols. The event partition provides a reusable bridge to multistate transition structures and group-life payment obligations.
The second block introduces the Marshall–Olkin parametric survivor law with nonnegative primitive exponential hazard rates a,b,c. Joint survivor at two different horizons depends on the maximum horizon because the shock affects both lives. Separate the independent-case boundary c=0 from the strictly dependent case c>0. Theorems on marginal survivors, diagonal joint survival, normalisation, positivity and the comparison with independently multiplied observed marginal survivors quantify exactly how the shared hazard creates dependence. This is a model-specific calculation, not an assertion that arbitrary observed lifetimes have independent components.
The third block prices cause-contingent insurance benefits by multiplying actual measured first-cause probabilities by separately specified amounts and a common deterministic discount. Benefit amounts are in currency; discount factors are dimensionless; failure times are in years. A three-way benefit schedule must specify an explicit common-shock payment amount because simultaneous failure cannot be assigned to only one idiosyncratic cause without a contractual rule. Scaling, additivity, positivity and the full-first-cause partition provide actuarial accounting results. The capstone connects the joint model's strict dependence with real cause-event probabilities and nonnegative expected claim value.
The proposed root is the principal actuarial theorem. Its intended actuarial mathematical relationship is illustrated by
This is a substantive nontrivial model commitment that excludes degenerate substitutes. This formula is stated only under the hypotheses and timing conventions of the actual Lean target. Subordinate theorem declarations provide the named formal prerequisites in the local source inventory. Each supporting milestone requires its own genuine proof rather than a textual assertion that an identity is obvious.
The results supply a reusable mathematical foundation for joint-life and last-survivor annuities, cause-specific death benefits and pensions involving disability, death and retirement triggers. They expose why observed first-failure data alone cannot determine every latent competing-risk dependence structure, a limitation studied by Tsiatis (1975). The Marshall–Olkin published shock model supports the probabilistic modelling motivation. The event formulation can later be joined with formal survival distributions, conditional hazards and reserve calculations while preserving simultaneous-event conventions.
The major proof obligations concern event measurability, countable additivity, event partition exhaustiveness and strict versus non-strict comparisons. Algebraic exponential survivor formulas do not by themselves establish independence of primitive failure times or the distribution of the first-cause variable. A genuine random-shock claim requires an actual probability measure and events. The capstone's source model is deliberately finite and avoids declaring a general copula representation without its full distributional hypotheses. A published source on competing-risk nonidentifiability, Tsiatis (1975), https://pmc.ncbi.nlm.nih.gov/articles/PMC432231/, describes why additional identifying assumptions are necessary.
This graph contains formal definitions of observed times and cause probabilities, supporting theorem targets for disjoint probability partitions and the Marshall–Olkin family, and one main actuarial claim-value capstone. General copulas, a fully general conditional joint-lifetime distribution and parametric shock-cause probability from three genuinely independent exponential random variables are natural extensions. The proposed current theorem graph is fully specified in the local dependency inventory. A remote declaration check with sorry placeholders validates only elaboration. Accepted proofs and a moderator-published mission are separate future stages. The staged inventory comprises 14 definitions and 34 open theorem targets. It uses the pinned Mathlib revision and a guarded remote private compiler. The proposed definitions also provide reusable results for future actuarial missions and downstream applications. The planned graph is recorded independently of theorem proof acceptance. The mathematical identities are already established in published actuarial or probability literature; the proposed Lean results remain new unproved formal targets. Every target remains open until an accepted proof is verified, and no owner item is to be confirmed or submitted for moderator review without human assessment.
The Cramér–Lundberg surplus model values how initial risk capital and premiums absorb claims arriving according to a Poisson process. Under exponential claim severities it admits an explicit ruin formula and Lundberg exponent. Promislow (2015), Fundamentals of Actuarial Mathematics, Chapter 23, covers martingales, adjustment coefficients and the compound Poisson surplus model. Rather than reproduce an elementary bounded gambler's-ruin recursion from previous missions, we formalise the distinctive exponential-severity transform and the actual renewal convolution integral required by the classical model.
Assume claim-count intensity lambda>0, premium rate c>0, independent claim amounts with Exp(beta) rate beta>0, and the net profit condition c beta>lambda. The expected aggregate loss over t is lambda t/beta. The risk adjustment coefficient R=beta-lambda/c is then strictly between zero and beta. The exponential severity MGF is beta/(beta-r) only for r<beta. Its net-loss exponent λ(M_X(r)-1)-cr vanishes at R. Define the explicit candidate ψ(u)=(lambda/(c beta))*exp(-R u) and the actual convolution ∫_0^u ψ(u-x) beta exp(-beta x) dx.
Let be the Poisson claim-arrival intensity, the premium income per year and the rate of independent exponential claim sizes. The expected claim amount is ; consequently, the expected aggregate loss over duration is . The expected surplus accounting identity is
The strict net profit condition makes the expected rate of capital accumulation positive.
For a severity with an exponential distribution, the moment generating function is finite only for :
The Lundberg equation compares the exponential claim cost with the premium contribution. Under the net profit condition, its nonzero adjustment root is
The theorem targets establish the necessary denominator and sign restrictions, together with the corresponding exponential transform identity.
Define the classical exponential-severity ruin candidate for initial capital by
The capstone verifies both the derivative of this function and the genuine convolution with the exponential severity density. The resulting integro-differential identity is
Proving that the candidate satisfies this equation is a nontrivial analytic step. Identifying it with the probability of the actual stochastic first-passage ruin event requires a separately constructed Poisson surplus process and appropriate renewal uniqueness or stopping-time arguments, which remain outside this mission.
The classical Lundberg risk-model literature motivates this setup. The capstone proves that an authentic positive adjustment root exists under stated assumptions, that the analytically defined net-loss moment transform is one at the adjustment root, and that the candidate function differentiates and solves the compound Poisson renewal differential/integral equation using the integral defined in Lean. This is substantially stronger than proving the algebraic exponential ansatz alone, and its boundary ψ(0)=lambda/(c beta) and capital monotonicity are separately covered. Existing missions establish finite-horizon ruin and bounded stopping ingredients. This mission goes beyond them by requiring the actual convolution integral with exponential severities, rather than postulating a renewal formula. All the new formal targets remain open Lean declarations, not accepted proofs. The stochastic identification of this unique analytic solution with the infinite-horizon ruin probability is a further theorem, not asserted without probabilistic martingale or renewal uniqueness hypotheses.
The exponential moment generating function exists for r<beta, not at r=beta; strict positive intensity, net profit and nonzero denominators are enforced. The ruin differential equation has an integral convolution and a remaining severity-tail term, and the sign is sensitive to whether the surplus decreases at claim arrivals. The candidate is only defined as the proposed analytic ruin function; an equation-satisfying candidate alone cannot be claimed to equal the actual stopping-time ruin event probability. Lean differentiability and interval integration are checked remotely against a pinned revision, never via local Lean.
The formal target covers expected compound Poisson loss and premium cashflows, the exponential severity transform, adjustment equation, renewal convolution and candidate solution for strictly positive exponential severities and premium rate, with u≥0 for probability interpretations. It does not directly construct a Poisson stochastic process, prove an exponential martingale from its probability law or prove uniqueness of a renewal equation solution. Those are explicit future reusable probability-theory extensions; the finite positive capital formula is formalised as a candidate until supported by a stochastic theorem.
These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.
The transition-intensity generator and prospective reserve equation are the key bridge between finite actuarial multi-state valuations and continuous-time life-contingency models. Promislow (2015), Chapter 19, and the research article Markov models and Thiele's integral equations for the prospective reserve establish the broader context. LXXV treats discrete-time state and duration resets; this mission creates genuinely continuous-time transition and actuarial reserve targets.
Three finite employment/life statuses admit a time-local generator Q with off-diagonal rates r_ij≥0 and diagonal Q_ii equal to minus the total rate of leaving state i. The short-period matrix I+hQ is stochastic only under a step-size condition, and no Euler approximation is misrepresented as the exact matrix exponential. A separate exact two-status alive/dead model at constant mortality intensity mu has survival exp(-mu t) and an absorbing death row. For this analytically solvable submodel, a finite-term prospective reserve incorporates continuous running payments, a death benefit and a discount force delta.
Let denote the annualised instantaneous rate of moving from state to a different state . The model begins with three states and constructs the generator from nonnegative off-diagonal rates, rather than assuming that the transition matrix already has the desired properties.
For a time increment , the Euler approximation retains unit row sums. Its entries represent valid nonnegative transition weights only when and . This step-size condition is part of the mathematical result.
The next group treats an insured person who is alive initially and whose death state is absorbing. With constant mortality intensity , the probabilities of remaining alive and having died by duration are
The targets establish nonnegativity, normalisation, the Chapman–Kolmogorov semigroup law and the derivatives of survival and death probabilities. This exact exponential model is distinct from the finite-step Euler approximation above.
Let be a continuous benefit outgo rate, the benefit on death, the force of interest and the contract maturity. For , the constant-intensity prospective reserve is
The capstone derives its terminal condition and differentiates this defined reserve to obtain
This is an exact alive/dead actuarial result. A general nonstationary three-state reserve differential system requires further transition-kernel and differentiability hypotheses and is not claimed here.
As explained in the continuous-time reserve literature, the main target derives the conservation property of Q and its short-step transition matrix, exact exponential Chapman–Kolmogorov for the alive/dead process, and a derivative identity for an explicit prospective reserve, namely V'(t)=(delta+mu)V(t)-b-mu B, V(T)=0. This is a mathematically defensible continuous-time stepping stone toward full time-inhomogeneous three-state reserve systems. It does not take the desired ODE as a premise.
Conservativity requires cancelling the generator diagonal against all off-diagonal exit rates. Euler steps require nonnegative h and h times the total departure rate at most one for nonnegative stay probability. Exponential semigroup identities require correct absorbing death treatment. Derivative calculations combine the exponential chain rule and nonzero delta+mu, with negative time-to-maturity kept outside the physical future-time domain when discussing positivity. Previously established actuarial models have described finite state-transition accounting and single-state Thiele expressions, while all new theorems in the current formalisation remain open. The generator and transition operators in this mission are independently specified, so row conservation and the ODE are proof obligations rather than assumed axioms. Nonstationary general-state Kolmogorov equations remain separate open mathematical work and are not asserted by this special constant-rate capstone.
A three-status arbitrary conservative generator with valid Euler short-step and a continuous-time two-status exponential Markov insurance submodel. The Thiele result is derived for an absorbing-life special case, not a general three-state nonstationary Thiele system and not a semi-Markov duration-dependent forward integro-differential law. The nontrivial capstone must substantively differentiate a reserve derived from dated benefits, not merely rename a differential equation or assume the desired target. The generalised setting is supported by explicit structural lemmas but needs further probability and differentiability formalisation before a complete multi-state ODE can be asserted. All targets are original formal derived claims; the declarations are not accepted proofs.
These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.