Hugging Face Daily Papers · June 2, 2026 · 6 min read

A Formally Verified Library of Mathematical Finance in Lean 4

Mirrored from Hugging Face Daily Papers for archival readability. Support the source by reading on the original site.

Like Read original ↗

A Lean 4 library of formal mathematical-finance theorems, built on Mathlib and Degenne' BrownianMotion.\n","updatedAt":"2026-06-02T11:01:19.324Z","author":{"_id":"66f6d54078e0f4f61e463622","avatarUrl":"/avatars/5db4c794134d13d83d2881bf291ea1ff.svg","fullname":"Raphael Coelho","name":"raphaelrrcoelho","type":"user","isPro":false,"isHf":false,"isHfAdmin":false,"isMod":false,"isUserFollowing":false}},"numEdits":0,"identifiedLanguage":{"language":"en","probability":0.8136456608772278},"editors":["raphaelrrcoelho"],"editorAvatarUrls":["/avatars/5db4c794134d13d83d2881bf291ea1ff.svg"],"reactions":[],"isReport":false}},{"id":"6a1ec839faffc43213978c56","author":{"_id":"6960eca92f7ad9b043b5cbe0","avatarUrl":"/avatars/e68dcc7fd04f143d849d40414866e633.svg","fullname":"Noah","name":"noahml","type":"user","isPro":false,"isHf":false,"isHfAdmin":false,"isMod":false,"isUserFollowing":false},"createdAt":"2026-06-02T12:10:33.000Z","type":"comment","data":{"edited":false,"hidden":false,"latest":{"raw":"Made an audio walkthrough of this paper for anyone who wants to skim it on the go:\nhttps://researchpod.app/episode/cb0502c2-9225-4428-948d-081e909e200b\n\nGenerated automatically by ResearchPod — happy to take feedback from the authors.","html":"Made an audio walkthrough of this paper for anyone who wants to skim it on the go: <a href=\"https://researchpod.app/episode/cb0502c2-9225-4428-948d-081e909e200b\" rel=\"nofollow\">https://researchpod.app/episode/cb0502c2-9225-4428-948d-081e909e200b</a>\nGenerated automatically by ResearchPod — happy to take feedback from the authors.\n","updatedAt":"2026-06-02T12:10:33.767Z","author":{"_id":"6960eca92f7ad9b043b5cbe0","avatarUrl":"/avatars/e68dcc7fd04f143d849d40414866e633.svg","fullname":"Noah","name":"noahml","type":"user","isPro":false,"isHf":false,"isHfAdmin":false,"isMod":false,"isUserFollowing":false}},"numEdits":0,"identifiedLanguage":{"language":"en","probability":0.8471313714981079},"editors":["noahml"],"editorAvatarUrls":["/avatars/e68dcc7fd04f143d849d40414866e633.svg"],"reactions":[],"isReport":false}},{"id":"6a1f8ab35b70251eb1fd7026","author":{"_id":"63d3e0e8ff1384ce6c5dd17d","avatarUrl":"https://cdn-avatars.huggingface.co/v1/production/uploads/1674830754237-63d3e0e8ff1384ce6c5dd17d.jpeg","fullname":"Librarian Bot (Bot)","name":"librarian-bot","type":"user","isPro":false,"isHf":false,"isHfAdmin":false,"isMod":false,"followerCount":360,"isUserFollowing":false},"createdAt":"2026-06-03T02:00:19.000Z","type":"comment","data":{"edited":false,"hidden":false,"latest":{"raw":"This is an automated message from the [Librarian Bot](https://huggingface.co/librarian-bots). I found the following papers similar to this paper. \n\nThe following papers were recommended by the Semantic Scholar API \n\n* [An Explicit Solution to Black-Scholes Implied Volatility](https://huggingface.co/papers/2604.24480) (2026)\n* [From Swap Axioms to Weighted Geometric Means: A Characterization of AMMs](https://huggingface.co/papers/2604.16898) (2026)\n* [Analytic approximation for Bachelier option prices and applications](https://huggingface.co/papers/2605.02040) (2026)\n* [Risk-Controlled Lean-as-Judge for Natural-Language Mathematical Reasoning](https://huggingface.co/papers/2605.28365) (2026)\n* [Non-unique time and market incompleteness](https://huggingface.co/papers/2604.23608) (2026)\n* [Option Pricing under Stochastic Volatility and Jumps:A PIDE Framework with Empirical Evidence](https://huggingface.co/papers/2605.30562) (2026)\n* [Against a Universal Trading Strategy: No-Arbitrage, No-Free-Lunch, and Adversarial Cantor Diagonalization](https://huggingface.co/papers/2604.13334) (2026)\n\n\n Please give a thumbs up to this comment if you found it helpful!\n\n If you want recommendations for any Paper on Hugging Face checkout [this](https://huggingface.co/spaces/librarian-bots/recommend_similar_papers) Space\n\n You can directly ask Librarian Bot for paper recommendations by tagging it in a comment: `@librarian-bot recommend`","html":"This is an automated message from the <a href=\"https://huggingface.co/librarian-bots\">Librarian Bot</a>. I found the following papers similar to this paper. \nThe following papers were recommended by the Semantic Scholar API \n<ul>\n<li><a href=\"https://huggingface.co/papers/2604.24480\">An Explicit Solution to Black-Scholes Implied Volatility</a> (2026)</li>\n<li><a href=\"https://huggingface.co/papers/2604.16898\">From Swap Axioms to Weighted Geometric Means: A Characterization of AMMs</a> (2026)</li>\n<li><a href=\"https://huggingface.co/papers/2605.02040\">Analytic approximation for Bachelier option prices and applications</a> (2026)</li>\n<li><a href=\"https://huggingface.co/papers/2605.28365\">Risk-Controlled Lean-as-Judge for Natural-Language Mathematical Reasoning</a> (2026)</li>\n<li><a href=\"https://huggingface.co/papers/2604.23608\">Non-unique time and market incompleteness</a> (2026)</li>\n<li><a href=\"https://huggingface.co/papers/2605.30562\">Option Pricing under Stochastic Volatility and Jumps:A PIDE Framework with Empirical Evidence</a> (2026)</li>\n<li><a href=\"https://huggingface.co/papers/2604.13334\">Against a Universal Trading Strategy: No-Arbitrage, No-Free-Lunch, and Adversarial Cantor Diagonalization</a> (2026)</li>\n</ul>\n Please give a thumbs up to this comment if you found it helpful!\n If you want recommendations for any Paper on Hugging Face checkout <a href=\"https://huggingface.co/spaces/librarian-bots/recommend_similar_papers\">this</a> Space\n You can directly ask Librarian Bot for paper recommendations by tagging it in a comment: <code><a href=\"/librarian-bot\">@librarian-bot</a> recommend</code>\n","updatedAt":"2026-06-03T02:00:19.202Z","author":{"_id":"63d3e0e8ff1384ce6c5dd17d","avatarUrl":"https://cdn-avatars.huggingface.co/v1/production/uploads/1674830754237-63d3e0e8ff1384ce6c5dd17d.jpeg","fullname":"Librarian Bot (Bot)","name":"librarian-bot","type":"user","isPro":false,"isHf":false,"isHfAdmin":false,"isMod":false,"followerCount":360,"isUserFollowing":false}},"numEdits":0,"identifiedLanguage":{"language":"en","probability":0.7521100640296936},"editors":["librarian-bot"],"editorAvatarUrls":["https://cdn-avatars.huggingface.co/v1/production/uploads/1674830754237-63d3e0e8ff1384ce6c5dd17d.jpeg"],"reactions":[],"isReport":false}}],"primaryEmailConfirmed":false,"paper":{"id":"2606.01356","authors":[{"_id":"6a1eb7bc808ddbc3c7d44032","user":{"_id":"66f6d54078e0f4f61e463622","avatarUrl":"/avatars/5db4c794134d13d83d2881bf291ea1ff.svg","isPro":false,"fullname":"Raphael Coelho","user":"raphaelrrcoelho","type":"user","name":"raphaelrrcoelho"},"name":"Raphael Coelho","status":"claimed_verified","statusLastChangedAt":"2026-06-02T12:03:29.052Z","hidden":false}],"publishedAt":"2026-05-31T00:00:00.000Z","submittedOnDailyAt":"2026-06-02T00:00:00.000Z","title":"A Formally Verified Library of Mathematical Finance in Lean 4","submittedOnDailyBy":{"_id":"66f6d54078e0f4f61e463622","avatarUrl":"/avatars/5db4c794134d13d83d2881bf291ea1ff.svg","isPro":false,"fullname":"Raphael Coelho","user":"raphaelrrcoelho","type":"user","name":"raphaelrrcoelho"},"summary":"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.","upvotes":1,"discussionId":"6a1eb7bc808ddbc3c7d44033","githubRepo":"https://github.com/raphaelrrcoelho/formal-mathfin","githubRepoAddedBy":"user","githubStars":2},"canReadDatabase":false,"canManagePapers":false,"canSubmit":false,"hasHfLevelAccess":false,"upvoted":false,"upvoters":[{"_id":"69bf60b85c598717b3b2261e","avatarUrl":"https://cdn-avatars.huggingface.co/v1/production/uploads/noauth/ZR5H3VKQ2VRcoWa-6CgUu.png","isPro":false,"fullname":"Михайлов Валентина","user":"carteryoung62","type":"user"}],"acceptLanguages":["en"],"dailyPaperRank":0,"markdownContentUrl":"https://huggingface.co/buckets/huggingchat/papers-content/resolve/2606/2606.01356.md"}">

Papers

arxiv:2606.01356

A Formally Verified Library of Mathematical Finance in Lean 4

Published on May 31

· Submitted by

Raphael Coelho on Jun 2

Upvote

Authors:

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 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.

View arXiv page View PDF GitHub 2 Add to collection