Tuza's conjecture: delete 2k edges to kill all triangles when only k are edge-disjoint (Erdős #167)

If $G$ is a graph with at most $k$ edge-disjoint triangles, can $G$ be made triangle-free after removing at most $2k$ edges? In standard notation: writing $\nu(G)$ for the maximum size of a collection of pairwise edge-disjoint triangles in $G$ (a triangle packing) and $\tau(G)$ for the minimum number of edges whose deletion destroys every triangle (a triangle edge-cover), the conjecture asserts $\tau(G)\leq 2\nu(G)$ for every graph $G$. Deleting all $3$ edges of each triangle in a maximum packing shows $\tau(G)\leq 3\nu(G)$ trivially; $K_4$ and $K_5$ (where $\nu=1,2$ and $\tau=2,4$ respectively) show the factor $2$ would be best possible.

Acceptance. FULLY RESOLVES: (a) a proof that $\tau(G)\leq 2\nu(G)$ for all finite graphs — machine-checkable (Lean/Coq) preferred, else a complete written proof; or (b) a counterexample — an explicit graph $G$ (machine-readable, e.g. graph6) together with machine-checkable certificates of (i) an upper bound $\nu(G)\leq k$ (e.g. an ILP dual bound or exhaustive packing search transcript) and (ii) a lower bound $\tau(G)>2k$ (e.g. an UNSAT certificate that no $2k$-edge deletion set kills all triangles), plus the verification code. ADVANCES: a proven general bound $\tau\leq c\,\nu$ with $c$ strictly smaller than the best factor stated in the background ($66/23$, asymptotically); a proof of the conjecture for a substantial new graph class beyond those stated in the background (e.g. all $K_5$-free graphs, bounded-degree graphs, tripartite graphs); exhaustive certified verification of the conjecture for all graphs up to a stated order, with reproducible generation + ILP code and exhaustiveness certificate; or a Lean formalisation of the statement and the trivial/fractional bounds. Deliver the proof file, the counterexample + certificates + checker, or the verification code and attained order.