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 satisfies 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 agoh_giuga : AgohGiugaCongr := by⊢ AgohGiugaCongr
  sorryAll goals completed! 🐙

The Agoh-Giuga Conjecture, Giuga's formulation

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

The two statements of the conjecture are equivalent.

@[category research solved, AMS 11]
theorem 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 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 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⊢ 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)⊢ ¬((p * p * N).Coprime (p * N + 1) → p * p * N ∣ (p * N + 1) ^ (p * p * N - 1) - 1)
  rw [mul_assocp:ℕ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)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)] 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,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)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)) ← geom_sum_mul_of_one_le ((1).le_add_left (p * N)),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) ∣ (∑ i ∈ Finset.range (p * (p * N) - 1), (p * N + 1) ^ i) * (p * N + 1 - 1))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)) p.coprime_mul_iff_leftp:ℕ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))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))]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⊢ p - 1 ∣ a - 1
    have : Fact p.Prime := ⟨hp⟩refine_1a:ℕha₁:a.Compositeh:IsCarmichael ap:ℕhp:Nat.Prime phpa:p ∣ ah_forall:IsCarmichael athis:Fact (Nat.Prime p)⊢ 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 athis:Fact (Nat.Prime p)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)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 - 1refine_1p:ℕhp:Nat.Prime pthis:Fact (Nat.Prime p)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⊢ p - 1 ∣ p * k - 1
      by_contra hkp:ℕhp:Nat.Prime pthis:Fact (Nat.Prime p)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⊢ Falserefine_1p:ℕhp:Nat.Prime pthis:Fact (Nat.Prime p)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⊢ p - 1 ∣ p * k - 1
      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)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⊢ Falserefine_1p:ℕhp:Nat.Prime pthis:Fact (Nat.Prime p)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⊢ p - 1 ∣ p * k - 1
      absurd (squarefree_of_isCarmichael ha₁ h)p:ℕhp:Nat.Prime pthis:Fact (Nat.Prime p)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✝))refine_1p:ℕhp:Nat.Prime pthis:Fact (Nat.Prime p)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⊢ p - 1 ∣ p * k - 1
      simp [← mul_assoc, mul_comm, Nat.squarefree_mul_iff, ← sq, Nat.squarefree_pow_iff hp.ne_one]refine_1p:ℕhp:Nat.Prime pthis:Fact (Nat.Prime p)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⊢ p - 1 ∣ p * k - 1refine_1p:ℕhp:Nat.Prime pthis:Fact (Nat.Prime p)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⊢ p - 1 ∣ p * k - 1
    simp_all [IsCarmichael, Nat.FermatPsp, Nat.ProbablePrime, Nat.Composite]refine_1p:ℕhp:Nat.Prime pthis:Fact (Nat.Prime p)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)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)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)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⊢ Falserefine_1p:ℕhp:Nat.Prime pthis✝:Fact (Nat.Prime p)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⊢ p - 1 ∣ p * k - 1 simp_allAll goals completed! 🐙refine_1p:ℕhp:Nat.Prime pthis✝:Fact (Nat.Prime p)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⊢ p - 1 ∣ p * k - 1⟩refine_1p:ℕhp:Nat.Prime pthis✝:Fact (Nat.Prime p)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⊢ p - 1 ∣ p * k - 1
    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)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⊢ e.symm (↑g, 1) ≠ 0refine_1p:ℕhp:Nat.Prime pthis✝¹:Fact (Nat.Prime p)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 kthis:p * k ∣ (e.symm (↑g, 1)).val ^ (p * k - 1) - 1⊢ p - 1 ∣ p * k - 1 aesopAll goals completed! 🐙refine_1p:ℕhp:Nat.Prime pthis✝¹:Fact (Nat.Prime p)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 kthis:p * k ∣ (e.symm (↑g, 1)).val ^ (p * k - 1) - 1⊢ p - 1 ∣ p * k - 1))
      ((ZMod.isUnit_iff_coprime _ _).1 (byp:ℕhp:Nat.Prime pthis✝:Fact (Nat.Prime p)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⊢ IsUnit ↑(e.symm (↑g, 1)).valrefine_1p:ℕhp:Nat.Prime pthis✝¹:Fact (Nat.Prime p)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 kthis:p * k ∣ (e.symm (↑g, 1)).val ^ (p * k - 1) - 1⊢ p - 1 ∣ p * k - 1 simp [Prod.isUnit_iff]All goals completed! 🐙refine_1p:ℕhp:Nat.Prime pthis✝¹:Fact (Nat.Prime p)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 kthis:p * k ∣ (e.symm (↑g, 1)).val ^ (p * k - 1) - 1⊢ p - 1 ∣ p * k - 1)).symmrefine_1p:ℕhp:Nat.Prime pthis✝¹:Fact (Nat.Prime p)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 kthis:p * k ∣ (e.symm (↑g, 1)).val ^ (p * k - 1) - 1⊢ p - 1 ∣ p * k - 1
    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⊢ 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⊢ a ≠ 0posa:ℕ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⊢ p ^ a.factorization p ∣ b ^ (a - 1) - 1 grindAll goals completed! 🐙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⊢ p ^ a.factorization p ∣ b ^ (a - 1) - 1) |>.1 hpa)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⊢ p ^ a.factorization p ∣ b ^ (a - 1) - 1
        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⊢ p ^ a.factorization p ∣ b ^ (a - 1) - 1this,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⊢ p ^ 1 ∣ b ^ (a - 1) - 1 pow_one,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⊢ p ∣ b ^ (a - 1) - 1 ← CharP.cast_eq_zero_iff (ZMod 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⊢ ↑(b ^ (a - 1) - 1) = 0]
        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 - 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 athis:a.factorization p = 1one_le_b_pow:1 ≤ b ^ (a - 1)⊢ ↑(b ^ (a - 1) - 1) = 0 omegaposa:ℕ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 = 1one_le_b_pow:1 ≤ b ^ (a - 1)⊢ ↑(b ^ (a - 1) - 1) = 0posa:ℕ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 = 1one_le_b_pow:1 ≤ b ^ (a - 1)⊢ ↑(b ^ (a - 1) - 1) = 0
        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 = 1one_le_b_pow:1 ≤ b ^ (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 = 1one_le_b_pow:1 ≤ b ^ (a - 1)⊢ ↑b ^ (a - 1) - 1 = 0h,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 = 1one_le_b_pow:1 ≤ b ^ (a - 1)⊢ ↑b ^ ((p - 1) * w) - 1 = 0 pow_mulposa:ℕ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 = 1one_le_b_pow:1 ≤ b ^ (a - 1)⊢ (↑b ^ (p - 1)) ^ w - 1 = 0]
        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 = 1one_le_b_pow:1 ≤ b ^ (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
    dsimp [Nat.Composite]⊢ 1 < 561 ∧ ¬Nat.Prime 561h_comp:Nat.Composite 561⊢ IsCarmichael 561
    constructorleft⊢ 1 < 561right⊢ ¬Nat.Prime 561h_comp:Nat.Composite 561⊢ IsCarmichael 561 <;>left⊢ 1 < 561right⊢ ¬Nat.Prime 561h_comp:Nat.Composite 561⊢ IsCarmichael 561 norm_numh_comp:Nat.Composite 561⊢ IsCarmichael 561h_comp:Nat.Composite 561⊢ IsCarmichael 561
  apply (korselts_criterion 561 h_comp).mprh_comp:Nat.Composite 561⊢ Squarefree 561 ∧ ∀ (p : ℕ), Nat.Prime p → p ∣ 561 → p - 1 ∣ 561 - 1
  constructorlefth_comp:Nat.Composite 561⊢ Squarefree 561righth_comp:Nat.Composite 561⊢ ∀ (p : ℕ), Nat.Prime p → p ∣ 561 → p - 1 ∣ 561 - 1
  ·lefth_comp:Nat.Composite 561⊢ Squarefree 561 have h1 : 561 = 3 * 11 * 17 := by⊢ IsCarmichael 561lefth_comp:Nat.Composite 561h1:561 = 3 * 11 * 17⊢ Squarefree 561 norm_numlefth_comp:Nat.Composite 561h1:561 = 3 * 11 * 17⊢ Squarefree 561lefth_comp:Nat.Composite 561h1:561 = 3 * 11 * 17⊢ Squarefree 561
    rw [h1,lefth_comp:Nat.Composite 561h1:561 = 3 * 11 * 17⊢ Squarefree (3 * 11 * 17)lefth_comp:Nat.Composite 561h1:561 = 3 * 11 * 17⊢ (Squarefree 3 ∧ Squarefree 11) ∧ Squarefree 17 Nat.squarefree_mul (byh_comp:Nat.Composite 561h1:561 = 3 * 11 * 17⊢ (3 * 11).Coprime 17lefth_comp:Nat.Composite 561h1:561 = 3 * 11 * 17⊢ (Squarefree 3 ∧ Squarefree 11) ∧ Squarefree 17 norm_numAll goals completed! 🐙lefth_comp:Nat.Composite 561h1:561 = 3 * 11 * 17⊢ (Squarefree 3 ∧ Squarefree 11) ∧ Squarefree 17), Nat.squarefree_mul (byh_comp:Nat.Composite 561h1:561 = 3 * 11 * 17⊢ Nat.Coprime 3 11lefth_comp:Nat.Composite 561h1:561 = 3 * 11 * 17⊢ (Squarefree 3 ∧ Squarefree 11) ∧ Squarefree 17 norm_numAll goals completed! 🐙lefth_comp:Nat.Composite 561h1:561 = 3 * 11 * 17⊢ (Squarefree 3 ∧ Squarefree 11) ∧ Squarefree 17)]lefth_comp:Nat.Composite 561h1:561 = 3 * 11 * 17⊢ (Squarefree 3 ∧ Squarefree 11) ∧ Squarefree 17
    refine ⟨⟨(Nat.prime_iff.mp (byh_comp:Nat.Composite 561h1:561 = 3 * 11 * 17⊢ Nat.Prime 3 norm_numAll goals completed! 🐙 : Nat.Prime 3)).squarefree, (Nat.prime_iff.mp (byh_comp:Nat.Composite 561h1:561 = 3 * 11 * 17⊢ Nat.Prime 11 norm_numAll goals completed! 🐙 : Nat.Prime 11)).squarefree⟩, (Nat.prime_iff.mp (byh_comp:Nat.Composite 561h1:561 = 3 * 11 * 17⊢ Nat.Prime 17 norm_numAll goals completed! 🐙 : Nat.Prime 17)).squarefree⟩
  ·righth_comp:Nat.Composite 561⊢ ∀ (p : ℕ), Nat.Prime p → p ∣ 561 → p - 1 ∣ 561 - 1 intro p hp hp_dvdrighth_comp:Nat.Composite 561p:ℕhp:Nat.Prime php_dvd:p ∣ 561⊢ p - 1 ∣ 561 - 1
    have h1 : 561 = 3 * (11 * 17) := by⊢ IsCarmichael 561righth_comp:Nat.Composite 561p:ℕhp:Nat.Prime php_dvd:p ∣ 561h1:561 = 3 * (11 * 17)⊢ p - 1 ∣ 561 - 1 norm_numrighth_comp:Nat.Composite 561p:ℕhp:Nat.Prime php_dvd:p ∣ 561h1:561 = 3 * (11 * 17)⊢ p - 1 ∣ 561 - 1righth_comp:Nat.Composite 561p:ℕhp:Nat.Prime php_dvd:p ∣ 561h1:561 = 3 * (11 * 17)⊢ p - 1 ∣ 561 - 1
    rw [h1righth_comp:Nat.Composite 561p:ℕhp:Nat.Prime php_dvd:p ∣ 3 * (11 * 17)h1:561 = 3 * (11 * 17)⊢ p - 1 ∣ 561 - 1righth_comp:Nat.Composite 561p:ℕhp:Nat.Prime php_dvd:p ∣ 3 * (11 * 17)h1:561 = 3 * (11 * 17)⊢ p - 1 ∣ 561 - 1] at hp_dvdrighth_comp:Nat.Composite 561p:ℕ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 561p:ℕ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 561p:ℕ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 561p:ℕ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 561p:ℕhp:Nat.Prime php_dvd:p ∣ 3 * (11 * 17)h1:561 = 3 * (11 * 17)h3:p ∣ 3⊢ Nat.Prime 3right.inlh_comp:Nat.Composite 561p:ℕhp:Nat.Prime php_dvd:p ∣ 3 * (11 * 17)h1:561 = 3 * (11 * 17)h3:p ∣ 3this:p = 3⊢ p - 1 ∣ 561 - 1 norm_numAll goals completed! 🐙right.inlh_comp:Nat.Composite 561p:ℕhp:Nat.Prime php_dvd:p ∣ 3 * (11 * 17)h1:561 = 3 * (11 * 17)h3:p ∣ 3this:p = 3⊢ p - 1 ∣ 561 - 1 : Nat.Prime 3).eq_one_or_self_of_dvd p h3).resolve_left hp.ne_oneright.inlh_comp:Nat.Composite 561p:ℕhp:Nat.Prime php_dvd:p ∣ 3 * (11 * 17)h1:561 = 3 * (11 * 17)h3:p ∣ 3this:p = 3⊢ p - 1 ∣ 561 - 1
      subst thisright.inlh_comp:Nat.Composite 561h1: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 561p:ℕ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 561p:ℕ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 561p:ℕ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 561p:ℕ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 561p:ℕhp:Nat.Prime php_dvd:p ∣ 3 * (11 * 17)h1:561 = 3 * (11 * 17)h11_17:p ∣ 11 * 17h11:p ∣ 11⊢ Nat.Prime 11right.inr.inlh_comp:Nat.Composite 561p:ℕhp:Nat.Prime php_dvd:p ∣ 3 * (11 * 17)h1:561 = 3 * (11 * 17)h11_17:p ∣ 11 * 17h11:p ∣ 11this:p = 11⊢ p - 1 ∣ 561 - 1 norm_numAll goals completed! 🐙right.inr.inlh_comp:Nat.Composite 561p:ℕhp:Nat.Prime php_dvd:p ∣ 3 * (11 * 17)h1:561 = 3 * (11 * 17)h11_17:p ∣ 11 * 17h11:p ∣ 11this:p = 11⊢ p - 1 ∣ 561 - 1 : Nat.Prime 11).eq_one_or_self_of_dvd p h11).resolve_left hp.ne_oneright.inr.inlh_comp:Nat.Composite 561p:ℕhp:Nat.Prime php_dvd:p ∣ 3 * (11 * 17)h1:561 = 3 * (11 * 17)h11_17:p ∣ 11 * 17h11:p ∣ 11this:p = 11⊢ p - 1 ∣ 561 - 1
        subst thisright.inr.inlh_comp:Nat.Composite 561h1: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 561p:ℕ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 561p:ℕhp:Nat.Prime php_dvd:p ∣ 3 * (11 * 17)h1:561 = 3 * (11 * 17)h11_17:p ∣ 11 * 17h17:p ∣ 17⊢ Nat.Prime 17right.inr.inrh_comp:Nat.Composite 561p:ℕhp:Nat.Prime php_dvd:p ∣ 3 * (11 * 17)h1:561 = 3 * (11 * 17)h11_17:p ∣ 11 * 17h17:p ∣ 17this:p = 17⊢ p - 1 ∣ 561 - 1 norm_numAll goals completed! 🐙right.inr.inrh_comp:Nat.Composite 561p:ℕhp:Nat.Prime php_dvd:p ∣ 3 * (11 * 17)h1:561 = 3 * (11 * 17)h11_17:p ∣ 11 * 17h17:p ∣ 17this:p = 17⊢ p - 1 ∣ 561 - 1 : Nat.Prime 17).eq_one_or_self_of_dvd p h17).resolve_left hp.ne_oneright.inr.inrh_comp:Nat.Composite 561p:ℕhp:Nat.Prime php_dvd:p ∣ 3 * (11 * 17)h1:561 = 3 * (11 * 17)h11_17:p ∣ 11 * 17h17:p ∣ 17this:p = 17⊢ p - 1 ∣ 561 - 1
        subst thisright.inr.inrh_comp:Nat.Composite 561h1: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 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 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 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 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 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 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 scoped 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 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