The board / number theory / #12
Erdős Problem #12
OPENdatabase updated 2025-08-31
No proof or disproof is known, and it isn't known whether a finite computation could settle it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
A set `A` is "good" if it is infinite and there are no distinct `a,b,c` in `A` such that `a ∣ (b+c)` and `b > a`, `c > a`.
Let \(A\) be an infinite set such that there are no distinct \(a,b,c \in A\) such that \(a \mid (b+c)\) and \(b,c > a\). Is there such an \(A\) with \(\liminf \frac{|A \cap \{1, \dotsc, N\}|}{N^{1/2}} > 0\) ? The DeepMind prover agent has found a formal proof of this statement.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 7 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/12.Prizenone
Topicsnumber theory
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/12
Attempts
submit one →Read our working report →
Proved an elementary cylinder-budget theorem forcing convergence for the regular oriented-CRT block template used in the live comments, and exactly computed the finite harmonic optima M(N)=3/2 through
PARTIAL