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
On Sept 15, 2026 Purdue's Jensen Kohlmeyer and Liam Kruer (as "JenW1N") submitted a Lean 4 proof to the Conjectures.io bounty platform that disproves Erdős Problem #108, the Erdős–Hajnal question from the late 1960s of whether huge chromatic number forces a subgraph with large girth and large chromatic number. They built triangle-free graphs of arbitrarily large chromatic number whose four-cycle-free subgraphs are all 6-colourable. Their manuscript says the work "was developed with substantial assistance from OpenAI ChatGPT/Codex". On Oct 1 graph theorists Tung Nguyen and Bartosz Walczak published an exposition that lowers 6 to 3. They credit ChatGPT-6 Astra with discovering the key new proof.
Key facts
- Problem: for every r ≥ 4 and k ≥ 2, is there f(k,r) such that every graph with chromatic number ≥ f(k,r) has a subgraph of girth ≥ r and chromatic number ≥ k? (Erdős–Hajnal; Rödl proved r = 4). The answer is no already at girth 5 and k = 7
- Construction: arc graphs over an ordered multipartite random base graph (the Janzer–Steiner–Sudakov model); every C4-free subgraph splits into a bounded-degree-controlled part (4-colourable) and a forest (2 colours)
- Verification: the main theorem and the negation of Google DeepMind's pinned Formal Conjectures statement (ErdosProblems/108.lean) were proved in Lean 4 (v4.33.1) using only standard axioms; Conjectures.io lists it as Lean-verified and approved in human review, with a $3,833 reward paid
- AI disclosure (Kohlmeyer & Kruer): 'This work was developed with substantial assistance from OpenAI ChatGPT/Codex, including mathematical exploration, the preparation and checking of estimates, construction and debugging of the Lean proofs, and drafting and typesetting of the manuscript.' Conjectures.io's own write-up was 'prepared by Conjectures with Codex assistance from the accepted Lean submission'
- Nguyen & Walczak (arXiv 2609.40192, Oct 1): improved 6-colourable to 3-colourable. 'ChatGPT-6 Astra discovered a proof of Theorem 2.1, in particular proposing Lemma 5.1 as a suitable extension of Lemma 4.3.' The step from 6 to 4 was done 'entirely by the authors … with no AI tools involved'
- Nguyen & Walczak note that both earlier manuscripts 'lack any references to the literature except for' Janzer–Steiner–Sudakov, and that the Lean-derived write-up 'may not be readily accessible to researchers in graph theory'
- Platform: Conjectures.io (Bittensor subnet 66) pays for Lean-verified proofs of formalised open problems. By Oct 5 its results page listed 26 problems solved and $127,713 paid; JenW1N also has accepted solves of Erdős #859, #18(b), #1062(ii) and Green's open problems 24 and 40 (Sept 15–25)
- erdosproblems.com still showed #108 as OPEN with one proof claim on Oct 5, 2026
Science result
- Field
- mathematics / graph theory (chromatic number, girth)
- Problem
- Erdős Problem #108: Erdős–Hajnal high-girth, high-chromatic subgraph problem (open since 1969)
- Result
- Negative answer: for every M there is a triangle-free graph with χ > M whose C4-free subgraphs are all 6-colourable (Kohlmeyer–Kruer, Lean-verified); improved to 3-colourable by Nguyen–Walczak.
- AI system
- ChatGPT, Codex, GPT-6 Astra
- Human role
- AI-assisted: two Purdue authors developed the construction and the Lean proof with substantial ChatGPT/Codex help. In the follow-up, GPT-6 Astra found the proof of the 3-colourable lemma and the experts streamlined it.
- Verification
- Formal proof in Lean 4 (Conjectures.io, against DeepMind's Formal Conjectures statement) plus an independent expert exposition (arXiv 2609.40192); the 3-colour improvement is an unrefereed preprint
- Status
- confirmed
- Why surprising
- A 1960s Erdős–Hajnal problem was settled through a crypto-funded Lean bounty, by authors who credit ChatGPT/Codex, before it reached arXiv.
What happened
Erdős and Hajnal asked whether a graph with enormous chromatic number must contain a subgraph that has both large girth and large chromatic number. Rödl settled girth 4 (triangle-free subgraphs), and the general question stayed open as Erdős Problem #108. Google DeepMind's Formal Conjectures project had pinned it as a Lean statement. Conjectures.io, a Bittensor subnet that pays for Lean-checked proofs, offered a bounty for it.
On Sept 15, 2026 the solver "JenW1N", identified in the manuscripts as Purdue's Jensen Kohlmeyer with Liam Kruer, submitted a Lean proof of the negation. They take arc graphs of a carefully sized random multipartite graph. In these graphs any subgraph without a four-cycle is 6-colourable, yet the whole graph has arbitrarily large chromatic number. The platform verified the proof and approved it in human review. It paid the bounty and published an explanatory PDF that Codex prepared from the Lean code.
Graph theorists Tung Nguyen and Bartosz Walczak learned of the result from the Conjectures.io announcement. On Oct 1 they posted an exposition on arXiv that ties each step to the literature. Working without AI, they observed that the construction already gives 4 colours. They then asked ChatGPT-6 Astra for a 2-degenerate version of the key lemma. Astra found the proof, which brings the bound down to 3 colours.
Why it matters
This is a well-known problem from Erdős's list, and the counterexample comes with a machine-checked proof. Independent experts have checked it and improved on it. It also shows a new route for AI-assisted mathematics: paid, Lean-gated bounties outside arXiv, where the first write-up was itself machine-generated. Nguyen and Walczak's note criticises the lack of literature context in those write-ups. We found no Hacker News thread about the result, and we did not locate the original Conjectures.io announcement post on X.
Changelog
- 2026-10-05: created (06:30 run; found via the AI disclosure in arXiv 2609.40192, which the sweep's date window missed)
People
Related events
- Summer 2026 flood: dozens of named conjectures settled on arXiv with disclosed AI help (July–September catalogue) ★★★★
- Pre-release GPT-6 Astra disproves Erdős's 'first serious problem' (1931, $500) and proves the rational-exponents conjecture, all Lean-verified, in Epoch's FrontierMath Erdős runs ★★★★★
- ChatGPT Astra finds geometric triangle-free graphs with near-optimal chromatic number, the first improvement on Burling's 1965 box bound ★★★
Sources (7)
- paperKohlmeyer & Kruer: A counterexample to Erdős problem 108 via arc graphs (dated Sept 15, 2026)
- paperConjectures.io write-up: Erdős Problem 108, high chromatic number with six-colour C4-free subgraphs (Sept 17)
- officialConjectures.io problem page: Erdős 108
- officialConjectures.io results (bounties paid)
- paperarXiv 2609.40192: Nguyen & Walczak, On the solution to the Erdős–Hajnal problem on high-girth high-chromatic subgraphs
- docsErdős Problems #108
- codeGoogle DeepMind Formal Conjectures repository
id: 2026-09-15-erdos-108-high-girth-problem-disproved-conjectures-io · updated 2026-10-05 · open in the interactive timeline