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 · 10 linked sources Partial coverage
Armstrong and Loher announce five AI-assisted Lean developments in mathematical physics and hypoelliptic PDE Scott Armstrong and Amélie Loher Published: 8 sources

Armstrong's October 11 announcement links public developments covering stability of matter, ionization and thermodynamic and Thomas–Fermi limits; Fröhlich–Spencer phase-transition and localization results; Hörmander and Rothschild–Stein theory; the Kupiainen–Rhodes–Vargas DOZZ proof; and kinetic Aleksandrov estimates. Repository documentation provides source-facing theorem interfaces, dependencies and audit procedures. The LiebThirring repository also exposes an orchestration transcript, adding a concrete workflow artifact to the announcement.

Research relevance:

Potentially reusable formal infrastructure for analysis, probability and mathematical physics, alongside material for studying how supervised AI agents translate substantial papers into Lean.

Claim status:
Announcement date comes from supplied API created_at timestamps. Public repositories and author websites were directly read. Authors report AI-written code under supervision; several repositories report proofs using only standard Lean axioms and comparator checks. These are author-reported formalization and audit claims, not checks performed for this digest. No independent mathematical scrutiny was established.
Limitations:
The underlying mathematics largely predates this announcement. Armstrong reports work starting Monday and finishing Saturday; repository publication dates were not separately established. Scope differs by package: LiebThirring concerns nonrelativistic three-dimensional Coulomb matter and does not claim sharp kinetic constants; DOZZ excludes general-metric Weyl anomaly and the regime gamma at least 2. Kinetic estimates require stated ellipticity and exponent conditions. Intentional placeholders in comparator challenges must be distinguished from solution proofs. Faithfulness of all definitions and statements remains unaudited here.

Sources & further reading

Link to this entry
Tao publishes Math 2.0 slides outlining uses of AI that support mathematical understanding Terence Tao Published: 2 sources

Tao published slides from his October 9 Caltech lecture. Proposed research uses include clarifying opaque proofs, connecting literature, developing formal libraries, exploring altered hypotheses and reducing theoretical dependencies. He also recommends tracking resources and failed attempts when assessing AI capabilities. Today's earlier entry is retained after rereading the author-published resource.

Research relevance:

Offers concrete directions for research workflows beyond theorem production: investigate nearby statements, understand essential assumptions and improve reusable explanations and infrastructure.

Claim status:
Directly read the author's dated post and linked lecture slides. This is a research agenda with illustrative examples, not a new theorem, independently evaluated workflow or checked formalization.
Limitations:
The post appeared October 10 and the lecture occurred October 9. Examples include older work and do not establish new in-window results. Workflow effectiveness is not quantified, and references to forthcoming models do not establish tool availability.

Sources & further reading

Link to this entry
Coverage and limitations
  • Actually used public web search and opened primary websites, blogs and repositories. Publication dates were distinguished from search crawling dates. Previously covered results were excluded; today's earlier Math 2.0 item was rechecked and retained.
  • Read Armstrong's research website, repository directory and October 4 workflow post, Loher's homepage, and all five repositories linked in Armstrong's October 11 supplied posts. Official websites corroborate the researchers and their formalization activity; they did not independently authenticate the supplied X handle. The October 4 workflow post is older background, not new in-window news.
  • Read Tao's October 10 Math 2.0 post, its linked 29-page lecture PDF and his living summary. The PDF initially failed to open but succeeded through the author's link. Also consulted Xena, Gowers's Weblog, Shtetl-Optimized, Proofs and Prompts and OpenAI's repository history. No additional in-window correction was substantiated from the history, whose visible entry remained October 7.
  • Read Epoch's official arXiv explorer and methodology. The explorer is marked updated October 6; the October 9 supplied post does not establish a new dataset release. Its September percentage claims were not independently reproduced and were omitted as a separate news item.
  • Consulted public websites or official search results for Thomas Bloom, Daniel Litt, Alex Kontorovich, Boaz Barak, Lean, Project Numina, Harmonic and Axiom. Kevin Buzzard's Imperial profile and Xena were consulted. Searches for the supplied researchers were uneven; not every social handle was independently established. Attempted Alpöge, Bubeck and de Moura pages returned errors; Loher's Lean directory also failed. François Charton's identity and current activity were not independently established.
  • Supplied social collection: mathstodon.xyz was unavailable after an HTTPError; xenaproject.bsky.social reported ok with no posts. Both excluded replies and reposts and checked at most 300 posts. Complete pagination was not established; empty results do not establish inactivity.
  • Supplied X collection reported ok for every listed account. API posts were supplied for scottnarmstrong, thomasfbloom, littmath, alexkontorovich, boazbaraktcs and epochairesearch; only those supplied posts were directly available. __alpoge__, wtgowers, sebastienbubeck, f_charton, leonard41111588, leanprover, projectnumina, harmonicmath and axiommathai had empty supplied results.
  • Every supplied X feed used bounded collection, excluded replies and reposts and could include cached posts. No numerical pagination cap, complete-pagination evidence, skipped-account list or budget-exhaustion error was supplied in this refresh. Cached posts are not a fresh timeline read, API resolution is not identity verification, and the collection does not establish exhaustive access to X.
  • No source code was executed, no Lean proof was checked, and no shell, editing tool or private connector was used.

Requested coverage window: 2026-10-09T20:00:01.240844+02:00 — 2026-10-11T22:01:57.082757+02:00.

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

Archives 55
Older editions (25)