Counterexample Bounds for the Agoh–Giuga Conjecture #

Any counterexample to the Agoh–Giuga conjecture must be simultaneously Carmichael and Giuga. We prove structural properties any such counterexample must have:

It is odd and squarefree (from Carmichael/Giuga properties).
It has at least 3 prime factors (Carmichael property).
It has at least 9 prime factors (reciprocal sum argument for odd case).

Key lemma: reciprocal sum bound #

For any odd Giuga number n, the reciprocal sum ∑_{p | n} 1/p > 1. Since the sum of reciprocals of any 8 distinct odd primes is less than 1, an odd Giuga number must have at least 9 prime factors.

References #

Borwein, D., Borwein, J.M., Borwein, P.B., Girgensohn, R. (1996). "Giuga's conjecture on primality". Amer. Math. Monthly, 103(1), 40–50.

Reciprocal sum of Giuga numbers #

source

theorem IsGiugaNumber.dvd_sum_quot_sub_one {n : ℕ} (hg : IsGiugaNumber n) :

n ∣ ∑ p ∈ n.primeFactors, n / p - 1

For a squarefree Giuga number, n ∣ (∑_{p ∈ primeFactors} n/p - 1).

The proof uses CRT: for each prime factor q, the terms n/p with p ≠ q vanish mod q (since q ∣ n/p for distinct prime factors of squarefree n), while n/q ≡ 1 (mod q) by the Giuga condition.

source

theorem IsGiugaNumber.sum_quot_ge_succ {n : ℕ} (hg : IsGiugaNumber n) :

n + 1 ≤ ∑ p ∈ n.primeFactors, n / p

For a Giuga number n, the sum ∑_{p ∈ primeFactors} n/p ≥ n + 1.

Since n ∣ (∑ n/p - 1) and ∑ n/p ≥ 2 (because n/p ≥ 2 for any prime factor p of the composite n), we have ∑ n/p - 1 ≥ n.

source

theorem IsGiugaNumber.one_lt_sum_reciprocals {n : ℕ} (hg : IsGiugaNumber n) :

1 < ∑ p ∈ n.primeFactors, 1 / ↑p

For a Giuga number, the reciprocal sum ∑_{p | n} 1/p > 1.

This follows from ∑ n/p ≥ n + 1: dividing by n gives ∑ 1/p ≥ (n+1)/n > 1.

Odd Giuga numbers have ≥ 9 prime factors #

source

theorem nth_odd_prime_le_orderEmbOfFin {S : Finset ℕ} (hS : ∀ p ∈ S, Nat.Prime p ∧ Odd p) (i : Fin S.card) :

Nat.nth Nat.Prime (↑i + 1) ≤ (S.orderEmbOfFin ⋯) i

In the increasing enumeration of a finite set of odd primes, the i-th element is at least the (i+1)-st prime (skipping 2).

source

theorem odd_squarefree_card_primeFactors_product_le {n k : ℕ} (hodd : Odd n) (hsf : Squarefree n) (hcard : k ≤ n.primeFactors.card) :

∏ j ∈ Finset.range k, Nat.nth Nat.Prime (j + 1) ≤ n

If n is odd, squarefree, and has at least k prime factors, then n is at least the product of the first k odd primes.

This generalises first_nine_odd_primes_product_le_of_odd_squarefree_nine_primeFactors (the k = 9 special case).

source

theorem sum_reciprocals_le_of_odd_primes (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p ∧ Odd p) (hcard : S.card ≤ 8) :

∑ p ∈ S, 1 / ↑p < 1

Any set of at most 8 distinct odd primes has reciprocal sum < 1.

The i-th smallest element of any set of distinct odd primes is at least the i-th odd prime, so its reciprocal is at most that of the i-th odd prime. The sum of reciprocals of the 8 smallest odd primes {3,5,7,11,13,17,19,23} equals 111429982/111546435 < 1.

source

theorem IsGiugaNumber.nine_le_card_primeFactors_of_odd {n : ℕ} (hg : IsGiugaNumber n) (hodd : Odd n) :

9 ≤ n.primeFactors.card

Odd Giuga numbers have at least 9 prime factors.

All prime factors of an odd Giuga number are odd primes. The reciprocal sum exceeds 1 (by one_lt_sum_reciprocals), but any set of ≤ 8 odd primes has reciprocal sum < 1. So there must be ≥ 9 prime factors.