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 posts dated September 15, 2026 were established: Axiom's account of AI-assisted higher Dyson rank research and two essays on responsible mathematical research with AI. Archival social-media coverage remains limited.

Research updatesSelect an entry to read more

Axiom explains AI-assisted elliptic corrections for higher Dyson ranks and the scope of its Lean proofs Ken Ono Published: 3 sources

Ono's dated research post describes work with Claudia Alfes and Ashvin Swaminathan on higher Dyson rank generating functions. A finite recurrence yields a polynomial defect in an elliptic transformation law; Appell–Lerch corrections remove it, leading to finite theta decompositions. The post attributes exploratory discovery to collaboration with AxiomProver and reports four batches of sorry-free Lean proofs for key formulas. Older material presented in a new explanatory post: the underlying preprint was submitted on July 14, 2026.

Research relevance:

Relevant to partition theory, q-series and Jacobi forms, with a concrete example of separating AI-assisted discovery, human exposition and formal verification of an algebraic core.

Claim status:
Author announcement with an available preprint and public Lean repository. The claimed formalization covers selected formulas, not the entire paper. No independent proof scrutiny or Lean execution was performed for this digest.
Limitations:
Convergence and summability enter as explicit hypotheses in the reported formalization. The modular properties of the resulting theta coefficients remain open. Repository availability was checked during reconstruction; its exact historical state on September 15 was not established.

Sources & further reading

Link to this entry
Henry Cohn identifies the technical debt of poorly explained AI-generated mathematics Henry Cohn Published: 1 source

Cohn argues that even correct AI-generated solutions can impose substantial work on other researchers when their motivation, structure and reusable ideas remain obscure. He compares this burden to technical debt: obtaining an answer leaves the work of explanation and integration unfinished. His practical recommendation is that contributors take responsibility for clarifying their output, documenting the discovery process and helping the community understand it.

Research relevance:

Useful when deciding whether an AI-assisted result is ready to circulate, how to allocate verification and exposition work, and what constitutes a durable research contribution.

Claim status:
A dated guest essay on Terence Tao's blog expressing Cohn's assessment and recommendations. It announces no theorem and certifies no particular AI-generated proof.
Limitations:
The essay provides qualitative judgments rather than a controlled evaluation of model capabilities. Its discussion of mathematical understanding should not be read as an independent assessment of any previously reported conjecture resolution.

Sources & further reading

Link to this entry
Ben Antieau proposes standards for ambitious AI-assisted research that researchers can understand Ben Antieau Published: 2 sources

Antieau proposes combining contemplative mathematical work with ambitious collective programs assisted by language models, suggesting higher-dimensional algebraic geometry as one possible direction. Such programs would produce explanations, databases and teaching materials alongside results. His proposed standards include disclosure of AI collaboration, authors' ability to reconstruct the main ideas, responsibility for published claims, and a pace of work compatible with understanding and communication.

Research relevance:

Offers concrete research-group and authorship practices for mathematicians using AI, including how to evaluate outputs and organize larger projects.

Claim status:
A dated proposal on Antieau's own blog, crossposted the same day by Terence Tao. These are proposed norms and research directions, not adopted community rules or a new mathematical result.
Limitations:
The recommendations reflect the author's perspective and experience. The suggested large research programs are prospective; the essay supplies no new proof, benchmark or checked formalization.

Sources & further reading

Link to this entry
Coverage and limitations
  • Public web searches reconstructed September 15, 2026, rather than the latest news. Included dates come from original pages; search indexing dates were not used as publication dates. Pages without precise timestamps cannot establish publication time within the Paris civil day.
  • Read the dated posts on Terence Tao's What's New, Benjamin Antieau's original blog, Axiom's research blog, the associated arXiv abstract and submission history, and the public HigherDyson repository listing. The paper's full proof and Lean files were not audited or executed.
  • Consulted Kevin Buzzard's Imperial homepage, which links to the official Xena blog, and opened Xena. Tao's blog links to his Mastodon presence. Consulted Daniel Litt's homepage and the official Harmonic, Epoch AI and SAIR competition sites; these checks did not establish additional eligible posts.
  • Date-specific searches covering supplied personal and organizational handles yielded sparse historical evidence. No exhaustive X archive was available, and the supplied handles were not all authenticated against official websites. Axiom's X page and Gowers's Cambridge homepage returned access errors; Lean's official homepage returned an error; Project Numina's homepage and Tao's Mathstodon profile supplied no substantive readable content. No item relies on an unauthenticated social-media identity.
  • Excluded Lionel Levine's Math for AI safety despite an indexed September 15 listing: arXiv records its original submission as September 14, 2026 at 09:45 UTC. Excluded secondary digests recirculating earlier mathematical results and previously supplied items without an established new announcement.
  • An indexed Lean FRO LinkedIn snippet advertised September 15 as the Lean Kernel Challenge launch date, but an original announcement published on that day was not established. It was excluded. Other secondary snippets were discovery leads, not sources read in full.

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