Lean 4로 작성된 형식 검증된 수리 금융 라이브러리

초록

우리는 Lean 4 증명 보조기 위에 Mathlib와 BrownianMotion 패키지를 기반으로 구축된 수리 금융 라이브러리를 설명한다. 이 라이브러리는 광범위하다: 연속시간 확률미적분학의 측도론적 기초부터 파생상품 가격결정, 응용 위험, 포트폴리오 및 고정수익 이론에 이르기까지 열한 개 영역에 걸쳐 200개 이상의 'sorry'가 없는 정리를 포함하며, 우리가 아는 한 지금까지 가장 포괄적인 기계 검증된 수리 금융 개발이다. 광범위함은 배경일 뿐, 핵심이 아니다. 두 가지 점이 이 라이브러리를 단순한 목록 이상으로 만든다. 첫째, 연속 이론 깊숙이 들어가 L2 이토 적분을 유계 선형 등거리사상으로 구성하고, 위험중립 가격측도를 가정하는 대신 유도한다. 둘째, 자신의 충실성을 감사한다: 모든 결과는 그 Lean 명제가 주장하는 수학과 어떤 관계에 있는지에 따라 분류되며, 빌드로 강제된 게이트가 각 증명이 실제로 사용하는 공리를 고정하므로, 독자는 정확히 무엇이 증명되었고 무엇이 추가 가설 하에서만 증명되었는지를 명확히 볼 수 있다. 우리는 솔직한 소견으로 마무리한다: 고전적 수리 금융 위의 형식적 기초는 새로운 금융 이론보다는 알려진 결과들의 인증된 통일을 제공한다. 따라서 기여는 방법론적이고 인프라적이며, 충실성 감사와 함께 수리 금융을 위한 재사용 가능한 검증된 기초를 제공한다.

English

We describe a library of mathematical finance built in the Lean 4 proof assistant, on top of Mathlib and the BrownianMotion package. It is broad: more than two hundred sorry-free theorems across eleven areas, from the measure-theoretic foundations of continuous-time stochastic calculus through derivative pricing to applied risk, portfolio, and fixed-income theory, and, to our knowledge, the most comprehensive machine-checked development of mathematical finance to date. Breadth is the setting, not the point. Two things make it more than a catalogue. It reaches into the continuous theory far enough to construct the L2 Itô integral as a bounded linear isometry and to derive, rather than assume, the risk-neutral pricing measure. And it audits its own faithfulness: every result is classified by how its Lean statement relates to the mathematics it claims, and a build-enforced gate pins the axioms each proof actually uses, so a reader can see precisely what has been proved and what has only been proved under added hypotheses. We close with a candid finding: a formal base over classical financial mathematics yields certified unification of known results rather than new financial theory. The contribution is therefore methodological and infrastructural, reusable verified foundations for mathematical finance, together with the faithfulness audit.