Formalization of Gambler’s Ruin Problem in Isabelle/HOL

EasyChair Preprint 6165

Abstract

Gambler’s ruin problem is an exciting application of probability theory which is generally used to analyze various practical scenarios like the security of bitcoin protocol. In this article, we provide a comprehensive analysis of the formalization of Gambler’s ruin problem. First, we present a comprehensive background and pen-and-paper calculation. Second, we summarize how to quantify the Gambler’s ruin problem and prepare all necessary intermediate conclusions. Third, we explain the difficulties we faced during the final formalization and analyze the strategies to overcome these barriers. Our final result: The recursive probability equation aims to establish the complete quantitative analysis of random walk and assist others in developing advanced probability analysis based on what we endeavor here.

Keyphrases: Gambler's Ruin Problem, formal verification, probability theory, random walk, theorem proving

@booklet{EasyChair:6165,
  author    = {Zibo Yang},
  title     = {Formalization of Gambler’s Ruin Problem in Isabelle/HOL},
  howpublished = {EasyChair Preprint 6165},
  year      = {EasyChair, 2021}}