---

Claim. The answer to Problem 1009 is yes: for every $c>0$ there is $f(c)$ such that every graph on $n$ vertices with at least $\lfloor n^2/4\rfloor+k$ edges, $k<cn$, has at least $k-f(c)$ edge-disjoint triangles. The claimed result is Theorem 1 of E. Győri, On the number of edge-disjoint triangles in graphs of given size, Combinatorics (Eger, 1987), Colloq. Math. Soc. János Bolyai 52, North-Holland, Amsterdam (1988), 267--276, as a refereed later paper states it: a graph with $n$ vertices and $t_2(n)+k$ edges, where $k=o(n^2)$ and $n\to\infty$, has at least $k-O(k^2/n^2)$ edge-disjoint triangles (Blumenthal, Lidický, Pehova, Pfender, Pikhurko and Volec, Combin. Probab. Comput. 30 (2021), 271--287, in the proof of its Lemma 11, p. 8 of the arXiv copy; the corpus's card is blumenthal_2021_sharp_bounds_decomposing_graphs_edges_triangles). The site adds, as its reading of the paper, that the theorem gives $f(c)\ll c^2$, and that no loss occurs ($f(c)=0$) when $n$ is odd and $c<2$, or when $n$ is even and $c<3/2$. The no-loss sentence is a statement for $n$ large in terms of $c$: Section 5 of the 2021 paper states Győri's ranges, $k\le2n-10$ for odd $n$ and $k\le3n/2-5$ for even $n$, "for large $n$", cites a correction, and calls the two bounds sharp, and the paper of Balogh and Wigal (Combinatorica 2025, read in arXiv:2502.16683v2, p. 10; card) reports the same ranges and points to Győri's 1992 correction of the paper; as a statement for every $n$ it fails for $K_5$, $K_6$ and Sauer's graph on ten vertices, as the problem page checks. The step from the attested theorem to the question is an authored conversion on the problem page: with $C$, $\delta$ and $n_0$ taken from the theorem, $k<cn$ and $n\ge\max(n_0,c/\delta)$ give at least $k-Cc^2$ triangles, and for smaller $n$ the trivial bound $0>k-cn$ suffices, so $f(c)=\max\bigl(Cc^2,\,c\max(n_0,c/\delta)\bigr)$ answers the question. Whether $f(c)\ll c^2$ holds for every $c$ depends on constants not visible in the attestation. Erdős's own theorem ([Er71], item 3) is the case $c<\tfrac12$ with $f(c)=0$, and Sauer's example there shows $f(2)\ge1$.

Acceptance. The site's curator, Thomas Bloom, labels the problem proved and credits Győri [Gy88] with the proof (the reviewed evidence; Bloom took no part in the paper), after the forum comments of 21 and 29 October 2025 identified Theorem 1 and corrected the deduction; the proof-claim tab is empty; the community database records the problem proved, with its last update dated 31 October 2025. The paper appeared in a proceedings volume (Colloq. Math. Soc. János Bolyai 52, 1988, whose year gives this page's nominal date; the zbMATH record Zbl 0706.05029 identifies the volume and carries a review summarizing the result as $ed_3(n,\lfloor n^2/4\rfloor+t)=t-o(t)$); no evidence that the volume was refereed is in hand, so refereed is not listed. The theorem is attested by the refereed quotation above, and the 2021 paper (p. 8, its [13, Theorem 1]) and Balogh and Wigal (Theorem 1.6, p. 2, their [8]) attribute to Győri's journal paper, Combinatorica 11 (1991), 231--243, the generalization to $r$-cliques, $r\ge3$, whose case $r=3$ is this theorem; that paper is not held and is known by attestation only, so it is not listed as the claimant's refereed publication either. Balogh and Wigal's correction reference [9] (p. 10) concerns the 1988 paper's exact ranges. The thread's second comment doubts the quantified restatement in the 2021 paper (the form with $\varepsilon k^2/n^2$); the claim recorded on this page uses only the first sentence of the attestation, with a fixed implied constant. Read depth: the attestation was read clause by clause; nothing of Győri's text, constants or range of $n$ was read, and nothing is independently reviewed by this project. The acceptance rests on the curator's credit, supported by the refereed attestation, and is to be rechecked against a readable copy of [Gy88] when one becomes available.

Formalization. The file src/latest/ErdosProblems/Erdos1009.lean of Boris Alexeev's repository plby/lean-proofs (2,373 lines at the pinned commit of 2026-09-15, linked above; first committed 17 August 2026; headed leanprover/lean4:v4.33.0 mathlib v4.33.0; it imports Mathlib modules and two sibling developments of the repository, ErdosProblems.Erdos207.Prefix and ErdosProblems.Erdos127.CutComposition) declares itself "a Lean formalization of a solution to Erdős Problem 1009" and names E. Győri as informal author and Codex and GPT-5.6 Sol as formal authors. Its theorem erdos_1009 (line 2347) states: for every real $c>0$ there is a natural $f$ such that for all $n$, $k$ and every SimpleGraph (Fin n) with at least $n^2/4+k$ edges and $k<cn$, there is a family $P$ of triangles of the graph, pairwise edge-disjoint in the file's encoding (TriangleFamilyOn, IsTrianglePacking), with $k\le|P|+f$; its docstring gives the explicit choice $f=210000\,C^2$ for any natural $C>c$. The file has no sorry, axiom or native_decide. The formal-conjectures statement of the problem (added 19 September 2026, described on the problem page) names this line in its formal_proof attribute; its packings are finite sets of $3$-cliques pairwise sharing at most one vertex, a different encoding, and the bridge between the two is in neither file. The file is not built, audited or kernel-checked in this corpus, and no outside examination of it is published, so the page lists no formalized evidence; the repository also carries an account of the proof (tex/1009.tex), which this page does not cover.