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.

Research updatesSelect an entry to read more

2 entries · 8 linked sources Partial coverage
Anthropic and Theorem release Rocq artifacts from large-scale AI-assisted binary verification Keane Lucas, Aengus Lynch, Luna Tong, Luke Champine, Zygi Straznickas, Dino Distefano, Harshikaa Agrawal, Evyatar Ben Asher, Ava Howell, Sami Jawhar, Chris Rohlf, Nickolai Zeldovich, Nicholas Carlini, Rajashree Agrawal, Jason Gross, and Theorem Published: 4 sources

Anthropic reports that Claude generated machine-checked Rocq proofs for 239 fuzz-test entry points across 123 OSS-Fuzz libraries after patching discovered failures. The specifications assert normal termination without modeled memory-safety errors or failed assertions for every input below 64 MB. Proofs operate over compiled RISC-V instructions using Theorem’s formal Linux-process and instruction semantics; Anthropic reports roughly 180 million lines of Rocq in total and has released a subset of the artifacts, including proofs that did not expose unpatched bugs. The work is relevant to mathematical AI because it demonstrates proof generation at a scale far beyond manual review and makes specification design, trusted semantics, proof reuse, and kernel checking the central workflow.

Research relevance:

This is a concrete public test of whether language-model proof generation can scale by exploiting highly repetitive formal arguments. Anthropic reports that shared workspaces reduced token use by 17 percent in a smaller experiment, suggesting a potentially useful research pattern: accumulate reusable formal lemmas and let agents adapt existing proof structures rather than begin independently. The released repository and semantics provide material for scrutiny by formal-methods researchers.

Claim status:
Available artifacts supporting an organizational claim. Anthropic and Theorem state that the Rocq kernel checked the generated proofs and invite independent verification. Public repositories contain theorem statements, proofs, analyses, and formal RISC-V/Linux-process semantics, but this digest did not execute them and found no completed independent reproduction. The claimed bug discoveries and scale figures remain reports by the collaborating organizations.
Limitations:
The central results are no-crash guarantees for selected fuzz-test entry points, not proofs that entire libraries are correct or bug-free. They assume single-threaded, statically linked RISC-V binaries, musl libc, fixed memory budgets, modeled Linux behavior, and inputs below 64 MB; most deployed systems use different architectures and linking arrangements. AddressSanitizer and the selected entry points do not cover every possible defect or caller misuse. Trust remains in the theorem statements, Rocq checker, formal machine and OS semantics, compilation stack, and hardware. Because Claude could patch targets, specification gaming was possible; the authors say patches were penalized, logged, and audited. Some proofs were withheld where publication could reveal unpatched vulnerabilities.

Sources & further reading

Link to this entry
MathEconLib opens a broad Lean library for economic and political theory MathEconLib contributors, with support announced by Axiom Math Published: 4 sources

MathEconLib was announced as open source and its public repository provides a Mathlib-based Lean 4 library spanning preferences, probability, optimization, game theory, mechanism design, social choice, and general equilibrium. The repository advertises formalizations including Debreu-style utility results, KKT and duality results, Nash and Walrasian existence, Arrow’s and Gibbard–Satterthwaite theorems, fixed-point theory, and optimal transport. It also supplies worked examples, tests, a glossary, generated documentation, and an agent plugin.

Research relevance:

For researchers working on autoformalization, the project offers a sizable domain-specific target with explicit economic objects rather than isolated theorem exercises. Its stated design requires public declarations to be exercised by examples or semantic witnesses, an attempt to detect formal statements that typecheck yet are vacuous, reversed, or unusable. The pinned Lean and Mathlib versions and documented import surface could also make it a practical corpus for theorem retrieval and proof-generation experiments.

Claim status:
Open-source release with inspectable Lean source. The repository states that its results contain no sorry declarations or project-specific axioms beyond Lean’s standard axioms, but this digest did not build the project, audit every theorem statement, or confirm correspondence with the cited informal economics. Axiom Math’s supplied direct X posts announce that it co-founded and continues to support the project; the project website could not be read independently.
Limitations:
Kernel acceptance would establish only that each formal conclusion follows from its formal assumptions. It would not show that the definitions faithfully capture the intended economic concepts, that modeling assumptions are empirically appropriate, or that theorem names match the strongest standard formulations. The repository was extremely new, displayed very little commit history, and no independent mathematical audit was found. It pins Mathlib v4.29.0 rather than the newest Lean environment. The original release date is taken from the supplied X API post because no dated release page was accessible.

Sources & further reading

Link to this entry
Coverage and limitations
  • Window checked: 2026-10-21T20:00:01+02:00 through 2026-10-23T08:00:01+02:00. Previously reported items were excluded.
  • Directly read Anthropic’s dated research report and the public Theorem repositories containing released proofs and machine semantics. No proofs were executed, and no independent reproduction or comprehensive expert review was found.
  • Directly read the public MathEconLib GitHub repository. Its website, https://mathecon.dev, was inaccessible through the web reader, so the site itself could not be inspected. The release date comes from Axiom Math’s supplied X API posts, not from a dated repository release.
  • The supplied X API collection directly returned bounded, reply-free and repost-free results for all listed X accounts. Relevant posts appeared for @__alpoge__, @AlexKontorovich, and @axiommathai; @scottnarmstrong’s posts were not substantive for this digest. The remaining listed X feeds returned no posts. Empty bounded results do not establish inactivity, cached posts may be included, pagination completeness was not specified, and API resolution is not independent identity verification.
  • The Anthropic item was found through Levent Alpöge’s supplied X post, but the substantive claims and date were checked against Anthropic’s official report and Theorem’s repositories. The feed account itself was not independently authenticated.
  • Axiom Math’s identity and work on Lean tooling were cross-checked against https://axiommath.ai/ and https://axiommath.ai/engineering/. The claimed collaboration on MathEconLib was announced through Axiom Math’s supplied direct X feed; the repository is under the separate danlyng account, and the inaccessible project website prevented a fuller authorship check.
  • Kevin Buzzard’s Bluesky feed was collected successfully but contained no qualifying original posts within the bounded, reply-free and repost-free collection of at most 300 posts. Terence Tao’s Mathstodon collection failed with an HTTP error after checking at most 300 posts; therefore no direct Mathstodon timeline was available.
  • Terence Tao’s official blog archive was consulted; no new qualifying post after the previously reported 2026-10-21 entry was visible. Simon Frieder’s blog and several other supplied accounts yielded no qualifying, independently substantiated item in the window. Search indexing can lag publication, and this was not exhaustive access to X or the wider web.

Requested coverage window: 2026-10-21T20:00:01.150138+02:00 — 2026-10-23T08:00:01.746363+02:00.

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

Archives 55
Older editions (25)