AI & Maths watch GitHub

Archived edition

Updates on artificial intelligence for mathematical research, proof discovery and formal verification, with links to papers, code and tools.

At a glance2 entries · 5 linked sources Partial coverage

Two substantive updates in the requested window: OpenAI withdrew three manuscripts and revised others; Scott Aaronson reported early expert scrutiny of the claimed Unique Games proof. Social-media coverage and account authentication remain incomplete.

Research updatesSelect an entry to read more

OpenAI withdraws three Hodge-related manuscripts and publishes proof repairs OpenAI Published: 2 sources

A substantive correction to the previously covered October 6 release: OpenAI's revision history reports that a sign error invalidates a stabilization-trace cancellation argument in Algebraicity of Weil classes on split abelian eightfolds. It withdraws that manuscript and two dependent works on Kuga–Satake correspondences and the rational Hodge conjecture for products of K3 surfaces. It also reports revisions to 14 other manuscripts, reference updates to 13 dependent manuscripts, and six additional formalizations plus five supporting additions. The current README lists 719 manuscripts, replacing the earlier 722 count.

Research relevance:

Researchers using the collection should check dependency chains and revised hypotheses before relying on a manuscript. The corrections affect algebraic geometry, statistical mechanics, symplectic geometry and other areas.

Claim status:
Dated primary-source withdrawal and revision notices. OpenAI reports formalization coverage of 300 out of 719 top-line results; this is the publisher's accounting, not an independently reproduced verification result.
Limitations:
The repaired arguments and formalizations were not verified. The history does not establish independent refereeing or identify a complete external audit. Its formalization count should not be interpreted as certifying every assertion in the associated manuscripts.

Sources & further reading

Link to this entry
Early scrutiny of the claimed Unique Games proof exposes substantial exposition work Scott Aaronson, reporting observations by Dana Moshkovitz Published: 3 sources

Aaronson's new post adds expert reading observations to the previously reported OpenAI release. He relays Moshkovitz's difficulties reconstructing the claimed Unique Games argument: dispersed completeness and soundness claims, unclear citations, and an unfamiliar recursive code construction. She describes using AI to assemble claims about the noise gadget. OpenAI's accompanying Lean scope document describes a polynomial-time reduction from binary 3SAT to translation-constrained bipartite unique games with arbitrarily small fixed completeness and soundness errors.

Research relevance:

The conjecture concerns optimal approximation hardness. The report also illustrates a practical research task: extracting a coherent argument and checking its interfaces against a stated formal theorem.

Claim status:
Available manuscript and claimed formalization, accompanied by preliminary expert scrutiny reported through Aaronson. This is neither a completed independent proof audit nor evidence that this digest checked the formalization.
Limitations:
The underlying release occurred October 6; the news here is the October 7 scrutiny. The manuscript directory carries a September 23 date, which is not established here as its public publication date. Moshkovitz's observations are mediated by Aaronson. The PDF proof was not read, and the Lean scope description alone does not certify fidelity or successful compilation.

Sources & further reading

Link to this entry
Coverage and limitations
  • Public web searches covered October 7–8, 2026, with the requested cutoff of October 8 at 08:19 Europe/Paris. Publication dates were distinguished from search-engine crawl dates. Sources without publication times cannot be placed precisely against the cutoff.
  • Read OpenAI's repository README, October 7 revision history, and Unique Games formalization scope document. The manuscript's GitHub PDF page was accessible, but its proof text was not read. No code was executed and no Lean proof was checked.
  • Read Scott Aaronson's October 7 post, and consulted the homepages of Terence Tao's What's New, Gowers's Weblog, and Xena. Kevin Buzzard's Imperial homepage explicitly links to https://xenaproject.wordpress.com/, establishing the official blog address. Older posts were excluded from the items.
  • Consulted the official Lean, Axiom, Harmonic and Epoch AI websites. Project Numina's website returned no extractable text. These checks did not establish comprehensive news coverage or authenticate every supplied social-media handle.
  • Thomas Bloom's and Alex Kontorovich's academic websites were accessible. Alpöge's Harvard page returned no extractable text; attempted personal-site access for Bubeck, Litt, Barak and de Moura failed. The supplied identities and handles were not treated as certified.
  • Direct X access attempts for Lean and Project Numina failed. Tao's Mathstodon page yielded only minimal text. Indexed X profiles and third-party mirrors supplied leads, not reliable current timelines; their relative dates were not used to establish news dates. Buzzard's Bluesky feed and the remaining supplied accounts were not comprehensively consulted.
  • Searches for dated arXiv papers and autoformalization news did not yield another sufficiently supported item. Secondary October 7 coverage largely repeated the previously reported October 6 release; promotional headlines and unsubstantiated breakthrough claims were excluded.

Requested coverage window: 2026-10-07T03:49:06.902718+02:00 — 2026-10-08T08:19:28.116236+02:00.

Public web research; coverage is not exhaustive. A source link is not a certification of a claim.

Archives 32
Older editions (2)