Naoki Takata
January 9, 2026
We investigate proposed upper bounds for the clique transversal number τ(G) of a graph G on n vertices. Specifically, we disprove two conjectured bounds: τ(G) ≤ n − ω(n)√n for some function ω(n) → ∞, and τ(G) ≤ n − c√n log n for some constant c > 0. The counterexample in both cases is the empty graph, for which τ(G) = n. All results have been formally verified in the Lean 4 theorem prover using the Mathlib library.
As a proof of existence for this paper, the Keccak-256 hash of the PDF has been recorded on the Ethereum blockchain.
Timestamp: January 10, 2026 (date recorded on the blockchain)
All theorems are formalized in Lean 4 (Mathlib commit f897ebcf72cd16f89ab4577d0c826cd14afaafc7). The verification used Aristotle, an automated theorem proving system for Lean 4.
Naoki Takata
X: @naokitakata
Email: [ntakata [at] proton.me]
This is a preprint. Comments are welcome!