lean_workbook_plus_65567

Proved

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

The probability of same-color-ness is $\dfrac {4}{10} \cdot \dfrac {16}{16 + N} + \dfrac {6}{10} \cdot \dfrac {N}{16+N} = \dfrac {29}{50}.$ This is a simple linear equation. We get $N=\boxed{144}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_65567  (n : ℕ)
  (h₀ : 0 < n)
  (h₁ : (4:ℝ) / 10 * (16:ℝ) / (16 + n) + 6 / 10 * n / (16 + n) = 29 / 50) :
  n = 144   :=  by sorry

Source

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

View graph