---

Claim. Write $c_4(G)$ for the least number of cliques of order at most $4$ whose edge sets partition $E(G)$, so $\mathrm{cp}(G)\le c_4(G)$, and $M(n)=\lfloor n(n+1)/6\rfloor$. Theorem A of Juan Pablo Traverso Gianini's Paper IV asserts an absolute constant $b$ with $c_4(G)\le M(n)+b\le n^2/6+n/6+b$ for every chordal graph $G$ of every order $n$, which gives the $n^2/6+O(n)$ bound of Problem 81 and answers it with yes; Theorem B asserts that for all sufficiently large $n$ the bound is $M(n)$ itself and that $M(n)$ is the exact maximum of the clique partition number over chordal graphs of order $n$. The first public posting is the author's draft v0.8, Clique partitions of chordal graphs: mixed rounding and construction in the critical regime, committed to the author's repository on 22 September 2026 (the claim's date) and registered on the site's proof-claims tab the same day; the current manuscript is v1.23, Clique partitions with rooted simplicial defect: quantitative stability and sharp eventual bounds, dated 1 October 2026, which keeps Theorems A and B, adds quantitative stability (a graph with $c_4(G)\ge M(n)-\delta$ is within $16\delta$ edge edits of a complete-split graph, with one clique root controlling every near-optimal partition), extends the bounds to fixed rooted simplicial defect, and recovers the extremal family of Okechukwu's paper. The abstracts describe the method as a mixed fractional packing of triangles and $K_4$'s rounded with the nibble of Paper III when the fractional value leaves a quadratic margin, and, in the critical regime, a descent along vertex-copy steps to a root clique followed by an explicit edge-coloring construction on the original graph with savings controlled by missing links and outside edges. This record rests on the v0.8 and v1.23 front matter, abstracts and theorem statements; this corpus has not checked the proofs. The paper reuses infrastructure of the author's Papers I–III, among it the nibble of Paper III, whose split-graph result is recorded on its own claim page, as lineage rather than as a result the proof rests on; the author states that the formal proof chain does not depend on the results of the other two full claims and claims no priority for the extremal value.

Submission note. Posted to erdosproblems.com as a proof claim by Juan Pablo Traverso Gianini (account jpt) on 22 September 2026, giving "models from OpenAI and Anthropic, Aristotle from Harmonic" as the AI used:

This is a formal proof that every chordal graph on $n$ vertices admits an edge partition into at most $n^2/6+O(n)$ cliques, all of order at most foursuff, and that for a large $n$, the exact maximum is (\lfloor n(n+1)/6\rfloor) (attained by complete-split graphs). This proof is an alternative method to the previously posted by @morluto: it uses fractional packings of triangles and $K_4$'s and separates two cases: - Away from the extremal value, a quadratic margin absorbs the subquadratic rounding loss. - In the critical regime, a descent argument finds a suitable root, and an explicit edge-colouring construction produces a partition with savings controlled by missing links and edges outside the root. The Lean 4 proof is sorry-free and has no unproved external theorem interfaces. Its final declarations use only [propext, Classical.choice, and Quot.sound]. This is an official public draft version, the final version will be released soon. Notes: This is Paper IV of my series on chordal clique partitions, building on Papers I–III. The repository includes English and Spanish manuscripts, frozen Lean sources, pinned dependencies, reproduction instructions, and audit logs. During this project, I developed Certo-Math (https://github.com/jtraverso/certo-math), a computational tool used for testing, finding counterexamples, exploring solutions and generating certificates... before formalizing in Lean.

Depends on. Nothing in this wiki.

Formalization. The v0.8 package's frozen Lean sources (Lean and Mathlib v4.28.0) export PaperIV.Erdos81AllOrders.erdos81_all_orders, which states that there is a rational $C\ge0$ such that every chordal graph on Fin n has a clique partition with pieces of order at most $4$ and at most $n^2/6+Cn$ pieces, together with the additive form erdos81_all_orders_additive, the eventual sharp bound Erdos81Unconditional.erdos81_cliquePartition and the eventual maximum PaperTheorems.erdos81_max_eq; the author's audit reports that these take no unproved theorem interface as an argument and use only propext, Classical.choice and Quot.sound. The v1.22 release of 1 October 2026 carries a 607-module freeze with the same reported footprint and an AI-conducted adversarial audit the author reports as passed, and v1.23 changes only editorial text. This corpus has not compared the chordality definition and the partition model with the problem statement, and has not built, printed or audited the development, so it is no formalized evidence.

Standing. Claimed: an author preprint on GitHub, deposited on Zenodo as Papers I–IV on 1 October 2026 with v1.23 of Paper IV, developed and audited with AI systems (the proof-claims tab's notes name models from OpenAI and Anthropic and Aristotle from Harmonic) and, as the author states, with no human peer review. The one comment on the site's claim is the author's update of 1 October 2026 to v1.23. Two other full claims are pending on the same problem, Morluto, Luo, Huang and Lee's and Okechukwu's, all asserting the same answer. The site states that a listing on the tab is no guarantee of correctness.