Bibliography

1

Tudor Achim, Alex Best, Alberto Bietti, Kevin Der, Mathïs Fédérico, Sergei Gukov, Daniel Halpern-Leistner, Kirsten Henningsgard, Yury Kudryashov, Alexander Meiburg, Martin Michelsen, Riley Patterson, Eric Rodriguez, Laura Scharff, Vikram Shanker, Vladmir Sicca, Hari Sowrirajan, Aidan Swope, Matyas Tamas, Vlad Tenev, Jonathan Thomm, Harold Williams, and Lawrence Wu. Aristotle: IMO-level Automated Theorem Proving, 2025. URL: https://arxiv.org/abs/2510.01346, arXiv:2510.01346.

2

Wai-Sum Chan and Yiu-Kuen Tse. Financial Mathematics for Actuaries. World Scientific Publishing Company, New Jersey / London / Singapore, 3 edition, 2021.

3

Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction – CADE 28, pages 625–635, Cham, 2021. Springer International Publishing. URL: https://link.springer.com/chapter/10.1007/978-3-030-79876-5_37, doi:10.1007/978-3-030-79876-5_37.

4

Rémy Degenne, David Ledvinka, Etienne Marion, and Peter Pfaffelhuber. Formalization of Brownian motion in Lean, 2025. URL: https://arxiv.org/abs/2511.20118, arXiv:2511.20118.

5

Gabriel Hawawini. The Mathematics of Macaulay’s Duration. In Bond Duration and Immunization, pages 47–55. Routledge, 2017. First published 1982.

6

Gabriel A. Hawawini. On the Mathematics of Macaulay’s Duration: A Note. Working Paper 82/03, INSEAD, Fontainebleau, France, 1982. URL: https://flora.insead.edu/fichiersti_wp/inseadwp1982/82-03.pdf.

7

Jacques Janssen, Raimondo Manca, and Ernesto Volpe di Prignano. Mathematical finance. ISTE, London; John Wiley & Sons, Inc., Hoboken, NJ, 2009. Deterministic and stochastic models. URL: https://doi-org.eres.library.manoa.hawaii.edu/10.1002/9780470611692, doi:10.1002/9780470611692.

8

Bjørn Kjos-Hanssen. Interest: a Lean library for financial mathematics, 2026. Project website. URL: https://bjoernkjoshanssen.github.io/interest/.

9

Frederick R. Macaulay. Some Theoretical Problems Suggested by the Movements of Interest Rates, Bond Yields and Stock Prices in the United States since 1856. Number 24 in Publications of the National Bureau of Economic Research. National Bureau of Economic Research, New York, 1938.

10

Diego Marmsoler and Achim D. Brucker. Isabelle/Solidity: A deep embedding of Solidity in Isabelle/HOL. Form. Asp. Comput., 37(2), March 2025. doi:10.1145/3700601.

11

Carl Julius Norstrøm. A sufficient condition for a unique nonnegative internal rate of return. Journal of Financial and Quantitative Analysis, 7(3):1835–1845, 1972.

12

Alejandro Radisic. LeanCert: Verified numerical computation in Lean, 2026. Project website. URL: https://docs.leancert.io/.

13

Texas Instruments Incorporated. TI Business Analyst — Preprogrammed Financial and Statistical Capability. Product leaflet, 1977. Leaflet no. CL-207A. URL: http://www.datamath.org/Leaflets.htm#CL-207A.