Lee–Loh–Sudakov directed-cut conjecture proved with AI, Lean-verified
Awaiting review
The takeaway
A 2013 conjecture on judicious partitions of digraphs, answering Scott’s 2005 question for large graphs, was first proved by an AI research framework; the authors say the proofs are Lean-verified.
Status
- Claim
Awaiting review
- Our reporting
- Medium confidence
- Verification
- Lean-verified
- Importance
- 3 of 5
- Last verified
- 17 October 2026
Your AI and this story
- GPT-6 Astra169 days after its cutoff
- Claude Opus 5.5108 days after its cutoff
- Gemini 4 Argon199 days after its cutoff
- Grok 4.7138 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 108 days before it.
Key facts
- Paper: ‘Optimally large cuts in both directions’, Frederic Folz & Mykhaylo Tyomkyn, arXiv 2610.21381 [math.CO]
- Results: the sharp bound above for all large m (Theorem 1.1); ⌈m/6⌉ achievable for d = 2 and every m; a stability result describing near-extremal digraphs (Theorem 1.4)
- Background: Scott (Surveys in Combinatorics 2005) asked for the largest c(d) such that every digraph with minimum outdegree ≥ d has a bipartition with both directed cuts ≥ c·m; Lee, Loh & Sudakov (‘Judicious partitions of directed graphs’, arXiv 1305.2986, RSA 2016) conjectured c_d = (d−1)/(2(2d−1)) and showed it cannot be raised
- AI statement (quoted): ‘The proof of Theorem 1.2 was first discovered by the Altifina research framework, which combines multiple AI models—in this work, OpenAI’s ChatGPT 6 Astra and 6.1 Sol, as well as Anthropic’s Claude Opus 5.5. The proof was revised and extended by the second author, aided by ChatGPT 6 Astra, leading to the main results of this paper, Theorems 1.1 and 1.4. The proofs have been verified in Lean, and a certificate is available upon request. The presentation is human-written and proofread with ChatGPT 6 Astra.’
- Abstract: ‘The proofs were obtained by LLMs, with human input. They have been revised by the authors and verified in Lean.’ The Lean code is not public (certificate ‘available upon request’)
- First author’s affiliation is Altifina Discovery Lab (Überherrn, Germany), the company behind the framework; no Altifina announcement or Hacker News thread found by Oct 17
What happened
Folz and Tyomkyn’s preprint appeared in arXiv’s 16 Oct 2026 announcement. A random-partition argument needs a deterministic criterion (built from a partition of components into induced stars, going back to Erdős, Gyárfás and Kohayakawa) to guarantee both directed cuts are large at once. The authors say that criterion’s proof (Theorem 1.2) was first found by the Altifina framework, then revised and extended by Tyomkyn with ChatGPT 6 Astra into the sharp theorem and the stability result.
Why it matters
It is one more named conjecture by well-known combinatorialists (Po-Shen Loh, Benny Sudakov) settled with an AI-first proof. The Lean claim cannot be checked yet because the certificate is not public. The first author’s affiliation shows a small company running a multi-model “research framework” that combines OpenAI and Anthropic models.
What is disputed or not yet verified
| Verification | Unrefereed preprint; authors state Lean verification (certificate on request, not public) |
|---|
Sources
2 sources from 1 site. Numbers match the chips in the text.
2 sources: 2 primary
Primary
Changes
- Filed (arXiv /list/math/new page for 16 Oct 2026, read because the arXiv API returned HTTP 429; PDF read with pdftotext)