Albertson–Berman Induced Forest Conjecture

What the AI did

The paper's "Acknowledgments and AI disclosure" section states that the two-terminal gadget "was discovered, and substantial parts of the proof strategy were developed, through interaction with OpenAI GPT-5.6 Sol", while the author "selected the research problem, directed the computational search and subsequent proof development, and checked the resulting mathematical arguments and computational certificates". GPT-5.6 Sol also assisted in preparing the manuscript and the verification code.

Verification

Reproduced here on 12 August 2026. The refutation is a single finite object, so it is checkable outright rather than on trust. The 31-vertex seed $T$ was rebuilt from the paper's own definitions - the 14-vertex gadget's cyclic neighbour lists, the pentagonal-bipyramid base, the decorated rim edges, the stated labelling and the two completion edges - without running the author's code. That yields a simple 3-connected planar graph on 31 vertices with $87 = 3n-6$ edges, hence a triangulation, with the paper's degree multiset $4^1 5^{17} 6^6 7^7$. Its maximum induced forest was then computed exactly by two independent algorithms: an ILP with lazy cycle-elimination cuts, and a branch-and-bound minimum feedback vertex set with no LP involved. Both give $a(T) = 15$, equivalently a minimum feedback vertex set of exactly 16, against the 15.5 the conjecture requires. The two finite inputs to the symbolic argument were separately brute-forced - the terminal profile $(6,6,6,5)$ over all $2^{12}$ internal subsets, and $\beta = 3$ over all $2^7$ subsets of the core - and $M_k$ for $k = 2..5$ confirmed planar on $31k$ vertices with $93k-6$ edges, minimum degree five, every seed induced. Worth noting what the shipped verifier does not do: it certifies the gadget embedding, the profile, $\beta$ and the sphere certificates, but never computes $a(T)$ or $a(M_k)$, and says so. That computation is the one this site supplied. Not peer-reviewed, not on arXiv, no independent expert review.

Sources

• PaperA 15/31 Counterexample Family to the Albertson-Berman Conjecture · Preprint PDF
• CodeAuthor's verification script
• Independent workMakarov - a preprint claiming a somewhat different counterexample found independently without AI · Makarov - preprint PDF
• Problem recordMohar's open problem list: induced forests in planar graphs
• OtherMakarov, Large induced forests in planar multigraphs - calls the conjecture open, revised 9 Aug 2026