Erdős Problem 1057

References:

• erdosproblems.com/1057
• [AGP94] Alford, W. R. and Granville, Andrew and Pomerance, Carl, There are infinitely many Carmichael numbers. Ann. of Math. (2) (1994), 703--722.
• [Er56c] Erdős, P., On pseudoprimes and Carmichael numbers. Publ. Math. Debrecen (1956), 201--206.
• [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437.
• [Ha08] Harman, Glyn, Watt's mean value theorem and Carmichael numbers. Int. J. Number Theory (2008), 241--248.
• [Li22] J. D. Lichtman, Primes in arithmetic progressions to large moduli and shifted primes without large prime factors. arXiv:2211.09641 (2022).
• [Po89] Pomerance, Carl, Two methods in elementary analytic number theory. (1989), 135--161.

noncomputable def Erdos1057.carmichaelCounting (x : ℝ) : ℝ

Let $C(x)$ count the number of Carmichael numbers in the interval $[1,x]$.

Equations

• Erdos1057.carmichaelCounting x = ↑{n : ℕ | IsCarmichael n ∧ ↑n ≤ x}.ncard

theorem Erdos1057.erdos_1057 : sorry ↔ Filter.Tendsto (fun (x : ℝ) => Real.log (carmichaelCounting x) / Real.log x) Filter.atTop (nhds 1)

Is it true that $C(x)=x^{1-o(1)}$?

This is discussed in problem A13 of Guy's collection [Gu04].

theorem Erdos1057.erdos_1057.variants.upper_bound : ∃ c > 0, ∀ᶠ (x : ℝ) in Filter.atTop, carmichaelCounting x < x * Real.exp (-c * (Real.log x * Real.log (Real.log (Real.log x))) / Real.log (Real.log x))

Erdős [Er56c] proved $C(x) < x \exp\left(-c \frac{\log x\log\log\log x}{\log\log x}\right)$ for some constant $c>0$.

theorem Erdos1057.erdos_1057.variants.pomerance : sorry ↔ Filter.Tendsto (fun (x : ℝ) => -(Real.log (carmichaelCounting x / x) * Real.log (Real.log x)) / (Real.log x * Real.log (Real.log (Real.log x)))) Filter.atTop (nhds 1)

Pomerance [Po89] gave a heuristic suggesting that this is the true order of growth, and in fact $C(x)= x \exp\left(-(1+o(1))\frac{\log x\log\log\log x}{\log\log x}\right)$.

theorem Erdos1057.erdos_1057.variants.agp_infinite : Filter.Tendsto carmichaelCounting Filter.atTop Filter.atTop

Alford, Granville, and Pomerance [AGP94] proved that $C(x)\to \infty$.

theorem Erdos1057.erdos_1057.variants.agp_lower_bound : ∀ᶠ (x : ℝ) in Filter.atTop, carmichaelCounting x > x ^ (2 / 7)

Alford, Granville, and Pomerance [AGP94] proved that $C(x)>x^{2/7}$ for large $x$.

theorem Erdos1057.erdos_1057.variants.harman_lower_bound : ∀ᶠ (x : ℝ) in Filter.atTop, carmichaelCounting x > x ^ 0.33336704

The lower bound $C(x)> x^{0.33336704}$ was proved by Harman [Ha08].

theorem Erdos1057.erdos_1057.variants.lichtman_lower_bound : ∀ᶠ (x : ℝ) in Filter.atTop, carmichaelCounting x > x ^ 0.3389

This exponent was improved to $0.3389$ by Lichtman [Li22].