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 dated September 13, 2026: a practical Lean agent workflow, Bryna Kra’s account of purported Nivat proofs, and Daniel Litt’s proposals for preserving mathematical expertise. No new theorem is certified by this digest.

Research updatesSelect an entry to read more

A practical Lean workflow lets coding agents iterate on build feedback pandaman64 Published: 2 sources

A short practitioner article describes moving from completion and chat-based proof generation to an agent that writes Lean, reads unresolved goals from lake build output, and repeatedly repairs its proofs. The author reports experimenting with a HOL formalization and argues that a dedicated proof-state MCP interface is not always necessary for this basic feedback loop.

Research relevance:

A concrete workflow to consider for research formalization: give an agent access to compiler feedback and inspect the resulting statements, dependencies and proofs.

Claim status:
Dated practitioner report with a linked public repository. It is neither a controlled evaluation nor independent verification of the generated proofs.
Limitations:
The Japanese source displays September 13 without a posting time or timezone. It provides no systematic success rates or costs. Its speculation about model training is unsupported, and its broad characterization of the earlier Navier–Stokes announcement is not adopted here. The repository was read through the web; nothing was run.

Sources & further reading

Link to this entry
Bryna Kra reports purported Nivat proofs and calls for accountable mathematical explanation Bryna Kra Published: 1 source

Kra reports receiving several manuscripts claiming the full Nivat conjecture during the preceding week. Some authors acknowledged limited AI assistance; none accepted her invitation to explain their arguments over Zoom. She connects this experience to reviewing pressures and proposes distinguishing credit for discovery, proof, formalization and explanation, while requiring authors to communicate a proof’s mechanism.

Research relevance:

A specialist’s account of how purported AI-assisted solutions reach researchers in symbolic dynamics, with practical implications for refereeing, authorship and the assimilation of new arguments.

Claim status:
First-person report and research-practice essay. Kra explicitly says a proposed proof is not a theorem and declining discussion does not establish AI use. This publication does not announce an accepted resolution of Nivat’s conjecture.
Limitations:
The manuscripts and their correctness were not assessed for this digest. The source establishes the essay’s September 13 date, not the individual manuscripts’ dates. Its general claims about frontier-model capabilities are the author’s assessments.

Sources & further reading

Link to this entry
Daniel Litt proposes evaluating mathematical understanding through defenses and sustained discussion Daniel Litt Published: 1 source

In A beginning for mathematics, Litt separates the value of mathematical results from evidence of their producer’s expertise. He proposes PhD assessment centered on rigorous explanation, regular demonstrations of understanding through unfamiliar examples, stronger seminar discussion, and greater recognition for building compelling research programs. AI assistance would be compatible with these expectations, provided researchers understand the mathematics.

Research relevance:

Concrete proposals for supervisors, hiring committees and research groups adapting their evaluation practices to abundant machine-generated mathematical text.

Claim status:
Dated institutional and research-practice proposal. Its premise of forthcoming broadly superhuman mathematical AI is explicitly a premise, not a demonstrated result.
Limitations:
The essay does not validate particular AI-generated theorems or provide empirical evidence that the proposed assessment methods succeed. Its capability forecasts and claims about inexpensive production of research papers remain attributed to Litt.

Sources & further reading

Link to this entry
Coverage and limitations
  • Public web searches reconstructed September 13, 2026, rather than the latest news. Included dates come from publication dates displayed on source pages; exact posting times and their conversion to Paris time were not available.
  • Read the included Zenn article, Daniel Litt’s personal blog, and Bryna Kra’s guest post on Terence Tao’s blog. Also consulted Tao’s September archive, Kevin Buzzard’s Imperial webpage and Xena blog, the Epoch AI homepage, and public GitHub repositories.
  • Buzzard’s Imperial webpage explicitly identifies https://xenaproject.wordpress.com/ as his Xena blog. Litt’s essay was accessed through his personal website. Official Lean material corroborates the leanprover account, and Harmonic’s official Aristotle website references HarmonicMath. The remaining supplied account identities were not independently established against official websites.
  • Date-specific searches covered the supplied X handles in grouped queries, but yielded no additional adequately documented target-day announcements. X timelines, Tao’s Mathstodon archive and Buzzard’s Bluesky archive were not exhaustively consulted. Search silence does not establish inactivity.
  • Project Numina’s homepage returned no readable text. The Palomar Albert-algebra record yielded a detailed indexed snippet reporting registration and mechanical checks on September 13, but its opened page exposed almost no content; the repository was accessible, while an attempted fixed-revision README retrieval failed. This lead is excluded because the dated record and mathematical scope could not be adequately inspected.
  • Excluded September 13 secondary coverage of earlier Fermat and fluid-equation announcements, and repetitions of the supplied September 11 declaration. Nestor Guillen’s September 13 Tao crosspost was also excluded after its linked original was found at a September 12 publication URL; original-day eligibility was not established for September 13.
  • Indexing and crawling dates were not treated as publication dates. Current pages can contain later edits and comments; this reconstruction is not an immutable snapshot of what was visible that day. No source code was executed and no Lean proof was checked.

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