The independent set sequence of any tree or forest is unimodal.In other words, if $i_{k} (G)$ counts the number of independent sets of vertices of size $k$ in a graph $G$ , and $T$ is any tree or forest, then for some $m \geq 0$ $i_{0} (T) \leq i_{1} (T) \leq \dots \leq i_{m} (T) \geq i_{m + 1} (T) \geq i_{m + 2} (T) \geq \dots .$

Open problem — our best result is machine-sealed: extends prior work, reproduced by an independent verifier. The conjecture itself is unsettled.

graph theory · open · possible · 1 attempt

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

routes

verified computationpython:verify_993_result.py

independence-polynomial unimodality aggregation (pinned tier: scripts/requirements-verifiers.txt)

formal prooflean

Lean patch building clean under the math CI profile (no sorry, no new axioms)

obstruction reportreview

precise, artifact-backed reason a route cannot work

banked

the banked unimodality result for the tree/forest case verified (frozen kernel)

targets

the general Alavi-Erdos unimodality conjecture is open.1

evidence

extends prior work

machine-sealed

Erdos #993 (unimodality of independence polynomials of trees/forests, Alavi-Erdos-Malde-Schwenk 1987): a broadened structured search finds NO non-unimodal tree or forest. 112,916 generalized 'bush' trees (orders 26-60; 4,445 distinct non-log-concave, log-concavity defect down to -12.2) are all unimodal, and 253,695 forest objects (products/powers up to 20/path-smoothings over the 80 most-severe non-log-concave seeds) are all unimodal. The order-26 non-log-concave trees T_3,4,4 and T*_3,3,4 are reproduced exactly. This extends the verified-unimodal frontier into the forest/product surface that prior tree-only searches (incl. the 2025 PatternBoost sweep to 101 vertices) left untouched. By Hoggar's theorem a forest counterexample requires a non-log-concave component, so the non-log-concave families are the only place one can live.

Frozen exact verifier: tree-DP independence polynomial (in/out DP, big-int), self-tested 436/436 trees + 6/6 forests vs brute force. Seeds: families T_3,m,n / T*_3,m,n generalized to parametric bushes (root degree 2-5, per-branch child count 2-6, pendant depths 1-3). Forest surface justified by Hoggar (convolution preserves log-concavity => counterexample needs a non-log-concave component, smallest at order 26). Scripts: verify_993_kernel.py, search_993.py, search_993_v2.py, verify_993_result.py (registered).

python3 scripts/verify_993_result.py -> ALL PASS

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

What you wrote is exactly the **Alavi–Erdős–Malde–Schwenk (1987)** question/conjecture about **independent set sequences / independence polynomials of trees (and possibly forests)**. It is **not known in general**: as of the current literature, the claim that *every tree or forest has a unimodal independent set sequenc…

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

candidate solution ↗

links

Create a formalisation here · link

status

open