---

Claim. For the zero-inclusive threshold cofactorThreshold of formal-conjectures (the largest $m$ such that every $n$-element finite set of natural numbers has at least $m$ values $a/\gcd(a,b)$), the file lean/Erdos539SqrtFC.lean of the public repository KitaKen1/erdos-539-sqrt-disproof at its commit of 5 September 2026 states threshold_div_sqrt_tendsto, that $h(n)/\sqrt n\to\infty$, with no hypothesis, and derives from it the negative answers to the two formal-conjectures variants asking whether $h(n)=O(\sqrt n)$ and whether $h(n)=\Theta(\sqrt n)$. If sound, the Erdős--Szemerédi lower bound $h(n)\gg n^{1/2}$ is not sharp in order. The README describes the argument as a weak form of the polynomial Freiman--Ruzsa theorem, vendored from the public teorth/pfr project, combined with an induction on dimension in the Granville--Roesler vector form, and discloses that OpenAI Codex assisted with the proof development, formalization and exposition; the README revision of the same day at the repository's head names the system as OpenAI Codex (GPT-6 Astra).

Covers. The lower bound $h(n)/\sqrt n\to\infty$, a bound proved if the development is sound; it shows that the Erdős--Szemerédi lower bound of order $\sqrt n$ on Granville and Roesler's claim page is not the truth and answers the formal-conjectures variants $h(n)=O(\sqrt n)$ and $h(n)=\Theta(\sqrt n)$ in the negative, questions neither the site nor Erdős asks. Not covered: any explicit rate of growth of $h(n)/\sqrt n$, and the order of $h(n)$ itself, which the exponent result on the preprint's claim page confines to $n^{1/2+o(1)}$ and nothing confines further.

Provenance. The repository is public under the GitHub account KitaKen1; the lakefile of its sibling repository names Kenta Kitamura as copyright holder, and this page takes that name for the claimant. The formal-conjectures file at the pinned commit of 2026-09-18 carries the two negative answers as research solved variants with formal_proof attributes naming lines 36--39 and 41--44 of the file. This corpus has not built, replayed or audited the development, no statement-fidelity review exists, and no kernel credit is claimed.

Standing. Claimed. No paper states the result: the site's commentary (page last edited 15 June 2026) records only the exponent $1/2$, its thread does not mention this development, its proof-claim tab was empty on 2026-10-07, and no registry entry, refereed version or independent review was found. The README itself says that the exact order of $h(n)$ remains undetermined.

Depends on. No page of this wiki.