Skip to content

Erdős problem 538

If each integer has at most rr representations m=pam = pa with pp prime and a∈A⊆[1,N]a \in A \subseteq [1, N], what is the best upper bound for ∑a∈A1/a\sum_{a \in A} 1/a? The candidate proof gives the matching order Θr(log⁡N/log⁡log⁡N)\Theta_r(\log N / \log\log N).

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

538.lean

Retained formal statement1 of 2

Let r≥2r\geq 2 and suppose that A⊆{1,…,N}A\subseteq\{1,\ldots,N\} is such that, for any mm, there are at most rr solutions to m=pam=pa where pp is prime and a∈Aa\in A. Give the best possible upper bound for ∑n∈A1n\sum_{n\in A}\frac{1}{n}.

The order is known — ∑ 1/n = Θ_r(log N / loglog N) (see erdos_538.matching_order) — but the sharp constant is not. This asks whether maxMass r N has a well-defined leading constant c_r in c_r · log N / loglog N.

FormalConjectures/ErdosProblems/538.leanErdos538.erdos_5386 linesExact file
True ↔  ∀ (r : ℕ),    2 ≤ r →      ∃ c,        0 < c ∧          Filter.Tendsto (fun N => Erdos538.maxMass r N * Real.log (Real.log ↑N) / Real.log ↑N) Filter.atTop (nhds c)
OpenStatement only, no proof