Skip to content

Erdős problem 443

Let m,n1m,n\geq 1. What is #{k(mk):1km/2}{l(nl):1ln/2}?\# \{ k(m-k) : 1\leq k\leq m/2\} \cap \{ l(n-l) : 1\leq l\leq n/2\}? Is it (mn)o(1)\leq (mn)^{o(1)} for all sufficiently large m,nm,n?

Sources

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

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

443.lean

Retained formal statement2 of 2

Let m,n1m,n\geq 1. What is #{k(mk):1km/2}{l(nl):1ln/2}?\# \{ k(m-k) : 1\leq k\leq m/2\} \cap \{ l(n-l) : 1\leq l\leq n/2\}? Is it (mn)o(1)\leq (mn)^{o(1)} for all sufficiently large m,nm,n?

This was solved independently by Hegyvári [He25] and Cambie (unpublished), who show that if m>nm>n then the set in question has size mO(1/loglogm),\leq m^{O(1/\log\log m)}, and that for any integer ss there exist infinitely many pairs (m,n)(m,n) such that the set in question has size ss.

FormalConjectures/ErdosProblems/443.leanErdos443.erdos_443.parts.ii1 lineExact file
True ↔ ∀ (ε : ℝ), 0 < ε → ∃ n₀, ∀ (m n : ℕ), n₀ < nn < m → ↑(Erdos443.A nErdos443.A m).card < (↑m * ↑n) ^ ε
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.

Search problems.science

Find a Problem, Result, source, or page