Actuarial Mathematics

 

Title: Actuarial Mathematics
Author: Yosuke Ito (glacier345 /at/ gmail /dot/ com)
Submission date: 2022-01-23
Abstract: Actuarial Mathematics is a theory in applied mathematics, which 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. The first formalization is about the theory of interest which deals with interest rates, present value factors, an annuity certain, etc. I have already formalized the basic part of Actuarial Mathematics in Coq (https://github.com/Yosuke-Ito-345/Actuary). This entry is currently the partial translation and a little generalization of the Coq formalization. The further translation in Isabelle/HOL is now proceeding.
BibTeX:
@article{Actuarial_Mathematics-AFP,
  author  = {Yosuke Ito},
  title   = {Actuarial Mathematics},
  journal = {Archive of Formal Proofs},
  month   = jan,
  year    = 2022,
  note    = {\url{https://isa-afp.org/entries/Actuarial_Mathematics.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.