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 .$

verifiedThe problem is open. The best result here is machine-verified: extends prior work, re-checked by an independent verifier.

graph theory · open · possible · 1 attempt

Work on an Open Task

use this data

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

Ways to settle this problem3

Each route names what would count as a proof and how it would be checked.

dead ends1 · 50%
open1 · 50%

Verified computationverified_computation · python:verify_993_result.py

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

A full formal proof checked by the Lean kernelformal_proof · lean

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

Obstruction reportobstruction_report · review

precise, artifact-backed reason a route cannot work

Proven dead ends1

Knowing what can't work is a result — kept on record at full ink.

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

vf_7eba52ea8a9bc742

Open tasks1

What's still unproven here, ranked by how much depends on it.

the general Alavi-Erdos unimodality conjecture is open.

vf_7eba52ea8a9bc742

deps1

Evidence1

extends prior work

machine-verified

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 ↗

Connections1

Create a formalisation here · link

Check it yourself

One command re-derives this record's receipts on your machine.

vela reproduce examples/erdos-problems

Search Vela