The Coq mailing list

[伊藤洋介 <glacier345 AT gmail.com>]

Dear Coq users,

My name is Yosuke Ito, working as an actuary at a life insurance company in Japan.

Now I am pleased to announce that I have formalized the basic part of

actuarial mathematics using Coq.

https://github.com/Yosuke-Ito-345/Actuary

This package offers some basic actuarial notations and well-known formulas of

annuities, life tables, premiums and reserves of life insurance.

The proofs are based on the Coq standard library, MathComp and Coquelicot.

The main result at this stage is that the prospective reserve and the retrospective reserve of

an endowment life insurance coincide:

Examples.v

Theorem res_eq_pros_retro : forall (t x n : nat), x+t < ω -> t <= n -> n > 0 ->
  \V_{t & x:n} = \P_{x:n} * \s''_{x:t} - \A_{x`1:t} / \A_{x:t`1}.

This package is still at an early stage, so there is plenty of room for further development.

Notice that future updates may not be backward compatible.

Since I am new to Coq, any comment or advice is appreciated.

Best regards,

--

伊藤洋介

Yosuke Ito

https://github.com/Yosuke-Ito-345

glacier345 AT gmail.com