Abstract
Actuarial Mathematics is a theory in applied mathematics.This is mainly used for determining the prices of insurance products and evaluating the liability of a company associating with insurance contracts.It is related to calculus, probability theory and financial theory, etc.
In this entry, I formalize the very basic part of Actuarial Mathematics in Isabelle/HOL.It includes the theory of interest, survival model, and life table.The theory of interest deals with interest rates, present value factors, an annuity certain, etc.The survival model is a probabilistic model that represents the human mortality.The life table is based on the survival model and used for practical calculations.
I have already formalized the basic part of Actuarial Mathematics in Coq (https://github.com/Yosuke-Ito-345/Actuary) in a purely axiomatic manner.In contrast, Isabelle formalization is based on the probability theory and the survival model is developed as generally as possible.Such rigorous and general formulation seems very rare; at least I cannot find any similar documentation on the web.
This formalization in Isabelle is still at an early stage, and I cannot guarantee the backward compatibility in the future development.
If you heavily depend on this entry, please let me know.
(Updated April 7th, 2024.)
License
History
- April 7, 2024
- Added some lemmas with fractional age assumptions in the theory Life_Table. Modified the existing theories; contact the author for incompatible changes.
- July 8, 2023
- Added the theories Survival_Model, Life_Table and Examples. Updated the theories Preliminaries and Interest.
- January 23, 2022
- Submitted the theories Preliminaries and Interest.