Download PDFOpen PDF in browser

Formalization of Gambler’s Ruin Problem in Isabelle/HOL

EasyChair Preprint 6165

6 pagesDate: July 27, 2021

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

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