After Jake Fennick’s MA project in the proof assistant Isabelle in 2019, I have advised two Master’s students whose project focused on another popular proof assistant, Lean:

• Hugh Chou, 2021: Formalizing my paper on a conflict in the Carmo and Jones approach to contrary-to-duty deontic obligations.
• Ryan T. Sasaki, 2022: Formalizing a time-invariance theorem for Redington immunization in financial mathematics.