---

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 the catalog'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 posted to the site's proof-claims tab under the name Plasma AI, from the account jacobparish, on 27 September 2026, as the site's proof claim 367, filed after Asad Shahab's independent proof claim 358 of the same day (see Priority below), 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 write-up is the paper linked from the posting (preprint link, pinned to the same commit).

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, and 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 (verdict refutation-failed; grade pass for the report and for independence, tier 2 asserted), bound to the lean/ tree the non-author clean gate of 2026-09-29 checked, which is the tier 2 warrant of docs/anatomy.md "Tiers" and 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, and the paper linked as preprint is the write-up held in the repository, not a posting on a preprint server. The site labels 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, and the $k\ge4$ branch is a closed native proof whose truth does not rest on that attribution.

Priority. Asad Shahab's independent proof claim for the seven-cycle case (claim page) was submitted to the site earlier on the same day, so the seven-cycle argument is the project's own in authorship and not in priority; the standing above does not rest on priority or on community acceptance.