---
id: "2026-10-17-erdos-hajnal-all-paths-nguyen-astra-deepmind"
url: "https://postcutoff.com/e/2026-10-17-erdos-hajnal-all-paths-nguyen-astra-deepmind/"
as_of: "2026-10-20T07:28:00+02:00"
date: "2026-10-17"
date_precision: day
category: science
importance: 5
confidence: medium
status: [Awaiting review]
verification: Lean-verified
sources: 4
editor: human editor
human_review: null
version: null
---

As of: 2026-10-20 07:28 CEST.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/e/2026-10-17-erdos-hajnal-all-paths-nguyen-astra-deepmind/

# Erdős–Hajnal conjecture proved for every path P_t

Full title: Erdős–Hajnal conjecture proved for every path P_t: Tung H. Nguyen, with ChatGPT-6 Astra proving key lemmas; a DeepMind internal model reached the same result independently, and Claude Opus 5.5 manuscripts claim P6 and all paths

arXiv 2610.24887 (17 Oct 2026), "Erdős–Hajnal for excluding paths" by Tung H. Nguyen (Oxford), proves that every path P_t has the Erdős–Hajnal property: P_t-free graphs on n vertices have a clique or stable set of size n^c. The previous frontier was P5 (Nguyen–Scott–Seymour, 2023). The paper credits ChatGPT-6 Astra with the full purity version of Lemma B.2 and with a proof of Lemma 3.9 for r = 5, which the author generalized; the main ideas are the author's. The paper also reports that a Google DeepMind internal model independently proved the P6 case and then all paths, with a Lean formalization (to be posted on GitHub, not arXiv), and that two Claude Opus 5.5 manuscripts on GitHub claim P6 and all P_t, without independent expert review.

## Key facts
- Paper: 'Erdős–Hajnal for excluding paths', Tung H. Nguyen (Titchmarsh Research Fellow, Oxford), arXiv 2610.24887 [math.CO], 17 Oct 2026. Theorem 1.2: 'P_t has the Erdős–Hajnal property for all t ≥ 1.' Theorem 1.3 extends it to the subdivided claws S_{1,2,t} and S'_{1,2,t} (covering the bull, E and the bird)
- Conjecture (Erdős and Hajnal, 1977): for every graph H there is b with every H-free graph G having a clique or stable set of size |G|^(1/b). It remains open in general
- New ingredient (abstract): 'a novel Gyárfás path argument based on the ideas of bookkeeping blockades and splitting paths'
- AI declaration, verbatim: 'ChatGPT-6 Astra was mathematically involved in Subsections 3.3 and 4.1 and Section B; the ideas in the rest of this paper are entirely due to the author.' The author asked Astra for a weaker version of Lemma B.2 and 'Astra then succeeded in proving the full purity version'; after discussions directed by the author, 'Astra discovered a proof of Lemma 3.9 for r = 5', which the author extended to all r; Subsection 4.1 was 'cleaned up by Astra'. Writing by the author with copy-editing from ChatGPT-6 Luna; figures by ChatGPT-6 Sol
- Google DeepMind (concurrent work section): a team 'including Junehyuk Jung, Joonkyung Lee, Thang Luong, and Aranyak Mehta' told the author that 'a DeepMind internal model had produced a proof of the Erdős–Hajnal property of P6; the proof was verified by Joonkyung Lee and accompanied by a Lean formalisation'. They then 'obtained further results including the P_t case'. The Google team will post its AI-generated manuscript and Lean proof on GitHub rather than arXiv, 'since they want to ensure that their material on the arXiv meets the standards of the mathematical community'. 'At the time of submission, neither team had seen the other's manuscript'
- Claude manuscripts named in the paper: 'an anonymous GitHub repository contains an AI-generated manuscript claiming to prove the Erdős–Hajnal property of P6, produced by Claude Opus 5.5; and another GitHub repository by Yuwen Zhou contains a manuscript claiming to prove Theorem 1.2 (also available on Zenodo), assisted by Claude Opus 5.5 … We are not aware of independent expert reviews of either manuscript'
- The P6 repository is machine-qed/erdos-hajnal-six-vertex-path (created 27 Sep 2026): a 24-page paper plus Lean 4, 'produced by Claude Opus 5.5 (Anthropic) and has not been refereed'; it proves a polynomial Rödl property with τ < 10^−15, not computed numerically
- Yuwen Zhou (UBC Okanagan), OctopusTide/erdos-hajnal-all-paths (created 8 Oct 2026, Zenodo DOI 10.5281/zenodo.23270286): the Lean main theorem AllPathsLocal.eh_all_paths takes three hypotheses (hRodl, a combinatorial lemma hcomb and EH for P6), so the formal statement is conditional on inputs supplied as assumptions, as the README shows
- Not found as of 20 Oct morning: the DeepMind manuscript or repository (google-deepmind GitHub org checked; newest maths repo is cryptids, 9 Oct), an announcement by DeepMind, or expert reactions on HN

## What happened

The Erdős–Hajnal conjecture says that forbidding any fixed induced subgraph H forces a polynomial-size clique or stable set,
far more than the logarithmic size guaranteed in general. Paths were a central test case: P5 was settled in 2023 by Nguyen, Scott
and Seymour. Nguyen's new paper does every path. Its AI declaration is unusually exact about which lemmas GPT-6 Astra proved.

The paper's "Concurrent work" section reports a race. A Google DeepMind and Google Research team contacted Nguyen to say an internal
model had proved the P6 case, checked by Joonkyung Lee and in Lean. After Nguyen told them about his P_t result, the model was run
further and also produced the P_t case. The two teams agreed to publish separately and on different platforms. Two GitHub projects
built with Claude Opus 5.5 also claim P6 and all paths.

## Why it matters

It is a major case of one of the central open problems in graph theory, reached almost at once by a human mathematician working
with one lab's model and, on his account, by another lab's model working largely on its own. DeepMind's choice to keep its
AI-generated manuscript off arXiv reflects the current argument over AI-written papers.

## What is disputed or not yet verified

- Verification: Unrefereed arXiv preprint; DeepMind's P6 proof verified by Joonkyung Lee with Lean (not yet public); the Claude manuscripts have Lean code but no expert review, and Zhou's Lean theorem is conditional

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 170 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 109 days after its cutoff
- Gemini 4 Argon (training cutoff March 2026): 200 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 139 days after its cutoff

## Sources

1. [arXiv 2610.24887: Erdős–Hajnal for excluding paths (Tung H. Nguyen)](https://arxiv.org/abs/2610.24887) (arxiv.org, paper)
2. [machine-qed/erdos-hajnal-six-vertex-path: P6 proof produced by Claude Opus 5.5, with Lean (unrefereed)](https://github.com/machine-qed/erdos-hajnal-six-vertex-path) (github.com, code)
3. [OctopusTide/erdos-hajnal-all-paths: Yuwen Zhou's all-paths manuscript and Lean code](https://github.com/OctopusTide/erdos-hajnal-all-paths) (github.com, code)
4. [Zenodo record of Zhou's manuscript](https://doi.org/10.5281/zenodo.23270286) (doi.org, paper)

## Changes

- 2026-10-20 (filed): Created (PDF read in full text; GitHub repositories checked)

## Related

- 2026-10-20: [AI-assisted results in the 20 Oct 2026 arXiv listing](https://postcutoff.com/e/2026-10-20-ai-assisted-results-october-20-listing/index.md)
- 2026-10-19: [Erdős–Szemerédi sunflower conjecture proved for every k ≥ 3](https://postcutoff.com/e/2026-10-19-erdos-szemeredi-sunflower-conjecture-gpt-6-astra-pro/index.md)
- 2026-09-15: [Erdős–Hajnal high-girth problem (Erdős #108) disproved with ChatGPT/Codex help and a Lean proof, via the Conjectures.io bounty; experts sharpen it with GPT-6 Astra](https://postcutoff.com/e/2026-09-15-erdos-108-high-girth-problem-disproved-conjectures-io/index.md)