Giuga's conjecture in arithmetic form: no composite Giuga--Carmichael number
OpenFCP.AgohGiuga.giuga_conjecture_arithGiuga's conjecture, arithmetic form. Let be an integer and suppose that for every prime dividing both
hold. Then is prime.
Equivalently: no composite number is simultaneously a Giuga number and a Carmichael number. This is the open kernel of the Agoh--Giuga conjecture. By Giuga's criterion, an integer satisfies exactly when the two displayed families of divisibilities hold, so the conjecture "the congruence forces primality" is equivalent to the statement above. A composite satisfying the hypotheses is known to have at least digits (Borwein, Borwein, Borwein and Girgensohn, 1996), and later computations push the bound much further.
Primes satisfy the hypotheses trivially: for prime the only prime divisor is itself, , and every number divides .
Formalization Note All arithmetic is in the natural numbers; is exact division since , and the subtractions are truncated natural subtraction, which is harmless because and .
import Mathlib
namespace FCP.AgohGiuga
theorem giuga_conjecture_arith (n : ℕ) (hn : 2 ≤ n)
(h : ∀ p : ℕ, p.Prime → p ∣ n → p ∣ n / p - 1 ∧ (p - 1) ∣ n / p - 1) :
n.Prime := by sorry
end FCP.AgohGiuga