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

Three substantive publications or updates dated September 14, 2026: practical advice from Pavel Etingof, a firsthand AI-assisted research account from Beni Bogoşel, and Emily Riehl’s discussion of mathematical explanation. No new theorem or formalization announcement was established for this day.

Research updatesSelect an entry to read more

Etingof adds a dated update on AI-assisted refereeing, formalization and research habits Pavel Etingof Published: 2 sources

A new Section 12 updates Etingof’s May research guide. He recommends asking a model to annotate a LaTeX manuscript with corrections while preserving its text, then reviewing the suggestions. He favors fewer, carefully developed prompts and discussion with collaborators, warns that generated exposition still needs substantial editing, and retains the requirement that authors understand their work. The addendum also discusses improved autoformalization and encourages recorded mathematical explanations.

Research relevance:

Concrete guidance for using AI to scrutinize manuscripts while preserving mathematical understanding and author responsibility.

Claim status:
A dated advisory update, confirmed both in the PDF and on MIT’s mathematics website. Assessments of model capabilities and mathematical breakthroughs are Etingof’s claims, not independently established results in this digest.
Limitations:
September 14 is the date of the addendum, not the original guide. Its broad claims about recently solved problems are not accompanied here by independent proof scrutiny. Agreement among AI reviewers does not certify correctness.

Sources & further reading

Link to this entry
Bogoşel reports a research workflow combining notes, numerical code and directed AI agents Beni Bogoşel Published: 1 source

Bogoşel describes providing an agent with papers, unfinished notes and previously checked numerical code, then directing it toward an established research pattern. He reports obtaining theoretical arguments and improved numerical methods after iterative guidance, completing a large constrained-optimization investigation, and receiving two strategies for a collaborative project, one of which the collaborators checked. He also reports failure on another conjecture and difficulty keeping up with the volume of generated work.

Research relevance:

A firsthand account of an actionable workflow for unfinished mathematical projects: supply curated context, define specific gaps, iterate, and check selected outputs.

Claim status:
Author-reported research experience. Bogoşel says one proposed strategy was checked and another was probably correct; this is not independent verification by the digest.
Limitations:
The post does not identify the projects sufficiently to assess their theorems, proofs or numerical results, and provides no reproducible research artifacts. Experiences began in August; September 14 is the publication date of the account. Its references to earlier breakthroughs are not new announcements.

Sources & further reading

Link to this entry
Riehl argues that clarifying explanations remain central to mathematical research Emily Riehl Published: 1 source

In a guest essay on Tao’s blog, Riehl emphasizes finding simple explanations and abstractions that expose common structure. Her example explains the different preservation properties of direct and inverse images through adjoints. Responding to rapid advances in AI mathematics, she argues that consolidating discoveries and communicating them across specialties deserves recognition alongside extending the frontier.

Research relevance:

A useful criterion for evaluating AI-assisted research: whether a result produces an explanatory framework that mathematicians can understand, reuse and communicate.

Claim status:
A dated mathematical perspective essay, with an illustrative established example. It announces no new theorem, proof or formalization.
Limitations:
This is a personal account of research values, not an empirical evaluation of AI systems. It contributes a distinct explanatory perspective to the ongoing discussion rather than updating the previously reported theorem claims.

Sources & further reading

Link to this entry
Coverage and limitations
  • Public web searches reconstructed September 14, 2026, rather than the latest news. Included dates come from the sources themselves, not search-index timestamps. Publication times were not established, so precise alignment with Paris midnight boundaries remains uncertain.
  • Read the dated Beni Bogoşel post, Emily Riehl’s guest post on Terence Tao’s blog, MIT’s mathematics AI page, and the September 14 addendum to Pavel Etingof’s PDF. Also consulted Computational Complexity, Gowers’s Weblog and Xena. Kevin Buzzard’s Imperial webpage establishes https://xenaproject.wordpress.com/ as his blog.
  • Checked personal or institutional websites for Levent Alpöge, Scott Armstrong, Daniel Litt, Thomas Bloom, Alex Kontorovich, Leonardo de Moura and Boaz Barak, and organization websites for Harmonic, Axiom and Epoch AI. Official pages supplied some social links, but verification of every supplied handle remained incomplete. Sébastien Bubeck’s website and the attempted François Charton page were inaccessible; Project Numina’s homepage returned no readable text, and Lean’s homepage returned an error.
  • Date-specific searches covering the supplied X handles produced no reliably dated target-day posts. Other searches exposed indexed third-party social-media excerpts with relative dates; these were treated as leads, not authenticated posts or historical date evidence. X timelines, Tao’s Mathstodon archive and Buzzard’s Bluesky archive were not comprehensively consulted.
  • Excluded September 14 commentary that merely repeated earlier Navier–Stokes or Fermat formalization announcements, and the later repost of Daniel Litt’s September 13 essay. Computational Complexity’s dated post was read but primarily revisits earlier claims. Undated website entries and benchmark commentary without a dated primary announcement were excluded.
  • Etingof’s guide originally appeared in May 2026; only its explicitly dated September 14 addendum is included as new material. No source code was executed, no proof was independently verified, and Lean was not run.

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