---

Claim. For every integer $k\ge3$,

$$\chi_S\bigl(n,\lfloor n^2/4\rfloor+1,C_{2k+1}\bigr)=\frac{n^2}{8}+o(n^2) \qquad(n\to\infty),$$

where $\chi_S(n,e,G)$ is the least $r$ for which some simple graph with $n$ vertices and exactly $e$ edges has an $r$-coloring of its edges under which every copy of $G$ has pairwise distinct edge colors; this is the question of Problem 809 in the affirmative for every $k$ it asks about. The result is the project's claim L17, whose Lean surface states the question in erdosproblems.com's exact-edge form. The seven-cycle case is the project's own argument, a palette-savings proof followed in the research guide; the cases $k\ge4$ are the theorem of Bucić, Chen and Ma, formalized natively, and a subgraph restriction carries the result to exactly $\lfloor n^2/4\rfloor+1$ edges. The claim determines $\chi_S$ at no fixed $n$ and says nothing about $C_3$ or $C_5$. The development was public on GitHub from 24 September 2026 (see Priority below). It was posted to the erdosproblems.com proof-claims tab under the name Plasma AI, from the account jacobparish, on 27 September 2026, as erdosproblems.com's proof claim 367, filed after Asad Shahab's independent proof claim 358 of the same day, and registered on the Palomar registry on 30 September 2026 as PALOMAR-2026-09-30-000004 (theorem Erdos809.main_result, trust level high, automated review outcome neutral), which pins the repository at the linked commit. The posting also announces a second result outside this page and not part of L17: for the seven-cycle at every fixed edge density $q=e/n^2$ with $1/4<q<1/2$, the Bucić–Chen–Ma formula fails, with explicit lower and upper bounds and the exact coefficient left open. The research notes record the lower bound and the construction as the paper's results, not independently reviewed. The write-up is the paper linked from the posting (preprint link, pinned to the same commit). Later commits to the repository, up to the one that the research evidence compares, changed the paper's author line and one broken citation in it, the README, formalization.yaml, the toolchain and lake files and the Lean files, which moved to the module system, and added a Palomar preflight workflow; the paper's last change is eb385a8 of 29 September 2026, the version the research evidence holds.

Submission note. Posted to erdosproblems.com as a proof claim by Plasma AI (account jacobparish) on 27 September 2026, giving "GPT-6 Astra, Claude Fable 5.1" as the AI used:

Great work Asad! The team at Plasma AI and I independently found a proof of the $k=3$ case and have formalized it in Lean, together with the $k\ge4$ proof of Bucić, Chen, and Ma. We also investigate the asymptotic number of colors as the density $q=e/n^2$ increases above the Turán threshold. For odd cycles of length at least nine, Bucić, Chen, and Ma determine the exact asymptotic coefficient. For 7-cycles, we show that their formula fails at every fixed density $1/4<q<1/2$, and give explicit lower and upper bounds. The exact coefficient in this interval remains open.

The Palomar registry's description of entry PALOMAR-2026-09-30-000004:

A Lean proof resolving the Burr–Erdős–Graham–Sós conjecture (Erdős Problem 809): for every fixed odd cycle of length at least seven, the maximal anti-Ramsey threshold at floor(n²/4) + 1 edges is n²/8 + o(n²). The seven-cycle case is new to our knowledge. The development proves it and formalizes the stronger full-density result of Bucić, Chen, and Ma for odd cycles of length at least nine.

Scope. Full: the statement is the problem's for every $k\ge3$.

Depends on. L17, the project's claim card, which carries the statement, the proof account and the verification records.

Acceptance. Formalized: the proof is the Lean this corpus built and audited. It is kernel-checked on the axioms propext, Classical.choice and Quot.sound only. The whole statement was audited against the English statement by the project's fresh-context statement-fidelity review and distinct grade of 2026-10-02. The verdict was refutation-failed. The grade was pass for the report and for independence, with tier 2 asserted. The review is bound to the lean/ tree that the non-author clean gate of 2026-09-29 checked, and a grade decision applied the grade to the Lean v4.34.1 tree, which the non-author clean gate of 2026-10-13 checked. This is the tier 2 warrant of docs/anatomy.md "Tiers", and it is recorded on the claim card.

No other evidence kind applies. Nobody outside the repository has examined the proof, so nothing is listed as reviewed. There is no refereed write-up. The paper linked as preprint is the write-up held in the repository, not a posting on a preprint server. Bloom's catalog labeled the problem OPEN and credits only the $k\ge4$ result. The posting has no comments. The registry's automated review outcome is neutral, and its trust level concerns the build, not the mathematics. Neither the fidelity review nor its grade read the Bucić–Chen–Ma paper. The $k\ge4$ branch is a closed native proof whose truth does not rest on that attribution.

Priority. The project's proof was public first. The repository plasma-ai/erdos-809 was created public on 24 September 2026, and its first push, at 23:25 UTC that day, held the whole development: the seven-cycle proof assembled with the formalized cases $k\ge4$ into the statement for every $k\ge3$ (GitHub's event record of the repository, read on 2026-10-14). Asad Shahab's independent proof of the seven-cycle case (claim page) was published in his repository Asad-Shahab/erdos-809-lean, created public on 27 September 2026 at 03:47 UTC, and his proof claim 358 was submitted to erdosproblems.com before the project's 367 later that day. So the project published first, and Shahab filed first on erdosproblems.com. The standing above does not rest on priority or on community acceptance.