The board / number theory / #443
Erdős Problem #443
PROVED LEANdatabase updated 2026-02-04
The statement as posed is true, and a proof exists. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
The set \(\{k(m-k) : 1\leq k\leq m/2\}\), where `m / 2` is `ℕ` floor division.
Let \(m,n\geq 1\). What is \[\# \{ k(m-k) : 1\leq k\leq m/2\} \cap \{ l(n-l) : 1\leq l\leq n/2\}?\] Can it be arbitrarily large? This was solved independently by Hegyvári [He25] and Cambie (unpublished), who show that if \(m>n\) then the set in question has size \[\leq m^{O(1/\log\log m)},\] and that for any integer \(s\) there exist infinitely many pairs \((m,n)\) such that the set in question has size \(s\).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/443.Prizenone
Topicsnumber theory
Statement in LeanFormal Conjectures
Solution in Leanyes
OEISA401140
Original pageerdosproblems.com/443
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.