---

Claim. Let $f(N)$ be the extremal function of Problem 302, defined, as in the formal-conjectures statement file, through the predicate IsMaxNoTripleCard. The linked repository declares the Lean theorems Erdos302ReflectiveUpper.limsup_le_0_8461739827964010 and Erdos302ReflectiveUpper.eventually_le_0_8461739827964010, which state

$$\limsup_{N\to\infty}\frac{f(N)}{N}\le\frac{8461739827964010}{10^{16}},$$

and, equivalently, $f(N)\le(8461739827964010/10^{16}+\varepsilon)N$ for every $\varepsilon>0$ and all large $N$. The README gives the underlying constant as an exact rational $C=0.8461739827964009\ldots$ and the route: $[1,N]$ splits into disjoint scaled blocks of smooth numbers over a finite set of primes; a priority recurrence over a chain of $20$ prime sets, from $\{3\}$ up to the primes to $71$, bounds from below the number of elements a triple-free set must omit from each block, with corrections justified by $1{,}298$ branch-and-bound certificates checked in the kernel by decide +kernel; summing over the blocks gives $|A|\le CN+53{,}896{,}239$ for every triple-free $A\subseteq\{1,\ldots,N\}$. The constant is below $25/28$, Schuh's $373/420$ and Khanukov's $140803024/163562355\approx0.86085$, and is the smallest claimed.

Submission note. Posted to the site's forum by Kenta Kitamura on 25 September 2026:

I, Kenta Kitamura (KitaKen1 on GitHub), have submitted to Formal Conjectures a Lean-verified upper bound for Problem #302. Together with Cambie's lower bound, the bounds are now $(5/8+o(1))N \leq f(N) \leq (0.8461739827964010+o(1))N.$ The upper bound improves van Doorn's $9/10$.

The formal statement, proof, and verification materials are available at the links below.

GitHub: KitaKen1/erdos-302-upper-bound Formal Conjectures submission: PR #6580 Lean4Web: open the standalone proof (Lean/mathlib v4.35.0-rc2).

Verification: both complete proof versions passed Lean compilation, and the standalone file also runs in Lean4Web. For the final theorems, '#print axioms' reports only 'propext', 'Classical.choice', and 'Quot.sound'; no 'sorryAx'.

AI Usage Disclosure: This formalization, computer-assisted proof development, documentation, and repository packaging were developed by Kenta Kitamura (KitaKen1), with assistance from ChatGPT and OpenAI Codex using GPT-6 Astra, and Claude Code using Claude Opus 5.5.

Note: The upper bound also improves those in the proof claims for this problem on this forum, $373/420 \approx 0.888$ and $140803024/163562355 \approx 0.8609$.

Covers. The upper bound $\limsup f(N)/N\le0.8461739827964010$ only. It does not bear on the particular question, which Cambie's construction answers in the negative, and it does not determine the constant.

Standing. Claimed. The claimant is Kenta Kitamura, who announced the bound in the site's discussion thread on 25 September 2026; the post and the README say that the work was done with assistance from ChatGPT and OpenAI Codex using GPT-6 Astra, and Claude Code using Claude Opus 5.5. The README reports that both versions of the proof compile with no sorry and with the axioms propext, Classical.choice and Quot.sound only, and says that the proof has not been reviewed independently by a human expert. The formal-conjectures statement file, at the linked commit of 27 September 2026, adds the variant erdos_302.variants.upper_0_8461739827964010 with a sorry body and a formal_proof annotation pointing at this repository; that annotation is not an acceptance. The Lean is not among the Lean this corpus built and audited, so no formalized evidence is listed. The site's label is OPEN.