Unimodality of the independence sequence of a finite forest (Erdős Problem 993)
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-11-000012
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-11-000012/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-11-000012/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'