Why checking a math conjecture on every case up to a size is not a proof

The result in brief

A computer that checks every case of a math conjecture up to some size can rule out small counterexamples, but that is not a proof. Here is my own example. A conjecture posed by Alavi, Malde, Schwenk, and Erdős in 1987 covers trees and forests (collections of trees). I checked trees only. I extended the check from every tree with up to 29^▲ dots to every tree with up to 32, about 165 billion^▲ more trees, and it held for every one (a ▲ after a number links to a note about it at the bottom of the page). I posted the results on the problem's forum on August 2, 2026 and August 9, 2026. After that, two proof claims were listed on erdosproblems.com, the public list of Erdős problems, on September 21, 2026^▲ and September 27, 2026^▲, before that site paused new proof claims on October 6: a partial one, for all large enough forests, by Ethan X. Fang, Junwei Lu, Eran Nevo, Yuan Yao and Hailun Zheng, and one for every forest posted by Tong Zhang, whose authors used OpenAI's GPT 6.0 Astra. In October a version of the second, written in Lean so that a computer checks every step, was accepted by both proof checkers of Palomar, a public registry of such proofs. That is the kind of evidence my check could never give: it covers every forest, not only the small trees. As of November 7, 2026, neither paper has been refereed, neither cites my check, and teorth/erdosproblems, the community database of Erdős problems on GitHub, still records the problem as open.

Animation, no sound. A tree with 10 dots is drawn. Bars show how many ways there are to pick 0, 1, 2 and more of its dots with no line between any two picked dots: 1, 10, 36, 59, 45, 15, 2. The bars rise, peak once, and fall, and the peak is highlighted. Then 14 small trees appear one after another, each with its own bars rising and falling once, while a counter climbs to 109,972,410,221, the number of trees with 32 dots, and a check mark with 0 shows that none of them broke the pattern.

Headlines about computers or AI "solving" a math problem can describe very different things. Some describe a proof, and others describe a check of every case up to some size. This page uses one of my own results, a check that took an Erdős conjecture on trees three sizes past the old limit, to show what the second kind of result means and how to tell it apart from the first.

What the conjecture says#

A tree, in graph theory, is a set of dots (called vertices) joined by lines so that the whole thing is in one piece and has no cycles. One piece means you can get from any dot to any other by following lines. No cycles means you can never follow lines away from a dot and arrive back at it without retracing a line.

For any tree, count the ways to pick dots so that no two picked dots are joined by a line. There is exactly one way to pick no dots at all. Then count the ways to pick one dot, then two dots, then three, and so on. Writing these counts in a row gives a sequence of numbers. The animation above shows this row as bars, starting with that single way of picking nothing.

Alavi, Malde, Schwenk, and Erdős conjectured that for every tree (and every forest, a collection of trees), this row rises and then falls. It may stay level for a while, but it never falls and then rises again to a second peak. A conjecture is a statement that has been proposed as true but not proved. This one is easy to state and has had no accepted proof since 1987; the September 2026 claims noted above have not been checked. It is problem 993 on the public list of Erdős problems.

The notes at the bottom of the page use the technical words: a set of dots with no two joined is an independent set, a row with a single peak is unimodal, and a tree's order is its number of dots.

How the computer checked every tree of each size#

There are infinitely many trees, so no program can test them all. There are only finitely many trees of each size, so a program can test every one of them. "Every tree" here means every shape: two drawings count as the same tree if one can be turned into the other by moving the dots around without changing which dots are joined.

A Claude agent working under my direction wrote and ran the program; I set the checks it had to pass and reviewed the results. The program used nauty, a standard package for generating graphs, to produce every tree of each size, one at a time. For each tree it worked out the row of counts exactly, in whole numbers, and checked that the row never rises again after it has started to fall. It would have printed any tree that broke the pattern, and it printed none. My runs covered the sizes 20, 22 and 24 to 32; the other sizes up to the old limit rest on the earlier checks described below.

At the largest size, 32 dots, there are 109,972,410,221 trees. One size smaller there are 40,330,829,030, and all of them passed too. Each extra dot means about two and three-quarter times as many trees as the size before, so the largest size alone had about twenty times as many trees as the old limit. Everything ran on one machine; the two largest sizes were each split into 16 parts run separately.

How you show no tree was skipped#

A report of zero failures only means something if every case was actually tested. Software testing has the same problem: a test run that silently skips half its tests also reports zero failures. The fix there is to compare how many tests ran with how many should have run.

The same check works here. The number of trees of each size is already known and recorded in the OEIS, the Online Encyclopedia of Integer Sequences, as sequence A000055↗. At every size, the number of trees my program produced, at every size it ran, matched that recorded number exactly. For the sizes split into parts, the parts added together matched it.

A program that lost trees would have come up short, and one that made extra copies would have come up long. The count cannot catch a loss and an extra copy that cancel out: a program that skipped one tree and repeated another in its place would still get the right total. For that case I rely on the generator: the nauty tree generator is designed to produce each tree exactly once. I did not check that guarantee separately; the count match confirms only its totals.

Before going past the old limit, I reran some of the sizes that had already been checked. Earlier computations had checked every tree with up to 29 dots: the forum user JakeMallen reported it on the problem's forum at erdosproblems.com in January 2026, and Brett Reynolds published code (GitHub repository BrettRey/erdos-problem-993) and a preprint in March 2026. My program, written separately from Reynolds's code, produced the same number of trees as his at 28 and 29 dots and, like his, found no tree that broke the pattern at either size.

Why a check up to a size is not a proof#

A proof is an argument that shows the statement holds for trees of every size at once. This check, together with the earlier ones it extended, covers every size up to 32 dots and says nothing directly about larger trees.

Patterns that hold for every small case can still fail later. A classic example from arithmetic: the formula n × n + n + 41 gives a prime number for every whole number n from 0 to 39. At n = 40 it gives 1,681, which is 41 times 41.

What the tree check does show is that any tree that breaks the pattern has more than 32 dots, so a search for a counterexample can start above that size. The count at each size is public, so anyone writing a different program can compare their counts with these before searching larger trees.

Where the result is posted, and what Terence Tao's link means#

I posted the result as a comment on the problem's forum thread at erdosproblems.com, the public list of Erdős problems run by T. F. Bloom, in August 2026 (sizes 30 and 31 in the first comment, the largest size in the second). On October 6, 2026, the site paused new comments and proof claims on its problems; existing comments, mine included, stay up as an archive. The code and the count for each size are in a public repository.

The mathematician Terence Tao keeps a separate, crowdsourced database of Erdős problems on GitHub. On August 6, 2026, he merged (GitHub's word for accepting) my pull request adding problem 993's OEIS tree-count sequence, A000055, to his database. The pull request's description cites this check; the database entry itself links only the sequence, and erdosproblems.com now shows that link on the problem's page. It does not mean he endorses the result. On September 18, 2026, he merged a second pull request of mine, adding OEIS links to seven problems.

When you read that a computer or an AI "solved" a math problem, it helps to ask two questions. Was the result a proof covering every case, or a check of every case up to some size? And does its listing on a public page mean that experts accepted a proof, or only that a link to the work was added? For the tree result, it was a check that extended earlier ones to every tree up to 32 dots, and the database listing is a link to the OEIS tree counts that the check was measured against.

For specialists: the method

Erdős Problem #993 (Alavi, Malde, Schwenk and Erdős, 1987) conjectures that the independence sequence of every tree and every forest is unimodal. This check covers free (unlabeled) trees only, counted by A000055; forests on the same number of vertices are not implied, since unimodality is not preserved under products of polynomials. Trees were generated with nauty's gentreeg and streamed as edge lists. For each tree, the independence polynomial was computed exactly with the standard in/out subtree dynamic program, using 64-bit integer coefficients; a tree on 32 vertices has at most 2,147,483,649 independent sets (the star, two to the 31st plus one), so no coefficient can overflow. The scanned sequence includes the constant term, and the scan flags only a strict increase after a strict decrease, so plateaus are allowed. Large orders were split with gentreeg's residue classes (16 parts at orders 31 and 32), and the summed per-order counts match the OEIS values exactly. Before extending, the n = 28 and n = 29 tree counts of Reynolds's computation were reproduced exactly by this independent implementation. This is an exhaustive check up to the stated order and not a proof; it says nothing about larger orders.

@misc{orden2026explainercheckedisnotproved,
  author       = {Tyler Satchel Orden},
  title        = {Why checking a math conjecture on every case up to a size is not a proof},
  year         = {2026},
  howpublished = {Cyborg Mathematics},
  url    = {https://cyborgmathematics.com/writing/explainer-checked-is-not-proved}
}