Wolstenholme Prime

Reference: Wikipedia

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

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

def WolstenholmePrime.IsWolstenholmePrime (p : ℕ) : Prop

A prime $p > 7$ is called a Wolstenholme prime if $\binom{2p-1}{p-1} \equiv 1 (\pmod{p^4})$.

Equations

• WolstenholmePrime.IsWolstenholmePrime p = (p > 7 ∧ Nat.Prime p ∧ (2 * p - 1).choose (p - 1) ≡ 1 [MOD p ^ 4])

theorem WolstenholmePrime.wolstenholme_prime_16483 : IsWolstenholmePrime 16843

Two known Wolstenholme primes: 16843 and 2124679.

Formal proof linked here provided by AlphaProof

theorem WolstenholmePrime.wolstenholme_prime_2124679 : IsWolstenholmePrime 2124679

theorem WolstenholmePrime.wolstenholme_bernoulli (p : ℕ) : IsWolstenholmePrime p ↔ p > 7 ∧ Nat.Prime p ∧ ↑p ∣ (bernoulli' (p - 3)).num

Equivalently, a prime $p > 7$ is a Wolstenholme prime if it divides the numerator of the Bernoulli number $B_{p-3}$.

theorem WolstenholmePrime.wolstenholme_harmonic (p : ℕ) : IsWolstenholmePrime p ↔ p > 7 ∧ Nat.Prime p ∧ ↑(p ^ 3) ∣ (harmonic (p - 1)).num

Another equivalent definition is that a prime $p > 7$ is a Wolstenholme prime if it $p^3$ divides the numerator of the harmonic number $H_{p-1}$.

theorem WolstenholmePrime.wolstenholme_prime_infinite : {p : ℕ | IsWolstenholmePrime p}.Infinite

It is conjectured that there are infinitely many Wolstenholme primes.

Reference: Wikipedia