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

Two substantive entries were established for September 23, 2026: a conditional Lean formalization in analytic number theory and a new essay on understanding and auditability in AI-assisted mathematics. Significant gaps remain in social-media and archival coverage.

Research updatesSelect an entry to read more

Fiori's short-interval zeta results receive a conditional Lean registry record Andrew Fiori Published: 3 sources

Palomar recorded seven Lean statements concerning zero-density bounds for the Riemann zeta function in short intervals. Two arguments use Jensen's formula and Littlewood's lemma; a consequence gives a positive proportion of zeros in the middle band [alpha, 1-alpha] for each alpha in (0, 1/6), beyond suitable thresholds. The September 23 news is the formalization's registry publication, rather than an established date for the underlying mathematical discovery.

Research relevance:

A useful analytic-number-theory artifact showing how substantial complex analysis can be formalized while keeping imported estimates and numerical assumptions explicit.

Claim status:
The registry reports mechanical checking of seven statements. The repository provides Lean sources and describes conditional proofs. These reports were read; the proofs and checker were not independently run or audited.
Limitations:
The development assumes sixteen published analytic bounds and eleven numerical certificates computed outside Lean. These appear as hypotheses in theorem signatures. A clean axiom report therefore does not make the results unconditional. The current README was consulted retrospectively; its precise September 23 contents were not established.

Sources & further reading

Link to this entry
Schneider connects mathematical understanding with auditable AI research workflows Tapio Schneider Published: 1 source

In a guest essay on Tao's blog, Schneider argues that checked results become more useful when researchers can understand their mechanisms. He connects AI-generated proofs with climate modelling and computational fluid dynamics: search can accelerate discovery, while explicit equations, controlled numerical methods and individually testable components support trust. He proposes using AI to search for closures within physically constrained models.

Research relevance:

Relevant to mathematicians developing AI-assisted workflows for PDEs, numerical analysis and scientific modelling. It explains why verification, explanation and applicability require different forms of evidence.

Claim status:
A dated methodological essay, not a new theorem or an independent proof review. Its account of Lean verification of the earlier fluid-equation work is the author's characterization.
Limitations:
The discussion revisits the September 8 forced Navier–Stokes announcement without supplying a new proof certification. Schneider distinguishes that claim from the unforced problem and stresses that mathematical blow-up does not by itself explain physical turbulence. Empirical validation of learned closures remains restricted to tested conditions.

Sources & further reading

Link to this entry
Coverage and limitations
  • Public web searches reconstructed September 23, 2026, the Paris civil day. Publication dates came from original dated pages or registry publication timestamps, not search-index dates.
  • Read Terence Tao's September archive and Tapio Schneider's dated guest essay; consulted Kevin Buzzard's Imperial webpage and the linked official Xena blog at https://xenaproject.wordpress.com/.
  • Read Palomar's machine-readable recent-results feed and Andrew Fiori's public repository README. Individual registry JSON endpoints were inaccessible, and the registry entry page exposed only its JavaScript loading shell.
  • Consulted official websites for Lean, Axiom, Epoch AI, Harmonic, Daniel Litt and Leonardo de Moura. Alpöge's Harvard page returned no readable content; the attempted Project Numina website was inaccessible. Verification of all supplied social-account identities against official websites remained incomplete.
  • Date-specific searches across the supplied X handles returned no results. This does not establish that those accounts posted nothing. X timelines, Tao's Mathstodon account and Buzzard's Bluesky archive were not comprehensively consulted.
  • Excluded September 23 secondary reporting that repeated the September 21 AGMAI announcement. Also excluded OpenAI manuscript filenames containing September 23 because the currently accessible repository did not establish public release on that day.
  • An indexed September 23 autoformalization essay could not be opened and was excluded. Dated seminar events were not treated as publication dates. No proof was independently verified, and no Lean or source code was executed.

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