Erdős problem 726 · problems.science

As $n\to \infty$ ranges over integers $\sum_{p\leq n}1_{n\in (p/2,p)\pmod{p}}\frac{1}{p}\sim \frac{\log\log n}{2}$ ?

Sources

Browse retained paths and inspect the exact material available for this Problem.

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

726.lean

Retained formal statement1 of 2

As $n\to \infty$ ranges over integers $\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\in (p/2,p)\pmod{p}$ we mean $n\equiv r\pmod{p}$ for some integer $r$ with $p/2<r<p$ .

FormalConjectures/ErdosProblems/726.leanErdos726.erdos_7264 linesExact file

1True ↔2  Asymptotics.IsEquivalent Filter.atTop3    (fun n => ∑ p ∈ Finset.range (n + 1) with Nat.Prime p ∧ ↑p / 2 < ↑n % ↑p, 1 / ↑p) fun n =>4    Real.log (Real.log ↑n) / 2

OpenStatement only, no proof

Sources

Search problems.science