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?
Randomized algorithms for low-rank approximation — the randomized SVD of Halko, Martinsson and Tropp (HMT 2011), generalized Nyström, randomized subspace iteration, one-pass sketching (Tropp–Webber 2023) — multiply the input matrix by a random test matrix with independent standard normal entries. Every error bound for these methods rests on a small number of facts about such standard Gaussian matrices: they are invariant under rotations, disjoint blocks of a rotated copy are independent, and the second and fourth moments of a linearly transformed Gaussian matrix are given by explicit formulas. These facts are classical, but none of them is available in Mathlib, so a Lean development of randomized numerical linear algebra currently has to carry every one of them as an explicit hypothesis of its main theorems. This mission removes those hypotheses.
For , a standard Gaussian matrix of size is a random matrix whose entries are independent random variables. Its law, written , is the product measure on real arrays.
For a real matrix , is the squared Frobenius norm; is the dimension of its column space. A matrix has orthonormal columns when ; a square such matrix is orthogonal. For , a matrix with independent entries is written with , so that is an unbiased sketch of the identity.
For fixed , and with independent entries,
This is the exact mean-squared error of the sketched product as an estimator of , a direct consequence of Isserlis' pairing formula for Gaussian fourth moments. It is the goal because it is the one fourth-moment computation the series needs and because every other identity in the mission is a step towards it.
The results. Rotational invariance and block independence are the mechanism behind every conditioning argument in randomized linear algebra: writing the right singular vectors of the input as , the sketch splits into independent standard Gaussian blocks and , and one may condition on while treating as fresh. The second-moment identity then turns the deterministic range-finder bound into , and the approximate-multiplication identity gives the one-pass error terms. Almost-sure full rank is what makes a genuine pseudoinverse.
Formalizing them. Mathlib has the one-dimensional Gaussian measure, product measures, independence of coordinate projections, and (recently) the standard Gaussian measure on a finite-dimensional inner product space together with its invariance under linear isometries. None of the matrix-level statements above is in Mathlib. Once proved here they are reusable by every later mission in the series and by any formalization of randomized low-rank approximation, whose expectation-level inputs (e.g. ) follow from these milestones together with the inverse moments of Mission II.
Rotational invariance is not a computation with densities on that Mathlib supports out of the box: the clean route is through characteristic functions or through the basis-independence of the standard Gaussian on an inner product space, transported along the linear isometry of with the Frobenius inner product. Independence of the blocks requires identifying with a product measure and then projecting onto disjoint coordinate sets, with a completion of to an orthogonal matrix when . The moment identities are finite computations, but the fourth-moment identity needs the Gaussian moments , organized through Isserlis' pairing formula over a four-fold sum of indices; the obvious entrywise expansion produces terms that must be collapsed symbolically. Almost-sure full rank is the statement that the zero set of a nonzero polynomial ( of a maximal square submatrix) is Lebesgue-null, which must be established for the product Gaussian measure.
The sample space is the function type with the product -algebra; a sample is viewed as a matrix through the identity map . Expectations are real Bochner integrals: for an identity with a nonzero right-hand side this forces integrability, and the integrands here are polynomials in Gaussian entries. Laws are stated as equalities of pushforward measures; independence is Mathlib's IndepFun. Dimensions may be ; all statements remain true in that case. The hypothesis silently forces (vacuous otherwise), which matches the source.
The definition bundle GaussianMatrix_basic supplies the law , , , the spectral norm (Mathlib's operator norm), the smallest singular value and the pseudoinverse ; it is shared by the whole series. Welcome contributions: the Gaussian integration-by-parts and Isserlis lemmas for finite index sets, the identification of with Mathlib's stdGaussian on the Frobenius inner product space, and the "polynomial zero sets are null" lemma for product measures.
Series: I. Rotation Invariance and Moment Identities · II. Inverse Moments of the Pseudoinverse · III. Extreme Singular Values and Concentration. All three missions share the definition bundle GaussianMatrix_basic, published with Mission I, and the namespace GaussianMatrix.
Many insurance benefits depend on a policyholder's health or membership state rather than simply on being alive or dead. A disability annuity pays while a life occupies a disabled state; a critical illness or death benefit may be triggered by moving from one state to another. A rigorous multiple-state valuation therefore distinguishes payments for occupying a state from payments for a transition between states, and must also specify the timing of the payments.
The discrete-time models in Promislow, Fundamentals of Actuarial Mathematics, third edition, Chapter 19 §§19.2.1–19.2.3 [1], provide these two actuarial payment categories. Dickson, Hardy and Waters, Actuarial Mathematics for Life Contingent Risks, first edition, Chapter 8 [2], develop related multiple-state assumptions, transition probabilities, premium values and policy values. Norris, Markov Chains, §1.1 [3], supplies the finite-state stochastic-matrix foundation.
This mission develops the corresponding finite-horizon present-value formulas. It is the cashflow extension of the finite-state transition algebra in Mission X, but is designed as a self-contained draft while Mission X's definitions remain unpublished. The key mathematical obligations are correctly weighted transition benefits, state occupation annuities, finite-state distribution propagation, homogeneity and a capstone valuation decomposition.
Let be a finite set of insurance states. At the start of policy year , let represent the probability of state , and let be the conditional probability of occupying state at the end of the year, conditional on state at its start.
A state distribution must satisfy
A valid one-year transition kernel has nonnegative entries and rows summing to one:
The next year's marginal state distribution is obtained by propagating the current distribution through that kernel:
The supporting theorems show that nonnegativity and total probability are preserved by this operation. The transition kernels are allowed to change from one year to the next. A separate path-space process need not be constructed to establish these finite-sum valuation identities, but and must obey the propagation relationship to represent one coherent Markov insurance model.
Let be the payment made at the beginning of policy year to a contract then occupying state . For example, it could represent a disability annuity paid only while the person is disabled. The expected amount at that payment time is
The expected present value of the state-occupation cashflows over policy years is
A payment due at time zero is not discounted. A constant amount paid irrespective of state has its own expected value unchanged because the marginal state probabilities add to one. This is consistent with the state-occupation cashflow structure in [1, §19.2.3, equation (19.6)].
Let be the benefit payable at the end of policy year when the contract transitions from state to state over that year. The expected one-year amount is
The contract's expected present value of those transitions is
Unlike a reward depending only on the destination state, a transition-specific benefit may distinguish, for example, from . Keeping the pair explicit is necessary to represent such insurance benefits. This is the payment timing and transition structure considered in [1, §19.2.2, equations (19.2)–(19.4)].
The mission defines the complete finite-horizon value by adding the two types of cashflow:
Because finite sums are linear, scaling both monetary benefit schedules by a constant scales the entire expected present value by :
The capstone combines decomposition of the occupation and transition components with this scaling principle. Related milestones establish the zero-year, zero-benefit and one-year limits. For a one-year contract the exact timing reduces to
The displayed formula is deterministic expected-value algebra for finite state probabilities, rather than a claim about a pathwise cashflow random variable. The later development of a stochastic path-space model, conditional benefits and second moments remains a separate task.
The proposed Lean draft contains five definitions: a finite-state probability distribution, one-step distribution propagation, expected transition-stage reward, expected occupation-stage reward and the combined finite-term PV. Thirteen supporting theorems prove probability propagation, zero and constant payments, scaling, valuation decomposition and the one-year boundary. The final capstone packages the overall value decomposition and benefit scaling.
The formal theorem statements do not require the cashflow amounts to be nonnegative because their linearity is algebraic. Probability interpretation additionally requires legitimate state probabilities and transition kernels. The source explicitly avoids interpreting arbitrary arrays and as the marginals of one Markov chain unless they satisfy the propagation identity.
These declarations are proposed mathematical obligations, not accepted proofs. Individual Lean modules import only the definitions their statements actually use, with all imports before Lean commands. Because the local definitions are not yet published as importable Prove2Me modules, downstream theorem previews must be revisited after their definitions are confirmed and published.
[1] Promislow, S. David (2015), Fundamentals of Actuarial Mathematics, third edition, Wiley, Chapter 19, Multi-state Models, §§19.2.1–19.2.3. Equations (19.2)–(19.4) address transition-based insurance benefits and equation (19.6) addresses occupation-based annuity benefits.
[2] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2009), Actuarial Mathematics for Life Contingent Risks, first edition, Chapter 8, Multiple State Models, especially §§8.3–8.7 on states, transition probabilities, premiums and policy values.
[3] Norris, J. R. (1997), Markov Chains, Cambridge University Press, Chapter 1, §1.1 on stochastic matrices and discrete-time transition probabilities. The matrix-multiplication setting here permits different kernels at successive durations, in line with Promislow's non-stationary treatment.
Prospective policy reserves measure the expected present value of an insurer's remaining benefits less remaining premiums, per policy still in force at a valuation date. When premiums and benefits occur at annual dates, consecutive reserve values satisfy a one-year cashflow balance. That recursion is central to valuation systems, reserve roll-forwards and the decomposition of a life insurance premium into risk and savings components.
This mission develops the annual net premium reserve recursion for a finite-term life assurance. It builds on the conceptual framework of prospective policy values without importing unconfirmed declarations from earlier Prove2Me missions. The principal actuarial sources are Gerber, Life Insurance Mathematics, third edition, Chapter 6 §6.3, notably equation (6.3.4) [1], and Dickson, Hardy and Waters, Actuarial Mathematics for Life Contingent Risks, first edition, Chapter 7 §7.3.3 [2]. Both develop the balance between an opening reserve, the premium due and the expected benefit plus closing reserve.
A key objective is correct treatment of impossible conditional events: the aggregate expected-loss recursion does not require next-year survival to have positive probability, while the familiar conditional-reserve formula needs the next year's reserve to be defined for an in-force life.
Let be measurable curtate lifetime under a probability measure . Fix the contract term , integer valuation date , deterministic annual discount factor , death benefit and level premium . The insurer receives a premium at the start of each policy year for which . If , it pays the death benefit at the end of policy year , at calendar time .
The realised present value of the remaining net insurer loss, evaluated immediately before the time- premium, is
The date- premium appears in this expression and is worth one unit before multiplying by . Premiums earned before are excluded. The cashflow has finite calendar horizon even if the lifetime distribution is unbounded.
Define the probabilities of being in force, dying during the following year and surviving one further year by
The event partitions into two disjoint events, and , so
When , conditional annual death and survival probabilities are
No annual death-event independence assumption is made. The result follows directly from the disjoint partition of a natural-valued lifetime.
For , the future loss satisfies the pointwise identity
If the person dies in year , the current premium is collected and the discounted death benefit becomes due. If the person survives, the one-step-discounted continuation accounts for all remaining premiums and the eventual death benefit. Before the start of the contract's surviving period, all relevant terms vanish.
Taking expectations and using integrability of the finite-term cashflow gives the unnormalised recurrence
This identity remains meaningful when , because the future loss at is zero almost surely in that case. It is the safest formulation to prove before dividing by survival probabilities.
For , define the prospective reserve per policy in force at time as
The Lean definition uses ordinary real division, which is totalised at zero, but the actuarial interpretation above is asserted only under a positive survival-probability assumption. If both and , substitute and into the aggregate identity. Division by yields
The equation is the classical annual reserve balance: opening reserve plus premium equals the expected discounted claim and next-year reserve. Gerber [1, §6.3] also develops its decomposition into risk and savings premiums. This mission targets the core recursion and its probability and integrability prerequisites, rather than treating that later decomposition as already formalised.
The death-certain boundary is not hidden under a fictitious conditional reserve at . The aggregate identity above applies directly. A later extension can derive the explicit terminal conditional formula from it while preserving the zero-probability interpretation.
The draft introduces four definitions: the realised remaining loss, the in-force survival mass, death-year mass and prospective reserve quotient. Its twelve supporting theorems establish maturity and inception boundaries, the survival-event partition, conditional death/survival probabilities, loss integrability, the pointwise and integrated one-year recursions, reserve normalisation and the conditional reserve identity. A capstone combines the probability identity with the annual reserve recursion.
For , no covered future cashflow remains. At , , so the reserve is the unconditional expected loss at issue. The principal recursions allow any fixed real ; the usual insurance interpretation adopts a nonnegative discount factor. The proof obligations are finite-horizon and do not require a maximum possible lifetime.
The items are proposed Lean statements rather than accepted proofs. Their modules are dependency-ordered, with imports only at the beginning of each file. Until the supporting definitions have been individually published, downstream proof targets which import their modules must not be represented as ready for successful standalone compilation.
[1] Gerber, Hans U. (1997), Life Insurance Mathematics, third edition, Springer, Chapter 6, §6.3, Recursions, especially equations (6.3.4)–(6.3.10) and the premium risk/savings interpretation. Springer book DOI.
[2] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2009), Actuarial Mathematics for Life Contingent Risks, first edition, Chapter 7, Policy Values, §7.3.3, Recursive formulae for policy values. This chapter explicitly develops one-year annual policy-value recursions and related annual profit calculations.
[3] Open Actuarial Textbooks Project, Life Contingencies: Basic Life Contingent Benefits, Chapter 3, for the curtate-lifetime timing conventions used in the finite death-benefit and premium cashflows.
Life-contingent benefits may depend on more than whether an insured life is alive or dead. Disability, recovery, critical illness and multiple causes of exit can all be represented by finite sets of states with possible transitions between them. Multiple-state models make it possible to value benefits on a transition, annuities paid while occupying a state, and different amounts payable according to the insured's health or other status. Dickson, Hardy and Waters develop the actuarial multiple-state setting in Actuarial Mathematics for Life Contingent Risks (2009), Chapter 8 [1]. Promislow presents a discrete-time, potentially non-stationary Markov model and its insurance and annuity applications in Fundamentals of Actuarial Mathematics (2015), §§19.2.1–19.2.3 [2].
This mission establishes the finite-state, discrete-time algebra needed before tackling more difficult continuous-time transition intensities, differential equations or multistate reserves. The capstone connects composition of transition matrices with discounted state-dependent cashflows. The mathematical emphasis is on correct probabilities, annual timing and finite sums.
Let be a nonempty finite set of possible policyholder states. For one policy year, define as the probability of ending the year in state , conditional on starting in state . To represent a genuine transition kernel it must satisfy
The model allows a different transition matrix in each year. It does not assume a constant transition law or that every state can reach every other state. For two successive policy years, with transition kernels and , the two-step transition probability is
The intermediate state is summed out. This is the finite Chapman–Kolmogorov composition used in the non-stationary discrete Markov chain of [2, §19.2.1]. The proof must show that composing two nonnegative row-stochastic kernels produces another nonnegative row-stochastic kernel. Associativity,
then permits an arbitrary finite sequence of yearly transition matrices to be grouped without changing the resulting transition probabilities.
The matrix calculations alone are not a theorem asserting that an arbitrary stochastic process has the Markov property. They formalise the transition-probability algebra assuming the yearly probabilities are the kernels of a Markov model. Proving a full path-space conditional-probability construction is outside this mission.
Suppose an annual payment depends on the state occupied after the next transition. Write for the amount paid at the next year end when the new state is , and for the continuation value at that date. Let be the deterministic one-period discount factor. The one-step prospective value in current state is
Both and are measured at the next year end, so this formula applies precisely one period of discounting to both. A constant amount paid at the next year end has value , by the row-sum property. The valuation operator is linear in reward and continuation cashflows, and it is nonnegative when the discount factor, transition probabilities and cashflows are nonnegative.
For a payment arising only at the end of the second year, the two-stage recursion simplifies to
This identity reconciles backward valuation with forward transition-probability composition. It is the discrete precursor to larger actuarial valuation and reserve recursions. Promislow's §§19.2.2–19.2.3 discuss state- and transition-dependent insurance and annuity cashflows [2].
When the discount factor is zero, a payment made only at the next year end has zero present value. When all future rewards and continuation values are zero, the valuation is zero. Neither algebraic identity requires a particular health-state interpretation.
The theorem graph uses a finite state type and sums over all states. A true actuarial example must supply valid transition probabilities, distinguish payments made on entering a state from those made for occupying the state, and preserve the timing of an insurance payment at the end of the year. No independence between annual state indicators is assumed. Multistate variance calculations need joint transition probabilities rather than naively treating indicators as independent [2, §19.2.2].
The mission creates three definitions, twelve supporting theorems and one capstone. The proof path begins with row normalisation and nonnegativity, proves composition and associativity, and then develops constant, zero, linear and two-step discounted reward identities. The capstone combines the preservation of a stochastic kernel, associative composition and the two-step reward valuation.
These are proposed Lean theorem statements, not claims of completed proofs. This draft uses Mathlib's finite-sum and elementary order algebra, with no reliance on unpublished actuarial mission definitions.
[1] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2009), Actuarial Mathematics for Life Contingent Risks, first edition, Cambridge University Press, Chapter 8, Multiple State Models, especially §§8.2–8.4. This provides the actuarial interpretation of state transitions and the Markov modelling assumptions.
[2] Promislow, S. David (2015), Fundamentals of Actuarial Mathematics, third edition, Wiley, ISBN 9781118782460, Chapter 19, Multi-state Models, §§19.2.1–19.2.3. The discrete non-stationary transition model and subsequent state-dependent life insurance and annuity examples are the direct cashflow motivation.
[3] Norris, J. R. (1997), Markov Chains, Cambridge University Press, §1.1, Definition and Basic Properties. The book defines a stochastic matrix by its probability-distribution rows and states Theorems 1.1.1–1.1.3 on the Markov property and powers of the transition matrix. Its basic homogeneous-chain construction is a supporting special case, not an assertion that the time-varying matrices in this mission are all equal.
A net premium is usually set at policy inception. As an insured life survives and the remaining insurance term shortens, the expected future claim outgo and future premium income change. A prospective policy value measures the expected present value of the insurer's future loss on a policy that is still in force at the valuation date. This is the natural next stage after the equivalence principle of Actuarial Mathematics VIII. Dickson, Hardy and Waters provide the insurer's future-loss definition and the annual-cashflow policy-value framework in Actuarial Mathematics for Life Contingent Risks (2009), Chapter 7, §§7.3.1–7.3.3 [1]. Promislow covers both deterministic reserve recursions and the stochastic approach to reserves [2].
This mission formalises a finite-term life-assurance reserve at an integer valuation duration. Its central feature is survival conditioning: the reserve is a liability per surviving in-force policy, rather than the unconditional present value of the original contract. Separating these quantities avoids a common modelling error in stochastic policy values.
Let be measurable curtate future lifetime under a probability measure . Let denote the term, the valuation duration, a fixed per-period discount factor, the death benefit and the annual level premium.
Premiums are payable in advance at integer times while the life is alive. The benefit, if payable, occurs at the end of the year of death, at date . Only cashflows on or after duration enter the reserve, with discount exponents measured from .
The in-force survival event is
When , conditioning on this event gives the valuation basis for policies in force at . A statement about reserves conditional on survival must not silently assume that .
The remaining unit term-assurance benefit present value is
The remaining premium-annuity present value is
The realised future net loss is therefore
These finite expressions make it explicit whether a premium due at the valuation instant is included. Here is immediately before the premium at time , consistent with an annual premium payable in advance. The choice is essential when comparing reserve formulas across valuation conventions.
At the in-force event is certain. At or after , both remaining cashflow components vanish because the contract's coverage and premium period have ended.
For positive survival probability, the prospective term-policy reserve per in-force policy is
The second equality holds because the model defines the realised future loss as zero outside . It is a conditional-event expectation, rather than an unrestricted claim about conditional expectation with respect to an arbitrary sigma-algebra. The formal quotient definition makes the denominator explicit, and the principal reserve interpretation and capstone theorem retain as a hypothesis.
Linearity separates the reserve into benefit and premium components:
In particular, multiplying both cashflow amounts by gives
The finite payment period ensures integrability for any fixed real discount factor. When studying economic reserve properties, a nonnegative or positive discount factor can be imposed separately. No assumption of independence between survival indicators, benefits and premiums is made.
The principal boundary checks are survival at inception, ; exhaustion of cover at ; finite sums with ; and zero in-force probability. The total real-valued quotient happens to evaluate to zero when both its numerator and denominator are zero in Lean, but this does not create an actuarially meaningful conditional reserve for an impossible in-force event. The descriptive and main conditional theorems are explicitly scoped to positive probability.
Five definitions provide the in-force event, future benefit PV, future premium PV, future loss PV and the prospective reserve. Supporting theorems develop survival-event measurability, cashflow boundaries, nonnegativity where applicable, integrability, inception valuation, benefit–premium decomposition and scaling. The capstone combines the survival-normalised expected-loss identity, valuation decomposition and scaling.
The formalisation is deliberately self-contained at the level of future cashflow definitions so the owner Draft does not depend on the unconfirmed publication of any Mission VIII declarations. The intended later bridge is an exact identity between the duration-zero future loss and the loss-at-issue formula from Mission VIII, once those definitions are published. All theorems are proposed proof targets, not assertions of accepted proofs.
Gerber [4, §§6.3 and 6.5] provides an independent treatment of net premium reserves and annual reserve recursions. Its equation (6.5.6) expresses a whole-life net reserve through the premium difference, illustrating the same prospective viewpoint but not asserting the more general term-reserve theorem of this mission.
[1] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2009), Actuarial Mathematics for Life Contingent Risks, first edition, Chapter 7, Policy Values, Cambridge University Press. Relevant sections: §7.3.1 (future loss), §7.3.2 (policy values for annual cashflows) and §7.3.3 (recursive policy values), printed pages 176–195.
[2] Promislow, S. David (2015), Fundamentals of Actuarial Mathematics, third edition, Wiley, ISBN 9781118782460. In particular §6.3 (reserve recursion) and §15.5 (stochastic reserves).
[3] Dickson, Hardy and Waters (2009), Chapter 6, §6.5.1, equation (6.1), on the equivalence principle at policy inception, publisher book record.
[4] Gerber, Hans U. (1997), Life Insurance Mathematics, third edition, Springer, Chapter 6, Net Premium Reserves, §6.3 and §6.5, including the premium-difference reserve formula (6.5.6).
The equivalence principle is one of the foundational methods of setting premiums for life-contingent contracts. It requires that the insurer's expected present value of future benefits equal the expected present value of future net premium income at policy inception. As a result, the expected present value of the net future-loss random variable is zero. Dickson, Hardy and Waters define the net future-loss random variable in Actuarial Mathematics for Life Contingent Risks (2009), §6.4, and state the equivalence principle in §6.5.1, equation (6.1) [1]. Promislow develops the corresponding stochastic premium principle in Fundamentals of Actuarial Mathematics (2015), §15.6.1 [2].
This mission makes that principle a rigorous theorem for a finite-term life assurance financed by level premiums payable annually in advance. It proves that a unique net premium exists when at least one premium is due and nonnegative discount factors are used, and it separately addresses the zero-term case where uniqueness fails. The formal treatment distinguishes realised loss from expected loss, keeps mortality and discounting assumptions explicit, and avoids treating survival-contingent benefits and premiums as independent.
Let represent the probability space, with a measurable natural-valued curtate future lifetime . Let denote the policy term, the annual discount factor, a deterministic death benefit and a level premium.
A unit -year term assurance pays once, at the end of the year of death, if death occurs within the covered term. Its realised benefit present value is , reusing the published definition from Actuarial Mathematics II. In conventional cashflow notation,
This is the discrete term-assurance structure from [3, §3.2.2, equation (3.8)]. Premiums are due at the start of each covered year while the insured remains alive. The realised present value of unit premium income is
The insurer's discounted net future loss at inception is then
The same curtate lifetime determines both premium income and death benefit outgo. No independence assumption is made between these two random variables.
Because the sums are finite, their measurability and integrability can be established from measurability of for any finite real . Linearity of expectation gives
For a positive term and , the first premium at time zero is certain: . All subsequent premium present values are nonnegative. Consequently,
The denominator in the premium formula is therefore strictly positive. Solving the linear expected-loss equation leads to the net level premium
The theorem also proves uniqueness: any real premium satisfying must equal . This is the formal analogue of the equivalence premium calculation in [1, equation (6.1)]. As a related worked example, [1, equation (6.2)] gives a net premium for an endowment contract using the ratio of benefit and premium-annuity values. The mission specialises the general principle to an -year term assurance.
Linearity yields the scaling identity
for any constant . In particular, a zero benefit produces a zero premium under the ratio definition. A nonnegative benefit gives a nonnegative premium when , although the core algebraic scaling theorem does not require positive .
The boundary is deliberately distinct. Neither a term-assurance benefit nor a premium can occur, so . Every quoted level premium has zero expected loss in this empty contract, and uniqueness does not follow. The ratio definition is therefore paired with explicit theorem hypotheses rather than falsely suggesting a unique zero-term premium.
At and , the certain initial premium remains payable at inception, while all covered death benefits are paid at strictly positive times and have zero discounted value. The net premium is zero. At , all payment sums remain finite and integrable for fixed , so no artificial upper bound is needed for these finite-term results.
The mission introduces three definitions: the realised finite premium annuity-due present value, the realised term-policy loss, and the equivalence net premium. Supporting theorems establish the initial premium lower bound, measurability and integrability, positivity of the expected premium annuity, linearity of expected loss, existence and uniqueness of the equivalence premium, benefit scaling, and the zero-term and zero-discount boundaries. The capstone combines positivity, zero expected loss, uniqueness and benefit scaling.
The only previously published actuarial definition imported is the -year term-assurance present value from Mission II. The mathematical arguments use finite sums and integration under a probability measure, rather than relying on unproved statements from other draft missions. All declarations in this owner Draft are mathematical proof targets. Their presence in a proposal does not mean that their proofs have been accepted.
Gerber [4, §5.3.1] independently develops annual-premium term insurance, including its realised loss and the net premium equations (5.3.9)–(5.3.11). Those results corroborate the payment timing and the equivalence-premium construction adopted here.
[1] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2009), Actuarial Mathematics for Life Contingent Risks, first edition, Cambridge University Press, book DOI 10.1017/CBO9780511800146. See §6.4, The present value of future loss random variable, and §6.5.1, Net premiums, particularly equations (6.1)–(6.2).
[2] Promislow, S. David (2015), Fundamentals of Actuarial Mathematics, third edition, Wiley, ISBN 9781118782460. See §15.6.1, The equivalence principle, and §15.6, The stochastic approach to premiums.
[3] Open Actuarial Textbooks Project, Life Contingencies, Chapter 3, Basic Life Contingent Benefits, §3.2.2, equation (3.8), finite term assurance.
[4] Gerber, Hans U. (1997), Life Insurance Mathematics, third edition, Springer, Chapter 5, Net Premiums, particularly §5.3.1, equations (5.3.9)–(5.3.11), on finite term insurance and net annual premiums.
Whole-life assurance and a whole-life annuity-due are two fundamental life-contingent contracts. The assurance provides one unit of benefit at the end of the year of death, whereas the annuity-due provides one unit at the start of each year that the life is still eligible for payment, including time zero. Under a constant positive effective annual interest rate, their realised present values satisfy an exact finite-geometric-series identity. This provides an unusually direct connection between insurance benefits, annuity values and the distribution of curtate future lifetime. The relationship and its expected-value and variance consequences are stated in Life Contingencies, Chapter 3, equations (3.13)–(3.14) [1].
This mission formally develops that equivalence in Lean, starting from the individual cashflows and ending with a capstone theorem that combines the pointwise, expectation and variance results. It also isolates the assumptions needed for these results, supplies reusable bounds and integrability lemmas, and treats the zero-interest boundary separately. Related treatments of whole-life insurance and life annuities are available in the actuarial textbooks of Promislow [2] and Dickson, Hardy and Waters [3]. The mission's declarations are proposed proof obligations, not claims that every theorem has already been proved.
Let be the natural-valued curtate future lifetime of the insured life. In outcome , death occurs during policy year . Let be a flat, deterministic annual effective interest rate and define
The unit whole-life assurance, payable at the end of the year of death, has realised present value
This is the assurance contract defined in [1, §3.2.1, equation (3.7)]. The unit whole-life annuity-due makes payments at dates and therefore has realised present value
The annuity cashflow and the flat-interest specialisation are discussed in [1, §3.3.1, equations (3.11) and (3.13)]. The difference in timing is essential: the assurance payment occurs at , one year after the last annuity-due payment at .
For , the finite geometric sum gives
Equivalently, writing for the annual effective rate of discount,
These are pathwise statements. They hold for every realised natural-valued lifetime and require no assumptions about a mortality law or independence between annual survival events. They formalise the finite-series relationship in [1, equation (3.13)], rather than relying on an approximation or a selected life table.
Now let be a probability measure on and suppose that is measurable. The assumption implies , and the realised values obey
These deterministic bounds establish integrability, including the required second moments, even where has unbounded support across outcomes. Taking expectations of the pointwise identity yields
If and denote the corresponding actuarial values for a life aged , then
Translation by a constant leaves variance unchanged, and scaling multiplies variance by the square of the factor. Thus
The EPV and variance identities are stated in [1, equation (3.14)]. In particular, the variance factor is squared. No independence assumption is imposed: the assurance and annuity values are functions of the same lifetime, and the variance identity follows from their exact affine relationship.
At zero interest, , the whole-life annuity-due has realised value
This is a separate pointwise theorem. The expression is undefined at , and an arbitrary distribution of need not give a finite undiscounted expected payment count or a finite variance. An expectation theorem at zero interest would require a suitable first-moment assumption on , while a finite variance requires a second moment.
The simple assurance–annuity equivalence also relies on a flat deterministic interest basis. Under a non-flat yield curve the discounted cashflow series has varying discount factors and the same fixed geometric multiplier does not generally exist. The source expressly makes this limitation in [1, §3.3.1].
The mission adds one definition, the whole-life assurance realised present value, together with eleven supporting theorems and one capstone. The supporting graph establishes discount-factor positivity, the finite geometric sum, assurance positivity, the pointwise and unit identities, a boundedness lemma, integrability of both contracts, and their expected-value and variance relationships. A separate theorem handles zero interest. The capstone combines the key pathwise identity, expected-value relation, variance scaling and unit identity.
The only imported published actuarial definition is the existing whole-life annuity-due present-value definition from the earlier mission. The assurance definition is introduced here. The proposed proofs should use the appropriate finite-sum and probability-measure results from the pinned Mathlib, and no unproved theorem from another actuarial mission should be treated as an available proof dependency. These formal dependencies are distinct from the published textbook references below.
[1] Open Actuarial Textbooks Project, Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 3, Basic Life Contingent Benefits. Principal results: §3.3.1, equations (3.13)–(3.14), on the flat-interest annuity identity, EPV and variance. Assurance definition: §3.2.1, equation (3.7). Whole-life annuities: §3.3.1, equations (3.11)–(3.12).
[2] Promislow, S. David (2010), Fundamentals of Actuarial Mathematics, Wiley. Publisher book record, particularly Chapters 4, Life Annuities, and 5, Life Insurance. This provides wider actuarial background rather than an attribution of equations (3.13)–(3.14) to Promislow.
[3] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2019), Actuarial Mathematics for Life Contingent Risks, third edition, Cambridge University Press, particularly Chapters 4, Insurance Benefits, 5, Annuities, and 12, Yield Curves and Non-Diversifiable Risk. These chapters provide context for contract valuation and the distinction between flat and varying interest rates.
A whole-life annuity provides payments contingent on the annuitant remaining alive. A guaranteed life annuity adds a minimum number of payments, irrespective of early death. This alters the insurer's cashflows, since payments during the guarantee period are certain and subsequent payments depend on survival. It is an important contract structure for retirement income and provides a natural bridge between annuities certain, whole-life annuities and deferred life annuities. The payment definitions and expected present values are given in the Open Actuarial Textbooks Project's Life Contingencies, Chapter 3, §3.3.4, equations (3.19) and (3.20) [1]. Guaranteed payments are also covered within the broader treatments of life annuities in [2] and [3].
The objective of this mission is to formalise both annuities payable in advance (due) and annuities payable in arrears (immediate), including their exact cashflow decompositions, expected values and variances. It develops the mathematical justification for infinite survival-weighted sums when the distribution of lifetime is not bounded above. These are formal theorem targets to be proved, rather than results already established merely by publishing the statements.
Let be curtate future lifetime, where is the number of complete future years lived in outcome . Let be the number of guaranteed annual payments and let be a constant per-period discount factor. Each payment has unit amount, and an empty sum has value zero.
For an annuity-due, payments occur at times . The first payments at times are certain. Additional payments occur at times , if any.
For an annuity-immediate, payments occur at times . The first payments at times are certain. Additional payments occur at times , if any. The separate timing conventions are essential to the guaranteed-period boundary cases.
The guaranteed annuity-due has realised present value
For an annuity-immediate, the corresponding identity is
Here is the deterministic annuity-certain prefix and is the survival-dependent deferred continuation. The equations reproduce the underlying payment timing of [1, equations (3.19)–(3.20)]. They also connect to the deferred-annuity formulas in [1, equations (3.17)–(3.18)]. Additional pointwise theorems express each guaranteed value as its corresponding whole-life value plus the extra payments required when death occurs during the guarantee.
Let be a probability measure and assume that is measurable. For the analytical theorems, impose . Write . The expected present values are
and
The fixed prefix and survival-weighted tail are those in the guaranteed-annuity textbook formulas [1]. A formal proof must establish measurability and integrability and justify taking expectation through the infinite sum. The geometric bound supplied by makes these conclusions possible for a natural-valued lifetime distribution with unbounded support. No maximum attainable lifetime is assumed.
Since and are deterministic, adding them changes the expected values but does not change the variances:
These variance equalities are derived theorems, based on translation invariance of variance, rather than separate numbered statements in §3.3.4. The general survival-cashflow moment framework in [1, §3.1.1, equations (3.3), (3.5)–(3.6)] supplies background. No independence assumption between annual survival events is introduced.
When , both guaranteed annuities reduce to their corresponding whole-life annuities. When , the due annuity can still pay at time , while the immediate deferred continuation is empty and the guaranteed immediate payments remain. When , the due contract has its time-zero payment, and an immediate contract with still pays the certain instalments.
The finite realised-value identities hold algebraically for every real , including zero, one and negative values. The stated integrability, infinite expected-value and variance theorems deliberately use . In particular, an arbitrary undiscounted lifetime distribution need not have a finite expected payment count.
The mission introduces four definitions, fourteen supporting theorems and one capstone. The intended proof path establishes cashflow decompositions and zero-guarantee identities, develops geometric bounds and measurable survival events, proves the expected-value and variance relations, and then assembles the capstone from the supporting results.
The formal dependency graph reuses six published Prove2Me declarations: the curtate-survival event and its measurability theorem, together with whole-life and deferred present-value definitions for due and immediate annuities. These are technical dependencies, distinct from the bibliographic sources below. An unproved theorem from an earlier mission is not treated as an available proof dependency.
[1] Open Actuarial Textbooks Project, Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 3, Basic Life Contingent Benefits. Principal source: §3.3.4, equations (3.19)–(3.20). Related foundations: §3.3.1 (3.11)–(3.12), §3.3.3 (3.17)–(3.18), and §3.1.1 (3.3), (3.5)–(3.6). The explanatory sentence after (3.20) calls the contract deferred, although the section heading and displayed expressions describe a guaranteed annuity.
[2] Promislow, S. David (2010), “Life Annuities”, Chapter 4 of Fundamentals of Actuarial Mathematics, Wiley, DOI: 10.1002/9781119971528.ch4. The chapter's published summary includes guaranteed payments.
[3] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2019), Actuarial Mathematics for Life Contingent Risks, third edition, Cambridge University Press, Chapter 5, Annuities. General context for life-annuity valuation.
Whole-life and deferred life annuities extend survival-contingent payments beyond a fixed policy term. A whole-life annuity may pay on each eligible anniversary until death, while a deferred annuity begins after a specified waiting period. Both are standard components of pension and life-contingency valuation.
Actuarial Mathematics I established how to value finite cashflows. Missions III and IV provide curtate survival events and temporary annuity schedules. This mission develops the infinite-horizon valuation step: it justifies the lifetime payment series and its expected present value, including the conditions under which expectation can be exchanged with the discounted survival series.
Let be a probability space and let be a measurable curtate future lifetime. Define the survival event at time by
For expected present value statements, assume a deterministic annual discount factor satisfying
This condition provides a geometric bound on the payments and justifies exchanging expectation with the discounted survival series. No particular life table or independence between survival dates is assumed, and need not have a finite upper bound.
With unit payments in advance, a life with realised curtate lifetime receives a payment at time zero and at each subsequent beginning-of-year date through time . Its present value can be written
Its expected present value, given by equation (3.11), is
A whole-life annuity in arrears pays at times , with no payment at time zero:
Equation (3.12) gives its expected present value:
The payment in advance at time zero is certain, and the remaining payments match the arrears stream. Thus their pointwise and expected values satisfy
For a deferral period , a deferred annuity in advance has its first possible payment at time , with no payments before then. Equation (3.17) gives its indicator representation:
and its expected present value is
A deferred annuity in arrears starts at time and requires survival to that date. Equation (3.18) gives
with expected present value
The timing conditions matter. If , there is a due payment at time , but no immediate payment at time . When , each deferred annuity is its corresponding whole-life annuity.
The discounted cashflows in equations (3.17) and (3.18) are the corresponding whole-life streams with the first potential payment dates removed. Pointwise, this gives
and
Taking expectations gives the source's deferred-annuity valuation differences: each deferred annuity's expected present value is the corresponding whole-life expected present value less that of the temporary annuity.
The finite prefix sums reproduce the temporary-annuity schedules from Mission IV without importing its unpublished declarations. Mission IV remains a Draft, so its new theorems are not available as published imports. The two published curtate survival results from Mission III can be used.
The four new definitions use a finite payment sum for each realised natural-valued lifetime. Each realised cashflow therefore has finite support, even when the possible lifetimes are unbounded. The milestones connect these finite realised sums with infinite survival-indicator series, prove the deferred and initial-payment decompositions, establish integrability under the geometric discount condition, and derive four infinite expected-value formulas.
The capstone combines these formulas and decompositions for the same probability measure, curtate lifetime, discount factor and deferral period. The measure need not arise from a particular mortality model.
The condition applies to the expected present value claims. Pointwise present value identities hold for any real , since each realised natural-valued lifetime is finite and so produces only finitely many payments. At , an arbitrary lifetime distribution can have infinite expectation, so finite expected values cannot be assumed. The condition used here is sufficient; it is not claimed to be the sharpest possible condition under the source's financial discount assumptions.
The primary source is Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 3 §3.3.1 equations (3.11)–(3.12) and §3.3.3 equations (3.17)–(3.18). The temporary prefixes are the payment schedules from §3.3.2 equations (3.15)–(3.16), and the general expectation-of-cashflows step is equation (3.3).
This mission covers whole-life and deferred annuities. Guaranteed-period benefits, flat-interest assurance–annuity equivalence and continuous-time intensity-based valuations are separate later projects.
A life annuity pays a series of amounts while its recipient survives. A term assurance pays at most once during the policy term, whereas a temporary life annuity may pay several times. The indicators for its payments can therefore overlap, so a correct second-moment calculation must retain the dependence between them.
This mission formalises temporary life annuities payable in advance and in arrears, using the finite contingent-cashflow framework established in Actuarial Mathematics I. It reuses the curtate survival-event definition from Actuarial Mathematics III.
Let be a probability space, and let be the measurable curtate future lifetime, counting completed years. The event that the life survives to time is
These events are nested. For all ,
Consequently their indicators satisfy
This matters for second moments: survival to one payment date and survival to another are not mutually exclusive. Their intersection is survival to the later date. No independence assumption is made.
A unit temporary life annuity payable in advance makes up to payments, at times . The payment at time is made if . With deterministic annual discount factor , its random present value is
The expected present value is
These are the temporary-annuity-in-advance identities in Chapter 3, equation (3.15). The first payment, at time zero, is certain whenever .
A unit temporary life annuity payable in arrears has potential payments at times , for . A payment is made only if :
Its expected present value is
These are the corresponding payment-in-arrears identities in equation (3.16). In particular, a life with can receive the first payment of the annuity in advance, but no payment from the annuity in arrears.
The general moment calculations in Section 3.1.1 apply to the payment schedules in equations (3.15) and (3.16). Intersections of survival events reduce to the requirement to survive to the later date.
For payments in advance, the finite double-sum second moment is
For payments in arrears, it is
These are ordered double sums. Every ordered pair of payment dates contributes, including the diagonal terms and both orders of each off-diagonal pair. The corresponding variances are
The double-sum second-moment results are formal specialisations of the general moment equations (3.5)–(3.6). They are not additional numbered results in Section 3.3.2, which gives the expectation and present-value identities in equations (3.15) and (3.16).
The main theorem packages the expected values, second moments and variances of both annuities under the same , , and . Its supporting milestones establish the nesting of survival events and the products of their indicators, the finite payment schedules, and the successive valuation identities.
Both definitions are instances of the generic finite present-value construction from Actuarial Mathematics I. The curtate survival event is imported from Actuarial Mathematics III. Together, these provide reusable foundations for later missions on deferred and guaranteed life annuities.
The finite sums cover , when both annuities have zero present value, and , when the advance annuity includes the certain payment at time zero and the arrears annuity pays only if the life has completed at least one year. Algebraically, the identities allow any real . In actuarial applications, is normally positive. This mission asserts neither convergence of an infinite whole-life annuity nor statistical independence of survival payments.
The primary source is Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Open Actuarial Textbooks Project, Chapter 3 §3.1.1 equations (3.5)–(3.6) and §3.3.2 equations (3.15)–(3.16).
This is a draft mission and has not yet been published. It formalises finite-term annual payments. Continuous payment timing, deferred whole-life payments, guaranteed-period annuities and infinite valuation are planned separately.
An endowment assurance pays a fixed benefit either when the policyholder dies during the policy term or when the policy reaches its maturity date. It therefore brings death-contingent and survival-contingent payments together in one valuation framework.
Actuarial Mathematics I established general identities for valuing finite contingent cashflows. Mission II formalised unit term assurance and the mutually exclusive events of death in different policy years. This mission extends those foundations to pure endowments and endowment assurances, covering payment dates, expected present values, second moments and variances.
Let be a probability space. The exact future lifetime takes nonnegative real values, while the curtate future lifetime records completed years. Their relationship is
For a term , the textbook's pure-endowment payment in equation (3.9) depends on strict survival:
The endowment-assurance formula in equation (3.10), by contrast, uses a maturity payment when , equivalently when . Define
These events differ if death occurs exactly at time . Given the relationship between exact and curtate lifetime,
Thus equation (3.9) uses exact lifetime and excludes death at , whereas equation (3.10) uses curtate lifetime and includes it, since then . This endpoint identity clarifies the textbook's conventions; it is not itself a numbered textbook result. No assumption is made that death at a policy anniversary has probability zero.
Under the strict exact-lifetime convention, a unit pure endowment payable at time has random present value
Equation (3.9) gives its expected value and variance:
Here is a deterministic annual discount factor. The Lean algebra permits any real , including the conventional case of a positive discount factor.
The endowment assurance pays a unit benefit at the end of the policy year of death if death occurs within the first years. Otherwise, it pays at time . As in equation (3.10), its present value is defined by
The theorem expresses this value as the sum of the unit term assurance from Mission II and the curtate maturity payment:
The death benefit and maturity benefit are mutually exclusive. This gives the expected value and second moment:
The variance is then
The formalisation proves measurability of the strict and curtate survival events, the exact boundary-event bridge, disjointness of death during the term from survival to maturity, and the pure-endowment expectation and variance. It also proves the endowment decomposition, expectation, second moment and variance. The formal capstone brings these results together under one probability measure, using the same exact and curtate lifetimes, term and discount factor. It states the boundary bridge explicitly and includes the pure-endowment mean and variance, along with the endowment present value, mean, second moment and variance.
The formalisation reuses Mission II's definition of term-assurance present value rather than reconstructing it. The main namespace remains ActuarialValuation, so later life-annuity missions can use the survival-event lemmas.
The edge cases require care. When , the endowment assurance pays immediately. The strict pure endowment, however, still depends on whether . Death at exactly is represented separately and is never excluded by an unstated continuity assumption. The finite real-valued Lean identities permit negative or zero discount factors as a mathematical generalisation, although ordinary actuarial applications use positive discount factors.
The primary source is the Open Actuarial Textbooks Project, Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 2 §2.4.3, Chapter 3 §3.2.3 equation (3.9) and §3.2.4 equation (3.10).
Mission II, Actuarial Mathematics II: Term Assurance Present Values and Moments, is under moderator review at drafting time. Its relevant published definitions and theorem IDs are referenced directly.
This mission formalises unit benefits over a finite term with deterministic annual discounting. It establishes a finite-horizon result, not an infinite-horizon theorem. It does not cover immediate death benefits, arbitrary benefit scales, lifetime-dependent interest, infinite whole-life present values or the full continuous-time theory of mortality.
A sender can encode a classical message in a quantum state, transmit that state through a noisy quantum channel, and let a receiver measure the output. For researchers studying classical communication over quantum systems, the question is whether evaluating one channel use captures the benefit of encoding across several uses. Hastings established that the relevant information quantity can violate additivity when joint inputs are allowed. Hastings, 2009.
The result contributed here concerns the size of that discrepancy in finite dimensions. It gives channels for which positive single-use information is arbitrarily small while both the absolute two-use additivity gap and the relative benefit of two uses are arbitrarily large. The paper's introduction states the gap, capacity, and separation consequences; the released Lean theorem packages the small-information, gap, and ratio conclusions into one common-witness statement. Revised manuscript, Section 1, headline Lean theorem.
A finite-dimensional quantum channel is a completely positive, trace-preserving linear map on complex matrices, where the positive integers are its input and output dimensions. A density matrix is a positive semidefinite matrix with trace one. Such matrices represent the possible input states. The released development represents a channel by finitely many rectangular Kraus matrices , satisfying , with action . Concrete channel definitions.
The von Neumann entropy in bits is , where are the eigenvalues of , using . A finite ensemble consists of density matrices and real probabilities with . The Holevo quantity is
The supremum includes all normalized finite ensembles. For two uses, acts on joint inputs, including states entangled between the uses. Write , , and, when , . These are the released definitions chi, chiTwo, gap, and twoUseRatio. Definitions.
The broader release also studies operational classical capacity : the supremum of achievable classical message rates in bits per use. Its independent definition uses actual density-matrix codewords, a normalized positive-operator-valued measurement decoder, and average Born decoding error tending to zero over all positive block lengths. Arbitrary block inputs and joint decoding are allowed. That coding development provides context for the result; it is a separate released branch outside this contribution's initial import. Released operational definition.
The headline statement is
One channel witnesses every inequality. The lower-bound thresholds are arbitrary real numbers; they are not restricted to positive values in the Lean statement. Input and output dimensions may depend on the thresholds. The goal imposes no hard-coded dimension bound or numerical constant. It is the exact statement of Nonadditivity.DeterministicConsequences.exists_small_chi_large_gap_and_ratio. Source.
The supporting separation statement uses a sequence of genuine finite channels with
The separation statement is already proved for the selected deterministic family. It gives the two information limits asserted in the manuscript's Corollary 1.3, with no analytic channel-existence assumption. The formal family is totalized at its first two indices by the one-dimensional identity channel; this finite prefix does not affect either limit. Its members have positive single-use Holevo information for every . Released family, positivity, and limits.
The theorem gives unbounded absolute Holevo additivity gaps and unbounded two-use ratios for the same witnesses, even while their single-use information is arbitrarily small. This supplies an existence result rather than an efficient method for finding small channels with practical parameters. The manuscript separately proves explicit sufficient input dimensions; those bounds are not conclusions of the headline theorem. Manuscript, Corollaries 1.2–1.3.
The mathematical result is proved, and its principal endpoints already have machine-checked Lean proofs in release v1.0.0. This contribution imports the existing deterministic separation theorem and its dependency library, preserving their source provenance and proofs. The reusable material includes density matrices, concrete channels, entropy, finite ensembles, tensor products, and the finite-channel construction. Independent review of the correspondence between the formal statements and the manuscript remains useful. Release and verification scope.
The broader release additionally proves from independently defined physical codes, implying . It also proves a common-witness theorem combining small positive information with arbitrary capacity gain and two-use ratio. Those operational results are separate released context, rather than targets or imported milestones of this contribution. They concern unassisted memoryless communication and do not assert distinct-channel capacity nonadditivity or a strong converse. Released coding identity, released operational consequence.
A separate information estimate for each channel factor does not control inputs entangled across an entire block. The construction needs bounds valid for every such joint input, while retaining the favorable two-use behavior. Likewise, convergence of averaged matrix moments alone need not control exceptional eigenvalues and therefore cannot replace the needed norm control. These are substantive uniformity requirements in the paper's construction. Manuscript, Section 1.
Regrouping tensor powers of one fixed channel is insufficient for a gap linear in the regrouping length: the manuscript shows for a fixed . The existential goal instead allows channel dimensions and the channel itself to vary. Fixed-channel limitation.
The imported representation is ActualConsequences.FiniteQuantumChannel: finite, nonempty input and output index types, a finite environment index type, and a concrete Kraus channel. Entropy is computed spectrally with natural logarithms internally; holevoBits divides by . Supremum and infimum uses are accompanied by the developed nonemptiness and boundedness results. Positive tensor powers are indexed by a natural number meaning uses. Strict positivity of the goal's prevents division-by-zero interpretations of its ratio. The channel and information quantities must retain these physical definitions; numerical records assigned the desired values would not formalize the result. Formal representation, bit conversion.
The headline proof uses the alternate deterministic finite-channel construction. It does not assert the prescribed-dimension result. The imported library provides complex matrix analysis, positivity and trace normalization, tensor products, entropy inequalities, finite ensembles, and the construction's finite group and moment infrastructure. The full manuscript remains outside the completed formalization: general Haar convergence interfaces and the broader finite-dimensional realization statement retain their documented limitations. The release's correspondence findings remain qualified; no complete semantic audit or independent human certification is claimed. Formalization status, statement review.
635aa93eb3a2310b79fd5371e2ce311914ec5887.A quantum channel describes a physical process that transforms a quantum state into another state. Comparing two channels means comparing their possible outputs, including outputs obtained when the input is entangled with a reference system. This distinction matters in quantum information: an experiment can retain a reference while sending the other part of an entangled state through an unknown process. The resulting measure of distinguishability should account for that experiment.
For states, several divergence measures approach relative entropy when their order parameter approaches one. For channels, optimization over inputs and arbitrarily many channel uses introduces an additional question: does this continuity survive those optimizations? Jinzhao Wang and Yuxiang Yang answer that question for the regularized, stabilized sandwiched Rényi divergence in Continuity of Regularized Channel Rényi Divergences, arXiv:2609.28635v1, Theorem 1. This mission contributes the completed result and its supporting formal infrastructure.
Let and be nonzero finite-dimensional complex Hilbert spaces. A density operator is a positive operator with trace one. Two channels are completely positive, trace-preserving linear maps with the same input and output spaces.
The relative entropy compares density operators and . The sandwiched Rényi divergence is an order-dependent comparison, defined for , . The state, channel, and regularized divergences are measured in bits. Operator-level analytic lemmas may use natural logarithms; the state wrappers divide by . Singular states are allowed; the support conventions retain infinite values rather than assigning a finite substitute. These are the state quantities in the paper's equations (1.2)–(1.3).
The stabilized channel divergence optimizes the state divergence over normalized pure inputs on , where is a copy of . The channel acts on and the identity acts on . Writing , the convention is
where denotes either state divergence. The paper places the reference first; the formalization places it second and proves the tensor-factor convention agrees. A block of uses employs and a reference copy of . Its pure input may be entangled across every use. Equation (1.4) specifies this stabilization.
The regularized divergences are defined independently as positive-block suprema:
Two supporting targets establish that these definitions are the actual asymptotic limits in equation (1.5). For every fixed , ,
and
The main goal is Theorem 1:
This is convergence from both sides. Each target includes infinite divergence. The block identities are supporting identifications, rather than extra premises of the main theorem.
The main result identifies a single limit after optimization over entangled inputs and unbounded block lengths. It permits near-one regularized Rényi quantities to approach regularized relative entropy for arbitrary channel pairs in the stated finite-dimensional setting. When the latter is infinite, the conclusion is convergence to positive infinity. The paper discusses applications to discrimination and asymptotic approximation; those operational conclusions are beyond this mission's targets. Wang–Yang, arXiv:2609.28635v1.
This is a contribution of a known, formally proved result, rather than an unsolved conjecture. The original public Lean development includes proofs of the definitions' supporting properties and both block identities. Its recorded verification reports Lean checking with a transitive axiom audit, Comparator statement comparison and Lean kernel replay, and independent Nanoda kernel checking. These records concern the original pinned development. They are unsigned and do not establish independent human review of correspondence to the paper. The converted contribution uses Lean 4.30.0 and Mathlib c5ea003. Its 95 Definition bundles and 27 theorem nodes have been published; every theorem has an ACCEPTED proof and public Proved status. Before upload, the exact statement and solution files compiled locally, their types and transparent definition values were compared with the frozen compatibility port, and a transitive axiom audit of every generated declaration found only propext, Classical.choice, and Quot.sound. These new checks are separate from the original Comparator and Nanoda records. Human review of correspondence to the paper is still required.
Pointwise continuity for a fixed pair of output states does not justify interchanging a limit with the supremum over all block inputs. That domain includes every positive block length, so finite-dimensionality of each block does not itself supply a uniform conclusion. The right-hand limit is particularly sensitive to the order of these operations. Singular inputs introduce a separate issue: support mismatch can force genuine infinity, and converting all expressions to ordinary real numbers would discard that case. The formalization must preserve these domains and conventions throughout, as documented in the paper-to-Lean mapping.
The Lean representation uses actual positive density operators, CPTP maps, reference systems, and tensor powers. State divergences have extended-real values; channel and regularized divergences take values in . Nonnegativity is proved for the admissible orders, so conversion to nonnegative extended reals preserves those values. Supremum definitions quantify over positive block lengths. The normalized block sequences are total at , which is irrelevant to convergence as .
The main formal statement uses a punctured neighborhood of one. A sufficiently small such neighborhood lies within , so totalized definitions at other real orders impose no assertion about their divergence interpretation outside the admissible range. No support inclusion, finite max-relative entropy, filter estimate, or Schatten estimate is assumed by the main theorem. Defining the limiting value to equal the desired conclusion, or replacing arbitrary channels by an easy special family, would not meet these targets.
The development builds on Mathlib and Lean-Quantum. Reusable components include extended-valued Fekete convergence, channel tensor identities, quantum testing quantities, prescribed-dilation approximation, and finite-dimensional Schatten bounds. The scope mapping records that the supporting decomposition estimate is formalized for , sufficient near one; it does not claim the paper's entire all-orders version. Contributions that improve reuse, verify the converted dependency graph, or extend separately stated results are welcome. The paper's later operational corollaries are excluded.
An -year term assurance pays a benefit if the insured person dies in one of the first policy years. It can pay only once. This matters when calculating the second moment: claims in different years cannot both occur, so the cross-products between them are zero.
Actuarial Mathematics I established finite expected present values, second moments and variances for general collections of contingent payments. This mission applies those results to one life and a fixed-term death benefit. It proves the familiar term-assurance formulas from reusable death-year events, rather than treating them as isolated actuarial notation.
Let be a probability space and let be a measurable curtate future lifetime: the number of complete future years lived before death. For , define the event of death during policy year by
Each event is measurable. The events are pairwise disjoint: if , then .
Fix a policy term and a constant annual discount factor . A unit benefit is payable at time if death occurs during year , for . Its random present value is
When , the sum is zero. The implementation uses the previously published `ActuarialValuation.presentValue` definition with the schedule of death-year events, reusing the general valuation machinery. The theorem statements allow any real , so the finite algebra also holds beyond the economic setting . The positive discount factors customary in the source are a special case.
The capstone proves these three identities together.
Expected present value:
Second moment:
Variance:
The second-moment simplification comes from the mutual exclusivity of distinct death-year events, not from independence. In the general double sum from Actuarial Mathematics I, every off-diagonal intersection of death-year events is empty, leaving a single sum.
The milestones proceed from measurability of each death-year event to disjointness across years, vanishing products of distinct death-year indicators, the finite present-value representation, the expected value, the second moment and the variance. The proposal gives each mathematical statement and Lean target type separately. The capstone combines the three moment identities for the same , , and .
The project uses the existing `ActuarialValuation` namespace and imports published Mission I results where they apply. All dates are annual, and benefits are payable at the end of the year of death. Multiple lives, benefits payable immediately on death, stochastic discounts, select-life models and whole-of-life infinite sums are outside the scope of this capstone.
A complete proof provides a reusable one-life mortality event model and a verified finite-term insurance valuation formula. The model can support a later mission on pure endowments and endowment assurances, where survival-to-term events complement death-in-term events, and another on temporary annuities, where survival events are nested rather than disjoint.
The results also make it straightforward to compare the traditional actuarial single-sum variance formula with the general dependent-cashflow theorem proved in Mission I.
The main mathematical source is Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 2 §2.4.3 for curtate future lifetime, Chapter 3 §3.1.1 equation (3.4) for disjoint-event moments, and §3.2.2 equation (3.8) for term-assurance present value, mean and variance.
These established actuarial formulas are not new mathematical conjectures. The contribution is a precise formal link in Lean from a curtate-lifetime model to the general contingent-payment valuation layer.
The death-year set must be shown measurable from the measurability of . The disjointness arguments must also cover degenerate cases such as . The generic second-moment theorem uses an ordered double sum. The proof must remove only terms justified by , retain the diagonal terms and use the correct end-of-year exponent .
All formal declarations are written for Prove2Me's pinned Mathlib revision `0df444a360eaa60ab8c11dca51a86af692955474`. No local Lean compiler is used. Any private preflight compilation, if needed, is performed through Prove2Me's remote system.
Life insurers and pension schemes promise cashflows whose payment depends on future events. A term assurance pays if the insured dies within a stated period. A pension pays when a member survives to an instalment date. A contingent survivor pension may continue after the member dies. These liabilities differ in the events triggering payment, but share one mathematical operation: discount the amounts payable and aggregate them to obtain a random present value. Expected present value is used in premium setting and liability valuation, while the second moment and variance quantify how much the discounted liability can vary.
The open textbook Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 3, §3.1, introduces uncertain discounted cashflows using indicators, and derives their expected values in equation (3.3). Its treatment also distinguishes independent indicators from indicators connected through death or survival. This mission establishes a finite-horizon generalisation of those identities that handles arbitrary dependencies among payment-triggering events.
Fix a measurable sample space with a probability measure . A finite set indexes distinct payment obligations. Each obligation has a non-negative integer payment date , a deterministic cashflow amount , and a measurable event that triggers payment. The deterministic discount function assigns a multiplier to each date. Write for the real-valued event indicator, equal to one on and zero otherwise.
The random present value is
The same date can support multiple obligations with distinct contingencies, such as member and survivor payments, pension tranches and expenses. The index distinguishes obligations even when their payment times coincide. Amounts may be positive, zero or negative and triggering events can be mutually exclusive, nested, independent or arbitrarily dependent. Finite schedules also allow no obligations. Each present value is bounded and has finite first and second moments because the schedule is finite, amounts are deterministic real numbers, and indicators are bounded.
The capstone theorem proves the expected present value, second moment and variance identities for the same random variable . The expected present value is
The second moment retains all dependence terms, including pairs of different obligations payable on the same date:
Consequently,
The finite identity for expected present value specialises the textbook's equation (3.3). The general joint-event second-moment identity extends its §3.1.1 discussion to arbitrary dependence. The goal combines all three formulas in a single result, with supporting milestone theorems for integrability, square-integrability, one-event expectation, the finite-schedule expectation formula, pairwise event interactions, the second moment and the variance.
A single reusable statement should allow a future mission to specify the trigger events and payment schedule of a policy and immediately obtain its discounted mean and variance. A life assurance can use disjoint death-year events, and an annuity can use nested survival-to-payment events. A guaranteed pension, deferred benefit, survivor pension or multiple-decrement model can use more general indicators. Later missions can also specialise the variance expression when events are known to be independent or mutually exclusive.
Examples of why the dependence assumptions matter. Write for each discounted obligation amount:
These specialisations use the same capstone rather than different definitions of actuarial present value.
The mathematical identities are established results of elementary probability and financial mathematics. The formalisation contribution is a stable actuarial cashflow interface connecting the relevant Lean measure-theoretic and probability results. It does not assert that the classical equations are newly discovered, or that general insurance reserving, stochastic interest rates or continuous-time survival models have already been formalised.
The event indicator is a bounded random variable, but its mathematical expectation is represented in Lean by integration against a measure. The development must reconcile the real-valued integrals with event probabilities represented as extended non-negative reals. Moreover, expanding the square of a finite random cashflow sum requires pairwise intersections without adding an independence assumption. The usual simplification that removes cross-terms is invalid for nested survival events or arbitrary dependent payment events.
The target also uses the real-valued variance from Mathlib. Its general API permits variables outside , so a faithful proof must establish square-integrability for the finite event-based present value rather than use any default value for an undefined or infinite variance.
The initial development is discrete-time and finite-horizon, with distinct payment obligations indexed by a finite set. Each obligation has a nonnegative integer payment time. Different obligations may have the same payment time. Discount multipliers and payments are deterministic real values; no positivity assumption is needed for the algebraic identities. Each trigger is a measurable event and the underlying measure is a probability measure. Empty index sets and zero or negative payments are included. The joint-event formula remains valid when the same outcome triggers more than one payment.
Use Mathlib's existing MeasureTheory.Measure, MeasurableSet, integration and ProbabilityTheory.variance rather than redefining them. A lightweight namespace ActuarialValuation should define the random present value and retain clear time and cashflow parameter names. Supporting results should be small and import only genuine mathematical dependencies. The formalisation uses a generic obligation index type and a payment-time function into the natural numbers. The event family and amounts are indexed by obligations rather than by time.
There is no finite-to-infinite inference in the target; infinite sums require separate convergence results. There are no mortality rates, hazard functions, Markov transition kernels or stochastic discount factors in this mission. Those are targets for later missions, building on the valuation layer.
Prove Lieb’s concavity theorem (Theorem 8.1.1, also stated as Theorem 3.4.1): for fixed Hermitian H, the function A ↦ tr exp(H + log A) is concave on positive-definite matrices. This is the deterministic foundation of Chapter 3’s probabilistic argument.
Milestones follow the book’s route through generalized Klein, relative-entropy nonnegativity, variational trace formulas, operator Jensen, matrix perspectives, and joint convexity of relative entropy. Logarithm and trace-exponential monotonicity are included as reusable comparisons. The domain allows noncommuting positive-definite matrices without trace normalization.
Source: Tropp, January 2015 version, Chapter 8. Lean statements compile; proofs remain open.
Shared definitions: Chapter 3; submit that draft first.
Control the spectral norm of a matrix series with independent standard Gaussian or Rademacher coefficients. The goal is Theorem 4.1.1, including its variance identity, expected-norm estimate, and tail bound for rectangular complex matrices.
Milestones are the Gaussian and Rademacher matrix mgf/cgf estimates (Lemmas 4.6.2–3) and the Hermitian series bound (Theorem 4.6.1). The formulation keeps the source’s constants, both coefficient laws, and the zero-variance case. The shared Chapter 3 tools connect these transform estimates to concentration.
Source: Tropp, January 2015 version, Chapter 4. Lean statements compile; proofs remain open.
Shared definitions: Chapter 3; submit that draft first.
Replace ambient matrix dimension by intrinsic dimension, the ratio of trace to spectral norm. The goal is intrinsic Matrix Bernstein (Theorem 7.3.1). Intrinsic Matrix Chernoff (Theorem 7.2.1) is a second major target within the mission.
Supporting milestones include the generalized Laplace bound, intrinsic-dimension trace estimate, block-diagonal identities, Hermitian Bernstein, and the expected-norm corollary. The statements retain the source’s constants, threshold restrictions, and matrix-valued mean or variance bounds. Nonzero proxies keep intrinsic dimension well-defined; the expectation constant is universal.
Source: Tropp, January 2015 version, Chapter 7. Lean statements compile; proofs remain open.
Shared definitions: Chapter 3; submit that draft first.
Control the spectral norm of a sum of independent, centered, bounded rectangular random matrices. The goal is Matrix Bernstein (Theorem 6.1.1), including the variance identity and both expected-norm and tail estimates.
Milestones cover Hermitian dilation, variance additivity, the bounded-summand mgf/cgf estimate (Lemma 6.6.2), and Hermitian Bernstein (Theorem 6.6.1). Chapter 3 supplies the general Laplace-transform machinery. The formulation uses the Euclidean operator norm, preserves the one-sided eigenvalue assumption in the Hermitian result, and includes deterministic zero sums.
Source: Tropp, January 2015 version, Chapter 6. Lean statements compile; proofs remain open.
Shared definitions: Chapter 3; submit that draft first.
Bound the extreme eigenvalues of a sum of independent positive-semidefinite random matrices. The goal is the complete Matrix Chernoff theorem (Theorem 5.1.1): both expectation estimates, both tails, and the identities for the mean’s extreme eigenvalues.
The supporting milestone is the matrix mgf/cgf estimate (Lemma 5.4.1); Chapter 3 supplies the master bounds. The Lean statement retains the different lower- and upper-tail deviation ranges, permits zero mean eigenvalues, and handles a zero summand bound explicitly.
Source: Tropp, January 2015 version, Chapter 5. Lean statements compile; proofs remain open.
Shared definitions: Chapter 3; submit that draft first.
Develop the reusable matrix Laplace-transform method behind Tropp’s concentration inequalities. The goal is Theorem 3.6.1: upper and lower tail and expectation bounds for sums of independent Hermitian random matrices, expressed through their matrix cumulant-generating functions.
Milestones cover the eigenvalue tail and expectation bounds (Propositions 3.2.1–2), probabilistic Lieb inequality (Corollary 3.4.2), and trace-cgf subadditivity (Lemma 3.5.1). This mission also supplies the series’ shared spectral, probability, and dilation definitions. Lieb’s underlying concavity theorem is the Chapter 8 goal.
The Lean statements give bounds for each admissible transform parameter, with explicit integrability hypotheses; optimization recovers the source’s infimum/supremum forms.
Source: Tropp, January 2015 version, Chapter 3. Lean statements compile; proofs remain open.
How many Euclidean symmetries can a real plane algebraic curve of degree have? Rotational symmetry of a curve is classically detected from the monomials of its equation in the complex coordinate : a rotation of order about the origin can preserve the curve only if the differences of the nonzero monomials satisfy a congruence modulo (Lebmeir and Richter-Gebert, Section 4; Lebmeir, Theorem 5.4). Bounds on the number of symmetries in terms of the degree enter symmetry detection algorithms (Alcázar, Lávička and Vršek) and incidence geometry: Pach and de Zeeuw, Lemma 2.6 use a bound of on the number of isometries of a curve in a distinct-distances argument.
The note Sharp symmetry bounds for real algebraic curves (C. Perassi, 2026; PDF) determines the sharp bounds, classifies the curves attaining the rotation bound in degree , and describes their Möbius geometry. This mission is the complete Lean formalization of that note.
Let be irreducible in , of total degree , and let , identified with a subset of through . Assume that is infinite and is not a circle. Write for the group of Euclidean isometries of with , and for its orientation-preserving subgroup (the rotations and translations preserving ).
For an integer and a nonreal with , the extremal family is
a curve of degree . Its closure in the Riemann sphere is acted on by Möbius maps and by anti-Möbius maps, a Möbius map composed with complex conjugation. In the coordinates , the family has the equation , whose zero set has bidegree .
The goal asserts the bounds only; their sharpness and the equality case are milestones.
The result. The bounds and are attained in every degree, so they cannot be improved as functions of alone; for the curves attaining the rotation bound form one explicit family up to similarity, with a complete invariant. The bound sharpens the auxiliary estimate used by Pach and de Zeeuw (no improvement of their distance exponent is claimed), and the quintic of equation (2) contradicts the degree restriction stated in Lemma 9 of the arXiv version of Alcázar, Lávička and Vršek (the journal version has not been checked).
The formalization. Every statement of the note is proved in Lean 4 with Mathlib: 208 theorems and 12 definition files here, all proved, using only the axioms propext, Classical.choice and Quot.sound. It contains material that Mathlib does not have yet and that is reusable on its own: the genus of a function field over defined through its places and holomorphic differentials, and its invariance under isomorphism; the places of quadratic covers and Kummer covers , with uniformizers and local Kähler differentials; the classification of places of a Dedekind domain; the four-chart atlas of with its Zariski topology; and Möbius and anti-Möbius maps acting on the Riemann sphere. Theorem 1 is also registered with the Palomar registry as PALOMAR-2026-09-18-000007. The Lean code was written by AI agents under the author's direction; the Lean kernel checks it. The results have not been reviewed by an independent human, and neither the kernel checks nor the registration certify novelty.
The first argument is Bézout: the images of a point of under the rotations about a common center are distinct points on one circle, so there are at most of them. This gives for , not , and it says nothing about which curves are extremal. A second obstacle is that a symmetry of the zero set need only fix the polynomial up to sign, as equation (2) shows, so invariant-theoretic arguments that assume do not apply directly. For the Möbius statements the difficulty is that a Möbius map of the sphere does not act on the real equation; the curve must be compactified and its singular points identified. In the formalization, the genus comparison of Remark 5 needs a genus that does not depend on a chosen model, which Mathlib does not provide.
MvPolynomial (Fin 2) ℝ), and the curve is their real zero set as a subset of . Geometric irreducibility means irreducibility over .ℂ ≃ᵢ ℂ preserving that subset. Group orders use Nat.card, which is for an infinite set, so finiteness is part of the statements.OnePoint ℂ with the action of .A real number is normal in base when every block of base- digits occurs in its expansion with limiting frequency , as it would in a sequence of independent uniformly random digits. Borel introduced the notion in 1909 and proved that almost every real number is normal in every base, by an argument that produces no example. This mission collects the two classical papers that do produce examples: Champernowne's construction of and the theorem of Copeland and Erdős, which shows that the concatenation of any sufficiently dense increasing sequence of integers, the primes included, is normal.
Timeline.
A digit sequence is a function ; is the first digit after the point. A word is a finite list of naturals. For , the occurrence count is the number of positions with for every ; overlapping occurrences each count.
The sequence is normal in base (IsNormalSeq b s) if, for every word with all entries ,
The -th base- digit of a real after the point is , and is normal in base (IsNormalReal b x) if is normal in base . The integer part of plays no role; for a rational with two expansions the floor selects the one not ending in repeated 's.
If is an increasing sequence of positive integers such that, for every , the number of exceeds for all large , then the digit sequence obtained by writing the base- expansions of one after another is normal in base . A machine-checked proof is on the platform.
These are the standard examples of explicitly given normal numbers, and the Copeland–Erdős block argument is the model for most later constructions. The mission also fixes a definition of normality for real numbers together with the transfer from digit sequences to reals, which other work on normal numbers can import.
All declarations live in the namespace Normal and use the definition bundle Normal_Core: count, IsNormalSeq, digit, IsNormalReal; ofDigits b s ; the concatenation operators flatten, digitsBE, concatDigits; the Champernowne and Copeland–Erdős constants.
Conventions: digits are read after the point with the floor convention above; frequencies are limits of real quotients; words of every length with entries are quantified; results for real numbers are stated for bases by hypothesis.
The proofs are imported from the repository xiangyazi24/normal and verified by the platform. Their auxiliary lemmas are published on the platform as dependencies of the milestones and are not listed as items of this mission.
The open question whether is normal is a separate mission and is not approached by the methods here, which rely on the number being given as an explicit concatenation of blocks.
Multiplying matrices is a basic operation whose asymptotic cost is measured by the number of scalar arithmetic operations needed as the matrix dimensions increase. The familiar entry-by-entry algorithm has cubic cost. The question addressed here is how small an exponent can describe exact multiplication of square matrices when algorithms may use more elaborate finite computations. OpenAI's October 2, 2026 paper establishes the bound for matrices over the complex numbers. Its Theorem 1.1 concerns asymptotic arithmetic complexity, with arbitrarily small positive slack in the exponent.
An arithmetic program is a finite sequence of register computations. A step can load a field constant, read an input entry, or add, subtract, or multiply two values from preceding registers. Constant loads and input reads have zero cost. Each addition, subtraction, and multiplication has cost one. There is no division operation in this program model. Outputs are selected registers, and a program is correct only when these outputs equal the matrix product for every pair of input matrices.
For a field , a real number is an admissible exponent if, for every real , there exists a real constant such that every integer size admits a correct program with cost at most . The constant must work uniformly for all sizes and all input entries. The chosen program may depend on and . The definition does not charge for a separate procedure that constructs these programs. The arithmetic matrix multiplication exponent is the real infimum of the set of admissible exponents.
The goal is exactly the complex-field exponent conclusion of OpenAI's Theorem 1.1:
In the Lean source, the quantity on the left is OAI.MatrixMultiplication.Arithmetic.omega ℂ. The bound on the right is the exact real rational (9 : ℝ) / 4, equal to . The inequality is non-strict. The theorem does not assert a strict inequality below , and it is not quantified over arbitrary fields.
The paper also states the corresponding algorithmic conclusion with every positive exponent slack. The goal here retains the exact infimum formulation used by its released comparator challenge. In particular, the bound should not be read as asserting that one fixed family has cost without any slack, or that an algorithm is efficient at a specified finite matrix size.
The result places above the asymptotic arithmetic exponent in a model with explicitly defined programs, outputs, correctness, and operation counts. It gives a statement that other formal developments can use without leaving those conventions implicit. The dependence on the complex field is part of that statement, so results using another field or another computational model require their own justified connection.
This is a port and verification of an existing proof, not a claim that the source theorem remains unproved. The released Lean development contains the proof entry point. Keeping the original definitions and conclusion allows compatibility changes to be reviewed independently of the mathematical claim.
An asymptotic exponent bound requires one uniform cost constant for every positive matrix size, while correctness quantifies over all pairs of matrices at each size. A computation for selected dimensions or selected inputs cannot satisfy those requirements. Arguments about tensors must also support the stated arithmetic program cost, including the operations needed for the relevant linear combinations. The infimum formulation makes its defining set and the interpretation of its bounds part of the supporting mathematics, rather than assumptions to insert into the target theorem.
The environment is Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Matrices are functions on finite index sets. Program evaluation and output selection give exact field values. The main theorem fixes the field to , excludes size zero from admissibility, and uses real powers for its cost estimates. Constants may be arbitrary complex numbers; no bit-cost interpretation is asserted.
The definition item preserves the original source block, including its rectangular matrix multiplication definitions and complex dual exponent. Those additional definitions support the shared source development but are not additional mission goals. A complete proof must establish the displayed bound without an admitted lemma, a new axiom, or an assumption equivalent to that bound. Reusable components include the arithmetic program model, finite tensor constructions, asymptotic bounds, and the bridge from tensor rank to arithmetic operations.
This entry records a completed elementary result in the campaign on odd numbers as sums of primes: every odd natural number greater than 1 is a sum of at most 4401 primes. It illustrates how an additive density estimate can reduce the number of prime summands in a Schnirelmann argument.
For every natural number , if is odd and , there is a multiset of primes with and . Repeated primes are allowed. The bound applies to every such , not only sufficiently large integers.
The goal references the existing proved 4401 theorem. Its statement is the campaign template instantiated with 4401.
The two supporting references are the density bound and Mann's theorem, both already proved.
Let and . The density estimate gives . Mann's theorem gives , so yields density at least . The sumset cover argument then produces 4400 odd prime summands, with one additional 3 to obtain the required parity. Explicit sums of 2s and 3s handle the remaining small and medium ranges. These steps are included in the accepted goal proof; they are not unfinished milestones.
All three referenced theorems have ACCEPTED proof submissions under the account moona3k, are marked Proved, and use Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. No new Lean statement or duplicate theorem is introduced by this proposal.
The density theorem's published source credits an extraction from the accepted 6101 proof. Mann's theorem is the classical additive density theorem of H. B. Mann; the accepted formalization follows the Dyson transform presentation cited in its theorem record. This entry assembles those existing results into the 4401 bound.
The 4401 bound was an intermediate improvement on 6101. It is not the current campaign frontier: the campaign now includes a proved bound of 27. This proposal preserves the earlier result and its proof route without claiming a new literature result or a new record.