연구팀이 Lean 4 증명 보조 도구를 사용하여 수학 금융 라이브러리를 개발했어요. 이 라이브러리는 11개 분야에 걸쳐 200개 이상의 오류 없는 정리를 포함하며, 현재까지 가장 포괄적인 기계 검증 개발이라고 해요. 위험 관리, 포트폴리오, 채권 이론 등 다양한 분야를 다루며, 기존 결과의 통일성을 인증하는 데 기여했어요.
L2 이토 적분과 위험 중립 가격 측정법을 직접 유도하는 등 연속 이론에 깊이 관여하며, 각 증명의 Lean 문장이 주장하는 수학과의 관계를 분류하여 신뢰성을 감사해요. 또한, 증명에 사용된 공리를 명시하여 독자가 정확히 무엇이 증명되었는지 확인할 수 있도록 설계됐어요.