OpenAI's “ten advances” in mathematics and theoretical computer science

OpenAI announced ten results produced with GPT-6 Astra, from sphere-packing bounds to Ramsey numbers, with Lean certificates; none has been peer reviewed, and two face credit disputes from mathematicians.

Problem
Ten open problems including sphere-packing upper bounds, non-sofic groups, Connes's rigidity conjecture and multicolor Ramsey numbers
Credit
GPT-6 Astra (OpenAI) · Manuscripts prepared by people with the model; Lean certificates written by the model
Checked
Lean certificates publishedPartial independent audit (arXiv:2608.14673)
Timeline
Announced 2026-08-01 → Lean repository 2026-08-05 → audit v3 2026-09-09
Sources
OpenAI announcementLean proofsIndependent audit (arXiv:2608.14673)
UN-
VERIFIEDLean certificates · not peer reviewed · credit disputed

The problem

OpenAI announced on 1 August 2026 that its GPT-6 Astra model had produced ten results on open problems:

  1. Sphere-packing upper bounds down to the Cohn–Elkies threshold.
  2. Exponentially improved bounds for binary and spherical codes.
  3. The existence of non-sofic groups.
  4. A disproof of Connes's rigidity conjecture.
  5. Lower bounds for the permanent in arithmetic circuits and formulas.
  6. Exponential parallel repetition for two-player quantum games.
  7. Polynomial-factor hardness of approximation for the closest vector problem.
  8. Ehrhart's volume conjecture in all dimensions.
  9. A superexponential lower bound for multicolor triangle Ramsey numbers (Erdős problem #183).
  10. Compactness and degeneracy conjectures in extremal graph theory (Erdős problems #146 and #180).

What AI did

According to OpenAI, the compute cost about $2,000 at its API rates. People prepared the manuscripts together with the model, and the model then wrote Lean certificates.

How it was checked

The Lean proofs are public. An independent audit (Sienicki and Sienicki, arXiv:2608.14673) found no confirmed substantive error in a principal result, though the depth of review varied: one chapter drew a specialist's request for major revision, and the results on Connes's conjecture and the closest vector problem have been corroborated by follow-up work. None of the ten has been peer reviewed.

Limitations

Scientific American (6 August 2026) reported mathematicians' objections over credit: Stephen Miller said the sphere-packing proof relies on a 2016 argument by him and a co-author without adequate credit, and Francesco Fournier-Facio said the key step for non-sofic groups combines ideas from 2016 and 2019 papers. OpenAI revised its original claim that there had been no progress for at least a decade. Lean certifies only the formal statements. We grade the group "unverified" until the results are reviewed one by one.

∎