A Formally Verified Library of Mathematical Finance in Lean 4 | Raphael Coelho | ResearchPod