lean_workbook_plus_38066

Proved

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

Prove that $\binom{p-1}{(p-1)/2}\equiv (-1)^\frac{p-1}{2}\pmod{p}$ for odd prime $p$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_38066 (p : ℕ) (hp : p.Prime) (hpo : Odd p) :
    ((p - 1).choose (p - 1) / 2) ≡ (-1 : ℤ) ^ (p - 1) / 2 [ZMOD p]   :=  by sorry

Source

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

View graph