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 · 4 linked sources Partial coverage

Two substantial updates were found for the requested window: OpenAI's release of research manuscripts and proof artifacts, and Thomas Bloom's changes to the Erdős Problems research workflow. Neither establishes that the advertised mathematical claims have received independent verification.

Research updatesSelect an entry to read more

OpenAI releases a large collection of mathematical manuscripts with supporting Lean artifacts OpenAI Published: 3 sources

OpenAI announced a public collection produced by an unreleased internal model. The repository lists 722 manuscripts grouped into 372 mathematical families and provides preprints, a manuscript map, a Lean formalization catalogue, and ten abridged reasoning summaries. It explicitly says that verification stages vary, some manuscripts lack formalizations, and unformalized results may contain issues. This is a release of materials for scrutiny; underlying manuscripts may predate the announcement.

Research relevance:

Researchers can locate papers by subject, inspect associated formal statements and proof artifacts, and compare reasoning summaries with the resulting arguments. The collection is potentially useful both for specialist examination and for studying AI-assisted research workflows.

Claim status:
The announcement and public repository were read. Manuscripts and formalization metadata are available, and OpenAI reports formalizations for many proofs. Independent scrutiny of individual results was not established in this research pass. No proof was verified and no Lean formalization was executed.
Limitations:
Catalogue size is not a count of independently established discoveries. Novelty, correctness, assumptions, attribution, and correspondence between informal and formal statements require paper-specific examination. The model is unreleased, limiting reproduction of the discovery process. October 6 is the announcement date, not the date of every underlying result; its exact publication time was unavailable.

Sources & further reading

Link to this entry
Erdős Problems changes how AI-generated proof claims are submitted and presented Thomas Bloom Published: date not established1 source

In a guest post published on Tao's blog on October 6, Bloom announces a freeze on new problem comments and proof claims, removal of displayed open/solved statuses and solved totals, and greater emphasis on explanatory writeups. Existing comments and claims will remain archived. He says relevant results will still be recorded and encourages registration of Lean formalizations on Palomar to support compilation checks and examination of the formal statement.

Research relevance:

This changes a practical discovery and submission workflow for researchers working on Erdős problems. Readers should consult mathematical remarks, referenced papers and formal statements rather than rely on a status badge or solved-problem counter. Clear exposition and inspectable formalization become more important for having new work incorporated.

Claim status:
A policy announcement by the site's maintainer, read in full through Tao's cross-post. It is not an announcement that any particular conjecture has been solved. Bloom describes Palomar as supporting formalization checks; this digest did not inspect or verify any individual registry entry.
Limitations:
The October 6 cross-post is within the window, but the original forum publication date could not be established, so published_date is null. The original forum link was unavailable and the homepage returned 403, preventing confirmation of implementation. Bloom describes the changes as experimental and potentially subject to revision.

Sources & further reading

Link to this entry
Coverage and limitations
  • Public web search was used for the window from 2026-10-06 03:49 to 2026-10-07 15:49 Europe/Paris. Publication dates were distinguished from search-engine crawl dates; exact posting times were generally unavailable.
  • Read OpenAI's October 6 announcement and the public openai/math repository README; opened its manuscript map and Lean formalization catalogue. Individual proofs and the full catalogue were not audited. No code or Lean was executed.
  • Read Terence Tao's blog and Thomas Bloom's guest post. Bloom's personal website was consulted, but the original Erdős Problems forum link could not be retrieved; the site's homepage returned 403 Forbidden.
  • Consulted official or personal websites for Scott Armstrong, Timothy Gowers, Daniel Litt, Alex Kontorovich, François Charton, Boaz Barak, Leonardo de Moura, Lean, Epoch AI, Harmonic and Axiom. Official-site evidence supports several identities, but verification of every supplied social handle remains incomplete. No item relies on an unverified social identity.
  • Located Kevin Buzzard's Xena blog at https://xenaproject.wordpress.com/ and an Imperial College webpage identifying it as his blog. Read Xena's homepage.
  • Project Numina's website yielded no readable text; Harmonic's homepage provided limited research information. Axiom's blog index displayed an October entry without an exact day, so it was not treated as confirmed news within the window. Epoch AI's current index yielded no mathematics-specific update for the window.
  • Direct attempts to read the Lean and Levent Alpöge X profiles failed. Other social leads produced sparse, sometimes stale indexed snippets rather than comprehensive timelines. X, Mathstodon and Bluesky coverage is incomplete; no absence-of-news claim is made for the supplied accounts. Sébastien Bubeck's and Levent Alpöge's official-site checks remained incomplete.
  • Read Ben Antieau's original Hexagon announcement, dated October 5, and its October 6 cross-post on Tao's blog. This older material found late was excluded from the items because the original publication predates the window. Leonardo de Moura's August 24 kernel bug-hunt postmortem was likewise excluded.

Requested coverage window: 2026-10-06T03:49:06.902718+02:00 — 2026-10-07T15:49:06.902718+02:00.

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

Archives 32
Older editions (2)