lean_workbook_plus_5572

Proved

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

The probability of drawing two marbles of the same color is $\frac {1000}{2001}$ , so the probability of them NOT being the same color is $1 - \frac {1000}{2001} = \frac {1001}{2001}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_5572 :
  1 - (1000 : ℝ) / 2001 = 1001 / 2001   :=  by sorry

Source

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

View graph