Actuarial Mathematics Formalizing Actuarial Mathematics in Isabelle/HOL is now proceeding: https://www.isa-afp.org/entries/Actuarial_Mathematics.html Documents The related presentation slides are stored in the "slide" directory.