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
Tao publishes Math 2.0 slides with concrete proposals for AI-assisted research Terence Tao Published: 2 sources

Tao released slides from his October 9 Caltech lecture, proposing uses of AI that strengthen mathematical understanding: improving opaque proofs, connecting literature into living research networks, building formal libraries, exploring modified hypotheses, and seeking proofs with fewer theoretical inputs. He also advocates reporting resource consumption and failed attempts when assessing AI capabilities. This adds a concrete lecture resource to his previously covered September 30 discussion of research-policy reports.

Research relevance:

Offers research mathematicians a practical agenda beyond isolated theorem solving: use AI to investigate the neighborhood of a theorem, test which dependencies are essential, and improve explanations and reusable mathematical infrastructure.

Claim status:
Directly read author-published post and lecture slides. These are proposals and illustrative examples, not a new theorem announcement, independently evaluated workflow study or checked formalization.
Limitations:
The post was published October 10; the lecture occurred October 9. Examples in the slides include older projects and do not establish new in-window results. Suggested workflows require mathematical judgment, and their effectiveness is not quantified here. Mentioned forthcoming models were not treated as available tools.

Sources & further reading

Link to this entry
Coverage and limitations
  • Public web searches were performed for dated mathematics and AI developments, Lean, autoformalization, and the supplied researchers and organizations. Search indexing dates were not treated as publication dates.
  • Directly consulted Tao's What's New blog, Math 2.0 post and lecture PDF, Xena, Gowers's Weblog, Shtetl-Optimized, Proofs and Prompts, and the OpenAI mathematics repository history. Previously covered material was excluded. The Navier-Stokes lost in translation arXiv page was also consulted; the older paper was not presented as an in-window development.
  • Consulted public websites for Lean, Axiom, Harmonic, Epoch AI, Leonardo de Moura, Boaz Barak, Thomas Bloom and Daniel Litt. Some pages offered sparse content. Project Numina's website yielded indexed content but its direct page extraction was empty; an attempted www address returned an error.
  • Kevin Buzzard's Imperial homepage explicitly links to https://xenaproject.wordpress.com/, establishing the official Xena blog. Tao's blog identifies its author and links to his Mastodon page. Official-site checks did not independently establish every supplied social handle; no substantive claim was attributed solely from an account name or API resolution.
  • Attempts to consult Sébastien Bubeck's website and the attempted Rutgers address for Alex Kontorovich returned errors. Levent Alpöge's Harvard page returned no readable content. Scott Armstrong's NYU profile was found through search. François Charton's supplied account was encountered through indexed social material, without an independently confirmed official-site account link.
  • Supplied social collection: mathstodon.xyz was unavailable after an HTTPError; replies and reposts were excluded and at most 300 posts were checked. xenaproject.bsky.social collection reported ok with no posts; replies and reposts were excluded and at most 300 posts were checked. Empty results do not establish inactivity, and complete pagination was not established.
  • Supplied X collection: __alpoge__, scottnarmstrong, wtgowers, harmonicmath, axiommathai and epochairesearch were unavailable after HTTP 400 errors, with incomplete timelines. No API posts were supplied for these accounts.
  • Supplied X collection: sebastienbubeck, thomasfbloom, littmath, alexkontorovich, f_charton, leonard41111588, boazbaraktcs, leanprover and projectnumina were unavailable because the per-run post or time budget was exhausted. No API posts were supplied; these timelines were not directly read.
  • All supplied X collection was bounded, excluded replies and reposts, and allowed cached material; no numerical pagination cap was provided. Cached material would not constitute a fresh timeline read. Indexed X and mirror snippets were used only as leads, without reliable current post dates or exhaustive timeline access.
  • No source code was executed, no Lean proof was checked, and no private connector, shell or editing tool was used.

Requested coverage window: 2026-10-09T20:00:01.240844+02:00 — 2026-10-11T08:00:02.064084+02:00.

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

Archives 55
Older editions (25)