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

4 entries · 6 linked sources Partial coverage
Lean 4.35 integrates project checking and comparison against trusted theorem statements Lean development team Published: 1 source

The release adds lake check to build, export and replay a project's proofs while restricting axioms. lake comparator additionally compares named solution theorems with a supplied challenge module. The --paranoid option invokes bundled external checkers as well as Lean's kernel. The release also introduces the experimental vcgen successor to mvcgen.

Research relevance:

These tools make it easier to assess AI-generated formalizations against a separately specified target and to repeat kernel checks without assembling several independent tools.

Claim status:
Available tool release described in directly read official documentation. The supplied October 13 social announcement points to release notes dated October 12. No commands were executed here.
Limitations:
Comparing formal statements does not establish that the challenge expresses the intended informal mathematics. Independent checkers must be requested. The documented build sandbox is currently available only on Linux, and vcgen remains experimental.

Sources & further reading

Link to this entry
Trellis reports completing a Goldberg–Seymour Lean formalization Wesley Pegden / Trellis project Published: date not established3 sources

Pegden's project page reports an autonomous run ending October 12 that formalizes the Goldberg–Seymour bound for finite loopless multigraphs, following Chen, Jing and Zang. Public artifacts include the root theorem, dependency documents and roughly 197,000 lines of Lean. The repository reports a separate isolated build and a root-axiom check restricted to Lean's three standard axioms.

Research relevance:

A substantial example of long mathematical autoformalization, with code and documentation intended to expose correspondence between manuscript arguments and formal proof dependencies.

Claim status:
Public formalization artifacts and author-reported checking, directly read on an institutional project page and its linked repository. This formalizes an existing theorem; it is not a new solution of an open conjecture. Independent community scrutiny was not established.
Limitations:
The original publication date is unknown; October 12 is the reported run-completion date. Cleanup remains in progress. The repository identifies its input manuscript as an editorial working version and companion references as ChatGPT-prepared notes, qualifying the project's broad description of using source manuscripts alone. Kernel acceptance and faithful representation of the original proof are separate questions; neither was checked here.

Sources & further reading

Link to this entry
Roberts identifies cleanup and correspondence checks for AI-generated proof artifacts David Roberts Published: 1 source

Roberts examines what makes generated mathematics useful beyond a theorem claim. He illustrates empty Lean namespaces and repetitive setup code in OpenAI's release, argues for readable exposition and artifact cleanup, and distinguishes disagreement between a written proof and its formalization from evidence that the theorem is false.

Research relevance:

Useful guidance for research workflows: inspect what supporting files establish, compare formal and written arguments, and prepare artifacts that specialists can meaningfully review.

Claim status:
Directly read independent commentary with concrete code excerpts. Roberts says he has not read the highlighted mathematical papers; the essay is not a correctness audit.
Limitations:
The translation-scrutiny preprint discussed in the essay is older material. Its full argument was not consulted in this refresh. Untidy or empty supporting files alone do not invalidate a theorem, and no code was executed.

Sources & further reading

Link to this entry
Huiberts argues for accountable exposition and attribution in AI-assisted research Sophie Huiberts Published: 1 source

In an expanded guest essay on Tao's blog, Huiberts argues that presenting a theorem entails explaining its new ideas, identifying established inputs and improving unclear exposition in the literature. Her proposal places this responsibility on the presenting researcher or organization, including when AI generates the argument.

Research relevance:

A practical publication standard: plan attribution, explanatory writing and review as part of AI-assisted mathematical research.

Claim status:
Directly read opinion and research-practice commentary, not a theorem or proof audit. The October 12 publication is an expanded version of an earlier personal-blog post.
Limitations:
October 12 dates the expanded guest version; the earlier version's original date was not established. Allegations about missing artifacts, priority and organizational motives were not independently adjudicated.

Sources & further reading

Link to this entry
Coverage and limitations
  • Window: October 11, 2026 at 20:00:01 through October 13, 2026 at 20:16:48 Europe/Paris. Public web search and page reading were used. No shell, private connector, code execution or Lean verification was performed.
  • Directly consulted Lean's official release notes and website; Wesley Pegden's Carnegie Mellon pages and linked Trellis repositories; Terence Tao's blog; David Roberts's essay; Kevin Buzzard's Xena blog and Imperial profile; Simon Frieder's blog index; Scott Armstrong's and Thomas Bloom's official websites; and OpenAI's public repository history. This was not an exhaustive survey of papers or repositories.
  • Lean's release notes date version 4.35.0 to October 12; the supplied X announcement is dated October 13. Trellis dates completion of its Goldberg–Seymour run to October 12, but the original public announcement date was not established. Search crawl dates were not treated as publication dates.
  • Princeton's October 13 article was directly read, but its Grothendieck-constant case study is identified there as an August 14 publication. It was excluded as older material newly publicized, rather than presented as a new mathematical result. Promotional and unsupported aggregator claims were excluded.
  • Scott Armstrong's official website links to X/Twitter, corroborating his social association. Buzzard's Imperial profile and Xena blog corroborate the project association, but ownership of the exact supplied Bluesky handle was not independently established. Thomas Bloom's official website was read without establishing the supplied X handle. The remaining supplied personal and organizational handles were not independently authenticated; substantive items rely on official pages and repositories.
  • Supplied X feeds had status ok with posts for __alpoge__, scottnarmstrong, thomasfbloom, littmath and leanprover. Their supplied post text was available, with dates taken from created_at. Cached posts may be included; no fresh X timeline was fetched here. The Lean post was followed to official documentation. Other supplied posts concerned safety or mathematical discourse and were not used to certify mathematical results.
  • Supplied X feeds had status ok with empty results for wtgowers, sebastienbubeck, alexkontorovich, f_charton, leonard41111588, boazbaraktcs, projectnumina, harmonicmath, axiommathai and epochairesearch. Every X feed excludes replies and reposts and uses bounded collection. Numeric pagination caps, pagination completion, budget limits and skipped-account information were not supplied. Empty results do not establish inactivity; these accounts did not receive exhaustive independent timeline or website checks.
  • The supplied mathstodon.xyz feed was unavailable after an HTTPError, with replies and reposts excluded and at most 300 posts checked. It provides no successfully collected Tao timeline. The xenaproject.bsky.social feed was ok but empty, with the same exclusions and 300-post cap; pagination completeness was not established.
  • Search snippets were used as leads and distinguished from opened sources. Previously covered October 6–11 announcements were not repeated without a substantiated update. Both items from today's earlier edition were re-read and retained. No proof correctness, semantic correspondence or independent Lean build was verified by this digest.

Requested coverage window: 2026-10-11T20:00:01.529738+02:00 — 2026-10-13T20:16:48.282951+02:00.

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

Archives 55
Older editions (25)