Prof. Kjos-Hanssen advised a Master’s student whose project focused on the popular proof assistant, Lean: Ryan Thomas Sasaki, 2022: Formalizing a time-invariance theorem for Redington immunization in financial mathematics.