erdos_971.variants.many_small

Specification

Erdős [Er49c] proved that for any `ε > 0` we have `p(a, d) < ε * φ(d) * log d` for `≫_ε φ(d)` many values of `a` (for all large `d`). [Er49c] Erdős, P., _On some applications of Brun's method_. Acta Univ. Szeged. Sect. Sci. Math. (1949), 57--63.

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof

Lean 4 Statement

theorem erdos_971.variants.many_small :
    ∀ ε > (0 : ℝ), ∃ C > (0 : ℝ), ∀ᶠ d in atTop,
      C * (d.totient : ℝ) ≤
        #{a < d | a.Coprime d ∧ (leastCongruentPrime a d : ℝ) < ε * d.totient * log d}

ID: ErdosProblems__971__erdos_971.variants.many_small

Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →

Docs

Verification Pipeline

How zero-trust verification works.

Read docs →

Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.