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

September 30, 2026: an available preprint and code release study cheaper agent interaction with Rocq and Lean; Tao announces practical recommendations for AI-assisted theoretical research. Coverage of social-media archives and several primary-source leads remains incomplete.

Research updatesSelect an entry to read more

Evolved prover interfaces reduce reported proof-generation costs, with a Lean accuracy tradeoff Jules Viennot, Guillaume Baudart, Marc Lelarge Published: 3 sources

The authors evolve an agent's prover interface by retaining model-proposed features that improve smaller models' performance. Their rocq-mcp-evolve server reportedly improves success rate, cost and time on held-out miniF2F-Rocq problems across four models. A Lean port reduces cost and time per solved problem on a PutnamBench subset, but has lower accuracy than lean-lsp-mcp. The paper links released servers, experiments and code.

Research relevance:

A practical option for researchers building AI-assisted formal-proof workflows: the interaction interface can affect expense and throughput without changing the underlying model.

Claim status:
Available preprint and public code; performance and machine-checking claims are the authors' reports. The original submission is September 30 at 11:44:15 UTC, within the Paris window. Version one was read; an October 1 revision exists.
Limitations:
Competition benchmarks and selected project tasks do not establish general research effectiveness. The authors cannot rule out PutnamBench contamination or prior model exposure to lean-lsp-mcp. No independent reproduction or proof checking was performed.

Sources & further reading

Link to this entry
Tao highlights concrete proposals for adapting theoretical research to AI Terence Tao; September 2026 Working Group Published: 2 sources

Tao's dated announcement links AI and TCS: The Next Six Months. The report proposes standardized AI Methodology sections recording human and AI contributions, stronger assessment of researchers' technical understanding, some doctoral training without AI, and investigation of barriers to funding reasonable model expenses.

Research relevance:

Provides usable practices for documenting AI-assisted proof development and preserving understanding in research, supervision and hiring.

Claim status:
September 30 announcement of an available working-group report dated September 28, arising from a September 9–10 workshop. These are proposals, not adopted community rules. The newly highlighted TCS report is distinct from the previously covered AGMAI recommendations.
Limitations:
The report acknowledges incomplete representation of the TCS community and describes some proposals as experiments. Applicability to other mathematical fields requires judgment; no mathematical theorem or formalization is announced.

Sources & further reading

Link to this entry
Coverage and limitations
  • Reconstructed the Paris civil day September 30, 2026 using public web searches and original dated sources. Search crawl dates were not treated as publication dates.
  • Read the September archive and September 30 post on Terence Tao's What's New, the Simons Institute working-group PDF, the original arXiv submission history and version-one HTML for Growing an Agent/Prover Interface, and its linked public GitHub repository. No code or proof assistant was executed.
  • Consulted Xena at https://xenaproject.wordpress.com/; Kevin Buzzard's Imperial webpage identifies it as his blog. Tao's blog links to his Mastodon presence. Mathstodon returned almost no readable content, and Buzzard's Bluesky profile could not be opened.
  • Checked personal or institutional pages for Scott Armstrong, Thomas Bloom, Daniel Litt, François Charton, Alex Kontorovich and Boaz Barak, alongside Gowers's blog. Armstrong and Barak provide social-account links. Official sites for Lean, Harmonic, Axiom and Epoch AI were also consulted. These checks did not establish every supplied handle's identity or provide complete dated post histories.
  • Levent Alpöge's Harvard page and Project Numina's website returned no readable text; Sébastien Bubeck's personal site and the attempted Leonardo de Moura homepage returned errors. Opening Lean's X profile also failed. Date-specific searches covering the supplied X handles produced incomplete indexed results, including older posts; no exhaustive X access is claimed.
  • MathsAI and other indexed digests supplied leads rather than certification. A MathsAI article link failed. LeanSide and a PNAS mathematical-discovery paper were encountered through indexed metadata, but their original publication chronology was not adequately established from readable primary pages, so they were excluded.
  • Excluded the September 30 CMSA seminar listing because its event date does not establish the page's publication date. Excluded renewed circulation of AGMAI's September 29 recommendations as a repeated item. A September 30 filename in the current OpenAI mathematics repository was insufficient to establish original release chronology or substantiate its mathematical claim.

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