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 · 5 linked sources Partial coverage
Lean 4.35 adds project checking and comparison against separately specified theorem statements Lean development team Published: 1 source

The release introduces lake check to build, export and replay project proofs while restricting axioms. lake comparator compares named solution theorems with statements in a supplied challenge module. The --paranoid option requests bundled external checkers alongside Lean's kernel. The release also introduces vcgen, a faster and more general successor to mvcgen.

Research relevance:

These tools simplify assessment of AI-generated formalizations against separately specified targets and make additional kernel checking easier to reproduce.

Claim status:
Available tool release described in directly read official documentation. The supplied October 13 social announcement follows the October 12 release date. No commands were executed here.
Limitations:
Statement comparison does not establish that a challenge captures the intended informal mathematics. External checkers must be requested. The documented build sandbox is currently available only on Linux.

Sources & further reading

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

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

Research relevance:

A substantial autoformalization example with public code and mathematical dependency documents for examining how a manuscript is represented formally.

Claim status:
Public artifacts and author-reported checking, directly consulted on an institutional project page and linked repository. This formalizes an existing theorem. Independent community verification was not established.
Limitations:
The original publication date is unknown; October 12 is the reported completion date. Cleanup continues. The repository identifies its input as an editorial working manuscript and companion references as ChatGPT-prepared notes, qualifying the project's source-manuscript-only description. Neither kernel acceptance nor mathematical fidelity 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 written and formal arguments from evidence that a theorem is false.

Research relevance:

Practical research guidance: 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. This is an assessment of presentation and artifacts, 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. Empty or untidy supporting files alone do not invalidate a theorem. 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. She assigns this responsibility to the presenting researcher or organization, including when AI generates the argument.

Research relevance:

A practical publication standard: include attribution, explanatory writing and specialist review in the work required to produce AI-assisted mathematical research.

Claim status:
Directly read opinion and research-practice commentary, not a theorem or proof audit. October 12 dates the expanded guest publication.
Limitations:
The earlier personal version could not be consulted in this refresh, and its original date remains unknown. Allegations about missing artifacts, priority and organizational motives were not independently adjudicated. The essay does not establish the correctness or incorrectness of the mathematical release.

Sources & further reading

Link to this entry
Coverage and limitations
  • Window: October 11, 2026 at 20:00:01 through October 13, 2026 at 20:25:48 Europe/Paris. Public web search and page reading were used. No shell, editing tool, private connector, code execution or Lean verification was used.
  • Directly consulted Lean's official release notes and website, Wesley Pegden's Carnegie Mellon pages and Goldberg–Seymour repository documentation, David Roberts's essay, Sophie Huiberts's guest essay, Tao's blog, the Xena blog, Buzzard's Imperial profile, Armstrong's and Bloom's research websites, Frieder's blog index, Axiom's homepage and OpenAI's repository history.
  • Huiberts's guest article initially returned errors but became accessible through Tao's blog link and was read. Her personal-blog version remained unavailable. Frieder's opened index carried a last-month crawl indication, limiting freshness.
  • Lean's official notes date the release to October 12; the supplied X announcement is October 13. A search-indexed GitHub release listing still showed release candidates, illustrating incomplete indexing. Trellis reports completion on October 12, but its original public publication date remains unknown. Crawl and indexing dates were not treated as publication dates.
  • Princeton's October 13 article was read, but it identifies its Grothendieck-constant case study as an August 14 publication. This older material newly publicized was excluded. OpenAI's displayed history contained October 7 changes already covered. Aggregator snippets about other large formalizations were leads only and did not establish new results.
  • Official websites corroborated Armstrong's X/Twitter association, Buzzard's Xena association and Pegden's Trellis project. Bloom's website was consulted without establishing his exact supplied handle. The other supplied social handles were not independently authenticated; included mathematical and tool claims rely on primary project sources. Most listed authors did not receive individual official-site checks.
  • Supplied X collection status was ok with posts for __alpoge__, scottnarmstrong, thomasfbloom, littmath and leanprover. Their supplied API text was read, with dates taken from created_at. Cached posts may be included; no fresh X timeline was fetched here. The Lean lead was checked against official documentation. The other posts did not substantiate new mathematical results.
  • Supplied X collection status was 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.
  • The supplied mathstodon.xyz collection was unavailable after an HTTPError, with at most 300 posts checked and replies and reposts excluded; it provides no collected Tao timeline. The xenaproject.bsky.social collection was ok but empty, with the same cap and exclusions. Its exact handle ownership and pagination completeness were not established.
  • Search snippets were distinguished from opened sources. Coverage of papers, repositories and social timelines is incomplete. No proof correctness, correspondence between informal and formal mathematics, or independent formalization build was verified.

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

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

Archives 55
Older editions (25)