Agoh-Giuga conjecture

Theorem · isWeakGiuga_iff_prime_dvd

A composite number $n$ is weak Giuga if and only if $p \mid (\frac{n}{p} - 1)$ for all prime divisors $p$ of $n$ .

Formal statement · Lean 4.lean

theorem isWeakGiuga_iff_prime_dvd {n : ℕ} (hn : n.Composite) :
    IsWeakGiuga n ↔ ∀ p ∈ n.primeFactors, p ∣ (n / p - 1) := by
  sorry

Proof. sorry

Nobody has tried yet.