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

FormalConjectures/ErdosProblems/

726.lean

Retained formal statement2 of 2

The classical estimate of Mertens states that $\sum_{p\leq n}\frac{1}{p}\sim \log\log n$ .

FormalConjectures/ErdosProblems/726.leanErdos726.erdos_726.variants.mertens_estimate2 linesExact file

1Asymptotics.IsEquivalent Filter.atTop (fun n => ∑ p ∈ Finset.range (n + 1) with Nat.Prime p, 1 / ↑p) fun n =>2  Real.log (Real.log ↑n)

SolvedStatement only, no proof