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 · 4 linked sources Partial coverage
Roberts identifies concrete cleanup and correspondence checks for AI-generated proof artifacts David Roberts Published: 2 sources

Roberts examines what makes mathematical output useful beyond a claimed theorem. His essay illustrates empty Lean namespaces and repetitive setup code in OpenAI's release, and argues that readable exposition and basic artifact cleanup should precede community assessment. He also distinguishes a mismatch between a written argument and its formalization from evidence that the mathematical result itself is false.

Research relevance:

Useful for designing research workflows: inspect what files actually establish, compare the written and formal arguments, and require explanations that make specialist review feasible.

Claim status:
Directly read independent commentary with concrete code excerpts. Roberts explicitly says he has not read the highlighted mathematical papers; this is not a correctness audit or an independently checked formalization.
Limitations:
The cited Navier-Stokes translation preprint was originally submitted October 6 and is older material discussed in a new essay. Only its abstract and submission history were consulted here. Empty or untidy supporting files alone do not invalidate a theorem, and no repository code was executed.

Sources & further reading

Link to this entry
Huiberts argues that AI-assisted results require accountable exposition and attribution Sophie Huiberts Published: 2 sources

In an expanded guest essay on Tao's blog, Huiberts argues that whoever presents a theorem must explain its new ideas, identify existing inputs and improve unclear parts of the literature. Applied to AI-assisted research, her proposal places responsibility on the presenting expert or organization rather than transferring the work of making manuscripts intelligible to readers.

Research relevance:

A practical publication standard for researchers using AI: budget for attribution, exposition and review before treating generated manuscripts as finished research outputs.

Claim status:
Directly read opinion and research-practice commentary, not a new theorem or proof audit. The October 12 publication is an expanded version of an earlier personal-blog post.
Limitations:
The original personal post's date was not established. October 12 dates the expanded guest version. Assertions about particular missing artifacts, priority disputes and corporate motives were not independently established here; the essay does not adjudicate the correctness of the release as a whole.

Sources & further reading

Link to this entry
Coverage and limitations
  • Window: October 11, 2026 at 20:00:01 Europe/Paris through October 13, 2026 at 16:17:50 Europe/Paris. Public web search was used; no shell, private connector or source code execution was used.
  • Directly read Terence Tao's blog, David Roberts's October 12 essay, Asaf Karagila's related essays, Kevin Buzzard's Xena blog, Simon Frieder's blog index, Axiom's publications page and OpenAI's repository history. Read the arXiv abstract and submission history for Navier-Stokes lost in translation, but not its full proof.
  • Tao's October 12 link collection led to older material: Buzzard's essay is dated October 1, Karagila's Partition Principle essay October 8, and his Lean essay October 10. These were not treated as new publications. OpenAI's displayed history contained October 7 changes already covered previously.
  • Kevin Buzzard's Imperial webpage corroborates the Xena project and blog association. Scott Armstrong's and Thomas Bloom's research websites were consulted, but exact social-handle ownership was not independently established. The remaining supplied X identities were not independently verified and their posts were not used as authenticated mathematical claims.
  • Supplied X collection status was ok for __alpoge__, scottnarmstrong, thomasfbloom and littmath, with posts provided. Their supplied API text was available for reading; this research did not perform a fresh X timeline read. The posts concerned AI safety or mathematical discourse and supplied no sufficiently substantiated new mathematical result.
  • Supplied X collection status was ok with empty results for wtgowers, sebastienbubeck, alexkontorovich, f_charton, leonard41111588, boazbaraktcs, leanprover, projectnumina, harmonicmath, axiommathai and epochairesearch. Each X feed excluded replies and reposts, used bounded collection and could include cached posts. Numeric pagination caps, completion and budget information were not supplied; empty results do not establish inactivity.
  • The supplied mathstodon.xyz collection was unavailable after an HTTPError, with at most 300 posts checked and replies and reposts excluded. The actor value does not identify a successfully resolved Tao account. The xenaproject.bsky.social collection was ok but empty, with the same 300-post cap and exclusions; ownership of that exact Bluesky handle was not independently verified.
  • Search-index snippets from aggregators and secondary reports were used only as leads. Their theorem claims were not adopted. Research did not exhaustively inspect all listed authors' official sites, project repositories or social timelines, and no proof or Lean build was verified.

Requested coverage window: 2026-10-11T20:00:01.529738+02:00 — 2026-10-13T16:17:50.056906+02:00.

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

Archives 55
Older editions (25)