First machine-checked formalization of the FTAP in Lean 4 across three settings, with explicit EMM construction via minimization of E[log(1+e<θ,Y>)] in the d-asset case.
The Lean mathematical library
1 Pith paper cite this work. Polarity classification is still indexing.
1
Pith paper citing it
fields
q-fin.MF 1years
2026 1verdicts
ACCEPT 1representative citing papers
citing papers explorer
-
The Fundamental Theorem of Asset Pricing, Formalized in Lean 4
First machine-checked formalization of the FTAP in Lean 4 across three settings, with explicit EMM construction via minimization of E[log(1+e<θ,Y>)] in the d-asset case.