Tuza's inequality for split graphs with two neighborhood types

Tuza's conjecture (1981) asks whether every finite simple graph $G$ satisfies $\tau_\triangle(G)\leq2\nu_\triangle(G)$ , where $\tau_\triangle$ is the minimum number of edges meeting every triangle and $\nu_\triangle$ is the maximum number of edge-disjoint triangles. Bonamy et al. (2022) note that it remains a real challenge even for split graphs, whose vertices split into a clique $C$ and an independent set $I$ . This entry concerns the split graphs in which the vertices of $I$ with at least two neighbours in $C$ have at most two distinct neighbourhoods in $C$ . Zeng (2026) settled this case when $|C|=8$ . Does the inequality hold for every clique size and every multiplicity?

Result: Proved(see note)
Status: Partial result
AI contribution: AI-discovered
Method: Computation
Field: Extremal graph theory; triangle packing and covering
Posed by: Zsolt Tuza (general conjecture, 1981); split graphs singled out by Bonamy et al. (DMTCS 2022); the two-type case with an eight-vertex clique proved by Zijian Zeng (2026).
Year posed: 1981
Years open: 45y
Solved: 2026-10-08
Model: OpenAI Codex (GPT-6 Astra)
Vendor: OpenAI
Collaborators: —
Verification: Lean-checked, statement unaudited
Publication: Announced
Significance: 10 / 100
Disclosed cost: —
Wikipedia: No dedicated article

What was actually shown

Every finite simple split graph with at most two distinct active outside neighborhoods satisfies $\tau_\triangle(G)\leq2\nu_\triangle(G)$ . Vertices of outside degree at most one may have arbitrary neighborhoods. Clique size, overlap and multiplicities are unrestricted. Multiplicity compression preserves both optima. Explicit packings and covers reduce the proof to 23,848,371 parameter tuples for $2\leq |C|\leq42$ , analytic reductions, and an interval certificate with 178,506 leaves for every $|C|\geq43$ . This extends Zeng's specified eight-vertex-clique case. Tuza's conjecture for arbitrary graphs and for unrestricted split graphs remains open.

What the AI did

OpenAI Codex (GPT-6 Astra) developed the graph reductions, packing and cover bounds, finite and interval certificates, complete Lean formalization, and manuscript. Human direction selected the problem and required the final theorem and its certificates to be checked in Lean.

Verification

Read by this site on 3 November 2026, not rebuilt. The headline theorem tuza_of_two_active_types in formal/Result.lean was read with its definitions: packingNumber is the largest set of triangles with pairwise disjoint edge sets, coverNumber the least set of graph edges meeting every triangle, and activeTypes the distinct neighbourhoods in K of outside vertices with at least two neighbours there, so the statement is the theorem as claimed with no extra hypothesis. The four hand-written Lean files contain no sorry, admit, axiom declarations, native_decide, unsafe or implemented_by. GitHub Actions run 37753142279 at commit 214ce3c succeeded on 8 October: 3,190 modules compiled from source in about 80 minutes, axioms propext, Classical.choice and Quot.sound, negative control rejected. The runner is a self-hosted Azure machine set up by the author, and the formal sources are unchanged at the current head 27fa3a6. A brute-force check written here, 2,625 two-type split graphs with clique size 2 to 5 and small multiplicities, found no violation. No independent expert has audited the formal statement.

Sources

Submitted by MathIsEvenEasier on 26 Oct 2026

Tuza's inequality for split graphs with two neighborhood types

What was actually shown

What the AI did

Verification

Sources

Discussion