The board / number theory / #793
Erdős Problem #793
PROVED LEANdatabase updated 2025-08-31
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).
A finite set `A ⊆ ℕ` is *strongly 2-primitive* if `a ∤ b * c` whenever `a, b, c ∈ A` with `a ≠ b` and `a ≠ c`.
`F n` is the maximal size of a strongly 2-primitive subset of `{1, …, n}`.
Let \(F(n)\) be the maximum possible size of a subset \(A \subseteq \{1, \ldots, n\}\) such that \(a \nmid bc\) whenever \(a, b, c \in A\) with \(a \neq b\) and \(a \neq c\). Is there a constant \(c\) such that \[F(n) = \pi(n) + (c + o(1)) n^{2/3} (\log n)^{-2}?\] A problem of Erdős [Er69, Er70b], who proved in [Er38] that \(F(n) = \pi(n) + O(n^{2/3} (\log n)^{-2})\). The answer is yes, with \(c = 27/2\): this was proved by GPT-5.6 Sol (prompted by Chojecki), refining the argument of [Er38]; see `erdos_793.variants.constant`.
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/793.Prizenone
Topicsnumber theory
Statement in LeanFormal Conjectures
Solution in Leanyes
OEISA399779
Original pageerdosproblems.com/793
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.