Three Graffiti.pc Conjectures on Largest Induced Trees: Proofs of Conjectures 141, 142, and 143
Alper Ferudun
math.CO
Aug 2, 2026 · v1
TL;DR
Machine-checked Lean 4 proofs accompany three graph-theory conjectures on largest induced trees, contributed to the Formal Conjectures repository.
Abstract
For a finite simple graph $G$, let $t(G)$ be the largest order of an induced tree and let $g(G)$ be the girth. We prove three consecutive conjectures of DeLaViña's Graffiti.pc program. First, writing $\ell(v)$ for the independence number of the subgraph induced by the neighbourhood of $v$, we prove $t(G) \ge \lfloor g(G)/2 \rfloor - 1 + \max_{v \in V(G)} \ell(v)$. Second, if $\mathrm{Per}(G)$ is the periphery and $f(G) = \max_x d(x, \mathrm{Per}(G))$, we prove $t(G) \ge \frac{2}{3} g(G) + f(G)$, and establish the stronger integral bound $t(G) \ge f(G) + \lceil 2g(G)/3 \rceil$ when $G$ contains a cycle. Third, if $δ'(G)$ is the second-smallest degree, counted with multiplicity, then every connected non-tree graph satisfies $t(G) δ'(G) \ge g(G) + 1$. These are Conjectures 141, 142, and 143 of Written on the Wall II. Complete, machine-checked Lean 4 proofs of all three formal statements accompany the manuscript.
Problem
Graffiti.pc Conjectures 141, 142, and 143 (Written on the Wall II) posit lower bounds on t(G), the largest order of an induced tree, in terms of girth, neighbourhood independence, distance from the periphery, and the second-smallest degree. These were listed as open.
Approach
Each conjecture is proved independently: Conjecture 141 follows from a sharper maximum-degree–girth bound for triangle-free cyclic graphs; Conjecture 142 uses a rooted shortest-cycle construction with a three-point metric estimate; Conjecture 143 reduces to a two-leaf induced-tree lemma via a maximality argument. Complete formal statements and proofs are developed in Lean 4 and submitted as Formal Conjectures pull requests #4454 and #4457, included as ancillary files.
Results
All three conjectures are proved, with stronger integral bounds established for cyclic graphs, and the Lean 4 proofs are machine-checked. Equality cases are characterized, e.g. for cycles C_g and complete bipartite graphs K_{a,b}.
