FormalConjectures.Wikipedia.AgohGiuga

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Agoh-Giuga conjecture

Reference: Wikipedia

open scoped Nat

/-

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_

-/

namespace AgohGiuga

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]

def AgohGiugaCongr : Prop :=
  ∀ p ≥ 2, p.Prime ↔ ∃ (k : ℤ),
  let B := bernoulli' (p - 1)
  p * B.num + B.den = k * p^2

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].

def AgohGiugaSum : Prop := ∀ p ≥ 2, p.Prime ↔
  p ∣ 1 + ∑ i ∈ Finset.Ioo 0 p, i^(p - 1 : ℕ)

The Agoh-Giuga Conjecture, Agoh's formulation

@[category research open, AMS 11]
theorem declaration uses 'sorry'agoh_giuga : AgohGiugaCongr := by⊢ AgohGiugaCongr
  sorryAll goals completed! 🐙

The Agoh-Giuga Conjecture, Giuga's formulation

@[category research open, AMS 11]
theorem declaration uses 'sorry'agoh_giuga.variants.giuga : AgohGiugaSum := by⊢ AgohGiugaSum
  sorryAll goals completed! 🐙

The two statements of the conjecture are equivalent.

@[category research solved, AMS 11]
theorem declaration uses 'sorry'agoh_giuga.variants.equivalence : AgohGiugaCongr ↔ AgohGiugaSum := by⊢ AgohGiugaCongr ↔ AgohGiugaSum
  sorryAll goals completed! 🐙

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

def IsWeakGiuga (n : ℕ) : Prop :=
    n.Composite ∧ n ∣ 1 + ∑ i ∈ Finset.Ioo 0 n, i ^ φ n

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

def IsStrongGiuga (n : ℕ) : Prop :=
    n.Composite ∧ n ∣ 1 + ∑ i ∈ Finset.Ioo 0 n, i ^ (n - 1)

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

@[category research solved, AMS 11, formal_proof using formal_conjectures at
"https://github.com/mo271/formal-conjectures/blob/2663234a28260853790aa5752d8d4550ff0ab1ca/FormalConjectures/Wikipedia/AgohGiuga.lean#L97"]
theorem declaration uses 'sorry'isWeakGiuga_iff_prime_dvd {n : ℕ} (hn : n.Composite) :
    IsWeakGiuga n ↔ ∀ p ∈ n.primeFactors, p ∣ (n / p - 1) := byn:ℕhn:n.Composite⊢ IsWeakGiuga n ↔ ∀ p ∈ n.primeFactors, p ∣ n / p - 1
  sorryAll goals completed! 🐙

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

@[category research solved, AMS 11]
theorem declaration uses 'sorry'isWeakGiuga_iff_sum_primeFactors {n : ℕ} (hn : n.Composite) :
    IsWeakGiuga n ↔ ∃ m : ℕ, ∑ p ∈ n.primeFactors, (1 / p : ℚ) - 1 / n = m := byn:ℕhn:n.Composite⊢ IsWeakGiuga n ↔ ∃ m, ∑ p ∈ n.primeFactors, 1 / ↑p - 1 / ↑n = ↑m
  sorryAll goals completed! 🐙

A composite Carmichael number is squarefree.

@[category textbook, AMS 11]
theorem squarefree_of_isCarmichael {a : ℕ} (ha₁ : a.Composite) (ha₂ : IsCarmichael a) :
    Squarefree a := bya:ℕha₁:a.Compositeha₂:IsCarmichael a⊢ Squarefree a
  have ha₂_forall := ha₂a:ℕha₁:a.Compositeha₂:IsCarmichael aha₂_forall:IsCarmichael a := ha₂⊢ Squarefree a
  simp_all [IsCarmichael, Nat.Composite, a.squarefree_iff_prime_squarefree, Nat.FermatPsp, Nat.ProbablePrime]a:ℕha₁:1 < a ∧ ¬Nat.Prime aha₂:∀ (b : ℕ), 1 ≤ b → a.Coprime b → a ∣ b ^ (a - 1) - 1ha₂_forall:∀ (b : ℕ), 1 ≤ b → a.Coprime b → a ∣ b ^ (a - 1) - 1⊢ ∀ (x : ℕ), Nat.Prime x → ¬x * x ∣ a
  rintro p hp ⟨N, rfl⟩p:ℕhp:Nat.Prime pN:ℕha₁:1 < p * p * N ∧ ¬Nat.Prime (p * p * N)ha₂:∀ (b : ℕ), 1 ≤ b → (p * p * N).Coprime b → p * p * N ∣ b ^ (p * p * N - 1) - 1ha₂_forall:∀ (b : ℕ), 1 ≤ b → (p * p * N).Coprime b → p * p * N ∣ b ^ (p * p * N - 1) - 1⊢ False
  apply absurd (ha₂_forall (p * N + 1) ((1).le_add_left _))p:ℕhp:Nat.Prime pN:ℕha₁:1 < p * p * N ∧ ¬Nat.Prime (p * p * N)ha₂:∀ (b : ℕ), 1 ≤ b → (p * p * N).Coprime b → p * p * N ∣ b ^ (p * p * N - 1) - 1ha₂_forall:∀ (b : ℕ), 1 ≤ b → (p * p * N).Coprime b → p * p * N ∣ b ^ (p * p * N - 1) - 1⊢ ¬((p * p * N).Coprime (p * N + 1) → p * p * N ∣ (p * N + 1) ^ (p * p * N - 1) - 1)
  have : Fact p.Prime := ⟨hp⟩p:ℕhp:Nat.Prime pN:ℕha₁:1 < p * p * N ∧ ¬Nat.Prime (p * p * N)ha₂:∀ (b : ℕ), 1 ≤ b → (p * p * N).Coprime b → p * p * N ∣ b ^ (p * p * N - 1) - 1ha₂_forall:∀ (b : ℕ), 1 ≤ b → (p * p * N).Coprime b → p * p * N ∣ b ^ (p * p * N - 1) - 1this:Fact (Nat.Prime p) := { out := hp }⊢ ¬((p * p * N).Coprime (p * N + 1) → p * p * N ∣ (p * N + 1) ^ (p * p * N - 1) - 1)
  rw [mul_assoc] at ha₁p:ℕhp:Nat.Prime pN:ℕha₁:1 < p * (p * N) ∧ ¬Nat.Prime (p * (p * N))ha₂:∀ (b : ℕ), 1 ≤ b → (p * p * N).Coprime b → p * p * N ∣ b ^ (p * p * N - 1) - 1ha₂_forall:∀ (b : ℕ), 1 ≤ b → (p * p * N).Coprime b → p * p * N ∣ b ^ (p * p * N - 1) - 1this:Fact (Nat.Prime p)⊢ ¬((p * p * N).Coprime (p * N + 1) → p * p * N ∣ (p * N + 1) ^ (p * p * N - 1) - 1)
  rw [mul_assoc, ← geom_sum_mul_of_one_le ((1).le_add_left (p * N)), p.coprime_mul_iff_left]p:ℕhp:Nat.Prime pN:ℕha₁:1 < p * (p * N) ∧ ¬Nat.Prime (p * (p * N))ha₂:∀ (b : ℕ), 1 ≤ b → (p * p * N).Coprime b → p * p * N ∣ b ^ (p * p * N - 1) - 1ha₂_forall:∀ (b : ℕ), 1 ≤ b → (p * p * N).Coprime b → p * p * N ∣ b ^ (p * p * N - 1) - 1this:Fact (Nat.Prime p)⊢ ¬(p.Coprime (p * N + 1) ∧ (p * N).Coprime (p * N + 1) →
    p * (p * N) ∣ (∑ i ∈ Finset.range (p * (p * N) - 1), (p * N + 1) ^ i) * (p * N + 1 - 1))
  simpa using (mul_dvd_mul_iff_right fun _ ↦ byp:ℕhp:Nat.Prime pN:ℕha₁:1 < p * (p * N) ∧ ¬Nat.Prime (p * (p * N))ha₂:∀ (b : ℕ), 1 ≤ b → (p * p * N).Coprime b → p * p * N ∣ b ^ (p * p * N - 1) - 1ha₂_forall:∀ (b : ℕ), 1 ≤ b → (p * p * N).Coprime b → p * p * N ∣ b ^ (p * p * N - 1) - 1this:Fact (Nat.Prime p)x✝:p * N = 0⊢ False simp_all only [mul_zero, not_lt_zero']All goals completed! 🐙).not.mpr
    ((ZMod.natCast_eq_zero_iff _ _).not.mp (byp:ℕhp:Nat.Prime pN:ℕha₁:1 < p * (p * N) ∧ ¬Nat.Prime (p * (p * N))ha₂:∀ (b : ℕ), 1 ≤ b → (p * p * N).Coprime b → p * p * N ∣ b ^ (p * p * N - 1) - 1ha₂_forall:∀ (b : ℕ), 1 ≤ b → (p * p * N).Coprime b → p * p * N ∣ b ^ (p * p * N - 1) - 1this:Fact (Nat.Prime p)⊢ ¬↑(∑ i ∈ Finset.range (p * (p * N) - 1), (p * N + 1) ^ i) = 0 simp [le_of_lt ha₁.1]All goals completed! 🐙))

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.

@[category textbook, AMS 11]
theorem korselts_criterion (a : ℕ) (ha₁ : a.Composite) :
    IsCarmichael a ↔ Squarefree a ∧
      ∀ p, p.Prime → p ∣ a → (p - 1 : ℕ) ∣ (a - 1 : ℕ) := bya:ℕha₁:a.Composite⊢ IsCarmichael a ↔ Squarefree a ∧ ∀ (p : ℕ), Nat.Prime p → p ∣ a → p - 1 ∣ a - 1
  refine ⟨fun h ↦ ⟨squarefree_of_isCarmichael ha₁ h, fun p hp hpa ↦ ?_⟩, fun h b hb hab ↦ ?_⟩refine_1a:ℕha₁:a.Compositeh:IsCarmichael ap:ℕhp:Nat.Prime phpa:p ∣ a⊢ p - 1 ∣ a - 1refine_2a:ℕha₁:a.Compositeh:Squarefree a ∧ ∀ (p : ℕ), Nat.Prime p → p ∣ a → p - 1 ∣ a - 1b:ℕhb:b ≥ 1hab:a.Coprime b⊢ a.FermatPsp b
  ·refine_1a:ℕha₁:a.Compositeh:IsCarmichael ap:ℕhp:Nat.Prime phpa:p ∣ a⊢ p - 1 ∣ a - 1 have h_forall := hrefine_1a:ℕha₁:a.Compositeh:IsCarmichael ap:ℕhp:Nat.Prime phpa:p ∣ ah_forall:IsCarmichael a := h⊢ p - 1 ∣ a - 1
    have : Fact p.Prime := ⟨hp⟩refine_1a:ℕha₁:a.Compositeh:IsCarmichael ap:ℕhp:Nat.Prime phpa:p ∣ ah_forall:IsCarmichael a := hthis:Fact (Nat.Prime p) := { out := hp }⊢ p - 1 ∣ a - 1
    let ⟨g, h⟩ := IsCyclic.exists_generator (α := (ZMod p)ˣ)refine_1a:ℕha₁:a.Compositeh✝:IsCarmichael ap:ℕhp:Nat.Prime phpa:p ∣ ah_forall:IsCarmichael a := hthis:Fact (Nat.Prime p) := { out := hp }g:(ZMod p)ˣh:∀ (x : (ZMod p)ˣ), x ∈ Subgroup.zpowers g⊢ p - 1 ∣ a - 1
    obtain ⟨k, rfl⟩ := hparefine_1p:ℕhp:Nat.Prime pthis:Fact (Nat.Prime p) := { out := hp }g:(ZMod p)ˣh✝:∀ (x : (ZMod p)ˣ), x ∈ Subgroup.zpowers gk:ℕha₁:(p * k).Compositeh:IsCarmichael (p * k)h_forall:IsCarmichael (p * k)⊢ p - 1 ∣ p * k - 1
    have hk : k.Coprime p := bya:ℕha₁:a.Composite⊢ IsCarmichael a ↔ Squarefree a ∧ ∀ (p : ℕ), Nat.Prime p → p ∣ a → p - 1 ∣ a - 1
      by_contra hkp:ℕhp:Nat.Prime pthis:Fact (Nat.Prime p) := { out := hp }g:(ZMod p)ˣh✝:∀ (x : (ZMod p)ˣ), x ∈ Subgroup.zpowers gk:ℕha₁:(p * k).Compositeh:IsCarmichael (p * k)h_forall:IsCarmichael (p * k)hk:¬k.Coprime p⊢ False
      obtain ⟨_, rfl⟩ := not_not.1 <| hp.coprime_iff_not_dvd.not.1 <| mt Nat.Coprime.symm hkp:ℕhp:Nat.Prime pthis:Fact (Nat.Prime p) := { out := hp }g:(ZMod p)ˣh✝:∀ (x : (ZMod p)ˣ), x ∈ Subgroup.zpowers gw✝:ℕha₁:(p * (p * w✝)).Compositeh:IsCarmichael (p * (p * w✝))h_forall:IsCarmichael (p * (p * w✝))hk:¬(p * w✝).Coprime p⊢ False
      absurd (squarefree_of_isCarmichael ha₁ h)p:ℕhp:Nat.Prime pthis:Fact (Nat.Prime p) := { out := hp }g:(ZMod p)ˣh✝:∀ (x : (ZMod p)ˣ), x ∈ Subgroup.zpowers gw✝:ℕha₁:(p * (p * w✝)).Compositeh:IsCarmichael (p * (p * w✝))h_forall:IsCarmichael (p * (p * w✝))hk:¬(p * w✝).Coprime p⊢ ¬Squarefree (p * (p * w✝))
      simp [← mul_assoc, mul_comm, Nat.squarefree_mul_iff, ← sq, Nat.squarefree_pow_iff hp.ne_one]All goals completed! 🐙
    simp_all [IsCarmichael, Nat.FermatPsp, Nat.ProbablePrime, Nat.Composite]refine_1p:ℕhp:Nat.Prime pthis:Fact (Nat.Prime p) := { out := hp }g:(ZMod p)ˣh✝:∀ (x : (ZMod p)ˣ), x ∈ Subgroup.zpowers gk:ℕha₁:1 < p * k ∧ ¬Nat.Prime (p * k)h:∀ (b : ℕ), 1 ≤ b → (p * k).Coprime b → p * k ∣ b ^ (p * k - 1) - 1h_forall:∀ (b : ℕ), 1 ≤ b → (p * k).Coprime b → p * k ∣ b ^ (p * k - 1) - 1hk:k.Coprime p⊢ p - 1 ∣ p * k - 1
    let e : ZMod (p * k) ≃+* ZMod p × ZMod k := ZMod.chineseRemainder hk.symmrefine_1p:ℕhp:Nat.Prime pthis:Fact (Nat.Prime p) := { out := hp }g:(ZMod p)ˣh✝:∀ (x : (ZMod p)ˣ), x ∈ Subgroup.zpowers gk:ℕha₁:1 < p * k ∧ ¬Nat.Prime (p * k)h:∀ (b : ℕ), 1 ≤ b → (p * k).Coprime b → p * k ∣ b ^ (p * k - 1) - 1h_forall:∀ (b : ℕ), 1 ≤ b → (p * k).Coprime b → p * k ∣ b ^ (p * k - 1) - 1hk:k.Coprime pe:ZMod (p * k) ≃+* ZMod p × ZMod k := ZMod.chineseRemainder ⋯⊢ p - 1 ∣ p * k - 1
    let s : ZMod (p * k) := e.symm (g, 1)refine_1p:ℕhp:Nat.Prime pthis:Fact (Nat.Prime p) := { out := hp }g:(ZMod p)ˣh✝:∀ (x : (ZMod p)ˣ), x ∈ Subgroup.zpowers gk:ℕha₁:1 < p * k ∧ ¬Nat.Prime (p * k)h:∀ (b : ℕ), 1 ≤ b → (p * k).Coprime b → p * k ∣ b ^ (p * k - 1) - 1h_forall:∀ (b : ℕ), 1 ≤ b → (p * k).Coprime b → p * k ∣ b ^ (p * k - 1) - 1hk:k.Coprime pe:ZMod (p * k) ≃+* ZMod p × ZMod k := ZMod.chineseRemainder ⋯s:ZMod (p * k) := e.symm (↑g, 1)⊢ p - 1 ∣ p * k - 1
    have : NeZero k := ⟨fun _ => byp:ℕhp:Nat.Prime pthis:Fact (Nat.Prime p) := { out := hp }g:(ZMod p)ˣh✝:∀ (x : (ZMod p)ˣ), x ∈ Subgroup.zpowers gk:ℕha₁:1 < p * k ∧ ¬Nat.Prime (p * k)h:∀ (b : ℕ), 1 ≤ b → (p * k).Coprime b → p * k ∣ b ^ (p * k - 1) - 1h_forall:∀ (b : ℕ), 1 ≤ b → (p * k).Coprime b → p * k ∣ b ^ (p * k - 1) - 1hk:k.Coprime pe:ZMod (p * k) ≃+* ZMod p × ZMod k := ZMod.chineseRemainder ⋯s:ZMod (p * k) := e.symm (↑g, 1)x✝:k = 0⊢ False simp_allAll goals completed! 🐙⟩
    have : p * k ∣ (e.symm (g, 1)).val ^ (p * k - 1) - 1 := h_forall _ (ZMod.val_pos.2 (byp:ℕhp:Nat.Prime pthis✝:Fact (Nat.Prime p) := { out := hp }g:(ZMod p)ˣh✝:∀ (x : (ZMod p)ˣ), x ∈ Subgroup.zpowers gk:ℕha₁:1 < p * k ∧ ¬Nat.Prime (p * k)h:∀ (b : ℕ), 1 ≤ b → (p * k).Coprime b → p * k ∣ b ^ (p * k - 1) - 1h_forall:∀ (b : ℕ), 1 ≤ b → (p * k).Coprime b → p * k ∣ b ^ (p * k - 1) - 1hk:k.Coprime pe:ZMod (p * k) ≃+* ZMod p × ZMod k := ZMod.chineseRemainder ⋯s:ZMod (p * k) := e.symm (↑g, 1)this:NeZero k := 
  {
    out := fun x =>
      False.elim
        (Eq.mp
          (Eq.trans
            (congr
              (congrArg And
                (Eq.trans (congrArg (LT.lt 1) (Eq.trans (congrArg (HMul.hMul p) x) (mul_zero p))) not_lt_one._simp_2))
              (congrArg (fun x => ¬Nat.Prime x) (Eq.trans (congrArg (HMul.hMul p) x) (mul_zero p))))
            (false_and ¬Nat.Prime 0))
          ha₁) }⊢ e.symm (↑g, 1) ≠ 0 aesopAll goals completed! 🐙))
      ((ZMod.isUnit_iff_coprime _ _).1 (byp:ℕhp:Nat.Prime pthis✝:Fact (Nat.Prime p) := { out := hp }g:(ZMod p)ˣh✝:∀ (x : (ZMod p)ˣ), x ∈ Subgroup.zpowers gk:ℕha₁:1 < p * k ∧ ¬Nat.Prime (p * k)h:∀ (b : ℕ), 1 ≤ b → (p * k).Coprime b → p * k ∣ b ^ (p * k - 1) - 1h_forall:∀ (b : ℕ), 1 ≤ b → (p * k).Coprime b → p * k ∣ b ^ (p * k - 1) - 1hk:k.Coprime pe:ZMod (p * k) ≃+* ZMod p × ZMod k := ZMod.chineseRemainder ⋯s:ZMod (p * k) := e.symm (↑g, 1)this:NeZero k := 
  {
    out := fun x =>
      False.elim
        (Eq.mp
          (Eq.trans
            (congr
              (congrArg And
                (Eq.trans (congrArg (LT.lt 1) (Eq.trans (congrArg (HMul.hMul p) x) (mul_zero p))) not_lt_one._simp_2))
              (congrArg (fun x => ¬Nat.Prime x) (Eq.trans (congrArg (HMul.hMul p) x) (mul_zero p))))
            (false_and ¬Nat.Prime 0))
          ha₁) }⊢ IsUnit ↑(e.symm (↑g, 1)).val simp [Prod.isUnit_iff]All goals completed! 🐙)).symm
    simp_all [p.totient_prime, sub_eq_zero, ZMod.val_pos, ← ZMod.natCast_eq_zero_iff,
      ← map_pow, ← Units.val_pow_eq_pow_val, ← orderOf_dvd_iff_pow_eq_one,
      orderOf_eq_card_of_forall_mem_zpowers]All goals completed! 🐙
  ·refine_2a:ℕha₁:a.Compositeh:Squarefree a ∧ ∀ (p : ℕ), Nat.Prime p → p ∣ a → p - 1 ∣ a - 1b:ℕhb:b ≥ 1hab:a.Coprime b⊢ a.FermatPsp b obtain ⟨h_sqfr, h_dvd⟩ := hrefine_2a:ℕha₁:a.Compositeb:ℕhb:b ≥ 1hab:a.Coprime bh_sqfr:Squarefree ah_dvd:∀ (p : ℕ), Nat.Prime p → p ∣ a → p - 1 ∣ a - 1⊢ a.FermatPsp b
    simp_all [a.squarefree_iff_prime_squarefree, Nat.FermatPsp, Nat.ProbablePrime, Nat.Composite]refine_2a:ℕb:ℕha₁:1 < a ∧ ¬Nat.Prime ahb:1 ≤ bhab:a.Coprime bh_sqfr:∀ (x : ℕ), Nat.Prime x → ¬x * x ∣ ah_dvd:∀ (p : ℕ), Nat.Prime p → p ∣ a → p - 1 ∣ a - 1⊢ a ∣ b ^ (a - 1) - 1
    refine if hb : _ = 0 then ⟨0, hb⟩ else (a.factorization_le_iff_dvd ha₁.1.ne_bot hb).1 fun p => ?_refine_2a:ℕb:ℕha₁:1 < a ∧ ¬Nat.Prime ahb✝:1 ≤ bhab:a.Coprime bh_sqfr:∀ (x : ℕ), Nat.Prime x → ¬x * x ∣ ah_dvd:∀ (p : ℕ), Nat.Prime p → p ∣ a → p - 1 ∣ a - 1hb:¬b ^ (a - 1) - 1 = 0p:ℕ⊢ a.factorization p ≤ (b ^ (a - 1) - 1).factorization p
    by_cases hp : p.Primeposa:ℕb:ℕha₁:1 < a ∧ ¬Nat.Prime ahb✝:1 ≤ bhab:a.Coprime bh_sqfr:∀ (x : ℕ), Nat.Prime x → ¬x * x ∣ ah_dvd:∀ (p : ℕ), Nat.Prime p → p ∣ a → p - 1 ∣ a - 1hb:¬b ^ (a - 1) - 1 = 0p:ℕhp:Nat.Prime p⊢ a.factorization p ≤ (b ^ (a - 1) - 1).factorization pnega:ℕb:ℕha₁:1 < a ∧ ¬Nat.Prime ahb✝:1 ≤ bhab:a.Coprime bh_sqfr:∀ (x : ℕ), Nat.Prime x → ¬x * x ∣ ah_dvd:∀ (p : ℕ), Nat.Prime p → p ∣ a → p - 1 ∣ a - 1hb:¬b ^ (a - 1) - 1 = 0p:ℕhp:¬Nat.Prime p⊢ a.factorization p ≤ (b ^ (a - 1) - 1).factorization p
    ·posa:ℕb:ℕha₁:1 < a ∧ ¬Nat.Prime ahb✝:1 ≤ bhab:a.Coprime bh_sqfr:∀ (x : ℕ), Nat.Prime x → ¬x * x ∣ ah_dvd:∀ (p : ℕ), Nat.Prime p → p ∣ a → p - 1 ∣ a - 1hb:¬b ^ (a - 1) - 1 = 0p:ℕhp:Nat.Prime p⊢ a.factorization p ≤ (b ^ (a - 1) - 1).factorization p by_cases hpa : p ∣ aposa:ℕb:ℕha₁:1 < a ∧ ¬Nat.Prime ahb✝:1 ≤ bhab:a.Coprime bh_sqfr:∀ (x : ℕ), Nat.Prime x → ¬x * x ∣ ah_dvd:∀ (p : ℕ), Nat.Prime p → p ∣ a → p - 1 ∣ a - 1hb:¬b ^ (a - 1) - 1 = 0p:ℕhp:Nat.Prime phpa:p ∣ a⊢ a.factorization p ≤ (b ^ (a - 1) - 1).factorization pnega:ℕb:ℕha₁:1 < a ∧ ¬Nat.Prime ahb✝:1 ≤ bhab:a.Coprime bh_sqfr:∀ (x : ℕ), Nat.Prime x → ¬x * x ∣ ah_dvd:∀ (p : ℕ), Nat.Prime p → p ∣ a → p - 1 ∣ a - 1hb:¬b ^ (a - 1) - 1 = 0p:ℕhp:Nat.Prime phpa:¬p ∣ a⊢ a.factorization p ≤ (b ^ (a - 1) - 1).factorization p
      ·posa:ℕb:ℕha₁:1 < a ∧ ¬Nat.Prime ahb✝:1 ≤ bhab:a.Coprime bh_sqfr:∀ (x : ℕ), Nat.Prime x → ¬x * x ∣ ah_dvd:∀ (p : ℕ), Nat.Prime p → p ∣ a → p - 1 ∣ a - 1hb:¬b ^ (a - 1) - 1 = 0p:ℕhp:Nat.Prime phpa:p ∣ a⊢ a.factorization p ≤ (b ^ (a - 1) - 1).factorization p obtain ⟨w, h⟩ := h_dvd p hp hpaposa:ℕb:ℕha₁:1 < a ∧ ¬Nat.Prime ahb✝:1 ≤ bhab:a.Coprime bh_sqfr:∀ (x : ℕ), Nat.Prime x → ¬x * x ∣ ah_dvd:∀ (p : ℕ), Nat.Prime p → p ∣ a → p - 1 ∣ a - 1hb:¬b ^ (a - 1) - 1 = 0p:ℕhp:Nat.Prime phpa:p ∣ aw:ℕh:a - 1 = (p - 1) * w⊢ a.factorization p ≤ (b ^ (a - 1) - 1).factorization p
        obtain ⟨ha₁, ha₂⟩ := ha₁posa:ℕb:ℕhb✝:1 ≤ bhab:a.Coprime bh_sqfr:∀ (x : ℕ), Nat.Prime x → ¬x * x ∣ ah_dvd:∀ (p : ℕ), Nat.Prime p → p ∣ a → p - 1 ∣ a - 1hb:¬b ^ (a - 1) - 1 = 0p:ℕhp:Nat.Prime phpa:p ∣ aw:ℕh:a - 1 = (p - 1) * wha₁:1 < aha₂:¬Nat.Prime a⊢ a.factorization p ≤ (b ^ (a - 1) - 1).factorization p
        apply Nat.Prime.pow_dvd_iff_le_factorization hp hb |>.1posa:ℕb:ℕhb✝:1 ≤ bhab:a.Coprime bh_sqfr:∀ (x : ℕ), Nat.Prime x → ¬x * x ∣ ah_dvd:∀ (p : ℕ), Nat.Prime p → p ∣ a → p - 1 ∣ a - 1hb:¬b ^ (a - 1) - 1 = 0p:ℕhp:Nat.Prime phpa:p ∣ aw:ℕh:a - 1 = (p - 1) * wha₁:1 < aha₂:¬Nat.Prime a⊢ p ^ a.factorization p ∣ b ^ (a - 1) - 1
        have : a.factorization p ≤ 1 := not_lt.1 fun h =>
          h_sqfr p hp <| (sq p ▸ (pow_dvd_pow p h).trans (a.ordProj_dvd p))posa:ℕb:ℕhb✝:1 ≤ bhab:a.Coprime bh_sqfr:∀ (x : ℕ), Nat.Prime x → ¬x * x ∣ ah_dvd:∀ (p : ℕ), Nat.Prime p → p ∣ a → p - 1 ∣ a - 1hb:¬b ^ (a - 1) - 1 = 0p:ℕhp:Nat.Prime phpa:p ∣ aw:ℕh:a - 1 = (p - 1) * wha₁:1 < aha₂:¬Nat.Prime athis:a.factorization p ≤ 1 := not_lt.mp fun h => h_sqfr p hp (sq p ▸ Dvd.dvd.trans (pow_dvd_pow p h) (Nat.ordProj_dvd a p))⊢ p ^ a.factorization p ∣ b ^ (a - 1) - 1
        replace : a.factorization p = 1 :=
          this.antisymm (hp.dvd_iff_one_le_factorization (bya:ℕb:ℕhb✝:1 ≤ bhab:a.Coprime bh_sqfr:∀ (x : ℕ), Nat.Prime x → ¬x * x ∣ ah_dvd:∀ (p : ℕ), Nat.Prime p → p ∣ a → p - 1 ∣ a - 1hb:¬b ^ (a - 1) - 1 = 0p:ℕhp:Nat.Prime phpa:p ∣ aw:ℕh:a - 1 = (p - 1) * wha₁:1 < aha₂:¬Nat.Prime athis:a.factorization p ≤ 1 := not_lt.mp fun h => h_sqfr p hp (sq p ▸ Dvd.dvd.trans (pow_dvd_pow p h) (Nat.ordProj_dvd a p))⊢ a ≠ 0 grindAll goals completed! 🐙) |>.1 hpa)
        simp_rw [posa:ℕb:ℕhb✝:1 ≤ bhab:a.Coprime bh_sqfr:∀ (x : ℕ), Nat.Prime x → ¬x * x ∣ ah_dvd:∀ (p : ℕ), Nat.Prime p → p ∣ a → p - 1 ∣ a - 1hb:¬b ^ (a - 1) - 1 = 0p:ℕhp:Nat.Prime phpa:p ∣ aw:ℕh:a - 1 = (p - 1) * wha₁:1 < aha₂:¬Nat.Prime athis:a.factorization p = 1 := LE.le.antisymm _fvar.824206 ((Nat.Prime.dvd_iff_one_le_factorization hp (korselts_criterion._proof_10 a ha₁)).mp hpa)⊢ p ^ a.factorization p ∣ b ^ (a - 1) - 1this, pow_one, ← CharP.cast_eq_zero_iff (ZMod p)]
        have one_le_b_pow : 1 ≤ b ^ (a - 1) := bya:ℕha₁:a.Composite⊢ IsCarmichael a ↔ Squarefree a ∧ ∀ (p : ℕ), Nat.Prime p → p ∣ a → p - 1 ∣ a - 1 omegaAll goals completed! 🐙
        push_cast [one_le_b_pow]posa:ℕb:ℕhb✝:1 ≤ bhab:a.Coprime bh_sqfr:∀ (x : ℕ), Nat.Prime x → ¬x * x ∣ ah_dvd:∀ (p : ℕ), Nat.Prime p → p ∣ a → p - 1 ∣ a - 1hb:¬b ^ (a - 1) - 1 = 0p:ℕhp:Nat.Prime phpa:p ∣ aw:ℕh:a - 1 = (p - 1) * wha₁:1 < aha₂:¬Nat.Prime athis:a.factorization p = 1 := LE.le.antisymm _fvar.824206 ((Nat.Prime.dvd_iff_one_le_factorization hp (korselts_criterion._proof_10 a ha₁)).mp hpa)one_le_b_pow:1 ≤ b ^ (a - 1) := Decidable.byContradiction fun a_1 => korselts_criterion._proof_11 a b hb p w ha₁ a_1⊢ ↑b ^ (a - 1) - 1 = 0
        simp_rw [posa:ℕb:ℕhb✝:1 ≤ bhab:a.Coprime bh_sqfr:∀ (x : ℕ), Nat.Prime x → ¬x * x ∣ ah_dvd:∀ (p : ℕ), Nat.Prime p → p ∣ a → p - 1 ∣ a - 1hb:¬b ^ (a - 1) - 1 = 0p:ℕhp:Nat.Prime phpa:p ∣ aw:ℕh:a - 1 = (p - 1) * wha₁:1 < aha₂:¬Nat.Prime athis:a.factorization p = 1 := LE.le.antisymm _fvar.824206 ((Nat.Prime.dvd_iff_one_le_factorization hp (korselts_criterion._proof_10 a ha₁)).mp hpa)one_le_b_pow:1 ≤ b ^ (a - 1) := Decidable.byContradiction fun a_1 => korselts_criterion._proof_11 a b hb p w ha₁ a_1⊢ ↑b ^ (a - 1) - 1 = 0h, pow_mul]
        simp_all +decide [CharP.cast_eq_zero_iff _ p,
          hp.coprime_iff_not_dvd.1 (hab.of_dvd_left (bya:ℕb:ℕhb✝:1 ≤ bhab:a.Coprime bh_sqfr:∀ (x : ℕ), Nat.Prime x → ¬x * x ∣ ah_dvd:∀ (p : ℕ), Nat.Prime p → p ∣ a → p - 1 ∣ a - 1hb:¬b ^ (a - 1) - 1 = 0p:ℕhp:Nat.Prime phpa:p ∣ aw:ℕh:a - 1 = (p - 1) * wha₁:1 < aha₂:¬Nat.Prime athis:a.factorization p = 1 := LE.le.antisymm _fvar.824206 ((Nat.Prime.dvd_iff_one_le_factorization hp (korselts_criterion._proof_10 a ha₁)).mp hpa)one_le_b_pow:1 ≤ b ^ (a - 1) := Decidable.byContradiction fun a_1 => korselts_criterion._proof_11 a b hb p w ha₁ a_1⊢ p ∣ a aesopAll goals completed! 🐙)), ZMod.pow_card_sub_one_eq_one]
      ·nega:ℕb:ℕha₁:1 < a ∧ ¬Nat.Prime ahb✝:1 ≤ bhab:a.Coprime bh_sqfr:∀ (x : ℕ), Nat.Prime x → ¬x * x ∣ ah_dvd:∀ (p : ℕ), Nat.Prime p → p ∣ a → p - 1 ∣ a - 1hb:¬b ^ (a - 1) - 1 = 0p:ℕhp:Nat.Prime phpa:¬p ∣ a⊢ a.factorization p ≤ (b ^ (a - 1) - 1).factorization p simp [a.factorization_eq_zero_of_not_dvd hpa]All goals completed! 🐙
    ·nega:ℕb:ℕha₁:1 < a ∧ ¬Nat.Prime ahb✝:1 ≤ bhab:a.Coprime bh_sqfr:∀ (x : ℕ), Nat.Prime x → ¬x * x ∣ ah_dvd:∀ (p : ℕ), Nat.Prime p → p ∣ a → p - 1 ∣ a - 1hb:¬b ^ (a - 1) - 1 = 0p:ℕhp:¬Nat.Prime p⊢ a.factorization p ≤ (b ^ (a - 1) - 1).factorization p simp_allAll goals completed! 🐙


@[category test, AMS 11]
lemma isCarmichael_561 : IsCarmichael 561 := by⊢ IsCarmichael 561
  have h_comp : Nat.Composite 561 := by⊢ IsCarmichael 561
    dsimp [Nat.Composite]⊢ 1 < 561 ∧ ¬Nat.Prime 561
    constructorleft⊢ 1 < 561right⊢ ¬Nat.Prime 561 <;>left⊢ 1 < 561right⊢ ¬Nat.Prime 561 norm_numAll goals completed! 🐙
  apply (korselts_criterion 561 h_comp).mprh_comp:Nat.Composite 561 := 
  id
    ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561)) (Eq.refl false),
      Mathlib.Meta.NormNum.isNat_not_prime (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
        (Mathlib.Meta.NormNum.not_prime_mul_of_ble 3 187 561 (Eq.refl 561) (Eq.refl false) (Eq.refl false))⟩⊢ Squarefree 561 ∧ ∀ (p : ℕ), Nat.Prime p → p ∣ 561 → p - 1 ∣ 561 - 1
  constructorlefth_comp:Nat.Composite 561 := 
  id
    ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561)) (Eq.refl false),
      Mathlib.Meta.NormNum.isNat_not_prime (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
        (Mathlib.Meta.NormNum.not_prime_mul_of_ble 3 187 561 (Eq.refl 561) (Eq.refl false) (Eq.refl false))⟩⊢ Squarefree 561righth_comp:Nat.Composite 561 := 
  id
    ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561)) (Eq.refl false),
      Mathlib.Meta.NormNum.isNat_not_prime (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
        (Mathlib.Meta.NormNum.not_prime_mul_of_ble 3 187 561 (Eq.refl 561) (Eq.refl false) (Eq.refl false))⟩⊢ ∀ (p : ℕ), Nat.Prime p → p ∣ 561 → p - 1 ∣ 561 - 1
  ·lefth_comp:Nat.Composite 561 := 
  id
    ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561)) (Eq.refl false),
      Mathlib.Meta.NormNum.isNat_not_prime (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
        (Mathlib.Meta.NormNum.not_prime_mul_of_ble 3 187 561 (Eq.refl 561) (Eq.refl false) (Eq.refl false))⟩⊢ Squarefree 561 have h1 : 561 = 3 * 11 * 17 := by⊢ IsCarmichael 561 norm_numAll goals completed! 🐙
    rw [h1, Nat.squarefree_mul (by norm_num), Nat.squarefree_mul (by norm_num)]lefth_comp:Nat.Composite 561 := 
  id
    ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561)) (Eq.refl false),
      Mathlib.Meta.NormNum.isNat_not_prime (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
        (Mathlib.Meta.NormNum.not_prime_mul_of_ble 3 187 561 (Eq.refl 561) (Eq.refl false) (Eq.refl false))⟩h1:561 = 3 * 11 * 17 := 
  Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
    (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul)
      (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 11)) (Eq.refl 33))
      (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 17)) (Eq.refl 561))⊢ (Squarefree 3 ∧ Squarefree 11) ∧ Squarefree 17
    refine ⟨⟨(Nat.prime_iff.mp (byh_comp:Nat.Composite 561 := 
  id
    ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561)) (Eq.refl false),
      Mathlib.Meta.NormNum.isNat_not_prime (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
        (Mathlib.Meta.NormNum.not_prime_mul_of_ble 3 187 561 (Eq.refl 561) (Eq.refl false) (Eq.refl false))⟩h1:561 = 3 * 11 * 17 := 
  Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
    (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul)
      (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 11)) (Eq.refl 33))
      (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 17)) (Eq.refl 561))⊢ Nat.Prime 3 norm_numAll goals completed! 🐙 : Nat.Prime 3)).squarefree, (Nat.prime_iff.mp (byh_comp:Nat.Composite 561 := 
  id
    ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561)) (Eq.refl false),
      Mathlib.Meta.NormNum.isNat_not_prime (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
        (Mathlib.Meta.NormNum.not_prime_mul_of_ble 3 187 561 (Eq.refl 561) (Eq.refl false) (Eq.refl false))⟩h1:561 = 3 * 11 * 17 := 
  Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
    (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul)
      (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 11)) (Eq.refl 33))
      (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 17)) (Eq.refl 561))⊢ Nat.Prime 11 norm_numAll goals completed! 🐙 : Nat.Prime 11)).squarefree⟩, (Nat.prime_iff.mp (byh_comp:Nat.Composite 561 := 
  id
    ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561)) (Eq.refl false),
      Mathlib.Meta.NormNum.isNat_not_prime (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
        (Mathlib.Meta.NormNum.not_prime_mul_of_ble 3 187 561 (Eq.refl 561) (Eq.refl false) (Eq.refl false))⟩h1:561 = 3 * 11 * 17 := 
  Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
    (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul)
      (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 11)) (Eq.refl 33))
      (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 17)) (Eq.refl 561))⊢ Nat.Prime 17 norm_numAll goals completed! 🐙 : Nat.Prime 17)).squarefree⟩
  ·righth_comp:Nat.Composite 561 := 
  id
    ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561)) (Eq.refl false),
      Mathlib.Meta.NormNum.isNat_not_prime (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
        (Mathlib.Meta.NormNum.not_prime_mul_of_ble 3 187 561 (Eq.refl 561) (Eq.refl false) (Eq.refl false))⟩⊢ ∀ (p : ℕ), Nat.Prime p → p ∣ 561 → p - 1 ∣ 561 - 1 intro p hprighth_comp:Nat.Composite 561 := 
  id
    ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561)) (Eq.refl false),
      Mathlib.Meta.NormNum.isNat_not_prime (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
        (Mathlib.Meta.NormNum.not_prime_mul_of_ble 3 187 561 (Eq.refl 561) (Eq.refl false) (Eq.refl false))⟩p:ℕhp:Nat.Prime p⊢ p ∣ 561 → p - 1 ∣ 561 - 1 hp_dvdrighth_comp:Nat.Composite 561 := 
  id
    ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561)) (Eq.refl false),
      Mathlib.Meta.NormNum.isNat_not_prime (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
        (Mathlib.Meta.NormNum.not_prime_mul_of_ble 3 187 561 (Eq.refl 561) (Eq.refl false) (Eq.refl false))⟩p:ℕhp:Nat.Prime php_dvd:p ∣ 561⊢ p - 1 ∣ 561 - 1
    have h1 : 561 = 3 * (11 * 17) := by⊢ IsCarmichael 561 norm_numAll goals completed! 🐙
    rw [h1] at hp_dvdrighth_comp:Nat.Composite 561 := 
  id
    ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561)) (Eq.refl false),
      Mathlib.Meta.NormNum.isNat_not_prime (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
        (Mathlib.Meta.NormNum.not_prime_mul_of_ble 3 187 561 (Eq.refl 561) (Eq.refl false) (Eq.refl false))⟩p:ℕhp:Nat.Prime php_dvd:p ∣ 3 * (11 * 17)h1:561 = 3 * (11 * 17)⊢ p - 1 ∣ 561 - 1
    rcases (hp.dvd_mul.mp hp_dvd) with h3 | h11_17right.inlh_comp:Nat.Composite 561 := 
  id
    ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561)) (Eq.refl false),
      Mathlib.Meta.NormNum.isNat_not_prime (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
        (Mathlib.Meta.NormNum.not_prime_mul_of_ble 3 187 561 (Eq.refl 561) (Eq.refl false) (Eq.refl false))⟩p:ℕhp:Nat.Prime php_dvd:p ∣ 3 * (11 * 17)h1:561 = 3 * (11 * 17)h3:p ∣ 3⊢ p - 1 ∣ 561 - 1right.inrh_comp:Nat.Composite 561 := 
  id
    ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561)) (Eq.refl false),
      Mathlib.Meta.NormNum.isNat_not_prime (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
        (Mathlib.Meta.NormNum.not_prime_mul_of_ble 3 187 561 (Eq.refl 561) (Eq.refl false) (Eq.refl false))⟩p:ℕhp:Nat.Prime php_dvd:p ∣ 3 * (11 * 17)h1:561 = 3 * (11 * 17)h11_17:p ∣ 11 * 17⊢ p - 1 ∣ 561 - 1
    ·right.inlh_comp:Nat.Composite 561 := 
  id
    ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561)) (Eq.refl false),
      Mathlib.Meta.NormNum.isNat_not_prime (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
        (Mathlib.Meta.NormNum.not_prime_mul_of_ble 3 187 561 (Eq.refl 561) (Eq.refl false) (Eq.refl false))⟩p:ℕhp:Nat.Prime php_dvd:p ∣ 3 * (11 * 17)h1:561 = 3 * (11 * 17)h3:p ∣ 3⊢ p - 1 ∣ 561 - 1 have : p = 3 := ((byh_comp:Nat.Composite 561 := 
  id
    ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561)) (Eq.refl false),
      Mathlib.Meta.NormNum.isNat_not_prime (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
        (Mathlib.Meta.NormNum.not_prime_mul_of_ble 3 187 561 (Eq.refl 561) (Eq.refl false) (Eq.refl false))⟩p:ℕhp:Nat.Prime php_dvd:p ∣ 3 * (11 * 17)h1:561 = 3 * (11 * 17)h3:p ∣ 3⊢ Nat.Prime 3 norm_numAll goals completed! 🐙 : Nat.Prime 3).eq_one_or_self_of_dvd p h3).resolve_left hp.ne_one
      subst thisright.inlh_comp:Nat.Composite 561 := 
  id
    ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561)) (Eq.refl false),
      Mathlib.Meta.NormNum.isNat_not_prime (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
        (Mathlib.Meta.NormNum.not_prime_mul_of_ble 3 187 561 (Eq.refl 561) (Eq.refl false) (Eq.refl false))⟩h1:561 = 3 * (11 * 17)hp:Nat.Prime 3hp_dvd:3 ∣ 3 * (11 * 17)h3:3 ∣ 3⊢ 3 - 1 ∣ 561 - 1; norm_numAll goals completed! 🐙
    ·right.inrh_comp:Nat.Composite 561 := 
  id
    ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561)) (Eq.refl false),
      Mathlib.Meta.NormNum.isNat_not_prime (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
        (Mathlib.Meta.NormNum.not_prime_mul_of_ble 3 187 561 (Eq.refl 561) (Eq.refl false) (Eq.refl false))⟩p:ℕhp:Nat.Prime php_dvd:p ∣ 3 * (11 * 17)h1:561 = 3 * (11 * 17)h11_17:p ∣ 11 * 17⊢ p - 1 ∣ 561 - 1 rcases (hp.dvd_mul.mp h11_17) with h11 | h17right.inr.inlh_comp:Nat.Composite 561 := 
  id
    ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561)) (Eq.refl false),
      Mathlib.Meta.NormNum.isNat_not_prime (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
        (Mathlib.Meta.NormNum.not_prime_mul_of_ble 3 187 561 (Eq.refl 561) (Eq.refl false) (Eq.refl false))⟩p:ℕhp:Nat.Prime php_dvd:p ∣ 3 * (11 * 17)h1:561 = 3 * (11 * 17)h11_17:p ∣ 11 * 17h11:p ∣ 11⊢ p - 1 ∣ 561 - 1right.inr.inrh_comp:Nat.Composite 561 := 
  id
    ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561)) (Eq.refl false),
      Mathlib.Meta.NormNum.isNat_not_prime (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
        (Mathlib.Meta.NormNum.not_prime_mul_of_ble 3 187 561 (Eq.refl 561) (Eq.refl false) (Eq.refl false))⟩p:ℕhp:Nat.Prime php_dvd:p ∣ 3 * (11 * 17)h1:561 = 3 * (11 * 17)h11_17:p ∣ 11 * 17h17:p ∣ 17⊢ p - 1 ∣ 561 - 1
      ·right.inr.inlh_comp:Nat.Composite 561 := 
  id
    ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561)) (Eq.refl false),
      Mathlib.Meta.NormNum.isNat_not_prime (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
        (Mathlib.Meta.NormNum.not_prime_mul_of_ble 3 187 561 (Eq.refl 561) (Eq.refl false) (Eq.refl false))⟩p:ℕhp:Nat.Prime php_dvd:p ∣ 3 * (11 * 17)h1:561 = 3 * (11 * 17)h11_17:p ∣ 11 * 17h11:p ∣ 11⊢ p - 1 ∣ 561 - 1 have : p = 11 := ((byh_comp:Nat.Composite 561 := 
  id
    ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561)) (Eq.refl false),
      Mathlib.Meta.NormNum.isNat_not_prime (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
        (Mathlib.Meta.NormNum.not_prime_mul_of_ble 3 187 561 (Eq.refl 561) (Eq.refl false) (Eq.refl false))⟩p:ℕhp:Nat.Prime php_dvd:p ∣ 3 * (11 * 17)h1:561 = 3 * (11 * 17)h11_17:p ∣ 11 * 17h11:p ∣ 11⊢ Nat.Prime 11 norm_numAll goals completed! 🐙 : Nat.Prime 11).eq_one_or_self_of_dvd p h11).resolve_left hp.ne_one
        subst thisright.inr.inlh_comp:Nat.Composite 561 := 
  id
    ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561)) (Eq.refl false),
      Mathlib.Meta.NormNum.isNat_not_prime (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
        (Mathlib.Meta.NormNum.not_prime_mul_of_ble 3 187 561 (Eq.refl 561) (Eq.refl false) (Eq.refl false))⟩h1:561 = 3 * (11 * 17)hp:Nat.Prime 11hp_dvd:11 ∣ 3 * (11 * 17)h11_17:11 ∣ 11 * 17h11:11 ∣ 11⊢ 11 - 1 ∣ 561 - 1; norm_numAll goals completed! 🐙
      ·right.inr.inrh_comp:Nat.Composite 561 := 
  id
    ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561)) (Eq.refl false),
      Mathlib.Meta.NormNum.isNat_not_prime (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
        (Mathlib.Meta.NormNum.not_prime_mul_of_ble 3 187 561 (Eq.refl 561) (Eq.refl false) (Eq.refl false))⟩p:ℕhp:Nat.Prime php_dvd:p ∣ 3 * (11 * 17)h1:561 = 3 * (11 * 17)h11_17:p ∣ 11 * 17h17:p ∣ 17⊢ p - 1 ∣ 561 - 1 have : p = 17 := ((byh_comp:Nat.Composite 561 := 
  id
    ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561)) (Eq.refl false),
      Mathlib.Meta.NormNum.isNat_not_prime (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
        (Mathlib.Meta.NormNum.not_prime_mul_of_ble 3 187 561 (Eq.refl 561) (Eq.refl false) (Eq.refl false))⟩p:ℕhp:Nat.Prime php_dvd:p ∣ 3 * (11 * 17)h1:561 = 3 * (11 * 17)h11_17:p ∣ 11 * 17h17:p ∣ 17⊢ Nat.Prime 17 norm_numAll goals completed! 🐙 : Nat.Prime 17).eq_one_or_self_of_dvd p h17).resolve_left hp.ne_one
        subst thisright.inr.inrh_comp:Nat.Composite 561 := 
  id
    ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561)) (Eq.refl false),
      Mathlib.Meta.NormNum.isNat_not_prime (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 561))
        (Mathlib.Meta.NormNum.not_prime_mul_of_ble 3 187 561 (Eq.refl 561) (Eq.refl false) (Eq.refl false))⟩h1:561 = 3 * (11 * 17)hp:Nat.Prime 17hp_dvd:17 ∣ 3 * (11 * 17)h11_17:17 ∣ 11 * 17h17:17 ∣ 17⊢ 17 - 1 ∣ 561 - 1; norm_numAll goals completed! 🐙

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

@[category research solved, AMS 11]
theorem declaration uses 'sorry'isStrongGiuga_iff {a : ℕ} (ha : a.Composite) :
    IsStrongGiuga a ↔ IsCarmichael a ∧ ∃ n : ℕ, ∑ p ∈ a.primeFactors, (1 / p : ℚ) - 1 / a = n := bya:ℕha:a.Composite⊢ IsStrongGiuga a ↔ IsCarmichael a ∧ ∃ n, ∑ p ∈ a.primeFactors, 1 / ↑p - 1 / ↑a = ↑n
  sorryAll goals completed! 🐙

Every strong Giuga number is a Carmichael number.

@[category research solved, AMS 11]
theorem declaration uses 'sorry'agoh_giuga.variants.isStrongGiuga_implies_isCarmichael
    (a : ℕ) (ha : IsStrongGiuga a) : IsCarmichael a := bya:ℕha:IsStrongGiuga a⊢ IsCarmichael a
  sorryAll goals completed! 🐙

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

@[category research solved, AMS 11]
theorem declaration uses 'sorry'agoh_giuga.variants.le_primeFactors_card_of_isStrongGiuga
    (a : ℕ) (ha : IsStrongGiuga a) : 9 ≤ a.primeFactors.card := bya:ℕha:IsStrongGiuga a⊢ 9 ≤ a.primeFactors.card
  sorryAll goals completed! 🐙

Giuga showed that a counterexample Giuga number has at least 1000 digits. Ref: G. Giuga, Su una presumibile proprieta caratteristica dei numeri primi

@[category research solved, AMS 11]
theorem declaration uses 'sorry'agoh_giuga.variants._1000_le_digits_length_of_isStrongGiuga
    (a : ℕ) (ha : IsStrongGiuga a) : 1000 ≤ (Nat.digits 10 a).length := bya:ℕha:IsStrongGiuga a⊢ 1000 ≤ (Nat.digits 10 a).length
  sorryAll goals completed! 🐙

Bedocchi showed that any Giuga number has at least 1700 digits. Ref: E. Bedocchi, Note on a conjecture about prime numbers

@[category research solved, AMS 11]
theorem declaration uses 'sorry'agoh_giuga.variants._1700_le_digits_length_of_isStrongGiuga
    (a : ℕ) (ha : IsStrongGiuga a) :
    (Nat.digits 10 a).length > 1700 := bya:ℕha:IsStrongGiuga a⊢ (Nat.digits 10 a).length > 1700
  sorryAll goals completed! 🐙

Borwein, Borwein, Borwein and Girgensohn showed that any strong Giuga number has at least 13000 digits. Ref: D. Borwein, J. M. Borwein, P. B. Borwein, and R. Girgensohn, Giuga’s conjecture on primality

@[category research solved, AMS 11]
theorem declaration uses 'sorry'agoh_giuga.variants._13000_le_digits_length_of_isStrongGiuga
    (a : ℕ) (ha : IsStrongGiuga a) : 13000 ≤ (Nat.digits 10 a).length := bya:ℕha:IsStrongGiuga a⊢ 13000 ≤ (Nat.digits 10 a).length
  sorryAll goals completed! 🐙


open Classical in

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

@[category research solved, AMS 11]
theorem declaration uses 'sorry'agoh_giuga.variants.isStrongGiuga_growth
    (G : ℕ → ℕ) (hG : G = fun x => Finset.Icc 1 x |>.filter IsStrongGiuga |>.card) :
    ∃ N O, ∀ n ≥ N, G n ≤ O * (n : ℝ).sqrt * (n : ℝ).log := byG:ℕ → ℕhG:G = fun x => (Finset.filter IsStrongGiuga (Finset.Icc 1 x)).card⊢ ∃ N O, ∀ n ≥ N, ↑(G n) ≤ O * √↑n * Real.log ↑n
  sorryAll goals completed! 🐙


end AgohGiuga