Graham conjectured that every finite set of points on a sphere is Ramsey. In September 2026 Dömötör Pálvölgyi, with ChatGPT, refuted it with seven points on a circle, and OpenAI classified exactly which finite sets are Ramsey, in Lean. Pálvölgyi’s appendix, labelled by its author as ChatGPT’s and unchecked, goes further: almost any seven points on a circle are not Ramsey. I decided both in Lean through OpenAI’s own theorem, with the rules sealed before any code ran, and the pull request that marks Graham’s conjecture solved in Google DeepMind’s list now links the proof.
The heptagon and Theorem A.3 are Dömötör Pálvölgyi’s, with ChatGPT; the classification that decides them is OpenAI’s. This page decides them in Lean; it is not new mathematics. The Lean is mine, written by Claude (Anthropic’s AI model) under my direction.
The rules were sealed before any code ran; four things differ from them, and the record keeps all four.
Take a finite set of points, like the corners of a triangle. It is Ramsey if, for any number of colours, once the dimension is high enough every colouring of space contains a copy of it, the same shape and size, all in one colour. In 1973 Erdős, Graham, Montgomery, Rothschild, Spencer and Straus proved that a Ramsey set must lie on a sphere. Graham conjectured the converse: every finite set on a sphere is Ramsey.
In DeepMind’s list the conjecture is Erdos174.erdos_174.variants.graham in FormalConjectures/ErdosProblems/174.lean, still marked open at commit 2055e5a.
On 20 September 2026 Pálvölgyi posted A cyclic non-Ramsey heptagon. Its Theorem 1 is the seven points above; its proofs are attributed to ChatGPT (“I contributed nothing to the proofs or ideas”), and its appendix, headed “Appendix by ChatGPT — unchecked”, states Theorem A.3: seven points on a circle whose parameters are generic are not Ramsey. Three days later OpenAI published a classification of finite Euclidean Ramsey configurations with its Lean in openai/math: a set is Ramsey exactly when it passes an algebraic test, the field criterion. OpenAI cites the heptagon and says A.3 “already implies” its own nine-point counterexample.
No one had the heptagon in Lean. DeepMind’s entry for Graham’s conjecture stayed open; on 31 October Anas Khan opened pull request #7706 to re-tag it as solved, with the statement ¬ (∀ …) and no proof.
| question | what was done | verdict |
|---|---|---|
| H1 · are the identities right? | two clean-room deciders, written from the paper alone: 97 and 152 identities, exact, with r and the t’s symbolic | CERTIFIED |
| H2 · is the heptagon not Ramsey, in Lean? | through OpenAI’s criterion and theorem, transported to DeepMind’s statement copied byte for byte | CERTIFIED |
| H3 · do the kernels accept it? | Lean from scratch on three roots; nanoda, con-ron, lean4lean, con-leche on the closures and the whole environment | CERTIFIED |
| H4 · is Theorem A.3 true as printed? | its finite content by both deciders; then a Lean proof on the same chain | CERTIFIED |
| D · the corollary in OpenAI’s nine-point shape? | seven points with independent parameters, OpenAI’s statement token for token | CERTIFIED |
| H5 · who did what first? | the dated sources | a reading |
| H6 · can the checks be fooled? | 11 planted fakes | 11 of 11 caught |
Before any Lean, two programs decided the paper’s algebra exactly, each written from the paper’s text alone, neither reading the other: one in SymPy (97 identities, all 97 CERTIFIED, its 11 planted false identities all refused), one in the Python standard library with its own polynomial arithmetic (152 identities, all CERTIFIED; 3 planted wrong versions of the heptagon and of A.3, each caught). For the heptagon: the moments vanish and the energy is Σλ‖D(p)‖² = −24/((2r−1)(2r−3)(2r−4)). For A.3, every finite identity of the proof holds for any seven distinct parameters; algebraic independence enters only where a derivation is chosen.
One remark on the paper. The main text’s Equation (2) asks the matrix M = Σλ D(p) pᵀ to vanish, and for the heptagon it does. For A.3’s points it does not: at t = (0, 1, 2, 3, 5, 7, 11) it is [[92/19825, -86/19825], [-86/19825, -92/19825]], symmetric and not zero. The appendix’s proof goes through Lemma A.1, which asks only that M be symmetric, so A.3 is right as printed; it could not have been proved through Equation (2). The Lean proof carries the symmetric form too.
On OpenAI’s chain, unchanged: a derivation D of the reals with D r = 1 (their exists_real_derivation), the pairing x ⊗ y ↦ D x · D y on their tensor ring, and Pálvölgyi’s weights give a nonzero trace, so the heptagon fails the criterion:
theorem not_fieldCriterion : ∀ (r : ℝ), 2 < r → Transcendental ℚ r → ¬OAI.EuclideanRamsey.FieldCriterion (HeptagonRamsey.Heptagon.heptagon r)
The necessity half of their classification turns that into the theorem, and a transport carries it to DeepMind’s definition, with the zero-dimensional case handled as in issue #7517:
theorem not_ramsey : ∀ (r : ℝ), 2 < r → Transcendental ℚ r → ¬OAI.EuclideanRamsey.Ramsey (HeptagonRamsey.Heptagon.heptagon r)
theorem graham_false' : ¬∀ {n : ℕ} (A : Set (EuclideanSpace ℝ (Fin n))), A.Finite → EuclideanGeometry.Cospherical A → Erdos174.IsRamsey AThe second statement is pull request #7706’s, token for token. DeepMind’s IsRamsey and the conjecture’s statement are copied from the pinned file, 273 and 113 bytes, and a script refuses the build if one byte differs (it refuses a one-token change, as it must). The build: 8,949 jobs, no warning from our files.
A.3 says: if three of the parameters are distinct and the other four are algebraically independent over the field the three generate, the seven points ((1 − t²)/(1 + t²), 2t/(1 + t²)) are not Ramsey. The Lean proof follows the appendix: Lemma A.1 in its symmetric form, a derivation vanishing on that field with prescribed values on the four (OpenAI’s construction generalised from ℚ to any base field), and the weighted moments by Lagrange interpolation.
theorem generic_seven_not_ramsey : ∀ (t : Fin 7 → ℝ),
(Function.Injective fun i => t ⟨↑i, ⋯⟩) →
(AlgebraicIndependent ↥(HeptagonRamsey.Generic.baseField t) fun i => t ⟨↑i + 3, ⋯⟩) →
¬OAI.EuclideanRamsey.Ramsey (HeptagonRamsey.Generic.circ t)Its corollary in exactly the shape of OpenAI’s nine-point theorem, seven points whose parameters are algebraically independent over ℚ, in their literal parametrisation (a script checks it against their statement token for token, and refuses two planted changes):
theorem seven_circle_configuration : ∀ (t : Fin 7 → ℝ),
AlgebraicIndependent ℚ t →
Function.Injective (HeptagonRamsey.Generic.literal t) ∧
(∀ (i : Fin 7), dist (HeptagonRamsey.Generic.literal t i) 0 = 1) ∧
¬OAI.EuclideanRamsey.Ramsey (HeptagonRamsey.Generic.literal t)wstrinz (Will Strinz) had certified one instance of A.3 exactly in October, three rational points and four independent ones. This is the first proof of the theorem as stated, and the first in Lean.
An audit that walks the dependency closure itself, and Lean’s own #print axioms, agree: all six theorems rest on propext, Classical.choice, Quot.sound and nothing else, closures of 29,244 to 34,515 constants. The audit refuses each of seven planted fakes (a sorry, an axiom, native_decide and four others) and passes a clean control.
Besides Lean’s own, the kernels below were each written apart from Lean. The rows marked “before the rename” ran on the same proofs before the library’s namespace was renamed for publication; the rename changed the name and nothing else, and the published code was re-run through Lean, nanoda and con-ron.
| kernel | on | what | verdict |
|---|---|---|---|
| Lean, from scratch | Heptagon.Transport | the whole import closure replayed into an empty environment · 38 min, 8.5 GB | accepts |
| Lean, from scratch | Generic.A3 | the whole import closure replayed into an empty environment · 38 min, 8.5 GB | accepts |
| Lean, from scratch | Generic.Seven | the whole import closure replayed into an empty environment · 36 min, 8.5 GB | accepts |
| nanoda | the six theorems’ closure | 38,527 declarations, only the three axioms permitted | accepts |
| con-ron | the six theorems’ closure | 36,840 declarations | accepts |
| nanoda | the corollary closure | 35,062 declarations · 8 s · before the rename | accepts |
| nanoda | the whole environment of both | 719,017 declarations · 5 min · before the rename | accepts |
| con-ron | the corollary closure | 33,485 declarations · 7 s · before the rename | accepts |
| con-ron | the heptagon’s whole environment | 702,354 declarations · 3 min · before the rename | accepts |
| con-ron | the whole environment of both | 702,480 declarations · 2 min · before the rename | accepts |
| lean4lean | the heptagon closure | 35,639 declarations · 53 s · before the rename | accepts |
| lean4lean | the A.3 closure | 33,048 declarations · 48 s · before the rename | accepts |
| lean4lean | the corollary closure | 33,482 declarations · 59 s · before the rename | accepts |
| lean4lean | the heptagon’s whole environment | 702,351 declarations · 51 min · before the rename | accepts |
| lean4lean | the whole environment of both | 702,477 declarations · 49 min · before the rename | accepts |
| con-leche | the heptagon closure | 35,642 declarations · 11 s · before the rename | accepts |
| con-leche | the A.3 closure | 33,051 declarations · 11 s · before the rename | accepts |
| con-leche | the corollary closure | 33,485 declarations · 10 s · before the rename | accepts |
| con-leche | the whole environment of both | 702,480 declarations · 12 min · before the rename | accepts |
A forged export, one theorem given another’s statement and its proof unchanged, is rejected by both kernels it was given to. Named gaps: leanchecker --paranoid does not exist in Lean v4.34.1 (its only flags are --verbose and --fresh); not run. The four second kernels read lean4export’s output: what they check is what the exporter wrote. nanoda on the whole environment accepted with the environment’s 15 axioms permitted (all declared in Lean’s core); with the hard error on it stops on core’s own Lean.trustCompiler. That the six theorems use only the three standard axioms rests on the audit and on the closure exports, checked with the hard error on. On the published code two second kernels were re-run (nanoda, con-ron) on the closure, not all four, and not the whole environment.
| prediction | prior | outcome |
|---|---|---|
| H1 CERTIFIED | 97% | yes |
| H2 CERTIFIED inside the three-week clock | 50% | yes |
| someone else’s Lean proof of the heptagon appears first | 35% | no: none found at the reveal, 19:24 UTC on 7 November: formal-conjectures, openai/math, the authors of the six-point Lean, a code search |
| H3: every second kernel accepts | 45% | yes |
| H4 read clean or better | 80% | yes |
| H4 CERTIFIED (A.3 in Lean) | 25% | yes |
| the corollary D CERTIFIED the same day | 80% | yes |
The Lean went faster than the rules budgeted: three weeks were allowed, and A.3 in Lean was given one chance in four. The priors are graded as written, not re-tuned.
This reading is dated 2026-11-07, from the sources themselves.
I offered the proof on pull request #7706, gaps first. Five minutes later its author, anxkhn (Anas Khan), added the link as the entry’s formal proof. He checked the linked source himself: IsRamsey byte-identical, the statement equal up to namespace and whitespace, no proof placeholders or custom axioms, his file building. He did not re-run the Lean 4.34.1 build or the kernels, and says so. The pull request is open, waiting on a maintainer.
He asked for an entry in Palomar, the registry formal-conjectures prefers for research results. It is in preparation; the link will move to it when it is listed.
Every question, every verdict rule and every prediction was written and committed before any code ran (notes/heptagon-preregistration-2026-11-07.md, with its dated amendments), and each stage was sealed: a salted fingerprint of the private work posted to a public registry and to Bitcoin through OpenTimestamps, proving the date without showing the content.