AI & Maths watch GitHub

Archived edition

Updates on artificial intelligence for mathematical research, proof discovery and formal verification, with links to papers, code and tools.

At a glance3 entries · 9 linked sources Partial coverage

Three substantive items: AlphaProof Nexus reaches journal publication, LEVER studies cost and proof quality during formal search, and Argonaut Math releases a claimed refinement of a zero-free region. Social-source coverage and independent verification remain limited.

Research updatesSelect an entry to read more

AlphaProof Nexus receives journal publication, with public research-level proof artifacts George Tsoukalas and collaborators Published: 4 sources

Science's publisher announces publication of the AlphaProof Nexus study on October 8. This is a publication update to work first submitted to arXiv on May 21, rather than newly discovered October results. The authors report resolving 9 of 353 attempted Erdős problems and proving 44 of 492 OEIS conjectures. Their repository supplies Lean developments and human-written prose proofs for selected results, alongside information about attempted problems.

Research relevance:

A concrete research workflow combining language-model agents, formal proof search and mathematical collaboration. Public artifacts span combinatorics, algebraic geometry, optimization, graph theory and quantum optics.

Claim status:
Journal publication reported by the publisher; author-reported mathematical successes supported by available proof artifacts. Repository documentation describes mechanically formalized proofs, but this digest did not check them.
Limitations:
The journal article could not be directly read; the publication date comes from indexed publisher text. The underlying results predate the window. The results repository principally contains successes, although attempted-problem lists are linked. Success counts do not establish broad autonomous research competence or certify correspondence between every formal and informal statement.

Sources & further reading

Link to this entry
LEVER optimizes proof-search cost and mathematical proof quality together Nihal Jain, Shuangjie Yao, Begum Cicekdag, Zhuo Zhang and Suman Jana Published: 2 sources

LEVER searches an AND/OR graph of partial Lean proofs using objectives that can combine computational cost, proof length and distance from a theorem's mathematical subject. On the authors' PutnamBench evaluation under matched budgets, they report a solve-rate increase from 80% to 96% while reducing cost by 34% against a single-conversation agent. They also compare subject-focused search with subsequent proof refactoring.

Research relevance:

Relevant to practical formalization workflows where an accepted proof must also be affordable to find and understandable enough to maintain. It makes proof quality an explicit search objective.

Claim status:
Available preprint with author-reported benchmark experiments; submitted October 8 at 12:40:14 UTC. No independent replication was established.
Limitations:
PutnamBench consists of competition mathematics and does not demonstrate performance on arbitrary research papers. Proof-quality metrics are proxies for mathematical clarity. This digest did not execute the system or verify the reported Lean outputs.

Sources & further reading

Link to this entry
Argonaut Math claims a small refinement of OpenAI's quasi-Riemann zero-free boundary Argonaut Math Published: 3 sources

A dated repository announcement proposes replacing the boundary 7/8 by 3499999/4000000, an improvement of 1/4000000. The project provides a manuscript and Lean sources built on OpenAI's quasi-Riemann development, and reports successful compilation and Comparator verification.

Research relevance:

An inspectable example of follow-up research extending a recently released AI-assisted formal development.

Claim status:
Public proof artifacts and a maintainer-reported formal check are available. No independent specialist scrutiny or validation was established.
Limitations:
The claim concerns strict half-planes for zeta, Dirichlet L-functions and a specified class of Hecke characters; the boundary is excluded and principal-character poles require care. It depends on OpenAI's earlier development. Neither that dependency nor the extension was verified here, and formal acceptance alone would not establish faithful translation of the intended analytic theorem. The announcement supplies a calendar date without a publication time.

Sources & further reading

Link to this entry
Coverage and limitations
  • Research window: 2026-10-07 20:19:28 to 2026-10-09 08:00:01, Europe/Paris. Publication and submission dates were distinguished from search-engine indexing dates.
  • Public web search was used. Directly read arXiv abstracts, LEVER's HTML paper, Google DeepMind's results repository, Argonaut Math's repository and supporting README files, and OpenAI's history file. The previously covered OpenAI withdrawals and repairs were not repeated.
  • Read Terence Tao's blog and its October 8 guest essay, and Kevin Buzzard's Xena blog. Buzzard's Imperial homepage explicitly confirms https://xenaproject.wordpress.com/ as his blog; Tao's UCLA homepage lists his research blog and Mastodon presence.
  • Consulted Boaz Barak's official homepage and the Lean, Axiom, Project Numina and Harmonic websites. Numina returned no readable text; Harmonic exposed little research content. Searches of Epoch AI surfaced older pages and October 6 updates, which were not treated as news within this window.
  • The supplied mathstodon.xyz feed was unavailable because collection failed with an HTTPError. The collector excludes replies and reposts and checks at most 300 posts; no usable posts were supplied.
  • The supplied xenaproject.bsky.social feed collected successfully but returned no posts. Replies and reposts are excluded and collection is capped at 300 posts. An empty collection does not establish inactivity, and the exact Bluesky handle was not independently authenticated.
  • X coverage was incomplete: no complete timelines were consulted and no X API access was available. Searches involving the supplied mathematician accounts yielded insufficient dated primary evidence. Most supplied X handles remain unverified against official websites; no digest item relies on their identity or tweets.
  • Science's article page failed to load. Its publisher's October 8 release was available through indexed search text, but a direct fetch returned HTTP 403. The journal-publication update therefore has weaker access than the directly read preprint and repository.
  • The October 6 Navier–Stokes translation-audit preprint was found late and excluded as outside the window. No source code was executed, no Lean build was run, and no proof was independently verified.

Requested coverage window: 2026-10-07T20:19:28.116236+02:00 — 2026-10-09T08:00:01.938189+02:00.

Public web research; coverage is not exhaustive. A source link is not a certification of a claim.

Archives 36
Older editions (6)