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

One substantial autoformalization preprint was published on September 17, 2026. A second dated preprint supplies a concurrent-discovery disclosure and corrects the chronology of an item in the previous digest. Archival social-media coverage remains limited.

Research updatesSelect an entry to read more

FormalFlow reports a Lean formalization of quantum soundness underlying MIP* = RE Sirui Lu, Ruixuan Deng, Yanqiao Zhu and Zhengfeng Ji Published: 2 sources

The authors introduce FormalFlow, which coordinates AI proving agents through a shared blueprint, nested planning and review under human supervision. They report completing a Lean 4 formalization of the quantum soundness of the classical low individual-degree test in 63 days, producing 126,367 lines of agent-generated Lean code. The paper documents how integration and statement review exposed incorrect registers, assumptions that effectively supplied conclusions, and missing side conditions.

Research relevance:

A substantial case study in formalizing research mathematics, with practical lessons about dependency tracking, statement fidelity and auditing beyond successful compilation. The theorem supports quantum complexity theory and MIP* = RE.

Claim status:
Available version-one preprint; the authors report machine checking and provide a detailed audit account. This digest read the paper but did not independently check the formalization. The work concerns a supporting theorem, not a formalization of all of MIP* = RE.
Limitations:
The corrected theorem preserves the published final error bound under strengthened assumptions, including 400md ≤ k and k > 0. Classical soundness is retained as an explicit premise rather than proved in this library. The reported development predates publication; arXiv version one was submitted at 07:26:49 UTC on September 17. A September 24 revision is later material.

Sources & further reading

Link to this entry
Concurrent linear-matroid secretary preprint adds an AI-discovery disclosure and corrects the earlier chronology Kristóf Bérczi, Shaddin Dughmi, Vasilis Livanos, José A. Soto and Victor Verdugo Published: 2 sources

This separately authored manuscript claims a 1/e guarantee for the secretary problem on linear matroids. Its disclosure attributes the main proof to a September 15 conversation with ChatGPT-6 Astra and says the authors discovered the September 16 Abdi–Banihashem–Hajiaghayi–Mittal manuscript while preparing their own submission on September 17. They describe the approaches as essentially identical. The previous digest already linked this manuscript under September 16; its original submission record establishes September 17 instead.

Research relevance:

The new disclosure provides a concrete example of concurrent AI-assisted discovery and an alternative exposition of a significant online-selection result.

Claim status:
Available proof preprint and author-attributed account of AI involvement. The existence of another manuscript is not independent verification of either proof, and the concurrent-discovery narrative has not been independently authenticated here.
Limitations:
The claimed resolution concerns linear matroids, not the secretary conjecture for arbitrary matroids. The online-representation result assumes a finite field; the known-matroid extension concerns matroids admitting a finitary modular extension. No Lean formalization is established by the consulted record. Submission occurred at 17:54:37 UTC, or 19:54:37 Paris time, on September 17; the reported proof discovery occurred September 15.

Sources & further reading

Link to this entry
Coverage and limitations
  • Public web searches reconstructed September 17, 2026, using original publication records rather than search-index dates. Both included arXiv submissions fall within the Paris civil day.
  • Read the FormalFlow version-one paper and arXiv publication records. The September 24 revision was identified as later material and was not used to establish what was announced on September 17.
  • Consulted Terence Tao’s September archive, Kevin Buzzard’s Xena blog, Proofs and Prompts, Sebastian Ullrich’s talks page, and the official websites of Lean, Epoch AI, Axiom and Harmonic. Project Numina’s website returned no readable content.
  • Checked supplied identity leads against personal or institutional websites where accessible, including Buzzard, Litt, Bloom and Barak. Buzzard’s Imperial homepage identifies https://xenaproject.wordpress.com/ as his project blog. Official-site corroboration of every supplied X handle was not achieved; no item relies on an unverified account identity.
  • X search results and third-party mirrors provided incomplete leads, not an exhaustive historical timeline. No complete September 17 coverage was obtained for the supplied accounts, Tao’s Mathstodon account or Buzzard’s Bluesky account. Relative dates in mirrors were not accepted as publication evidence.
  • Excluded Harvard’s September 17–18 summit and Georgia Tech’s September 17 Tex2Lean discussion because event dates do not establish publication dates. Ullrich’s dated talk listing likewise does not establish when its slides were published.
  • Excluded the September 17 Proofs and Prompts cross-post of a Royal Society letter received September 16: it concerns broader AI risk rather than a new mathematical result or research tool. Excluded promotional commentary and repeated coverage of earlier fluid-equation announcements.
  • MathsAI’s FormalFlow article was available as an indexed excerpt, but opening it failed; the digest instead uses the accessible primary preprint. An indexed secondary account of Tao’s analytic-number-theory talk was excluded because the original publication date was not established.
  • No source code was executed, no Lean build was run, and no proof was independently verified.

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