Carmichael numbers

DefinitionCarmichael numbers#✓fully proved

A natural number \(n\) is a Carmichael number if \(n > 1\), \(n\) is not prime, and \(a^n \equiv a \pmod{n}\) for every natural number \(a\).

def Nat.IsCarmichaelNumber (n : ℕ) : Prop :=
  1 < n ∧ ¬n.Prime ∧ ∀ a : ℕ, a ^ n ≡ a [MOD n]

Used by 4

Used byKorselt's criterion · Carmichael numbers via the residue ring · Alahmadi–Luca theorem on Carmichael numbers · Fermat-type characterizations of twin primes

TheoremCarmichael numbers via the residue ring#✓fully proved

A natural number \(n\) is a Carmichael number if and only if \(n > 1\), \(n\) is not prime, and \(x^n = x\) for every element \(x\) of \(\mathbb{Z}/n\mathbb{Z}\).

theorem Nat.isCarmichaelNumber_iff_zmod (n : ℕ) :
    Nat.IsCarmichaelNumber n ↔
      1 < n ∧ ¬n.Prime ∧ ∀ x : ZMod n, x ^ n = x

Uses 1 · Used by 1

Statement usesCarmichael numbers

Used byKorselt's criterion

TheoremKorselt's criterion#✓fully proved

A natural number \(n > 1\) is a Carmichael number if and only if \(n\) is squarefree, \(p - 1\) divides \(n - 1\) for every prime divisor \(p\) of \(n\), and \(n\) is not prime.

theorem Nat.isCarmichaelNumber_iff_korselt (n : ℕ) (hn : 1 < n) :
    Nat.IsCarmichaelNumber n ↔
      Squarefree n ∧
        (∀ p : ℕ, p.Prime → p ∣ n → (p - 1) ∣ (n - 1)) ∧ ¬n.Prime

Uses 2

Statement usesCarmichael numbers

Proof usesCarmichael numbers via the residue ring

TheoremInfinitely many Carmichael numbers with a prime number of prime factors (conditional)#●ready to prove

Suppose there is a real constant \(C\) such that for every natural number \(d \ge 2\) and every natural number \(c\) coprime to \(d\) there is a prime \(p \equiv c \pmod{d}\) with \(p \le C d (\log d)^2\) (Heath-Brown's conjecture on the least prime in an arithmetic progression). Then there are infinitely many Carmichael numbers \(n\) whose number of prime factors counted with multiplicity, \(\Omega(n)\), is prime.

public theorem_wanted infinite_carmichael_prime_cardFactors_of_heathBrown
    (hHB : ∃ C : ℝ, ∀ d : ℕ, 2 ≤ d → ∀ c : ℕ, Nat.Coprime c d →
      ∃ p : ℕ, p.Prime ∧ p ≡ c [MOD d] ∧ (p : ℝ) ≤ C * d * Real.log d ^ 2) :
    {n : ℕ | n.IsCarmichael ∧ (ArithmeticFunction.cardFactors n).Prime}.Infinite

Sources

• Thomas Wright, Carmichael Numbers with a Prime Number of Prime Factors, INTEGERS 24 (2024), Article A97, Theorem 1; the hypothesis is the paper's Conjecture 3.

TheoremAlford–Granville–Pomerance count of zero-sum subsequences#●ready to prove

Let \(G\) be an abelian group and let \(n\) be the least natural number \(m\) such that every sequence of \(m\) elements of \(G\) has a nonempty subsequence with product \(1\) (the Davenport constant of \(G\)). Let \(r\) and \(t\) be natural numbers with \(n < t < r\). Then for every sequence \(s_1, \dots, s_r\) of elements of \(G\), the number \(M\) of sets \(S \subseteq \{1, \dots, r\}\) with \(t - n \le |S| \le t\) and \(\prod_{i \in S} s_i = 1\) satisfies \(\binom{r}{t} \le \binom{r}{n} M\).

public theorem_wanted choose_le_choose_mul_card_prod_eq_one {G : Type*} [CommGroup G]
    [DecidableEq G] (n : ℕ)
    (hn : IsLeast {m : ℕ | ∀ s : Fin m → G, ∃ S : Finset (Fin m), S.Nonempty ∧
      ∏ i ∈ S, s i = 1} n)
    (r t : ℕ) (hrt : t < r) (htn : n < t) (s : Fin r → G) :
    r.choose t ≤ r.choose n *
      (Finset.univ.filter fun S : Finset (Fin r) =>
        t - n ≤ S.card ∧ S.card ≤ t ∧ ∏ i ∈ S, s i = 1).card

Sources

• Thomas Wright, Carmichael Numbers with a Prime Number of Prime Factors, INTEGERS 24 (2024), Article A97, Proposition 1, quoting Alford, Granville, and Pomerance, Theorem 2.1.

TheoremLinnik's theorem with exponent 5.2 (Xylouris)#●ready to prove

There is a real constant \(C\) such that for every natural number \(d \ge 1\) and every natural number \(c\) coprime to \(d\), there is a prime \(p \equiv c \pmod{d}\) with \(p \le C d^{5.2}\).

public theorem_wanted exists_prime_modEq_le_rpow_five_point_two :
    ∃ C : ℝ, ∀ d : ℕ, 1 ≤ d → ∀ c : ℕ, Nat.Coprime c d →
      ∃ p : ℕ, p.Prime ∧ p ≡ c [MOD d] ∧ (p : ℝ) ≤ C * (d : ℝ) ^ (5.2 : ℝ)

Sources

• Thomas Wright, Carmichael Numbers with a Prime Number of Prime Factors, INTEGERS 24 (2024), Article A97, Theorem 4, quoting Xylouris.

TheoremMany primes \(q\) with \(q - 1\) smooth#●ready to prove

Let \(1 < \theta < 2\). There are real constants \(\gamma > 0\) and \(Y\) such that for every real \(y > Y\), the number of primes \(q\) with \(y^\theta / \log y \le q \le y^\theta\) such that every prime divisor of \(q - 1\) is at most \(y\) is at least \(\gamma y^\theta / \log(y^\theta)\).

public theorem_wanted exists_card_smooth_shifted_primes_ge (θ : ℝ) (hθ : θ ∈ Set.Ioo 1 2) :
    ∃ γ Y : ℝ, 0 < γ ∧ ∀ y : ℝ, Y < y →
      γ * y ^ θ / Real.log (y ^ θ) ≤
        ({q : ℕ | q.Prime ∧ y ^ θ / Real.log y ≤ q ∧ (q : ℝ) ≤ y ^ θ ∧
          ∀ p : ℕ, p.Prime → p ∣ q - 1 → (p : ℝ) ≤ y}.ncard : ℝ)

Sources

• Thomas Wright, Carmichael Numbers with a Prime Number of Prime Factors, INTEGERS 24 (2024), Article A97, Lemma 1, quoting Lemma 5.1 of Matomäki and Lemma 2.1 of Wright.

TheoremCarmichael numbers with a prime number of prime factors in a range#●ready to prove

Assume Heath-Brown's conjecture in the following form: there is a real constant \(C\) such that for every natural number \(d \ge 2\) and every natural number \(c\) coprime to \(d\) there is a prime \(p \equiv c \pmod{d}\) with \(p \le C d (\log d)^2\). Let \(1 < \theta < 2\), and let \(\gamma > 0\) be such that for all sufficiently large real \(y\), the number of primes \(q\) with \(y^\theta / \log y \le q \le y^\theta\) such that every prime divisor of \(q - 1\) is at most \(y\) is at least \(\gamma y^\theta / \log(y^\theta)\). Then there is a real \(Y\) such that for every real \(y > Y\) there is a Carmichael number \(n\) with \(e^{(\gamma/4) y^\theta \log y} \le n \le e^{e^{19 \theta y}}\) whose number of prime factors counted with multiplicity, \(\Omega(n)\), is prime.

The paper's proof uses its Lemma 2, which assumes Heath-Brown's conjecture (the paper's Conjecture 3); here that assumption is an explicit hypothesis, as in Theorem 1.

public theorem_wanted exists_carmichael_prime_cardFactors_between_of_heathBrown
    (hHB : ∃ C : ℝ, ∀ d : ℕ, 2 ≤ d → ∀ c : ℕ, Nat.Coprime c d →
      ∃ p : ℕ, p.Prime ∧ p ≡ c [MOD d] ∧ (p : ℝ) ≤ C * d * Real.log d ^ 2)
    (θ : ℝ) (hθ : θ ∈ Set.Ioo 1 2) (γ : ℝ) (hγ : 0 < γ)
    (hQ : ∃ Y : ℝ, ∀ y : ℝ, Y < y →
      γ * y ^ θ / Real.log (y ^ θ) ≤
        ({q : ℕ | q.Prime ∧ y ^ θ / Real.log y ≤ q ∧ (q : ℝ) ≤ y ^ θ ∧
          ∀ p : ℕ, p.Prime → p ∣ q - 1 → (p : ℝ) ≤ y}.ncard : ℝ)) :
    ∃ Y : ℝ, ∀ y : ℝ, Y < y → ∃ n : ℕ, n.IsCarmichael ∧
      (ArithmeticFunction.cardFactors n).Prime ∧
      Real.exp (γ / 4 * y ^ θ * Real.log y) ≤ n ∧
      (n : ℝ) ≤ Real.exp (Real.exp (19 * θ * y))

Sources

• Thomas Wright, Carmichael Numbers with a Prime Number of Prime Factors, INTEGERS 24 (2024), Article A97, Theorem 3.

3 fully proved5 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.