Agoh-Giuga conjecture

Reference: Wikipedia

The Agoh-Giuga Conjecture.

References:

• Wikipedia: https://en.wikipedia.org/wiki/Agoh-Giuga_conjecture
• Wikipedia: https://en.wikipedia.org/wiki/Giuga_number
• G. Giuga, Su una presumibile proprieta caratteristica dei numeri primi
• E. Bedocchi, Note on a conjecture about prime numbers
• D. Borwein, J. M. Borwein, P. B. Borwein, and R. Girgensohn, Giuga’s conjecture on primality
• V. Tipu, A Note on Giuga’s Conjecture

def AgohGiuga.AgohGiugaCongr : Prop

The Agoh-Giuga Conjecture, Agoh's formulation. An integer p ≥ 2 is prime if and only if we have p*B_{p-1} ≡ -1 [MOD p]

Equations

• AgohGiuga.AgohGiugaCongr = ∀ p ≥ 2, Nat.Prime p ↔ ∃ (k : ℤ), let B := bernoulli' (p - 1); ↑p * B.num + ↑B.den = k * ↑p

def AgohGiuga.AgohGiugaSum : Prop

The Agoh-Giuga Conjecture, Giuga's formulation. An integer p ≥ 2 is prime if and only if it satifies the congruence ∑_{i=1}^{p-1} i^{p-1} ≡ -1 [MOD p].

Equations

• AgohGiuga.AgohGiugaSum = ∀ p ≥ 2, Nat.Prime p ↔ p ∣ 1 + ∑ i ∈ Finset.Ioo 0 p, i ^ (p - 1)

theorem AgohGiuga.agoh_giuga : AgohGiugaCongr

The Agoh-Giuga Conjecture, Agoh's formulation

theorem AgohGiuga.agoh_giuga.variants.giuga : AgohGiugaSum

The Agoh-Giuga Conjecture, Giuga's formulation

theorem AgohGiuga.agoh_giuga.variants.equivalence : AgohGiugaCongr ↔ AgohGiugaSum

The two statements of the conjecture are equivalent.

def AgohGiuga.IsWeakGiuga (n : ℕ) : Prop

A (weak) Giuga number is a number $n$ such that $$\sum_{i=1}^{n - 1}i^{\varphi(n)} \equiv -1\pmod{n}$$.

Equations

• AgohGiuga.IsWeakGiuga n = (2 ≤ n ∧ ¬Nat.Prime n ∧ n ∣ 1 + ∑ i ∈ Finset.Ioo 0 n, i ^ n.totient)

def AgohGiuga.IsStrongGiuga (n : ℕ) : Prop

A (strong) Giuga number is a number $n$ such that $$\sum_{i=1}^{n - 1}i^{n - 1} \equiv -1\pmod{n}$$

Equations

• AgohGiuga.IsStrongGiuga n = (2 ≤ n ∧ ¬Nat.Prime n ∧ n ∣ 1 + ∑ i ∈ Finset.Ioo 0 n, i ^ (n - 1))

theorem AgohGiuga.isWeakGiuga_iff_prime_dvd (n : ℕ) : IsWeakGiuga n ↔ ∀ p ∈ n.primeFactors, p ∣ n / p - 1

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

theorem AgohGiuga.isWeakGiuga_iff_sum_primeFactors (n : ℕ) : IsWeakGiuga n ↔ ∃ (m : ℕ), ∑ p ∈ n.primeFactors, 1 / ↑p - 1 / ↑n = ↑m

A number $n$ is weak Giuga if and only if $$ \sum_{p\mid n} \frac{1}{p} - \frac{1}{n} \in\mathbb{N}. $$

def AgohGiuga.IsCarmichael (n : ℕ) : Prop

A Carmichael number is a composite number n such that for all b ≥ 1, we have b^n ≡ b (mod n).

Equations

• AgohGiuga.IsCarmichael n = ∀ b ≥ 1, n.Coprime b → n.FermatPsp b

theorem AgohGiuga.squarefree_of_isCarmichael {a : ℕ} (ha₁ : 1 < a) (ha₂ : ¬Nat.Prime a) (ha₃ : IsCarmichael a) : Squarefree a

A composite Carmichael number is squarefree.

theorem AgohGiuga.korselts_criterion (a : ℕ) (ha₁ : 1 < a) (ha₂ : ¬Nat.Prime a) : IsCarmichael a ↔ Squarefree a ∧ ∀ (p : ℕ), Nat.Prime p → p ∣ a → p - 1 ∣ a - 1

A composite number a is Carmichael if and only if it is squarefree and, for all prime p dividing a, we have p - 1 ∣ a - 1.

theorem AgohGiuga.isStrongGiuga_iff (a : ℕ) : IsStrongGiuga a ↔ IsCarmichael a ∧ ∃ (n : ℕ), ∑ p ∈ a.primeFactors, 1 / ↑p - 1 / ↑a = ↑n

Giuga showed that a number n is strong Giuga if and only if it is Carmichael and ∑_{p|n} 1/p - 1/n ∈ ℕ (i.e., if and only if it is Carmichael and weak Giuga). Ref: G. Giuga, Su una presumibile proprieta caratteristica dei numeri primi

theorem AgohGiuga.agoh_giuga.variants.isStrongGiuga_implies_isCarmichael (a : ℕ) (ha : IsStrongGiuga a) : IsCarmichael a

Every strong Giuga number is a Carmichael number.

theorem AgohGiuga.agoh_giuga.variants.le_primeFactors_card_of_isStrongGiuga (a : ℕ) (ha : IsStrongGiuga a) : 9 ≤ a.primeFactors.card

Giuga showed that a Giuga number has at least 9 prime factors. Ref: G. Giuga, Su una presumibile proprieta caratteristica dei numeri primi

theorem AgohGiuga.agoh_giuga.variants.isStrongGiuga_growth (G : ℕ → ℕ) (hG : G = fun (x : ℕ) => (Finset.filter IsStrongGiuga (Finset.Icc 1 x)).card) : ∃ (N : ℕ) (O : ℝ), ∀ n ≥ N, ↑(G n) ≤ O * √↑n * Real.log ↑n

Let G(X) denote the number of exceptions n ≤ X to Giuga’s conjecture. Then for X larger than an absolute constant which can be made explicit, G(X) ≪ X^{1/2} log X. Ref: Vicentiu Tipu, A Note on Giuga’s Conjecture