Read the statement
The final theorem has only graph hypotheses: finiteness, a split partition, and at most two active types. Its conclusion uses the actual optimal cover and packing numbers.
Result.lean ↗Graph theory · Formal proof in Lean
Tuza’s inequality
for two types
In a split graph with at most two active neighborhood types, every triangle can be covered using at most twice as many edges as there are triangles in a maximum edge-disjoint packing.
Theorem
τ△(G) ≤ 2ν△(G)
Cover
Fewest edges meeting
every triangle
Packing
Most triangles sharing
no edge
Any clique sizeAny overlapAny multiplicities
The theorem applies to the graph class defined below. Tuza’s conjecture for arbitrary graphs remains open.
Graph class
What are the two types?
A split graph has a clique K, where every pair of vertices is joined, and an independent set I, with no edges between its vertices. Each vertex in I has neighbors in K.
We allow at most two distinct neighborhoods of size at least two, called S and T. Their sizes, overlap, and numbers of copies are arbitrary. Outside vertices of degree zero or one belong to no triangle and do not affect either optimum.
01 / Packing and covering
Find a packing and a cover.
Change the graph, then switch between a packing and a cover. These small witnesses illustrate the objects used by the proof.
This packingedge-disjoint triangles
This coveredges meeting all triangles
Why the cover works, and what the browser computes
Split the clique into A and B. Select every clique edge inside A or inside B. For each outside vertex, also select the spokes to the smaller of its two neighbor groups. A clique triangle has two vertices on the same side. A triangle using an outside vertex either has an already selected core edge, or crosses the cut and meets a selected spoke.
The browser chooses the least costly of the 64 cuts of this six-vertex clique. For the packing it tries a fixed, bounded collection of greedy orders and sum-color classes, keeping the largest edge-disjoint family it finds. It checks every displayed triangle and every cover incidence directly. The displayed packing gives a lower bound on ν△, and the cover gives an upper bound on τ△. Their sizes can differ from the optima. The example is limited to six clique vertices; the Lean theorem applies to every clique size.
C(A) = (|A| choose 2) + (|B| choose 2) + p min(|S ∩ A|, |S ∩ B|) + q min(|T ∩ A|, |T ∩ B|)
02 / Follow the dependencies
How the lemmas fit together
Select a node to read the result and open its Lean declaration. Each node groups several related lemmas.
03 / Why multiplicities can be capped
From matching colors to triangles
One neighborhood S. Assign each matching color to a different outside vertex. Edges of the same color never touch, so triangles at that center never reuse a spoke.
For compression, start with any packing, collect its used edges inside S, and recolor them. Assign their triangles to at most h(s) centers. Triangles outside this neighborhood group stay untouched, so the packing has the same size.
Why the cover number also stops changing
With s−1 twins, let J be the neighborhood edges not already selected in a cover. Each twin’s selected spokes meet every edge of J. The cheapest such spoke set Z gives |J| ≤ (s−1)|Z|, no more than the total number of selected spokes at all twins. Replace those spokes by J. This cover works for any number of extra twins at no greater cost.
Applying the packing and cover arguments gives a common cap h(s) that preserves both optima. The arguments allow the other neighborhood type to be present.
04 / A second way to pack triangles
Triangle sums give disjoint edge sets
For n ≥ 1, label the vertices by distinct residues modulo n. Color each triangle by the sum of its three labels. Every color class is an edge-disjoint packing.
a + b + c = a + b + d (mod n)
↓ cancel the shared edge
c = d (mod n)
↓ cancel the shared edge
c = d (mod n)
Two triangles of the same color sharing the edge ab must also have the same third vertex. They are the same triangle.
So each color class is a packing. The largest of n classes has at least 1/n of all triangles. This supplies a uniform packing bound for an arbitrary graph, including the clique core.
Lean: graph_triangle_packing ↗05 / The two certificate domains
Covering all clique sizes
Compression makes each fixed k finite. Normalization handles all large k together. Both reductions are proved in Lean.
After separate lemmas handle some parameter ranges, divide neighborhood sizes, overlap and capped multiplicities by k:
(x, y, w, α, β, ρ)
= (s/k, t/k, u/k, p/k, q/k, 1/k)
= (s/k, t/k, u/k, p/k, q/k, 1/k)
The remaining graphs map into a constrained six-dimensional real domain. A finite tree divides that domain into boxes. Every leaf has a checked inequality or is proved infeasible. The joins prove that no part of the domain is missed.
Rational interval arithmetic bounds every expression, and the soundness proofs connect these bounds to real inequalities. No floating-point evaluation is trusted.
01/43
Every integer k ≥ 43 gives a point in this interval. The endpoint ρ = 0 is included to make the domain closed; it is not the value of 1/k for any finite graph.
2–42finite parameter certificate
43–∞one uniform domain proof
The finite certificate covers 2 ≤ k ≤ 42, and the interval certificate covers k ≥ 43. For k < 2 there are no triangles.
06 / Inspect the evidence
Lean sources and build records
Inspect the proof
Four main modules connect the graph constructions to 3,186 generated certificate modules. All certificate sources are downloadable: about 10 MB compressed.
Sources & checksums ↗Rebuild & audit
Lean 4.34.0, pinned Mathlib. Final axioms: propext, Classical.choice, Quot.sound. No project axioms, proof holes, unsafe declarations or native decision shortcuts.
Public source build ↗Complete formalization verified · 8 October 2026. Public build 37753142279 compiled all 3,190 project modules from source. The final theorem passed, and the deliberately false control proof was rejected. The paper was revised on 26 October; the proof sources are unchanged.
Exact theorem & axiom output · Verification record · Paper (PDF) · LaTeX source
Where this fits
Packing triangles and removing them
Each triangle in an edge-disjoint packing forces us to remove a different edge if we want to eliminate all triangles. Thus ν△ ≤ τ△ for any graph. For the graphs studied here, the theorem also gives τ△ ≤ 2ν△.
For example, if a largest packing has 10 triangles, between 10 and 20 edge deletions are needed. Multiplicity compression reduces a graph with a clique of size k to at most 3k vertices while preserving both optima. Computing those optima remains a separate algorithmic problem.
Related work
Zijian Zeng’s 2026 preprint treats a specified eight-vertex clique part with two types. Here, the clique size is unrestricted.
Bonamy and coauthors prove the threshold-graph case, which includes nested neighborhoods. Our statement also permits crossing neighborhoods.
Huang and coauthors (18 October 2026) report three types for an eight-vertex clique part. Our result allows any clique size, with at most two types.
Full references are in the README.