Erdős problem 538

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

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

538.lean

Retained formal statement2 of 2

The reciprocal sum has matching order Θ_r(log N / loglog N): an explicit upper bound for every admissible A, together with a witnessing construction achieving the same order. This pins the order (up to the one iterated-logarithm factor) but not the sharp constant asked for in erdos_538.

FormalConjectures/ErdosProblems/538.leanErdos538.erdos_538.matching_order9 linesExact file

1∀ (r N : ℕ),2  2 ≤ r →3    2 ≤ N →4      (∀ (A : Finset ℕ),5          Erdos538.Admissible r N A →6            Real.log (Real.log (↑N + 1)) * ↑(Erdos538.reciprocalMass A) ≤ 2 * ↑r * (1 + Real.log (↑N * ↑N))) ∧7        ∃ A,8          Erdos538.Admissible r N A ∧9            Real.log (↑N + 1) ≤ 4 + 8192 * (↑(Nat.log 2 (Nat.log 2 N)) + 1) * ↑(Erdos538.reciprocalMass A)

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.