Back to Problems

erdos_971.variants.infinite_sequence

Specification

Erdős [Er49c] proved that the statement in `erdos_971` holds for infinitely many values of `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.infinite_sequence :
    ∃ c > (0 : ℝ), ∃ C > (0 : ℝ),
      {d : ℕ | C * (d.totient : ℝ) ≤
        #{a < d | a.Coprime d ∧ (leastCongruentPrime a d : ℝ) > (1 + c) * d.totient * log d}}.Infinite
ID: ErdosProblems__971__erdos_971.variants.infinite_sequence
Browse 300 unsolved math conjectures formalized in Lean 4
Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →
ASI Prize documentation for formal verification pipeline
Docs

Verification Pipeline

How zero-trust verification works.

Read docs →
Evaluation Results

Recent Submissions

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