Lean 4 中形式驗證的數學金融庫

研究論文提出一個在 Lean 4 證明助手中構建的數學金融圖書庫，基於 Mathlib 和 BrownianMotion 套件。該庫廣泛覆蓋十一個領域，擁有超過兩百個無 sorry 的定理，從連續時間隨機微積分的測度論基礎到衍生品定價，再到應用風險、投資組合和固定收益理論。論文強調，它不僅是目錄，還深入連續理論，構建 L2 伊藤積分並推導風險中性定價度量。此外，它審計自身的忠實性：每個結果都根據其 Lean 陳述與數學的關聯進行分類，並且構建強制閘門固定了證明實際使用的公理，讓讀者能精確看到證明了什麼以及僅在假設下證明了什麼。論文最後坦率指出，以經典金融數學為基礎的形式化基礎，產生的是已知結果的認證統一，而非新的金融理論。因此，貢獻在於方法論和基礎設施，為數學金融提供可重用的驗證基礎，並附帶忠實性審計。