Agoh-Giuga conjecture

Reference: Wikipedia

The Agoh-Giuga Conjecture.

References:

• Wikipedia: https://en.wikipedia.org/wiki/Agoh-Giuga_conjecture
• 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 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

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

def 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

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

theorem agoh_giuga : AgohGiugaCongr

The Agoh-Giuga Conjecture, Agoh's formulation

theorem agoh_giuga.variants.giuga : AgohGiugaSum

The Agoh-Giuga Conjecture, Giuga's formulation

theorem agoh_giuga.variants.equivalence : AgohGiugaCongr ↔ AgohGiugaSum

The two statements of the conjecture are equivalent.

def IsGiuga (p : ℕ) : Prop

A Giuga number is a counterexample to Giuga's conjecture.

Equations

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

def 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

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

theorem 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 agoh_giuga.variants.isGiuga_implies_nat_fermatPsp (a : ℕ) (ha : IsGiuga a) : IsCarmichael a

Every Giuga number is a Carmichael number.

theorem agoh_giuga.variants.isGiuga_iff (a : ℕ) : IsGiuga a ↔ IsCarmichael a ∧ ∃ (n : ℚ), ∑ p ∈ a.primeFactors, 1 / ↑p - 1 / ↑a = n

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

theorem agoh_giuga.variants.le_primeFactors_card_of_isGiuga (a : ℕ) (ha : IsGiuga 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 agoh_giuga.variants.isGiuga_growth (G : ℕ → ℕ) (hG : G = fun (x : ℕ) => (Finset.filter IsGiuga (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