Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL

TL;DR

This paper formalizes core concepts of financial mathematics and the Cox-Rubinstein model in Isabelle/HOL, proving market completeness and the uniqueness of fair prices for derivatives.

Contribution

It provides the first formal proof of the Cox-Rubinstein model's completeness and fair price uniqueness within a proof assistant, enhancing rigor in financial modeling.

Findings

Market completeness in the Cox-Rubinstein model

Existence of unique fair prices for derivatives

Formal verification of financial concepts in Isabelle/HOL

Abstract

We formalize in the proof assistant Isabelle essential basic notions and results in financial mathematics. We provide generic formal definitions of concepts such as markets, portfolios, derivative products, arbitrages or fair prices, and we show that, under the usual no-arbitrage condition, the existence of a replicating portfolio for a derivative implies that the latter admits a unique fair price. Then, we provide a formalization of the Cox-Rubinstein model and we show that the market is complete in this model, i.e., that every derivative product admits a replicating portfolio. This entails that in this model, every derivative product admits a unique fair price.