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_
Actions
Submit a Proof
Have a proof attempt? Submit it for zero-trust verification.
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
