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 glance3 entries · 5 linked sources Partial coverage

Three substantive sources dated September 29, 2026: a reusable Lean research library, AGMAI release recommendations, and Rachel Webb’s account of AI in mathematical research. Social-media archival coverage remains limited.

Research updatesSelect an entry to read more

GenLimitLib organizes a research literature into reusable Lean developments and reports new mathematical findings Shuangping Li and Peng Zhang Published: 3 sources

The preprint introduces a source-aligned Lean 4 library covering developments from 30 papers on language generation in the limit, a field introduced in 2024. The authors report repairing a published proof gap without changing its convergence bound, strengthening a replay-model impossibility example from four languages to three, and resolving a staircase-family special case of an open problem. Across five unpublished theorem tasks and 300 proof-generation runs, they report that library access raises kernel-checked success from 48% to 79%.

Research relevance:

A concrete research workflow: organize definitions and reusable lemmas across papers, expose differences in assumptions, and use the resulting library to discover connections and support further formal proofs.

Claim status:
Available preprint, mathematical arguments and public formalization repository; human auditing and kernel-checking results are reported by the authors. Independent verification was not established.
Limitations:
Coverage is explicitly selective: of 405 scoped source claims, 217 have full Lean coverage and 82 have partial coverage. Some developments omit computational or randomized guarantees. The experiment uses only five theorem tasks; its percentages do not establish general research performance. I did not execute Lean.

Sources & further reading

Link to this entry
AGMAI specifies release standards for AI-generated mathematics that lacks human understanding Advisory Group on Mathematics and Artificial Intelligence Published: 1 source

Following more than 600 responses, AGMAI publishes recommendations distinguishing papers understood by responsible mathematicians from output nobody yet understands. For the latter, it requests conventional exposition and attribution, timely deposit in independent scholarly repositories, disclosure of models and research-process information, formalization where practicable, and explicit documentation of remaining formalization assumptions. It also recommends funding community-led work to understand the results and broad, equitable access to public models.

Research relevance:

Provides practical criteria for assessing an AI-assisted research release: inspect precise statements, provenance, proof artifacts, assumptions and arrangements for expert scrutiny.

Claim status:
Dated advisory recommendations, extending the previously reported AGMAI announcement. They neither certify particular results nor establish binding community standards.
Limitations:
The statement says a clear plurality of respondents supported its recommendations; that is not unanimity. It explicitly opposes testing advanced mathematical problems on inaccessible proprietary models. Proposed funding and disclosure practices are recommendations, not evidence of implementation.

Sources & further reading

Link to this entry
Rachel Webb describes choosing AI assistance around mathematical understanding and collaboration Rachel Webb Published: 1 source

In a guest post on Tao’s blog, Webb describes research as crafting interesting mathematical narratives through definitions, lemmas and theorems. She expects LLM assistance with background material and standard arguments to accelerate exploration while retaining her criteria for mathematical interest. Her practical principle is to choose assistance that increases understanding and enjoyment, and to preserve conversations with colleagues rather than automatically routing every question to a machine.

Research relevance:

Useful guidance for deciding which research tasks to delegate while maintaining conceptual ownership, motivation and collaborative relationships.

Claim status:
Dated first-person research reflection; no new theorem, formalization or controlled productivity study is announced.
Limitations:
Claims about faster exploration reflect the author’s experience and expectations. The description of a machine knowing the literature should not be read as an established reliability guarantee. Tao notes that AI converted the post’s original file format.

Sources & further reading

Link to this entry
Coverage and limitations
  • Public web searches reconstructed September 29, 2026, the Paris civil day, during research on October 7. Search-index and crawl dates were not treated as publication dates.
  • Read GenLimitLib’s arXiv submission record and version-one HTML, and consulted its public GitHub repository. The submission timestamp, September 29 at 04:06:07 UTC, falls within the requested Paris window.
  • Read AGMAI’s dated statement and Rachel Webb’s guest post on Terence Tao’s blog; consulted Tao’s September archive and the Xena blog. Kevin Buzzard’s Imperial website explicitly links to https://xenaproject.wordpress.com/, establishing the official blog address.
  • Consulted official websites for Lean, Epoch AI, Axiom, Harmonic, Thomas Bloom, Boaz Barak, Alex Kontorovich and Levent Alpöge. These checks did not establish every supplied social handle. Project Numina’s website returned no readable text.
  • Date-specific searches using supplied names and handles produced no additional eligible original posts. X profile material and third-party mirrors were seen chiefly through indexed snippets, which did not establish September 29 publication dates. Direct access to Lean’s X profile and Buzzard’s Bluesky profile failed; Tao’s Mathstodon page exposed no readable post history. The supplied social accounts were not comprehensively consulted or authenticated.
  • Excluded the Leiden Declaration as older material found during this reconstruction: its official citation dates original publication to June 2, 2026. Excluded MathAgent because its original submission was September 28; an indexed September 29 update alone did not establish a substantive new announcement.
  • Excluded repetitions of the September 28 Poincaré and Thomson announcements, promotional material, and secondary claims about Millennium Prize problems without an eligible original dated source. Later commentary was not treated as information available on the target day.
  • No source code was executed, no Lean build was run, and no mathematical proof was independently verified.

Requested coverage window: 2026-09-29T00:00:00+02:00 — 2026-09-30T00: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)