News · 2026-10-05

An AI-assisted Erdős 993 proof claim is public, but acceptance remains unresolved

Tong Zhang has submitted a proof claiming that every finite forest has a unimodal independence polynomial, the statement associated with Erdős problem 993. The September 26 submission is public and describes AI assistance, but its mathematical acceptance remains unresolved, and separate Lean projects report machine checks that have not been independently rerun in the dossier.

Key facts

• The September 26 manuscript claims the all-forest conjecture dating to 1987.
• Its proof map combines a finite-order argument through 60 vertices with a general argument from 59 onward.
• The prize review request remains open; the author says the manuscript lacks independent human review and Lean certification.
• The primary source is Tong Zhang’s public submission.

A forest in mathematics is a graph with no cycles. An independent set is a choice of vertices with no connection between any two selected vertices. Count how many independent sets contain zero vertices, one vertex, two vertices and so on. The conjecture says these counts rise to a peak and then fall, allowing ties: they do not fall and later rise again. It is a compact statement about a large family of structures.

Tong Zhang’s manuscript is titled “Exact Certificates for Unimodality of Forest Independence Polynomials.” That title matters because the submission combines a written argument with computational certificates; it does not claim that a program simply enumerated every possible large forest. Its versioned repository provides a traceable artifact behind the public review request.

The submitted proof describes one argument for smaller forests and another for sufficiently large ones. Their ranges overlap: through 60 vertices for the finite-order part and from 59 onward for the general part. The overlap is like two bridge sections meeting with some shared span. It prevents an uncovered size range if both arguments are valid, but it does not establish that the bridge is structurally sound. Review still has to examine the actual reasoning and dependencies.

The submission discloses AI help with proof auditing, computational reproduction, research and manuscript preparation. It reports two scoped AI-assisted reviews that found no concrete gap in checked reductions. The author distinguishes those reviews from independent human peer review. A model checking another model’s argument may surface errors, but agreement among models is not an acceptance procedure and does not make a mathematical claim true.

Authorship also needs to remain version-specific. The September 26 submission identifies Tong Zhang as author and mathematical contributor. A later verification repository describes a Tong Zhang and Wei Li manuscript and names Wei Li as corresponding author. The circulating Reddit attribution should not be retroactively pasted onto the earlier version. The difference is documented; the dossier does not resolve it by inventing one combined authorship history.

The machine-check story is separate. Kevin Vallier’s repository describes an AI-agent-produced Lean formalization, including finite-order checks and a different large-order argument. Its notes report 271 uses of a mechanism called native_decide. That mechanism expands the trust assumptions to include relevant compiler and runtime behavior alongside Lean’s usual proof-checking foundation. The repository says no human reviewed the Lean code line by line.

Xiang Li’s repository reports a successful clean rebuild of 31,598 modules on October 2 and lists the axioms associated with its theorem. Its notes also distinguish its evidence audit from replaying the kernel check. The related prize submission is open. These are inspectable reports about particular formal artifacts, not independent reruns conducted for this briefing.

A helpful analogy is compiling a legal contract into a strict validation system. The system can verify that the encoded rules fit its logic. Someone still has to ensure that the encoded rules state the intended agreement. Proof assistants offer a much stronger check than persuasive prose, but the theorem statement, assumptions and translation all matter. Autoformalization explains the extra challenge of turning a natural-language argument into that formal statement.

The official Erdős problem page still describes the problem as open in the reviewed material. That label does not disprove a newer submission; neither does an open pull request prove its claim. The appropriate status is pending review. The public discussion establishes community circulation, not expert acceptance.

The strongest counterargument to a solved-by-AI headline is therefore procedural and mathematical: different manuscripts, formalization projects and build reports must not be collapsed into a single accepted theorem. The promising development is a concrete, versioned proof claim with computational support that others can inspect. The honest caveat is that the dossier establishes the existence and stated scope of those artifacts, not the correctness of the proof, independent machine reproduction or an awarded solution.

Primary source, verified: read the paper →

Ground Truth. (2026, October 5). An AI-assisted Erdős 993 proof claim is public, but acceptance remains unresolved. Ground Truth. https://groundtruth.day/news/erdos-993-proof-submission-awaits-review.html

@misc{groundtruth:erdos-993-proof-submission-awaits-review,
  title  = {An AI-assisted Erdős 993 proof claim is public, but acceptance remains unresolved},
  author = {{Ground Truth}},
  year   = {2026},
  month  = {oct},
  url    = {https://groundtruth.day/news/erdos-993-proof-submission-awaits-review.html}
}

Topics: mathematics · ai-research · formal-verification