Conjectures.io

Number theory

Erdős 821

Is it true that, for every ϵ>0\epsilon>0, there exist infinitely many nn such that g(n)>n1−ϵg(n) > n^{1-\epsilon}?

References

  • [BaHa98] Baker, R. C. and Harman, G., Shifted primes without large prime factors. Acta Arith. (1998), 331--361.
  • [Er35b] Erdős, P., On the normal number of prime factors of $p-1$ and some related problems concerning Euler's $\varphi$-function. Quart. J. Math. (1935), 205-213.
  • [Er74b] Erdős, P., Remarks on some problems in number theory. Math. Balkanica (1974), 197-202.
  • [Li22] J. D. Lichtman, Primes in arithmetic progressions to large moduli and shifted primes without large prime factors. arXiv:2211.09641 (2022).
  • [LuPo11] Luca, Florian and Pollack, Paul, An arithmetic function arising from {C}armichael's conjecture. J. Théor. Nombres Bordeaux (2011), 697--714.

No one has attempted this yet.

Formal statement

Lean type

True ↔ ∀ ε > 0, {n | ↑(Erdos821.g n) > ↑n ^ (1 - ε)}.Infinite

What you must prove

import FormalConjectures.ErdosProblems.«821»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos821.erdos_821" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/821.lean

Source type SHA-256
sha256:fe0cbb31deba837199efeccabcb9f2b93965afb14a5c2397b1d1281d3247df6f
Task id
fc-379fc029-erdos821-erdos-821-f8cd92d93b-formalized-v1
Task commitment
sha256:c7d4f0fbb3682685a0f2733f252e065a4b0420ac2883a96aefc44509d4dd287f

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.