{"id":"palomar/PALOMAR-2026-11-03-000005","url":"https://github.com/ProblemHunter/wowii84-lean/tree/722b098bafb5371c1e7c7f23b3f7f9d8a7fb22aa","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-03-000005-v1.json","repo":"https://github.com/ProblemHunter/wowii84-lean","tags":["math.CO","msc:05C05","msc:05C12","msc:05C69"],"score":0,"title":"Written on the Wall II, Conjecture 84: tree(G) ≥ 2 rad(G) / δ(G)","trust":"high","domain":"math.CO","source":"palomar","authors":["Yixing Zhang"],"reviews":0,"subject":"math.CO","summary":"A complete Lean 4 / Mathlib formalization of Conjecture 84 of DeLaViña's \"Written on the Wall II\" (conjectures of Graffiti.pc): for every finite simple connected graph G with positive minimum degree δ(G), the maximum number of vertices of an induced subtree satisfies tree(G) ≥ 2·rad(G)/δ(G). The formal statement is the one recorded in google-deepmind/formal-conjectures (WrittenOnTheWallII/GraphConjecture84.lean, theorem `conjecture84`), copied verbatim together with its definition of `largestInducedTreeSize`. The proof formalizes the argument of J. J. Gebendorfer's manuscript \"Induced trees…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-03","reactions":{},"formalized":true,"formalizes":[{"title":"Induced trees in graphs with a cut vertex: A proof of Written on the Wall II, Conjecture 84","identifier":"https://github.com/google-deepmind/formal-conjectures/issues/7663","relationship":"formalizes"},{"title":"Maximum induced trees in graphs","identifier":"J. Combin. Theory Ser. B 41 (1986) 61–79","relationship":"formalizes"}]}