A counterexample to a conjecture of Graffiti.pc on the forest number

A mix of human-written and AI-generated textHuman understanding: some partsmath.CO — Combinatorics

Contributed by Deep Bhattacharjee ↗

Version 1 / Oct 23, 2026 / CC BY 4.0

Abstract

Conjecture 66 of Graffiti.pc bounds the order of a largest induced forest of a connected graph from below by the even mode of the degrees of its complement divided by its average degree. We show that it is false, under every reading of its definitions and by an unbounded margin.

Provenance statement

Deep Bhattacharjee chose the problem and directed the work. Claude (Anthropic), through Claude Code, carried out the searches and computations, wrote the checking programs and the Lean 4 proofs and drafted the paper. Refutes Graffiti.pc Conjecture 66 under every reading. The proofs are written out in the paper; the programs and their outputs are in the release. The author approved the final version. Code and data: release v1.0.0, https://github.com/creelie/eConjectureWOWII66/releases/tag/v1.0.0.

Tools used

Anthropic
Claude CodeVersion Opus 5.5 Ultracode

References

  1. N. Alon, J. Kahn, P. D. Seymour, Large induced degenerate subgraphs, Graphs Combin. 3 (1987) 203--211.
  2. D. Bhattacharjee, P. Mandal, U. Bhattacharya, Resolving Erdős--Ulam monochromatic union-closed family conjectures, preprint (2026), arXiv:2610.02833.arXiv
  3. E. DeLaViña, Graffiti.pc: a variant of Graffiti, In: Graphs and Discovery , DIMACS Ser. Discrete Math. Theoret. Comput. Sci. 69 , Amer. Math. Soc., Providence, 2005, pp. 71--79.
  4. E. DeLaViña, Written on the Wall II (conjectures of Graffiti.pc), http://cms.uhd.edu/faculty/delavinae/research/wowII/; version of 26 July 2026 archived at https://web.archive.org/web/20260726061534/http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html.link
  5. S. Fajtlowicz, On conjectures of Graffiti, Discrete Math. 72 (1988) 113--118.
  6. The mathlib Community, The Lean mathematical library, In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs , ACM, New York, 2020, pp. 367--381.
  7. B. D. McKay, A. Piperno, Practical graph isomorphism, II, J. Symbolic Comput. 60 (2014) 94--112.
  8. L. de Moura, S. Ullrich, The Lean 4 theorem prover and programming language, In: Automated Deduction -- CADE 28 , Lecture Notes in Comput. Sci. 12699 , Springer, Cham, 2021, pp. 625--635.

Version history

  1. v1Submitted by Deep BhattacharjeeInitial depositCurrentOct 23, 2026