---

Claim. The preprint The Burr-Erdős-Graham-Sós conjecture for the seven-cycle (arXiv:2609.38286v1) proves the case $k=3$ of Problem 809,

$$f\bigl(n,\lfloor n^2/4\rfloor+1,C_7\bigr)=\Bigl(\frac18+o(1)\Bigr)n^2,$$

in the notation with at least $e$ edges, and the posting on the site's proof-claims tab says that with Bucić, Chen and Ma's theorem for $k\ge4$ this covers every $k\ge3$, the Lean development combining the new seven-cycle proof with a formalization of their argument in one statement, erdos_809, for all $k\ge3$. The posting describes the lower bound as the work: a walk condition replacing the common-$C_7$ condition on pairs of edges, a regularity and triangle-removal step that lifts walks to paths, a fractional matching of color-sharing triangular edges, a flag-algebra certificate on five vertices, a stability argument for graphs far from bipartite, and a peeling of low-degree vertices; the abstract speaks of a weighted palette inequality proved with an exact rational certificate on five sampled vertices. The posting says that cycles are simple and not necessarily induced, that colors are counted by the image, that a lemma attains the minimum with exactly $\lfloor n^2/4\rfloor+1$ edges, as the site's definition requires, and that the certificate is kernel-checked with the axioms propext, Classical.choice and Quot.sound only.

Submission note. Posted to erdosproblems.com as a proof claim by Asad Shahab (account asadshahab) on 27 September 2026, giving "GPT-6 Astra (OpenAI), Claude Opus 5.5 (Anthropic), Aristotle (Harmonic)" as the AI used:

This proves the $C_7$ case: $\chi_S(n,\lfloor n^2/4\rfloor+1,C_7)=(1/8+o(1))n^2$. With Bucić–Chen–Ma for $k\geq4$ that covers all $k\geq3$. The upper bound is the two-clique example; the work is the lower bound. I replace "two edges lie on a common $C_7$" by a walk condition: no 2-walk between one pair of endpoints plus a 3-walk between the other. After deleting $o(n^2)$ edges (regularity + triangle removal) these walks lift to real paths, so every colour class satisfies it. With min degree above $n/3$, triangular edges can only share colours in pairs (a fractional matching), and nontriangular edges are bounded via neighbourhoods. A flag-algebra certificate on 5 vertices combines the two. A stable version handles graphs far from bipartite; near-bipartite graphs have a large clique in the $C_7$ conflict graph. Peeling low-degree vertices finishes. Notes: The case $k\geq4$ is due to Bucić–Chen–Ma; the new part is $C_7$. The Lean formalization covers all $k\geq3$: erdos_809 combines the $C_7$ proof with a formalization of their argument. Cycles are simple, not necessarily induced; colours are counted by the image; a lemma shows the minimum is attained with exactly $\lfloor n^2/4\rfloor+1$ edges, as in the site's definition. The certificate is kernel-checked and the only axioms are propext, Classical.choice, Quot.sound. A standalone Python checker for the certificate is in certificate/. arXiv version to follow.

Scope. Full, as the Lean statement is described: the preprint's theorem is the seven-cycle alone, and the longer odd cycles are the formalized theorem of Bucić, Chen and Ma, whose own claim page is Bucić, Chen and Ma 2026.

Depends on. Nothing in this wiki; the claim is the claimant's own preprint and development.

Acceptance. Formalized. This corpus's verification built the repository at its pinned commit on 2026-10-08 (Lean v4.28.0, Mathlib v4.28.0, every dependency at the commit its manifest pins): the default target Erdos809, with all 402 of the development's modules, built with exit 0 and no errors, and the axioms of Erdos809.erdos_809 are exactly propext, Classical.choice and Quot.sound. The pinned commit is the repository's head of 27 September 2026, which carries the manuscript the posting gives as its proof; it adds that paper and its LaTeX source to its parent, the development as it stood at 03:47Z on 27 September 2026, and changes no Lean source or build configuration. The build was of the pinned commit, not of that parent, which is the revision named as the formal proof by a pull request to formal-conjectures, opened on 27 September 2026 and open and unmerged, that asks to mark the problem research solved; its statement file, linked above at the pull request's head commit, states the question for every $k\ge3$ with the seven-cycle and the longer odd cycles as variants. The repository has no comparator challenge file, so no fingerprint comparison was made; instead the statement of Erdos809.erdos_809 was audited clause by clause through the definitions its type reaches, Erdos809.CycleAsymptoticExtremalValue, CycleExtremalValue, CycleAttainableColorCount, ValidCycleColoring, CycleCopy, EdgeCount, usedColors and exactThreshold of the same namespace and Mathlib's SimpleGraph.Copy, SimpleGraph.Copy.mapEdgeSet, SimpleGraph.cycleGraph and IsLeast, and its meaning was compared with formal-conjectures' erdos_809 in place of a fingerprint. The audit found the statement equivalent to the problem's Statement, to the statement of L17 and to formal-conjectures' erdos_809: for every $k\ge3$ and every $\varepsilon>0$, at every large $n$ the least number of colors actually used, over the simple graphs on $n$ vertices with at least $\lfloor n^2/4\rfloor+1$ edges and the edge-colorings under which every copy of $C_{2k+1}$, not necessarily induced, is rainbow, exists and lies between $(1/8-\varepsilon)n^2$ and $(1/8+\varepsilon)n^2$. Each difference from the Statement's wording is an exact equivalence: at least rather than exactly $\lfloor n^2/4\rfloor+1$ edges is the equivalence the problem's Formulation states, and the development proves that the minimum is attained on a host with exactly that many edges; colors are counted as the image of the coloring, which gives the same minimum as a palette size; and an explicit $\varepsilon$–$N$ band on the attained minimum is equivalent to $\sim n^2/8$. No clause is vacuous: the minimum's existence is proved, not assumed, and the only hypothesis is $3\le k$. A trust scan of all 402 modules found no sorry, axiom, native_decide, implemented_by, extern, unsafe or opaque; the certificate files use decide +kernel, which the kernel checks, and the only set_options are the resource limits maxHeartbeats and maxRecDepth. The theorem's proof applies Erdos809.erdos_809_C7 for $k=3$ and, for $k\ge4$, Erdos809.erdos_809_long_odd_cycles, which the development calls its formalization of Bucić, Chen and Ma's argument, so the axiom check covers both. Not reviewed: the site labels the problem OPEN, its commentary credits only the $k\ge4$ result, the claim has no comments, and no outside review was found. Not refereed: the preprint arXiv:2609.38286 (v1, 29 September 2026) is not refereed, and this corpus has not read it; the acceptance rests on the Lean alone. The claim is independent of the project's own, recorded on its own claim page, and was filed on the site first, as the site's proof claim 358, before the project's 367, both on 27 September 2026.