Download PDFOpen PDF in browser

Formalization of Gambler’s Ruin Problem in Isabelle/HOL

EasyChair Preprint no. 6165

6 pagesDate: July 27, 2021


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: formal verification, Gambler's Ruin Problem, probability theory, random walk, theorem proving

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
  author = {Zibo Yang},
  title = {Formalization of Gambler’s Ruin Problem in Isabelle/HOL},
  howpublished = {EasyChair Preprint no. 6165},

  year = {EasyChair, 2021}}
Download PDFOpen PDF in browser