The Binomial Pricing Model in Finance: A Formalization in Isabelle

The binomial pricing model is an option valuation method based on a discrete-time model of the evolution of an equity market. It allows one to determine the fair price of derivatives from the payoff they generate at their expiration date. A formalization of this model in the proof assistant Isabelle is provided. We formalize essential notions in finance such as the no-arbitrage principle and prove that, under the hypotheses of the model, the market is complete, meaning that any European derivative can be replicated by creating a portfolio that generates the same payoff regardless of the evolution of the market.