---

Claim. Let $f(N)$ be the extremal function of Problem 302. The manuscript Two-sided computer-assisted progress on Erdős Problem 302 states two results. First, there are $\delta>0$ and $N_0$ with $f(N)\ge(5/8+\delta)N$ for all $N\ge N_0$: the set of Della Pietra's claim on Problem 301, which has density above $1/2$ and no relation of any length, is padded with all odd integers up to $N/4$, and the manuscript's lemma says that the padded set is still free of two-term relations. Second,

$$\limsup_{N\to\infty}\frac{f(N)}{N}\le\frac{140803024}{163562355}\approx0.86085 ,$$

below the recorded $9/10$ and below $25/28$, by a finite exact rational certificate at the modulus $Q=139{,}708{,}800$, described as $719$ divisor vertices, $12{,}675$ reciprocal-triple edges and $2{,}016$ embedded gadgets, whose forced omissions are summed over dilates as in the earlier upper-bound arguments.

Submission note. Posted to erdosproblems.com as a proof claim by Dmitry Khanukov (account khanukov) on 13 September 2026, giving "GPT-6 Astra, GPT-5.6 Sol" as the AI used:

Lower bound 5/8 becomes 5/8 + δ (>0) (Della Pietra's proof of Problem 301 and add all odd numbers up to a quarter of N) Upper bound 9/10 becomes ~0.86085, exactly 140803024/163562355 Full Lean 4 formalizations and the finite certificate are included in GitHub

Covers. A lower bound strictly above $5/8$ and an upper bound strictly below $9/10$ for the asymptotic density, both as estimates; the particular question is answered in the negative by Cambie's construction, a pending claim. Not covered: the asymptotic constant.

Depends on. Della Pietra's lower bound for Problem 301 supplies the set that the lower bound pads; the manuscript imports that development's Lean proof terms at pinned commits, and its lower bound stands or falls with that pending claim.

Standing. Claimed. The claimant is Dmitry Khanukov, who filed the claim as partial on the site's proof-claim tab on 13 September 2026 naming the systems GPT-6 Astra and GPT-5.6 Sol; the repository says that the finite packing was found by AI-assisted search and that AI systems assisted with code, proof audits and the Lean formalization. The result was first released on 16 August 2026 as the repository's version 0.1.0, with the same two constants; version 0.1.1 of 18 August 2026 added a comparison with Wang's manuscript on Problem 301, and version 0.2.0 of 13 September 2026, the one the tab links and this page carries as the preprint, added the end-to-end kernel-checked chain for the upper bound; the odd-quarter padding lemma behind the lower bound is already Lemma 3 of version 0.1.0. The repository describes the work as preliminary and unrefereed and says that its formalizations are not independent review; it has no arXiv version, no journal record and no independent review, and no comment stands under the claim. The claimant reports Lean 4 theorems for both bounds with no sorry and the axioms propext, Classical.choice and Quot.sound only, the lower bound importing Della Pietra's development as checked proof terms; only the statements were consulted; nothing was built, and the repository gives no formalized evidence. The site's label is OPEN, and the tab's standing notice says that listing a claim implies no examination.