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 dated items for September 24, 2026: a benchmark for local formal reasoning in analysis, a Lean proof-checker benchmark release, and Amit Sahai’s proposal for expanding human mathematical expertise. Archival social-media coverage remains limited.

Research updatesSelect an entry to read more

ProofGap separates local formal reasoning from complete proof construction in analysis Lihan Xie, Zhicheng Hui, Yingjun Lan, Zhehao Li, Xingzhi Qi, Siyue Huang, Jirui Liu, Chuxiao Zeng, Bohan Zhao and Qinxiang Cao Published: 3 sources

The preprint constructs 26,116 local proof obligations from solutions to 3,015 Demidovich analysis exercises and provides benchmark-native and Lean versions. Its reported experiments show a substantial gap between completing individual steps and proving their parent exercises: Goedel-Prover-V2-8B reaches 35.39% versus 4.28% at eight attempts. The arXiv record dates version 1 to September 24 at 09:30:22 UTC, within the Paris day.

Research relevance:

Offers a way to diagnose failures involving analytic side conditions and local derivations separately from global proof planning, with public data and code for evaluating research assistants.

Claim status:
Available preprint and public repository. The authors report Lean-verified reference proofs and checker-based experiments; these were not independently reproduced for this digest.
Limitations:
Inputs already supply formal contexts and goals, including earlier intermediate propositions as premises. Success therefore does not establish faithful autoformalization, detection of invalid informal steps, or complete proof composition. The benchmark chiefly concerns textbook analysis.

Sources & further reading

Link to this entry
Lean Kernel Arena archives its September proof-checker benchmark round The Lean Kernel Arena contributors; Joachim Breitner, editor Published: 2 sources

A Zenodo release preserves the September 2026 benchmark round for Lean proof checkers, including the rendered results site, raw JSON results and test suite. The record explicitly gives September 24 as its publication and creation date.

Research relevance:

Provides reproducible infrastructure for studying the checking stage of formal mathematics, relevant when AI systems generate large proof artifacts and checking cost becomes a practical constraint.

Claim status:
Published benchmark dataset with an accessible results site. This is a proof-checker evaluation release, not an announcement of a new mathematical theorem.
Limitations:
The maintainers state that results are comparable only within a round because checkers, tests and Lean versions change. Benchmark performance does not independently certify every mathematical artifact checked by a system. No tests were executed for this digest.

Sources & further reading

Link to this entry
Amit Sahai argues for expanding independent mathematical expertise alongside AI discovery Amit Sahai Published: 1 source

In a dated guest post on Tao’s blog, Sahai argues that accelerated AI discovery could increase the need for mathematicians who develop shared understanding of unfamiliar results and consequential technologies. He emphasizes independent expertise: a formal guarantee remains conditional on a model, whose assumptions and relationship to evidence require scrutiny. He discloses AI assistance in drafting the essay.

Research relevance:

A concrete contribution to research practice and training: mathematical explanation, interdisciplinary understanding and independent assessment become work that institutions must support as proof production accelerates.

Claim status:
Published opinion essay, not an empirical demonstration or a new proof. Its scenarios describe possible future demands on mathematical expertise.
Limitations:
The argument does not quantify future staffing needs or establish that AI has achieved the hypothetical capabilities discussed. It supplies no new formalization or research software.

Sources & further reading

Link to this entry
Coverage and limitations
  • Public web searches reconstructed the Paris civil day September 24, 2026. Inclusion dates come from original arXiv submission records, Zenodo publication metadata, and a dated blog post; indexing dates were not treated as publication dates.
  • Read ProofGap’s arXiv abstract and HTML paper, its public GitHub repository, the Lean Kernel Arena Zenodo record and results site, and Amit Sahai’s guest post on Terence Tao’s blog.
  • Consulted Tao’s September archive, Kevin Buzzard’s Imperial webpage and Xena blog, and official Lean, Axiom, Epoch AI, Project Numina and Harmonic websites. Buzzard’s institutional page confirms https://xenaproject.wordpress.com/ as his blog; Lean’s official links page identifies its official Twitter account.
  • Date-specific searches covering the supplied individual and organizational leads did not establish additional eligible posts. Most supplied X identities were not independently confirmed against official websites. No complete X timelines were consulted, and Mathstodon and Bluesky archives were not consulted; absence from search results does not establish absence of news.
  • MathsAI and other indexed pages supplied leads rather than proof verification. An indexed Ostmann conjecture entry dated September 24 could not be opened successfully. The current openai/math repository was readable, but its visible contents did not establish an original September 24 public release; conjecture-resolution leads from it were excluded.
  • Excluded previously covered Lean Pool material resurfacing in September 24 digests, month-only Project Numina material, and event listings whose event dates did not establish publication dates. September 24 newspaper discussions of the earlier Navier–Stokes announcement were seen in search results but did not establish a substantial new technical update.
  • No source code was executed, no Lean build was run, and no mathematical proof was independently verified.

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