math.CO — Combinatorics

A thrackle on n vertices has fewer than 4n/3 edges

Contributed by Tejasvi Singh Tomar

A thrackle is a drawing of a graph in the plane in which every two edges meet exactly once, either at a common endpoint or at a proper crossing. Conway conjectured that a thrackle with $n$ vertices has at most $n$ edges. We prove that a thrackle with $n\ge4$ vertices has at most $\frac43(n-1)$ edges, improving the bound $\frac{18}{13}(n-1)$ obtained by Tóth and, independently, by Scoppetto. The proof combines Xu's discharging argument with two computer searches, by the method of Fulek and Pach, showing that two generalized dumbbells in the sense of Fulek and Pach are not thrackleable: $\mathrm{DB}(6,8,-1)$ is a $6$-cycle and an $8$-cycle sharing one edge; $\mathrm{DB}(6,10,-3)$ is a $6$-cycle and a $10$-cycle sharing a path of three edges. A formal proof in Lean 4 derives the bound from five properties of thrackles and checks the computational facts it uses; Section 6 states what this proof trusts.

Author comments: Published on Zenodo: https://doi.org/10.5281/zenodo.24065370