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

Two substantive sources dated 7 September 2026 concern AI-assisted fluid singularity research: smooth-forcing blowup constructions reported as Lean-formalized, and a PINN-generated candidate for unforced Euler blowup. Archival and timezone gaps limit reconstruction of the complete Paris civil day.

Research updatesSelect an entry to read more

Tao explains AI-assisted smooth-forcing blowup constructions and their reported Lean formalization Terence Tao, discussing work by Levent Alpöge, Tristan Buckmaster and collaborators Published: 2 sources

Tao reports finite-time blowup constructions with smooth forcing for incompressible porous medium, two-dimensional Boussinesq and three-dimensional incompressible Euler equations. Building on Córdoba–Martínez-Zoroa, the method introduces high-frequency corrections that amplify singular behavior while controlling the forcing. He describes substantial AI assistance, Lean formalization, and ongoing human work to turn preliminary arguments into readable mathematics.

Research relevance:

A substantial example of AI-assisted PDE research coupled to formalization. Tao’s explanation supplies a useful route into the construction and illustrates why checked artifacts still need mathematical exposition.

Claim status:
Available preliminary proofs and reported Lean formalization. Tao provides informed independent discussion but explicitly says he has not fully digested the technical improvements. A later NYU institutional report, dated 14 September, states that the three papers were formalized and verified using Lean.
Limitations:
These are smooth-forcing results for the stated equations, not a resolution of unforced Euler or the Navier–Stokes Millennium problem. This digest did not inspect complete proofs or independently check Lean. The original post’s exact Paris publication time is unestablished; its current page includes later, incompletely dated edits.

Sources & further reading

Link to this entry
A physics-informed neural network proposes an unforced three-dimensional Euler singularity profile Anima Anandkumar, reporting joint work with Adarsh Ganeshram and Valentin Duruisseaux Published: 3 sources

Anandkumar announces evidence for self-similar finite-time blowup of Euler on R^3 without forcing or boundaries. A constrained physics-informed neural network searches for a nontrivial approximate profile; spline refinement supports tighter error bounds. The announcement studies transport-field properties relevant to damping and stability rather than presenting numerical discovery alone as a completed theorem.

Research relevance:

A complementary AI research workflow: neural numerical discovery followed by rigorous estimates and stability analysis. The unforced, boundary-free setting makes the candidate particularly relevant to PDE researchers.

Claim status:
Dated primary announcement of a candidate and supporting evidence, not an established complete blowup proof. The later arXiv version 1, submitted 9 September, describes a stability framework reduced to explicit estimates and computable constants. Anandkumar’s later guest post on Tao’s blog is dated 10 September.
Limitations:
Full nonlinear stability and closure of the required estimates remain essential. No independently checked complete proof or Lean formalization was established here. The announcement was subsequently edited, and its exact timestamp is unavailable; the later account places release in the evening of 7 September without establishing the timezone, leaving Paris-window membership uncertain.

Sources & further reading

Link to this entry
Coverage and limitations
  • Public web searches used explicit historical dates and the supplied account handles. Read Tao’s dated technical post, Anandkumar’s dated announcement, Anthropic’s research announcement, Buzzard’s Xena response, and arXiv abstract pages. Search snippets were treated as leads, not as full-source access.
  • Confirmed Xena’s address through Kevin Buzzard’s Imperial College webpage: https://xenaproject.wordpress.com/. Consulted Scott Armstrong’s research website and official sites for Epoch AI, Harmonic, Axiom and Project Numina. Project Numina’s homepage returned no readable content; Lean’s homepage and the Caltech Euler project page were inaccessible through the web tool.
  • Account authentication and historical social coverage remain incomplete. No exhaustive X archive was available, and most supplied handles could not be independently authenticated through official-site links. Mathstodon and Bluesky timelines were not systematically read; no item relies on a supplied handle as proof of identity.
  • Nature’s 7 September Fermat report had accessible publication metadata and introductory text, but its full article was paywalled. Excluded it as coverage of Anthropic’s 4 September announcement without an established substantive new update. Buzzard’s original assessment was also dated 4 September, despite a repost dated 7 September.
  • Later sources are explicitly identified in the entries. Current blog pages contain edits whose original timing cannot always be reconstructed. The included sources establish 7 September publication dates, but exact timestamps and conversion to the Paris window could not be established.
  • No proof was independently verified, no Lean development was executed, and no source code was run. This edition is not an exhaustive account of the day.

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