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

Today's edition retains saved research entries alongside the latest refresh. Public web research found substantive leads, but none could be reliably placed within October 8, 2026, 20:00:01 through October 9, 2026, 09:13:03 Europe/Paris. No items are included: older findings, previously covered results and developments with unresolved publication times were excluded. Significant access gaps prevent a confident no-news conclusion.

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
  • Actually used public web search and opened primary papers, repositories, project websites and mathematical blogs. No shell, private connector or source code execution was used.
  • Read Terence Tao's blog at https://terrytao.wordpress.com/, Gowers's Weblog at https://gowers.wordpress.com/ and Xena at https://xenaproject.wordpress.com/. Buzzard's Imperial website identifies Xena as his project: https://www.ma.imperial.ac.uk/~buzzard/. His indexed GitHub profile links the supplied Bluesky handle, but that is supporting evidence rather than independent authentication.
  • Consulted the personal websites https://alpo.ge/, https://www.scottnarmstrong.com/ and https://www.thomasbloom.org/. These establish the relevant mathematicians' websites; they did not independently authenticate all supplied X handles. No mathematical claim was accepted solely from a social account.
  • Opened https://lean-lang.org/, https://axiommath.ai/, https://epoch.ai/ and https://www.harmonic.fun/. https://projectnumina.ai/ returned no readable text. The similarly named https://numina.ai/ is a different business and was excluded. Searches did not establish complete coverage of Bubeck, Litt, Kontorovich, Charton, de Moura or Barak.
  • Read the arXiv abstract and HTML of https://arxiv.org/abs/2610.08144 and https://arxiv.org/html/2610.08144v1. This critique of semantic mismatches in AI autoformalization was submitted on October 6 at 10:58:01 UTC. Later October 8–9 reports do not make it an in-window result; it was excluded as older material found late. No proof was independently verified and Lean was not executed.
  • Read https://github.com/CrocSwap/integer-mult-bounds and pull requests https://github.com/CrocSwap/integer-mult-bounds/pull/61 and https://github.com/CrocSwap/integer-mult-bounds/pull/62. They describe AI-assisted conditional exponent improvements with finite certificates and scoped Lean arithmetic, while retaining assumptions from OpenAI's multiplication framework. October 8 dates were visible, but the relevant publication and revision times could not be established relative to the 18:00:01 UTC cutoff. Public GitHub API requests and the commit-history page failed; these leads were excluded rather than assigned speculative times.
  • The indexed OpenAI history at https://github.com/openai/math/blob/main/history.md describes October 7 withdrawals, repairs and additional formalizations. These precede the window and overlap previous coverage. Previously reported AlphaProof Nexus, LEVER and Argonaut Math items were not repeated without a confirmed substantive update.
  • https://www.erdosproblems.com/ and https://www.erdosproblems.com/blog could not be read. An indexed report of Bloom's discussion of 23 OpenAI-related Erdős problems remained a secondary lead. https://www.plasma.ai/research/erdos appeared in an indexed snippet announcing a record and a proof for Problem 809, but direct reading failed and exact timing was unresolved; it was excluded.
  • Supplied Bluesky collection for xenaproject.bsky.social: status ok, zero posts returned, replies and reposts excluded, at most 300 posts checked. Empty results do not establish inactivity or exhaustive pagination.
  • Supplied Mathstodon collection for actor mathstodon.xyz: unavailable because of an HTTPError; zero posts supplied, replies and reposts excluded, at most 300 posts checked. The supplied actor identifies a server rather than explicitly identifying Tao's account, so account-specific coverage is unresolved.
  • Supplied X collection for __alpoge__, scottnarmstrong, wtgowers, sebastienbubeck, thomasfbloom and littmath: each unavailable after HTTP 400, with incomplete timelines. No API posts were supplied for any of these accounts.
  • Supplied X collection for alexkontorovich, f_charton, leonard41111588, boazbaraktcs, leanprover, projectnumina, harmonicmath, axiommathai and epochairesearch: each unavailable because the per-run post or time budget was exhausted. No API posts were supplied; these timelines were not directly consulted.
  • All supplied X collections exclude replies and reposts, use bounded collection and permit cached posts. Numeric pagination caps and completed page counts were not supplied. Cached material is not a fresh timeline read, and API account resolution is not identity verification. Indexed social excerpts were treated only as leads; no complete X timeline access is claimed.
  • Search indexing dates were not treated as publication dates. The short overnight window, inaccessible primary pages, unresolved same-day timestamps and missing social timelines materially limit this edition.
  • 3 entries retained from earlier editions today; their sources were consulted in those editions, not necessarily during this refresh.

Requested coverage window: 2026-10-07T20:19:28.116236+02:00 — 2026-10-09T09:13:03.098805+02:00.

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

Archives 36
Older editions (6)