---

Claim. There is an absolute constant $C$ such that every split graph $G$ on $n$ vertices, a graph whose vertex set splits into a clique and an independent set, satisfies $|E(G)|-2\nu_3(G)\le n^2/6+Cn$, where $\nu_3(G)$ is the largest number of edge-disjoint triangles in $G$, and hence $\mathrm{cp}(G)\le n^2/6+Cn$, since the packed triangles and one $K_2$ per uncovered edge form a clique partition. These are Theorem 1.1 and Corollary 1.2 of Juan Pablo Traverso Gianini, Linear-error clique partitions of split graphs via structured triangle packing, Paper III of the author's series, preprint version 1.5 released on 23 August 2026 (the claim's date, which is also that of the author's comment on the site's thread announcing the result); the author registered it on the proof-claims tab on 29 August. Split graphs are chordal, and the earlier bound for them was $3n^2/16+O(n)$ by Chen, Erdős and Ordman (library card); the complete-split family $K_p\vee\overline{K}_{2p}$ has value $n^2/6+n/6$, so the coefficient $1/6$ is sharp and a linear term is necessary. The abstract separates three regimes by the ratio of independent to clique vertices: a bulk regime closed by an exact four-orbit linear program and the Haxell–Rödl theorem, a regime of few independent vertices closed by matchings and exact dense decompositions, and a regime near ratio $2$ closed by factorization, a polarization inequality and a list edge-coloring argument proved in an appendix. This record rests on the manuscript's front matter and abstract (version 1.5); this corpus has not checked the proof.

Submission note. Posted to erdosproblems.com as a proof claim by Juan Pablo Traverso (account jpt) on 29 August 2026, giving "GPT, Claude, Gemini, Aristotles." as the AI used:

I have proved that cp(G) ≤ n²/6 + Cn for every split graph G on n vertices, the result is accompanied by a Lean 4 Proof, final unconditional, sorry-free, axiom-clean theorem. (Proved on Paper III on the Zenodo link provided). Split graphs are a chordal subclass, Chen–Erdős–Ordman had 3n²/16 + O(n); my research improves the quadratic coefficient to the sharp value 1/6, matching the complete-split lower-bound family K_p ∨ K̄_2p, with the exact value n²/6 + n/6 (the linear term is necessary). While this settles Problem #81 at the n²/6 + O(n) for split graphs; the general chordal case remains open. Main proof ideas: given cp(G) ≤ |E| − 2ν₃(G), we can pack triangles at the right rate. In a split graph every triangle uses a clique edge, so clique edges are an scarce resource, cross edges are paired at common endpoints and assigned to free clique edges by factorization and a list edge coloring argument. This solution was developed with AI assistance. Notes: This is Paper III of a series. Paper I proves the fractional split bound |E| − 2ν₃* ≤ n²/6 + n/2; Paper II determines the exact finite maximum of the fractional cover functional over all chordal graphs, ⌊(2n+1)²/24⌋, attained by complete split graphs. Both Papers with Lean 4 Proof, final unconditional, sorry-free, axiom-clean theorem.

Covers. The statement of Problem 81 restricted to split graphs. General chordal graphs are not covered; the author's Paper IV, recorded on its own claim page, addresses them.

Depends on. Nothing in this wiki.

Formalization. The release carries a frozen Lean 4 source tree (lean_v1.4_freeze) whose final theorem surface the author describes as unconditional, with foundational footprint propext, Classical.choice and Quot.sound and no sorryAx on the public theorem path, compiled in an external clean-room run the author commissioned from an AI auditor. This corpus has not built, printed or audited it, so it is no formalized evidence.

Standing. Claimed: an author preprint on GitHub, with the series deposited on Zenodo under the concept DOI linked above (the Papers I–III deposit is a separate record), developed and audited with AI systems at the author's request (the proof-claims tab names them as GPT, Claude, Gemini and Aristotles) and, as the author states, not human peer reviewed. The one comment on the site's claim (Cipollini, 30 August 2026) says that GPT, as the comment names it, had given the commenter the same split-graph result by different arguments. The site states that a listing on the tab is no guarantee of correctness.