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

1 entry · 2 linked sources Partial coverage
Tristan Buckmaster proposes privacy, open infrastructure, and revised credit for AI-assisted mathematics Tristan Buckmaster Published: 2 sources

In a guest essay hosted on Terence Tao’s official blog, Buckmaster argues that a machine-certified result would settle truth without supplying human understanding. He identifies rigorous mathematical physics as a particularly promising target for AI, where systems might help turn heuristic physical derivations into proofs with explicit regimes and error bounds. For everyday research practice, he recommends institutional agreements with zero-data-retention and auditing provisions, opt-in treatment of user data, independently funded open-weight infrastructure, detailed AI-use disclosure, and greater credit for exposition, shared tools, and collaborative projects. The post explicitly says that an LLM assisted with editing.

Research relevance:

The essay translates broad concern about AI in mathematics into concrete workflow and governance proposals relevant to researchers entering unpublished ideas into commercial systems. Its suggested emphasis on rigorous mathematical physics also identifies a plausible research program where AI assistance could have mathematical value beyond producing isolated theorem statements.

Claim status:
Published opinion and policy proposal, not an announcement of a new proof, formalization, or independently checked mathematical result. The host page identifies it as a guest post by Tristan Buckmaster, and Buckmaster’s identity and NYU affiliation are corroborated by his official NYU page. Claims about particular companies, costs, data practices, and the quality of earlier manuscript releases remain the author’s assertions and were not independently established for this digest.
Limitations:
The post provides strategic recommendations rather than tested technical methods, code, benchmarks, or formal artifacts. Its forecasts about capability growth and changes to mathematical careers are speculative. References to a hypothetical Lean certification do not report an actual Lean development, and this digest did not execute Lean or verify any proof. Several strong criticisms of AI companies would require a separate source-by-source investigation.

Sources & further reading

Link to this entry
Coverage and limitations
  • Directly read Terence Tao’s official What’s New blog, including the new guest post, and checked the linked official NYU profile identifying Tristan Buckmaster. Also checked the Xena Project blog, Simon Frieder’s supplied blog domain through web search, the Lean organization and release pages on GitHub, Lean-related search results, Papers With Lean, Project Numina, and recent arXiv-oriented search results. Search indexing is not exhaustive, and some project pages exposed little or no readable text.
  • The supplied X API collection was available but bounded for @__alpoge__, @scottnarmstrong, @wtgowers, @SebastienBubeck, @thomasfbloom, @littmath, @AlexKontorovich, @f_charton, @Leonard41111588, @boazbaraktcs, @leanprover, @ProjectNumina, @HarmonicMath, @axiommathai, and @EpochAIResearch. Replies and reposts were excluded; cached posts may be present; the pagination or post cap was not specified; and API account resolution is not independent identity verification. Empty feeds for several accounts do not establish inactivity. The few supplied posts in the window were either unrelated commentary, links without enough independently verified mathematical substance, or continuations of previously reported material.
  • The supplied Bluesky collection for @xenaproject.bsky.social succeeded but returned no posts. Replies and reposts were excluded, and at most 300 posts were checked. The empty result does not prove there were no relevant posts.
  • Direct Mathstodon collection for Terence Tao failed with an HTTP error. Replies and reposts were excluded and at most 300 posts would have been checked. Consequently, Tao’s Mathstodon activity could not be assessed.
  • No direct X API feed was supplied for Terence Tao, and direct X access beyond the supplied API posts was not assumed. Indexed X snippets were treated only as leads. The narrow time window, failed Mathstodon access, bounded social collection, and incomplete search indexing make this edition partial rather than exhaustive.

Requested coverage window: 2026-10-20T20:00:02.062739+02:00 — 2026-10-22T08:00:01.150138+02:00.

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

Archives 55
Older editions (25)