lean_workbook_plus_10680

Proved

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

If we have a random variable that follows a binomial distribution \n $X\sim B(n=2m,p=1/2)$ ,\n with mean $E\{ X\}=np=m$ ,\n and variance $\sigma^{2}=E\{(X-E\{ X\})^{2}\}=np(1-p)=m/2$ ,

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_10680 (m : ℕ) : ∃ n : ℕ, n = 2 * m ∧ ∃ p : ℝ, p = 1 / 2 ∧ ∃ μ : ℝ, μ = n * p ∧ ∃ σ : ℝ, σ ^ 2 = n * p * (1 - p)   :=  by sorry

Source

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

View graph