Prove2Me

lean_workbook_plus_13963

Proved

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

Let f(m,n)f(m,n) be the expected number of points Alice gets with mm red and nn black cards. Remark that f(m,0)=f(0,m)=mf(m,0) = f(0, m) = m , and also f(m,m)=12+f(m,m−1)f(m,m) = \tfrac{1}{2} + f(m,m-1) for all mm . Now, for m≠nm\ne n , we have f(m,n)=nm+n(f(m,n−1)+T(n>m))+mm+n(f(m−1,n)+T(m>n)), f(m,n) = \tfrac{n}{m + n}\left(f(m,n-1) + T(n > m)\right) + \tfrac{m}{m + n}\left(f(m-1,n) + T(m > n)\right), where we define T(S)=1T(S) = 1 if SS is true and T(S)=0T(S) = 0 if SS is false for an assertion SS . Use this recursion a few times to get f(3,3)=4110→051.f(3,3) = \tfrac{41}{10}\to\boxed{051}.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_13963  (f : ℕ → ℕ → ℝ)
  (h₀ : ∀ m, f m 0 = m)
  (h₁ : ∀ m, f 0 m = m)
  (h₂ : ∀ m, f m m = 1 / 2 + f m (m - 1))
  (h₃ : ∀ m n, m ≠ n → f m n = n / (m + n) * (f m (n - 1) + if n > m then 1 else 0) + m / (m + n) * (f (m - 1) n + if m > n then 1 else 0)) :
  f 3 3 = 41 / 10   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph