Proof claims for the Erdős tree conjecture: one for large forests, one for all sizes

The conjecture: in every tree and every forest, the numbers of independent sets of each size form a unimodal sequence. In plain words, take a network of dots and lines and count the ways to pick no dots, one dot, two dots and so on, with no two picked dots joined by a line (such a pick is an independent set). The conjecture says these counts rise and then fall, and never fall and then rise again, though they may stay level for a stretch; that shape is what unimodal means. A tree is a network in one piece with no loops; a forest is one or more trees side by side. For networks in general the counts need not rise and then fall: in the 1987 paper that posed the question, Alavi, Malde, Schwenk and Erdős showed that every possible pattern of rises and falls occurs in some network. It is problem 993 on erdosproblems.com↗, the public list of Erdős's problems, which has a discussion forum for each problem.

Two proof claims were posted as preprints, on September 21 and September 27, 2026. The problem site lists them as proof claims and says that a listing does not mean anyone there has examined them. I have not checked either proof. In October a Lean version of the second, all-sizes proof was registered on Palomar, a public registry of Lean proofs, and accepted by both of its proof checkers (details below). Neither paper has been refereed, and teorth/erdosproblems, the community database of Erdős problems on GitHub, still records the problem as open. Nothing here reports any statement by Terence Tao about either claim. Each claim links a version of its proof written in Lean, a program that checks a proof step by step.

In date order: the first claim was posted on September 21; on September 25, B. Reynolds reported in the problem's forum that he had re-run its Lean version; the second claim was posted on September 27, and its revised manuscript on October 6; on October 11 a Lean version of a later revision of that proof was registered on Palomar and accepted by both of its proof checkers. The sections below take one claim at a time.

Earlier steps in this story, with their dates: my computer check, which extended the check from every tree with up to 29^▲ dots to every tree with up to 32 (a ▲ beside a number means it has a note, listed at the end of the page), was posted on the problem's forum on August 2, 2026 and August 9, 2026; its last run finished on August 4, 2026. Tao merged my pull requests adding OEIS links to his database of Erdős problems on August 6 and September 18. Those steps are on the pages linked just below.

Who is who: the first claim's five authors are named in the table. The second claim was posted by Tong Zhang; its September manuscript is by Tong Zhang and Wei Li (Zenodo↗), and the October 6 revision, by Wei Li, Kevin Vallier and Tong Zhang, is a later version of the same Zenodo record. B. Reynolds, who posted code for one of the earlier tree checks, posts in the problem's forum as BrettRey2.

The first claim's paper, arXiv:2609.20961↗, covers every forest above some size. The paper proves that such a size exists but does not compute it, so nobody knows how far a computer check would have to go to cover the smaller forests. In particular, this claim together with the check of every tree up to 32 dots does not settle trees, since the claim's size could be larger than that. The paper itself says the conjecture for forests of every size remains open. In his September 25 forum post, B. Reynolds reported that he had re-run the claim's Lean version, that it went through with nothing left unproved, and that its formal statement matches the paper's main theorem. His post says the re-run was done with AI assistance (Claude). Lean itself checks the build; the reading that the formal statement matches the paper was made with AI help, so it is an AI-assisted check, not a referee's.

The second claim's current manuscript, by Wei Li, Kevin Vallier and Tong Zhang, is on Zenodo↗ and on arXiv as 2610.07943↗. It reuses bounds from the authors' own September manuscript and from the first claim's paper, so it relies on those being right as well as on its own argument. Its first Lean version accepted answers from compiled code in one part without checking each step. A later Lean version, in the repository selfreferencing/erdos993-palomar↗, has every step checked by Lean's own core checker and uses only Lean's three standard axioms. It was registered on Palomar, a public registry of Lean proofs announced by Terence Tao in August, on October 11, 2026, and both of Palomar's independent proof checkers accepted it. Its formal statement is taken from google-deepmind/formal-conjectures, a public library of open problems stated in Lean, where another contributor wrote it and a reviewer of that project approved it on October 9, before the proof was registered; it covers every finite forest and every finite tree. The Lean follows version 2.15 of the manuscript, which is on Zenodo with restricted access; the arXiv paper is an earlier version. The repository says that AI systems wrote and reviewed all of the Lean and that no person has read it; a Lean check makes that matter less, since what a reader has to check is the short formal statement, not the proof. Neither manuscript has been refereed.

Status#

On October 6, 2026, Thomas Bloom, who runs erdosproblems.com, stopped showing whether problems are open or solved, and paused new comments and proof claims; the existing ones stay up as an archive (his announcement↗). So no new claim can be listed there for now. Bloom said he will link Lean formalisations once they are registered on Palomar, and the all-sizes proof now has one. teorth/erdosproblems, the GitHub database kept by the mathematician Terence Tao, still records the problem as "falsifiable", which its contributing guide defines as open, with a single finite counterexample enough to disprove it, and as not formalized; it may simply not have been updated. That record does not assess either claim. As of November 7, I have not seen the Palomar entry linked from the problem's page on erdosproblems.com.

Where my check fits#

My check (Claude agents working under my direction wrote and ran the code) extended the check from every tree with up to 29^▲ dots to every tree with up to 32, about 165 billion^▲ more trees, counted by shape (unlabeled: trees that differ only in how the dots are numbered count once), including all 109,972,410,221 trees of the largest size, and none breaks the pattern. Neither claim cites it. If the all-sizes proof is right, my check is an independent computation that agrees with it on every tree up to that size. Checking trees does not settle forests: a forest's row of counts is the product of its trees' rows, multiplied as polynomials are, and multiplying rows that each have a single peak can give a row that does not.

For specialists: methods, Lean details and version history

In standard terms the conjecture says the independence polynomial of every forest is unimodal.

Earlier limit. The check to 29^▲ vertices was first reported on the problem's forum by the forum user JakeMallen on January 7, 2026; Reynolds posted code and results for it on March 12, 2026. His Zenodo preprint is the reference that Hibi, Kara and Vien cite for this limit in arXiv:2604.18824 (April 2026), a paper with no computation of its own.

First claim. The argument shows that for large forests a central interval of the sequence is log-concave, using the hard-core model (random independent sets weighted by size), and, by counting, that the initial part rises and the final part falls. The main theorem says only that some size N₀ exists: the paper works with sufficiently large forests throughout and does not make N₀ explicit. Reynolds's forum post on his re-run (September 25, 2026) reports that the Lean build completes with no sorry, that the axiom check lists only propext, Quot.sound and Classical.choice, Lean's three standard axioms, and that the formal statement uses Mathlib's independent sets, the usual single-peak unimodality and Mathlib's acyclic graphs.

Second claim, current version. The October manuscript splits forests by size. A "case" below is a triple (n, a, k): n is the number of vertices, a the size of a largest independent set, and k a position in the row of counts where a dip could occur. Lean's kernel is its small core checker; native_decide is a Lean command that runs compiled code and accepts its answer instead of having the kernel check each step.

Forests	In the manuscript	In the Lean version (section 8)
25 or more vertices	A moment argument	Follows the manuscript; 411 finite checks run with native_decide
24 or fewer vertices	Exact formulas at 249 cases (section 6.3), without listing forests: 206 settled by hand, 43 by exact rational arithmetic (section 6.5)	A different method: 249 exact certificates, one per case, checked by the kernel, again listing no forest

The first Lean formalization of the claim states a final theorem covering every finite forest with no extra premise. Its native_decide checks add the axioms Lean.ofReduceBool and Lean.trustCompiler to the three standard ones, so the trusted base includes the Lean compiler; the small-forest part uses only the three standard axioms. The later version registered on Palomar (PALOMAR-2026-10-11-000012, repository pinned at commit c020ce11) replaces every native_decide with checks the kernel carries out itself (decide +kernel, about 13,700 of them), so its axioms are the three standard ones only; its README reports that NanoDa and con-ron, Palomar's two kernel checkers, accepted it, and that it follows version 2.15 of the manuscript (Zenodo, restricted access), of which arXiv:2610.07943 is an earlier version. The same README lists an independent Lean formalization of the September manuscript by another person (lixiang90/forest-unimodality) whose README reports a clean rebuild on October 2; its one-line description still says verification is pending.

Version history. The September manuscript was a computer-assisted proof in two parts: forests with up to 60 vertices, by inequalities certified by exact computation without listing forests, and forests with 59 or more, by a probabilistic argument, the parts overlapping at 59 and 60. The October record calls the new version a second proof and says the first remains available under its own DOI.

AI role. The claims page names Odin Automatic AI Research Agent for the first claim and "GPT6.0 astra" for the second. The September Zenodo record says "OpenAI's GPT 6.0 Astra assisted with the computational work; the authors provided the overall proof strategy"; the October record discloses substantial AI contributions to the mathematical arguments, the formal proofs and the text.

What a Lean build settles. When a build finishes with nothing left unproved, its formal statement is proved from the axioms it uses. A person still has to check that the formal definitions mean what the words mean, that the formal statement says what the claim says, and which axioms were used. For the first claim, the forum report says it checked all three.

This page reports claims as listed on erdosproblems.com when I last read it, on October 29, 2026, and the Palomar registration as described in its repository, read November 7, 2026. I have not checked either proof. My check covers trees only, up to a fixed size, and is evidence for the conjecture, not a proof of it.

@misc{orden2026erdostreeconjectureproofclaims,
  author       = {Tyler Satchel Orden},
  title        = {Proof claims for the Erdős tree conjecture: one for large forests, one for all sizes},
  year         = {2026},
  howpublished = {Cyborg Mathematics},
  url    = {https://cyborgmathematics.com/writing/erdos-tree-conjecture-proof-claims}
}