Skip to content

Erdős problem 726

Start work

As n→∞n\to \infty ranges over integers ∑p≤n1n∈(p/2,p)(modp)1p∼log⁡log⁡n2\sum_{p\leq n}1_{n\in (p/2,p)\pmod{p}}\frac{1}{p}\sim \frac{\log\log n}{2}?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

726.lean

Retained formal statement1 of 2

As n→∞n\to \infty ranges over integers ∑p≤n1n∈(p/2,p)(modp)1p∼log⁡log⁡n2\sum_{p\leq n}1_{n\in (p/2,p)\pmod{p}}\frac{1}{p}\sim \frac{\log\log n}{2}?

A conjecture of Erdős, Graham, Ruzsa, and Straus [EGRS75].

By n∈(p/2,p)(modp)n\in (p/2,p)\pmod{p} we mean n≡r(modp)n\equiv r\pmod{p} for some integer rr with p/2<r<pp/2<r<p.

FormalConjectures/ErdosProblems/726.leanErdos726.erdos_7264 linesExact file
True ↔  Asymptotics.IsEquivalent Filter.atTop    (fun n => ∑ p ∈ Finset.range (n + 1) with Nat.Prime p ∧ ↑p / 2 < ↑n % ↑p, 1 / ↑p) fun n =>    Real.log (Real.log ↑n) / 2
OpenStatement only, no proof