AI 中文总结
本研究证明了Graffiti.pc程序提出的三个关于图的最大诱导树阶数与围长等参数关系的猜想，并给出了经Lean 4机器验证的完整形式化证明。
AI 中文摘要
对于有限简单图$G$，设$t(G)$为最大诱导树的阶数，$g(G)$为围长。我们证明了DeLaViña的Graffiti.pc程序提出的三个连续猜想。首先，用$\u2113(v)$表示顶点$v$的邻域诱导子图的独立数，我们证明$t(G) \u2265 \u230a g(G)/2 \u230b - 1 + \u2192_{v \u2208 V(G)} \u2113(v)$。其次，若$\u2113(G)$为图的外围，$f(G) = \u2192_x d(x, \u2113(G))$，我们证明$t(G) \u2265 \frac{2}{3} g(G) + f(G)$，并在$G$含环时建立了更强的整数界$t(G) \u2265 f(G) + \u2308 2g(G)/3 \u2309$。第三，若$\u2206'(G)$为计重数的第二小度，则每个连通非树图满足$t(G) \u2206'(G) \u2265 g(G) + 1$。这些是《Written on the Wall II》中的猜想141、142和143。本文附带了所有三个形式化命题的完整、经机器验证的Lean 4证明。
英文摘要
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.
Comments16 pages. Complete Lean 4 proofs of all three formal statements are included as ancillary files; see Google DeepMind Formal Conjectures pull requests #4454 and #4457
