K_h-minor-free separators O(h√n): two AI-assisted proofs
Awaiting review
Importance: major (4 of 5)The takeaway
Two preprints claim the 1990 Alon–Seymour–Thomas conjecture that every n-vertex K_h-minor-free graph has a balanced separator of size O(h√n).
Status
- Claim
Awaiting review
- Our reporting
- Medium confidence
- Verification
- Lean-verified
- Importance
- Major (4 of 5)
- Last verified
- 3 November 2026
Your AI and this story
- GPT-6 Astra187 days after its cutoff
- Claude Opus 5.5126 days after its cutoff
- Gemini 4 Argon217 days after its cutoff
- Grok 4.7156 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 126 days before it.
Key facts
- Conjecture: Alon, Seymour, Thomas, ‘A separator theorem for nonplanar graphs’ (JAMS 1990) proved O(h^{3/2}√n) and conjectured O(h√n)
- arXiv 2611.00663 (Conroy, Le, Spalding-Jamieson): proof builds on Le’s 2026 framework; new idea is a short hitting walk on vertex expanders (length O(k/ψ(G)) hitting k large subsets)
- AI disclosure 2611.00663 (verbatim): ‘The key technical ideas of this paper are due to GPT-6 Astra, with some simplification due to Claude Opus 5.5. A Lean formalization of our main result was produced using a combination of GPT-6 Astra and Claude Opus 5.5 … The human authors claim no role in developing the technical ideas.’ The rewritten human proof has ‘a slightly worse constant than the formalization’
- arXiv 2610.40270 (Xinheng Lin): separator of size ≤ min{n, 21h√n} for h ≥ 3; ‘developed under the author’s guidance with the assistance of ChatGPT 6pro … GPT 6.1 Sol (Max) was also used to check the proof repeatedly’
- Verification status: two independent unrefereed preprints; 2611.00663 has a Lean formalization of the main result (definitions checked by the authors); no expert commentary or HN discussion found by 3 Nov
What happened
Within four days two independent preprints claimed the O(h√n) separator bound for K_h-minor-free graphs conjectured by Alon, Seymour and Thomas in 1990. Lin’s paper (listed in the 30 Oct catalogue) was written with ChatGPT 6 Pro. The Conroy–Le–Spalding-Jamieson paper says the ideas came from GPT-6 Astra, with simplifications by Claude Opus 5.5, and that the main result was formalized in Lean.
Why it matters
The separator theorem underlies many algorithms on minor-closed graph classes. Two separate AI-assisted proofs, one with a Lean check, make this one of the stronger AI-originated claims on a well-known conjecture so far, though neither is refereed.
What is disputed or not yet verified
| Verification | Preprints; Lean formalization for 2611.00663 |
|---|
Sources
2 sources from 1 site. Numbers match the chips in the text.
2 sources: 2 primary
Primary
Changes
- Filed. Promotes the Lin lead of 30 Oct