AI & Maths watch GitHub

Retrospective research digest

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 September 21 entries were established: a preprint on maintaining reusable Lean formalizations with AI agents, and a mathematics advisory-group announcement containing substantial but undocumented mathematical claims. Social-media archival coverage remains limited.

Research updatesSelect an entry to read more

Lean Pool preprint describes an AI-maintained archive of reusable formalized mathematics Vasily Ilin Published: 3 sources

Ilin presents Lean Pool as a maintained home for completed Lean developments beyond Mathlib's scope. The paper describes importing permissively licensed projects, repairing compatibility as Lean and Mathlib evolve, and optimizing compilation time and memory use. Admission combines mechanical checks with LLM review of mathematical statements and project quality; searchable documentation aims to make archived results usable in subsequent formalizations.

Research relevance:

Addresses a practical research bottleneck: preserving and reusing formal proofs across dependency upgrades, with provenance and discoverable theorem statements. Researchers can consult the archive before independently formalizing prerequisites.

Claim status:
Public preprint and public code are available. The author reports operational maintenance workflows and formal-proof admission checks. This digest did not build the archive, execute Lean, or independently verify those reports.
Limitations:
The paper discloses that almost all text beyond its human-written opening page was produced by AI. Kernel acceptance alone does not establish that a formal statement faithfully captures its intended informal theorem; LLM review supplies no independent guarantee of that correspondence. The current GitHub state may include changes after September 21.

Sources & further reading

Link to this entry
OpenAI announces an independent mathematics advisory group and claims over 100 problem resolutions OpenAI Published: 2 sources

OpenAI announces an unpaid, independent mathematics advisory group, including Timothy Gowers and Martin Hairer, to advise on significance, review, dissemination and research standards. The announcement also claims that an internal model has resolved more than 100 longstanding open problems. The new development relative to the earlier fluid-equation announcement is the broader claim and the advisory arrangement; the page does not enumerate these problems or supply their proofs.

Research relevance:

Relevant to researchers assessing unpublished AI-generated results, coordinating scrutiny and seeking access to research tools. The group's remit concerns communication and mathematical standards, with freedom to publish criticism.

Claim status:
The dated primary announcement establishes the announced advisory arrangement. The claimed problem resolutions remain attributed to OpenAI; this source does not establish available proofs, independent scrutiny or checked formalizations for the claimed collection. Membership does not certify the mathematical claims.
Limitations:
The page provides no problem inventory or corresponding proof artifacts for the more-than-100 claim. It explicitly excludes advice on the pace of internal mathematical progress. Its September 21 date is established, but no publication time or timezone is supplied. Later assessment: the group's October 6 statement expressly says its advisory role should not be interpreted as endorsement of the results or their production process.

Sources & further reading

Link to this entry
Coverage and limitations
  • Reconstructed September 21, 2026, for the Paris civil-day window using public web searches and primary pages. Search-index and crawl dates were not treated as publication dates.
  • Read the Lean Pool arXiv record, portions of its version-one full text, and its public GitHub README. The recorded submission time, 17:57:30 UTC, falls within the Paris window. The current repository was consulted for context; its present statistics were not attributed to September 21.
  • Read OpenAI's dated announcement and the advisory group's website. The group's September 29 recommendations and October 6 statement are later material, not September 21 announcements.
  • Consulted Terence Tao's September blog archive and Kevin Buzzard's Xena blog. Buzzard's Imperial webpage explicitly links to https://xenaproject.wordpress.com/, establishing the official blog address. No additional qualifying September 21 entry was established from these blogs.
  • Checked official Lean, Axiom, Epoch AI and Harmonic pages for source provenance. Project Numina's homepage returned no readable text. These checks did not certify every supplied social-media handle; unconfirmed account identities were not used as evidence.
  • Date-specific indexed searches covering all fifteen supplied X leads and Tao's Mathstodon lead returned no qualifying posts. Individual academic handles and Buzzard's Bluesky identity were not fully authenticated against official pages. Complete X, Mathstodon and Bluesky archives were unavailable; empty search results do not establish absence of activity.
  • Secondary indexed leads were used only for discovery. The undated Release the Proofs letter was excluded because its reference to September 21 does not establish its own publication date. The Hawai'i Public Radio article's September 21, 23:01 HST timestamp falls on September 22 in Paris and was excluded. Previously supplied results were not repeated.

Requested coverage window: 2026-09-21T00:00:00+02:00 — 2026-09-22T00:00:00+02:00.

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

Archives 32
Older editions (2)