Reduction of the Agoh–Giuga Conjecture

We reduce the Agoh–Giuga conjecture to the nonexistence of certain numbers.

Main results

• conjecture_iff_no_carmichael_giuga: the conjecture holds if and only if no number is simultaneously Carmichael and Giuga.
• no_odd_giuga_implies_conjecture: a sufficient condition — if no odd Giuga number exists, then the conjecture holds (since every Carmichael number is odd).

Reduction chain

1. prime → giugaSum = -1 (proved: agoh_giuga_forward)
2. composite + giugaSum = -1 → Carmichael ∧ Giuga (structural_forward)
3. Carmichael ∧ Giuga → giugaSum = -1 (structural_backward)
4. Carmichael → odd (IsCarmichaelNumber.odd)

Combining (2) and (3): the conjecture's reverse direction (no composite counterexample) is equivalent to the nonexistence of Carmichael-Giuga numbers. Combining with (4): it suffices to show no odd Giuga number exists.

theorem conjecture_iff_no_carmichael_giuga : (∀ n ≥ 2, Nat.Prime n ↔ giugaSum n = -1) ↔ ¬∃ (n : ℕ), IsCarmichaelNumber n ∧ IsGiugaNumber n

The Agoh–Giuga conjecture is equivalent to: no number is simultaneously Carmichael and Giuga.

theorem no_odd_giuga_implies_conjecture (h : ∀ (n : ℕ), IsGiugaNumber n → ¬Odd n) (n : ℕ) : n ≥ 2 → (Nat.Prime n ↔ giugaSum n = -1)

If no odd Giuga number exists, the conjecture holds. Every Carmichael number is odd, so a Carmichael-Giuga number would be an odd Giuga number.

theorem no_carmichael_giuga : ¬∃ (n : ℕ), IsCarmichaelNumber n ∧ IsGiugaNumber n

The open conjecture: no number is simultaneously Carmichael and Giuga.

theorem agoh_giuga_conjecture (n : ℕ) : n ≥ 2 → (Nat.Prime n ↔ giugaSum n = -1)

The Agoh–Giuga conjecture (full, open problem).

n ≥ 2 is prime if and only if ∑_{i=1}^{n-1} i^{n-1} ≡ -1 (mod n).