IDEAS home Printed from https://ideas.repec.org/p/arx/papers/2606.01356.html

A Formally Verified Library of Mathematical Finance in Lean 4

Author

Listed:
  • Raphael Coelho

Abstract

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 three 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. To our knowledge it is the most comprehensive machine-checked development of mathematical finance to date. Two things make it more than a catalogue. It reaches into the continuous theory far enough to construct the $L^2$ It\^o 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 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 above), not a new financial result.

Suggested Citation

  • Raphael Coelho, 2026. "A Formally Verified Library of Mathematical Finance in Lean 4," Papers 2606.01356, arXiv.org, revised Jul 2026.
    • Handle: RePEc:arx:papers:2606.01356
    as

    Download full text from publisher

    File URL: https://arxiv.org/pdf/2606.01356
    File Function: Latest version
    Download Restriction: no
    ---><---

    References listed on IDEAS

    as
    1. Harrison, J. Michael & Kreps, David M., 1979. "Martingales and arbitrage in multiperiod securities markets," Journal of Economic Theory, Elsevier, vol. 20(3), pages 381-408, June.
    2. Margrabe, William, 1978. "The Value of an Option to Exchange One Asset for Another," Journal of Finance, American Finance Association, vol. 33(1), pages 177-186, March.
    3. Cox, John C. & Ross, Stephen A. & Rubinstein, Mark, 1979. "Option pricing: A simplified approach," Journal of Financial Economics, Elsevier, vol. 7(3), pages 229-263, September.
    4. Black, Fischer & Scholes, Myron S, 1973. "The Pricing of Options and Corporate Liabilities," Journal of Political Economy, University of Chicago Press, vol. 81(3), pages 637-654, May-June.
    Full references (including those not matched with items on IDEAS)

    Citations

    Citations are extracted by the CitEc Project, subscribe to its RSS feed for this item.
    as


    Cited by:

    1. Raphael Coelho, 2026. "The Fundamental Theorem of Asset Pricing, Formalized in Lean 4," Papers 2606.28990, arXiv.org.

    Most related items

    These are the items that most often cite the same works as this one and are cited by the same works as this one.
    1. Bjork, Tomas, 2009. "Arbitrage Theory in Continuous Time," OUP Catalogue, Oxford University Press, edition 3, number 9780199574742.
    2. Lim, Terence & Lo, Andrew W. & Merton, Robert C. & Scholes, Myron S., 2006. "The Derivatives Sourcebook," Foundations and Trends(R) in Finance, now publishers, vol. 1(5–6), pages 365-572, April.
    3. Suresh M. Sundaresan, 2000. "Continuous‐Time Methods in Finance: A Review and an Assessment," Journal of Finance, American Finance Association, vol. 55(4), pages 1569-1622, August.
    4. Nordahl, Helge A., 2008. "Valuation of life insurance surrender and exchange options," Insurance: Mathematics and Economics, Elsevier, vol. 42(3), pages 909-919, June.
    5. Scholes, Myron S, 1998. "Derivatives in a Dynamic Environment," American Economic Review, American Economic Association, vol. 88(3), pages 350-370, June.
    6. Mondher Bellalah, 2009. "Derivatives, Risk Management & Value," World Scientific Books, World Scientific Publishing Co. Pte. Ltd., number 7175.
    7. Campbell, Rachel A. & Kräussl, Roman, 2006. "Does patience pay? Empirical testing of the option to delay accepting a tender offer in the US banking sector," CFS Working Paper Series 2006/32, Center for Financial Studies (CFS).
    8. Carl Chiarella & Xue-Zhong He & Christina Sklibosios Nikitopoulos, 2015. "Derivative Security Pricing," Dynamic Modeling and Econometrics in Economics and Finance, Springer, edition 127, number 978-3-662-45906-5, June.
    9. Munk, Claus, 2015. "Financial Asset Pricing Theory," OUP Catalogue, Oxford University Press, number 9780198716457.
    10. Sanjay K. Nawalkha & Xiaoyang Zhuo, 2022. "A Theory of Equivalent Expectation Measures for Contingent Claim Returns," Journal of Finance, American Finance Association, vol. 77(5), pages 2853-2906, October.
    11. Philipp N. Baecker, 2007. "Real Options and Intellectual Property," Lecture Notes in Economics and Mathematical Systems, Springer, number 978-3-540-48264-2, December.
    12. Mark Broadie & Jerome B. Detemple, 2004. "ANNIVERSARY ARTICLE: Option Pricing: Valuation Models and Applications," Management Science, INFORMS, vol. 50(9), pages 1145-1177, September.
    13. Jun Yu & Michael J. Tomas, 2023. "An Alternative Method for Analytical Solutions of Two‐Dimensional Black‐Scholes‐Merton Equation," Journal of Applied Mathematics, John Wiley & Sons, vol. 2023(1).
    14. Ammann, Manuel & Kind, Axel & Wilde, Christian, 2003. "Are convertible bonds underpriced? An analysis of the French market," Journal of Banking & Finance, Elsevier, vol. 27(4), pages 635-653, April.
    15. Grosen, Anders & Lochte Jorgensen, Peter, 2000. "Fair valuation of life insurance liabilities: The impact of interest rate guarantees, surrender options, and bonus policies," Insurance: Mathematics and Economics, Elsevier, vol. 26(1), pages 37-57, February.
    16. Timothy Johnson, 2015. "Reciprocity as a Foundation of Financial Economics," Journal of Business Ethics, Springer, vol. 131(1), pages 43-67, September.
    17. Jamshidian, Farshid, 2008. "Numeraire Invariance and application to Option Pricing and Hedging," MPRA Paper 7167, University Library of Munich, Germany.
    18. Davide Lauria & W. Brent Lindquist & Svetlozar T. Rachev & Yuan Hu, 2025. "Bridging Asset Pricing and Market Microstructure: Option Valuation in Roll’s Framework," JRFM, MDPI, vol. 18(5), pages 1-43, April.
    19. Anthony Neuberger, 2023. "The Black–Scholes paper: a personal perspective," Decisions in Economics and Finance, Springer;Associazione per la Matematica, vol. 46(2), pages 713-730, December.
    20. Maria-Teresa Bosch-Badia & Joan Montllor-Serrats & Maria-Antonia Tarrazon-Rodon, 2015. "Corporate Social Responsibility: A Real Options Approach to the Challenge of Financial Sustainability," PLOS ONE, Public Library of Science, vol. 10(5), pages 1-37, May.

    More about this item

    Statistics

    Access and download statistics

    Corrections

    All material on this site has been provided by the respective publishers and authors. You can help correct errors and omissions. When requesting a correction, please mention this item's handle: RePEc:arx:papers:2606.01356. See general information about how to correct material in RePEc.

    If you have authored this item and are not yet registered with RePEc, we encourage you to do it here. This allows to link your profile to this item. It also allows you to accept potential citations to this item that we are uncertain about.

    If CitEc recognized a bibliographic reference but did not link an item in RePEc to it, you can help with this form .

    If you know of missing items citing this one, you can help us creating those links by adding the relevant references in the same way as above, for each refering item. If you are a registered author of this item, you may also want to check the "citations" tab in your RePEc Author Service profile, as there may be some citations waiting for confirmation.

    For technical questions regarding this item, or to correct its authors, title, abstract, bibliographic or download information, contact: arXiv administrators (email available below). General contact details of provider: https://arxiv.org/ .

    Please note that corrections may take a couple of weeks to filter through the various RePEc services.

    IDEAS is a RePEc service. RePEc uses bibliographic data supplied by the respective publishers.