---

Submission note. Posted to erdosproblems.com as a proof claim by Tong Zhang (account TongZhang) on 27 September 2026, giving "GPT6.0 astra" as the AI used:

The proof consists of two parts, covering $n\le60$ and $n\ge59$. For $n\le60$, we derive inequalities from the structural properties of forests. For $n\ge59$, we assign weights to independent sets according to their cardinality, reducing the required coefficient inequalities to probabilistic estimates.

The claim. For every finite forest $F$ the sequence $i_0(F),i_1(F),\ldots,i_{\alpha(F)}(F)$ of its independent-set counts by size is unimodal: the statement of Problem 993 in full (T. Zhang and W. Li, Unimodality of forest independence polynomials, Zenodo, 27 September 2026, doi:10.5281/zenodo.22999166, CC BY 4.0; submitted to the site's proof-claims tab the same day by the first author, naming GPT6.0 astra as a tool). The authors' summary splits the proof in two: forests on at most $60$ vertices are handled by inequalities derived from the structure of forests, and forests on at least $59$ vertices by weighting independent sets by their size, which reduces the needed comparisons of adjacent coefficients to probabilistic estimates; a thread comment by the first author explains the latter as a conditional-binomial representation of the size of a random independent set in the hard-core model, with the weights the marginal occupation probabilities, and credits the paper of Fang, Lu, Nevo, Yao and Zheng (their claim page) as the inspiration. The Zenodo record cites the code of the computer-assisted part at a fixed revision of the repository zhangzenozhang-jpg/forest-unimodality-arxiv-verification (the first code link), and its update of 30 September 2026 states that the paper's arXiv submission was withdrawn on 28 September 2026, before it was publicly announced, pending a revision for clarity.

The revision and the formalization. A second version, Unimodality of forest independence polynomials, version 2.2 by W. Li, K. Vallier and T. Zhang (Zenodo record 23182492, 6 October 2026, CC BY 4.0; posted on arXiv the same day as arXiv:2610.07943v1, 81 pages, whose comments field calls it a provisional manuscript being rewritten before journal submission and discloses substantial AI contributions), presents what its description calls a second proof, with the threshold lowered to $25$ vertices: forests on at least $25$ vertices by the paper's Sections 2--5 and Appendix B, and forests on at most $24$ vertices by exact counting (its Section 6, by hand except for exact rational evaluations of two formulas at $43$ parameter triples); the thread comment of 6 October 2026 announcing it says the revision removes part of the computer-assisted verification and reorganizes the proof, and that the authors intend a shorter and less computational version; the record cites its supplementary code at a fixed revision of zhangzenozhang-jpg/forest-unimodality-v2.2-supplement (the second code link). Its Lean 4 development (selfreferencing/erdos993-forest-unimodality-lean at the pinned commit, Lean v4.28.0 with Mathlib v4.28.0, 1,352 modules in the closure, Apache 2.0) names erdos993_v22_final in Erdos993Lean/Analytic/V22/Final.lean as its main theorem, stated for acyclic simple graphs on every vertex count; its README says the development follows Sections 2--5 and Appendix B for the large forests and replaces Section 6 for the small ones by $249$ kernel-checked rational certificates of a linear relaxation; its README reports no sorry and the axioms propext, Classical.choice and Quot.sound together with Lean's compiler axioms Lean.ofReduceBool and Lean.trustCompiler, from $411$ compiled finite checks. Those are the repository's own statements; no build or audit of the development by this corpus, and no comparison of the formal statement with the problem's wording, is recorded.

Depends on. Nothing in this wiki as a premise: the paper of Fang, Lu, Nevo, Yao and Zheng is credited as the inspiration for the method, not used as an input, and the claim covers every forest itself.

Standing. Claimed. The thread (three comments as of 2026-10-06) holds a commenter's question about the length of the asymptotic part, the author's reply, and the author's announcement of the revision, to which the site's moderator appended the formalization link; the site labels the problem FALSIFIABLE (2026-10-06), the revision is an unrefereed arXiv preprint, and no referee, named reviewer or independent build is recorded, so the page lists no evidence.