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 · 6 linked sources Partial coverage
MathEconLib releases a broad Lean library for economic and political theory MathEconLib contributors; support announced by Axiom Math Published: 3 sources

Axiom Math’s supplied X posts announce the open-source release of MathEconLib. The public Econlib repository describes a Mathlib-based library covering preferences, probability, optimization, game theory, mechanism design, social choice and equilibrium. Its advertised results include utility representation, Nash existence, Arrow’s impossibility theorem and Walrasian existence. Examples, tests and an agent-plugin directory are available.

Research relevance:

The library offers a domain-specific corpus for autoformalization, theorem retrieval and research workflows. Its documented policy requires public results to have external consumers or semantic witnesses, addressing the practical danger of formally valid statements that fail to express useful mathematics.

Claim status:
Public source release with advertised formalizations. The README claims no sorry declarations or additional axioms beyond Lean’s standard three. This digest read the repository description but did not build the project, audit theorem statements or verify those claims. The announcement date comes from the supplied X post’s created_at timestamp.
Limitations:
The project website was inaccessible, leaving the announcement-to-repository connection incompletely corroborated. Formal acceptance would establish consequences of formal assumptions, not fidelity to intended economic concepts. The repository pins Mathlib v4.29.0 and showed only two commits. No independent audit was found.

Sources & further reading

Link to this entry
Anthropic and Theorem publish Rocq artifacts from AI-assisted binary verification Anthropic and Theorem Published: 3 sources

Anthropic reports that Claude patched failures and produced Rocq proofs for 239 entry points across 123 OSS-Fuzz libraries, covering inputs up to 64 MB under specified machine assumptions. The public proof repository currently lists 60 entry points in 25 libraries. Its stated property compares sanitized and ordinary compiled binaries and establishes that the sanitizer detects no error within the prescribed limits.

Research relevance:

For mathematical AI, this is an inspectable experiment in generating and reusing large formal proofs. It highlights how proof generation depends on reusable lemmas, precise theorem statements and trusted mathematical models of computation.

Claim status:
Organizational report with public proof artifacts. The collaborators describe machine-checked Rocq proofs; this digest did not run Rocq or independently reproduce the results. The public subset must be distinguished from the larger reported experiment. This replacement makes that quantitative distinction explicit.
Limitations:
The guarantees concern selected entry points and modeled behavior, not complete library correctness. They assume single-threaded, statically linked RISC-V binaries, fixed memory budgets and modeled Linux behavior. The semantics repository explicitly warns that its model is incomplete and contains unchecked assumptions. Some artifacts are withheld to avoid exposing unpatched vulnerabilities.

Sources & further reading

Link to this entry
Coverage and limitations
  • Research window: 2026-10-21T20:00:01.150138+02:00 through 2026-10-23T09:13:07.009469+02:00. Public web search was used. Earlier items from today were rechecked and retained; previously covered older material was excluded.
  • Directly read Anthropic’s dated report, Theorem’s public proof repository and machine-semantics repository, and the Econlib repository README. These are primary organizational sources, not independent reproductions. No code or proof checker was executed.
  • MathEconLib’s announced website, https://mathecon.dev, remained inaccessible through the web reader. Axiom Math’s official engineering page was read to cross-check the organization and its Lean work, but it did not independently establish ownership of the separate danlyng repository or authenticate the supplied X account.
  • Consulted Terence Tao’s official blog and archive, Kevin Buzzard’s Xena blog, and Simon Frieder’s blog. Buzzard’s Imperial homepage explicitly links Xena, establishing its official connection. No additional qualifying dated post was established. Search results and blog archives may be incomplete or stale.
  • All 15 supplied X feeds reported successful bounded API collection. Posts were supplied for @__alpoge__, @scottnarmstrong, @alexkontorovich and @axiommathai. The feeds for @wtgowers, @sebastienbubeck, @thomasfbloom, @littmath, @f_charton, @leonard41111588, @boazbaraktcs, @leanprover, @projectnumina, @harmonicmath and @epochairesearch returned no posts. Replies and reposts were excluded; cached posts were included. Pagination completeness and numerical collection budgets were unspecified, and no skipped accounts were reported. Empty results do not establish inactivity. These supplied posts were not a fresh timeline read during this research, and API resolution does not authenticate identities.
  • The supplied xenaproject.bsky.social collection succeeded with no posts, excluding replies and reposts and checking at most 300 posts. Its pagination completeness was unspecified. The supplied mathstodon.xyz collection failed with an HTTP error under the same 300-post cap; no direct Tao Mathstodon timeline was available.
  • Alpöge’s institutional homepage returned no readable content, so his X identity was not independently authenticated. His post served only as a lead to Anthropic’s official report. Other supplied social commentary lacked sufficient primary evidence or research substance for inclusion.
  • Older material found late was excluded: David Harvey’s integer-multiplication assessment is dated 2026-10-20; Microsoft’s KLS announcement is dated 2026-10-21 without a primary-source publication time establishing eligibility after the window opened, and describes proofs from earlier October. The autoformalized-specification paper arXiv:2610.30059 was submitted at 17:19:33 UTC on October 21, before the window opened, despite later indexing. A tensor-network library page displayed an October 22 update, but no specific substantive change was established.

Requested coverage window: 2026-10-21T20:00:01.150138+02:00 — 2026-10-23T09:13:07.009469+02:00.

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

Archives 55
Older editions (25)