0.1 Introduction

In this article we report on a project to formalize interest theory in the proof assistant Lean [ 3 ] in a library, Interest [ 8 ] .

Presently it includes results on the existence of a unique solution for any of these given the others: the present value of an annuity PV; future value FV; periodic payment PMT (equivalently, coupon rate \(r\) for a bond); prevailing interest rate I/Y (yield); Macaulay duration \(D\); maturity date \(n\).

In order to deduce the maturity date and the yield rate from the Macaulay duration we made use of Aristotle [ 1 ] by Harmonic, which saved a lot of time.

The mathematical theory of interest, often known simply as financial mathematics within actuarial science, is important in the real world and is due for a formal treatment.

We focus on the pricing of bonds and annuities in settings in which financial calculators are used by actuaries.

Calculators such as the BA II Plus Professional are used by actuaries to make critical decisions. Consequently, formal verification of the underlying mathematics is important.

The Annuity Equation is a staple of actuarial science and financial mathematics, relating a payment [PMT], present value [PV], future value [FV], interest rate [I/Y], and number of periods [N]. The BA II Plus Professional calculator allows a solution for any one of these five variables given the others, using keystrokes such as [CPT] [PMT]. In the first half of the project we verify the unique solvability of the Annuity Equation for each variable under a non-par bond assumption. In the second half, we replace the annuity equation by an equation defining the Macaulay duration in terms of maturity, yield rate, and coupon rate for a bond, and obtain similar results. In this half we make use of Harmonic’s tool Aristotle.

0.2 The annuity equation

The Annuity Equation ?? is often left implicit in textbooks on financial mathematics such as [ 2 ] . (We write interest per year, I/Y, as IY since it is a single variable.)

Nevertheless, it should be considered well known. In our formalization, we assume that PV has the opposite sign of the common sign of PMT and FV. This avoids uniqueness issues stemming from Descartes’ Rule of Signs, as in Norstrøm’s Criterion [ 11 ] .

The form ?? gives the impression that division \(x \mapsto x^{-1}\) is necessary, but the equation can also be stated in a future value perspective that makes sense over a ring if we define the interest rate by \(i=\IY /100\).

In terms of the discount factor \(v=1/(1+i)\), another form is

In terms of \(x=v^{-n/2}{\gt}0\), this becomes

Solving for \(x\), we obtain

This inequality is (unsurprisingly) also encountered in our Lean code.

The Annuity Equation has apparently been implemented in financial calculators since their introduction half a century ago (June 13, 1976 for the original Texas Instruments Business Analyst [ 13 ] ). Here we formalize the fact one can solve for any of these five variables given the other four. This is rather explicit for PV, FV, PMT, and N, but requires Newton’s method for I/Y (interest per year). However, our proof is mathematical and does not concern itself with computability. It instead sticks to mathematical existence and uniqueness.

0.2.1 Some sample results from the project

The following results should be cross-referenced with the dependency graph at [ 8 ] and may be skipped if the reader is not simultaneously studying that graph and the associated documentation pages.

0.3 Macaulay duration

Whether maturity of a bond can be recovered from the Macaulay duration [ 9 ] depends on whether the coupon rate \(r\) is less than the yield rate \(i\). See Table 1. The fact that there can be two solutions when \(r{\lt}i\) and \(1+1/i{\lt}d\) is illustrated in [ 2 , Figure 8.3 on page 251 ] , where the situation is described as a “deep discount” bond. It was first discovered by Hawawini [ 6 , 5 ] .

Aristotle [ 1 ] provided a single proof that \(D{\lt}1+1/i\) suffices, without doing a case split on whether \(r{\lt}i\).

0.4 Solving exercises with Aristotle and LeanCert

Actuarial exam questions are used to qualify students for actuarial careers. As such, the correctness of their solution affects actuaries directly. We demonstrate that LeanCert [ 12 ] , a new tool for verified interval arithmetic in Lean, can be used to formally verified such solutions. Since solutions may also involve tedious computations, we also make use of Aristotle. Our test case is [ 2 , Exercise 1.36 ] , which reads as follows:

Assume that \(\delta (t)=\frac1{10(1+t)^3}\) and \(A(0)=100\). Find the amount of interest earned in the fifth year.

The correct solution is \((e^{7/144}-e^{6/125})\cdot 100\) which in the solution at the end of the book [ 2 , Appendix B ] is given simply as 0.064.

To verify this we prove the following lemma:

Here \(a\) is the accumulation function, \(A\) is the accumulated amount function, and \(I\) is the earned interest function as introduced in [ 2 ] . We evaluate the associated integrals by hand, then use Aristotle to formally verified the solutions, and finally use LeanCert to obtain the bounds \((0.064, 0.065)\). This proof of concept opens the door to formally verifying financial mathematics exams (such as Exam FM of the Society of Actuaries) prior to delivering them to students.

0.5 Conclusion

The actuarial and financial mathematics literature is vast (see for example [ 7 ] ) and we have only laid some of the groundwork. A general continuation would be to add stochastic components. Related initiatives include formalization of Brownian motion in Lean [ 4 ] and, tangentially, formalization of smart contracts [ 10 ] .

A very concrete next task would be to clarify to what extent two of our six variables can be computed from the other four: For instance, can yield rate and maturity be computed from present value, future value, Macaulay duration, and coupon rate?

Acknowledgments.

This work was partially supported by grants from the Simons Foundation (#704836 to Bjørn Kjos-Hanssen) and Majesco Inc. (University of Hawai‘i Foundation Account #129-4770-4).