lean_workbook_plus_37160

Disproved

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

Prove that $\binom{2p}{p}\equiv 2 \pmod{p^{3}}$ (without using Wolstenholme of course).

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_37160 : ∀ p : ℕ, p.Prime → (Nat.choose (2 * p) p) % (p ^ 3) = 2   :=  by sorry

Source