lean_workbook_plus_50647

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Let $p$ be the probability that $A$ wins if $A$ is up by $1$ point, $q$ be the probability that $A$ wins if the game is tied (what we are looking for), and $r$ be the probability that $A$ wins if $A$ is losing by $1$ point. We have $p=\frac{7}{10}+\frac{3}{10}q$ , $q=\frac{7}{10}p+\frac{3}{10}r$ , $r=\frac{7}{10}q$ . Solving this system yields $q = \boxed{\frac{49}{58}} \approx 84.483\%$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_50647  (p q r : ℚ)
  (h₀ : p = 7 / 10 + 3 / 10 * q)
  (h₁ : q = 7 / 10 * p + 3 / 10 * r)
  (h₂ : r = 7 / 10 * q) :
  q = 49 / 58   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph