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

Three substantive sources dated September 27, 2026: an AI-assisted improvement in bounds for distinct zeta zeros, a reported Lean formalization of two-dimensional Navier–Stokes existence theory, and practical proposals for preserving research judgment in doctoral training. Social-media archival coverage remains limited.

Research updatesSelect an entry to read more

AI-assisted preprint improves the claimed lower bound for distinct zeta zeros to 83.699% Kristian Muri Knausgård Published: 2 sources

The preprint claims liminf N_d(T)/N(T) ≥ 0.83699288145242, improving the cited bound of approximately 0.83625. A matrix inequality with a clipping parameter retains an overlap correction even when nearby critical-line zeros have multiplicity two. The author discloses substantial assistance from OpenAI Codex and Anthropic Claude in the arguments, formalization and writing.

Research relevance:

A concrete AI-assisted number-theory result with an unusually explicit account of formalized components, imported analytic hypotheses and computational dependencies.

Claim status:
An available proof and ancillary Lean files accompany the announcement. The author reports formal proofs of matrix inequalities, counting components and exact arithmetic, and a separate-hardware replay of an imported interval computation. Independent scrutiny of this new paper was not established.
Limitations:
The complete zeta theorem is not formalized: operator reductions, energy asymptotics, the local computational inequality, pinching, averaging and smoothing enter as hypotheses. Several dependencies remain unrefereed. I did not check the proof or run Lean. The manuscript bears September 26; its original arXiv submission was September 27 at 00:19:21 UTC.

Sources & further reading

Link to this entry
AI-assisted Lean development formalizes a Galerkin construction for two-dimensional Navier–Stokes Weinan Wang Published: 3 sources

Wang reports a Lean 4 formalization of global Leray–Hopf weak solutions for unforced two-dimensional Navier–Stokes equations on arbitrary bounded open domains with no-slip boundaries and solenoidal L² initial data. On rectangles, the development also covers finite-horizon solutions with continuous forcing in the dual energy space. The acknowledgments disclose ChatGPT and Claude assistance.

Research relevance:

Reusable analysis infrastructure includes divergence-free graph spaces, spectral coordinates, transport cancellation, Ladyzhenskaya estimates and space–time compactness. Abstract Hilbert-space components may support other evolution-equation formalizations.

Claim status:
A mathematical exposition and public Lean repository are available. Formalization is reported by the author; no independent compilation or audit was established in this research.
Limitations:
The stated scope is two-dimensional weak existence, with the forced result restricted to rectangles and finite horizons. It does not establish three-dimensional regularity or singularity claims. I did not execute Lean or verify correspondence between code and paper. Original arXiv submission: September 27 at 00:02:19 UTC.

Sources & further reading

Link to this entry
Jess Werk proposes departmental practices that reward understanding and verification Jess Werk Published: 1 source

In a guest post on Tao’s blog, Werk proposes live, unassisted doctoral assessments, explicit defense rubrics, regular board explanations, clear boundaries for AI use, and faculty incentives for mentoring and verification. She argues that departments should protect the practice through which students acquire the judgment needed to supervise AI-assisted research.

Research relevance:

Concrete proposals for mathematics departments adapting doctoral training and research assessment to increasingly automated discovery, extending the discussion to faculty incentives.

Claim status:
A dated opinion essay with practical recommendations, not a mathematical result or an empirical demonstration that the proposed policies work.
Limitations:
The author writes from astronomy. The recommendations require adaptation to mathematics and are not presented as an adopted institutional policy. The faculty retreat underlying part of the discussion occurred September 17; this guest post was published September 27.

Sources & further reading

Link to this entry
Coverage and limitations
  • Reconstructed the Paris civil day September 27, 2026 using public web searches. Both included preprints have original arXiv submission timestamps within that day; search-index dates were not used as publication evidence.
  • Read the original arXiv records and HTML papers for 2609.33043 and 2609.33033, and consulted the FluidGalerkinLean repository page. No code was executed and no Lean build or proof was independently verified.
  • Read Terence Tao’s September archive and Jess Werk’s dated guest post. Consulted Tao’s curated Mastodon page, which does not provide a complete historical account timeline.
  • Confirmed the Xena blog address, https://xenaproject.wordpress.com/, through Kevin Buzzard’s Imperial College homepage. Consulted Xena; older September material was excluded.
  • Date-specific indexed searches covering all fifteen supplied X handles returned no results. This does not establish that those accounts were inactive. Their identities were not fully authenticated against official websites, and no account-derived claim was included. Complete X, Mathstodon and Bluesky timelines were not consulted.
  • Consulted the official websites of Lean, Axiom, Epoch AI and Harmonic; these landing pages did not establish a qualifying September 27 announcement. Project Numina’s website returned no readable text. Attempts to open the supplied Palomar data endpoint and possible institutional pages for Gowers and Alpöge failed.
  • Read the September 30 AI4Math Radar as a later discovery aid, then checked original sources. Its dates and relevance scores were not treated as authoritative. Excluded its September 26 and September 28–29 papers.
  • Consulted Dan Rockmore’s September 27 New York Review of Books essay but omitted its retrospective discussion of earlier announcements. Also excluded indexed event listings, promotional material, undated leads and repeated previously supplied items. The resulting edition is selective, not exhaustive.

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