{"id":"palomar/PALOMAR-2026-10-11-000012","url":"https://github.com/selfreferencing/erdos993-palomar/tree/c020ce114a4b21ee164946547093e40452af898a","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-11-000012-v1.json","repo":"https://github.com/selfreferencing/erdos993-palomar","tags":["math.CO","msc:05C69","msc:05C05","msc:05C31","msc:05A20","combinatorics","forests","lean-formalization"],"score":0,"title":"Unimodality of the independence sequence of a finite forest (Erdős Problem 993)","trust":"high","domain":"math.CO","source":"palomar","authors":["Kevin Vallier","Tong Zhang"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 and Mathlib formalization of the theorem that the independence sequence of every finite forest is unimodal: the numbers of independent sets with 0, 1, 2, ... vertices weakly increase up to some index and weakly decrease after it. This is the statement listed as Erdős Problem 993; later sources attribute the question to a 1987 paper of Alavi, Malde, Schwenk and Erdős. The first claimed proof for all finite forests is by T. Zhang and W. Li (self-archived preprints, September 2026). This repository formalizes a second proof, by W. Li, K. Vallier and T. Zhang: it adapts the public…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-11","reactions":{},"formalized":true,"formalizes":[{"title":"Unimodality of Forest Independence Polynomials","identifier":"arXiv:2610.07943v1","relationship":"adapts"},{"title":"Unimodality of Forest Independence Polynomials","identifier":"doi:10.5281/zenodo.23269638","relationship":"formalizes"},{"title":"Exact Certificates for Unimodality of Forest Independence Polynomials: A consolidated proof manuscript and reproducible supplement","identifier":"https://github.com/zhangzenozhang-jpg/-forest-unimodality-proof","relationship":"adapts"},{"title":"Unimodality of Forest Independence Polynomials","identifier":"doi:10.5281/zenodo.22999166","relationship":"adapts"},{"title":"Chromatic polynomials and logarithmic concavity","identifier":"doi:10.1016/0095-8956(74)90071-9","relationship":"formalizes"}]}