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 separately specified theorem statements Lean development team Published: 1 source

The release adds lake check to build, export and replay project proofs while restricting axioms. lake comparator also 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 the experimental vcgen 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 documented in directly read official release notes. The supplied October 13 social announcement follows the October 12 release date. No commands were executed here.
Limitations:
Statement comparison does not establish that the challenge captures the intended informal mathematics. External checkers must be requested. The documented build sandbox is currently available only on Linux; 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 established2 sources

Pegden's project page reports an autonomous run ending October 12 that formalizes the Goldberg–Seymour chromatic-index bound for finite loopless multigraphs, following Chen, Jing and Zang. It 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 accompanying mathematical dependency documents for investigating correspondence between a manuscript and its formal representation.

Claim status:
Public artifacts and author-reported checking, directly consulted on an institutional project page and linked repository. This formalizes an existing theorem; it is not a new solution of an open conjecture. Independent community verification was not established.
Limitations:
The publication date is unknown; October 12 is the reported run-completion date. Cleanup remains ongoing. The repository identifies the input as an editorial working manuscript and companion references as ChatGPT-prepared notes, qualifying the project's broad source-manuscript-only description. Neither kernel acceptance nor fidelity to the original mathematics 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. Roberts says he has not read the highlighted mathematical papers; this is not a correctness audit.
Limitations:
The translation-scrutiny preprint discussed in the essay is older material, and 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: 2 sources

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. This responsibility belongs 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's original date was not established. Allegations about missing artifacts, priority and organizational motives were not independently adjudicated. This 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:20:11 Europe/Paris. Public web search and source reading were used. No shell, editing tool, private connector, source code execution or Lean verification was used.
  • Directly read Lean's official release notes and website, Wesley Pegden's Carnegie Mellon project page and Goldberg–Seymour repository documentation, David Roberts's essay, Sophie Huiberts's guest essay and personal-blog version, Tao's blog index, the Xena blog, Buzzard's Imperial profile, Armstrong's research website, Frieder's blog index and OpenAI's repository history. Today's earlier items were rechecked and retained with their qualifications.
  • Lean's release notes date version 4.35.0 to October 12; its supplied X announcement is dated October 13. Trellis reports run completion on October 12, but its original public announcement date remains unknown. Indexing and crawl dates were not treated as publication dates.
  • Princeton's October 13 article was directly consulted, but it identifies its Grothendieck-constant case study as an August 14 publication. This older material newly publicized was excluded. Search snippets concerning geometrization formalization were leads only; no substantive in-window update was established. OpenAI's displayed history still described October 7 changes already covered previously.
  • Armstrong's official website links to X/Twitter. Buzzard's institutional profile corroborates his formalization work, and the Xena blog was consulted, but the exact supplied Bluesky handle was not independently verified. Other supplied social handles were not independently authenticated against official websites. Mathematical and tool claims included here rely on primary project sources rather than presumed account identities.
  • Supplied X collection status was ok with posts for __alpoge__, scottnarmstrong, thomasfbloom, littmath and leanprover. Their supplied API text was read, with post dates taken from created_at. Cached posts may be included; this research did not fetch fresh X timelines. The Lean announcement 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. All X feeds exclude replies and reposts and use bounded collection. Numeric pagination caps, pagination completion, collection budget limits and skipped-account information were not supplied. Empty results do not establish inactivity.
  • The supplied mathstodon.xyz feed was unavailable after an HTTPError; replies and reposts were excluded and at most 300 posts were checked. It supplies 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 for either feed.
  • Frieder's opened blog index showed older entries and carried a last-month crawl indication, limiting freshness. Not every listed author's official website, repository or timeline was exhaustively inspected. Search snippets were distinguished from opened sources. No proof, semantic correspondence or independent formalization build was verified.

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

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

Archives 55
Older editions (25)