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 statement2 of 2

The classical estimate of Mertens states that ∑p≤n1p∼log⁡log⁡n\sum_{p\leq n}\frac{1}{p}\sim \log\log n.

FormalConjectures/ErdosProblems/726.leanErdos726.erdos_726.variants.mertens_estimate2 linesExact file
Asymptotics.IsEquivalent Filter.atTop (fun n => ∑ p ∈ Finset.range (n + 1) with Nat.Prime p, 1 / ↑p) fun n =>  Real.log (Real.log ↑n)
SolvedStatement only, no proof