---

Claim. Van Doorn's Theorem 2 (p. 3 of the note) states that every $S\subseteq\{1,\ldots,n\}$ with $|S|\ge9n/10+\log(n)^3+1$ contains distinct $x,y,z$ with $1/x+1/y=1/z$. For the extremal function of Problem 302 this gives

$$f(N)<\frac{9N}{10}+(\log N)^3+1 ,$$

the upper bound $f(N)\le(9/10+o(1))N$ that the site records. The proof (pp. 3--4) counts disjoint dilates of the triples $\{2,3,6\}$ and $\{4,5,20\}$, each a solution, each of which a solution-free set must miss in at least one element; more than $n/10-\log(n)^3-1$ such triples are pairwise disjoint.

Covers. An upper bound for the estimate of $f(N)$. Not covered: the asymptotic constant, which the recorded bounds place between $5/8$ and $25/28$; the note does not touch the particular question, which Cambie's construction answers.

Standing. Claimed. The site's curator, Thomas Bloom, states in the problem's commentary that van Doorn has proved the bound and links the note, but the site labels the problem OPEN and lists no parts, so the credit is not an acceptance and no reviewed evidence is listed. The archived copy of the page of 25 March 2025 already credits the bound to an unpublished note, so the result predates its public posting; the note was published by the author in their GitHub repository on 11 August 2025 (the file's single commit, linked above), the date this page carries. The note is undated in its text, has no arXiv version, no journal record and no independent review, so there is no refereed evidence; no Lean built by this corpus checks it, so there is no formalized evidence, and the formal-conjectures statement file's variant for this bound, upper_nine_tenths, cites the note with a sorry body. The library's source card cites the note, of which no file is held; the statement was read clause by clause and the proof for structure, with the inequalities of its Lemma 4 not rechecked.