Wolstenholme Prime

Theorem · wolstenholme_theorem

Wolstenholme's theorem states that any prime $p > 3$ satisfies $\binom{2p-1}{p-1} \equiv 1 (\pmod{p^3})$ .

Formal proof linked here provided by AlphaProof. *Reference:* Wikipedia

Formal statement · Lean 4.lean

theorem wolstenholme_theorem (p : ℕ) (h : p > 3) (hp : Nat.Prime p) :
    (2 * p - 1).choose (p - 1) ≡ 1 [MOD p ^ 3] := by
  sorry

Proof. sorry

Nobody has tried yet.