What was already known
Bukh and Conlon proved the corresponding result for finite families of forbidden graphs in 2018. Later work established many ranges of rational exponents for a single forbidden graph, but the full single-graph conjecture of Erdős and Simonovits remained open.
AI involvement
Epoch's provenance account says GPT-6 Astra found the proof in a network-isolated run without problem-specific hints or human steering. Thomas Bloom selected and reviewed the formal task; Tom Adamczewski operated the harness and packaged the output with documented mechanical porting changes. Conlon, Janzer, Jiang, Kim, Lee, Liu, Longbrake and Yepremyan later explained the proof and its mathematical antecedents.
The original run provenance explicitly reports no problem-specific hints or human steering. Human statement selection, mechanical packaging and later explanation are credited separately.
Importance
Resolves a longstanding central question in extremal graph theory: every rational growth exponent between one and two is realized by a single bipartite forbidden graph.
Limitations
The assessed result is the single-graph statement for 1 ≤ r < 2. It does not resolve the stronger Bukh–Conlon rooted-tree-power conjecture or the Kang–Kim–Liu subdivision conjecture. The proof builds on substantial earlier human mathematics. The autonomous run used a larger budget outside the fixed FrontierMath Erdős scoring protocol. Formal verification is reported by the benchmark and repository CI for the pinned statement; this review inspected their statement and verification records without rerunning Lean. The later human exposition explains the argument and its sources; it is not a second AI discovery or evidence of journal peer review.
Technical verification
The benchmark reports pristine-container Comparator checking of the full statement. Successful CI for the exact pinned commit is publicly recorded; the reviewed theorem matches the 1 ≤ r < 2 bipartite single-graph scope.
Independent checking
Eight named extremal combinatorialists give a complete human exposition of the claimed AI proof and explain how it uses earlier methods; no journal peer review is asserted.
- Checker
- Conlon, Janzer, Jiang, Kim, Lee, Liu, Longbrake and Yepremyan
- Scope
- Human reconstruction and explanation of the rational-exponents proof; the stronger related conjectures remain open.
- Basis
- Reported by the linked checker
- Check date
- 2026-10-13
Formal checking
Successful CI for the pinned source commit reports build and Comparator verification. AIProofWatch inspected the public run status and contract, without rerunning the prover.
- Checker
- Epoch AI benchmark harness and repository Lean/Comparator CI
- Scope
- Erdos571.erdos_571: every rational 1 ≤ r < 2 is the extremal exponent of a finite bipartite graph, with standard axioms only.
- Basis
- Reported by the linked checker
- Check date
- 2026-09-21
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Conlon, Janzer, Jiang, Kim, Lee, Liu, Longbrake and Yepremyan give a human exposition of the central rooted-graph construction and upper-bound argument, connecting it to prior results. This October account supersedes the original repository’s September note that the proof had not yet been digested.
Correction and publication history
Historical backfill after primary-source provenance, exact formal statement, successful pinned CI and October 13 human exposition were reviewed under CURATION.md. Original report date follows Bloom's September 3 proof sketch. Notifying events are disabled.
Read this published revision