AI & Maths watch GitHub

Retrospective research digest

Updates on artificial intelligence for mathematical research, proof discovery and formal verification, with links to papers, code and tools.

At a glance5 entries · 11 linked sources Partial coverage

September 28, 2026: two substantial Lean formalization announcements, an optimization proof workflow, an agent framework applied to algebraic geometry, and a redesigned mathematical exposition initiative. Verification claims remain attributed to their authors.

Research updatesSelect an entry to read more

FrenzyMath announces an AI-assisted Lean formalization of the Poincaré conjecture FrenzyMath Published: 2 sources

FrenzyMath announces a complete Lean 4 formalization following Morgan and Tian's exposition of the Hamilton–Perelman proof. The team reports a full build and Comparator verification against Mathlib-only statements, using an independent kernel and only the standard axioms propext, Classical.choice and Quot.sound. It reports roughly 3.2 million lines of code produced through human–AI collaboration.

Research relevance:

A substantial potential expansion of formal infrastructure for topology, differential geometry and Ricci flow, with a public artifact for examining large-scale AI-assisted formalization.

Claim status:
Original dated announcement with public code and author-reported formal verification. This formalizes an existing theorem; it is not a new solution of the conjecture. Independent mathematical review was not established.
Limitations:
The team acknowledges that code quality remains far from its goal of reusable infrastructure. The current announcement also mentions another group's same-day formalization, whose original release chronology was not independently reconstructed. Current repository documentation contains subsequent restructuring; no build or statement audit was performed here.

Sources & further reading

Link to this entry
Vals AI publishes a claimed Lean proof of the seven-point Thomson problem Hung Tran Published: 2 sources

Tran reports that ten Claude agents produced proofs that the regular pentagonal bipyramid minimizes Coulomb energy among seven distinct points on the unit sphere, uniquely up to isometry and relabeling. The proposed argument combines exact three-point semidefinite certificates, interval rigidity and local minimality. The announcement reports acceptance by Lean and a second kernel implementation.

Research relevance:

A concrete research claim in discrete geometry and energy minimization, accompanied by fixed theorem statements, an informal proof, formal code and verification records.

Claim status:
Original dated announcement and available proof package; kernel acceptance and Comparator checks are reported by the publisher. The repository explicitly states that the statement is not human-certified and the work is not peer reviewed.
Limitations:
The package identifies its underlying snapshot as September 27; September 28 is the announcement date. Formal statement adequacy and mathematical correctness were not independently assessed here. The result concerns exactly seven points and Coulomb energy, not general Thomson problems.

Sources & further reading

Link to this entry
Peppy presents AI-assisted analytic proofs of tight optimization convergence bounds Jaewook J. Suh, TaeHo Yoon, Edward Duc Hien Nguyen, Bicheng Ying and Shiqian Ma Published: 3 sources

The preprint combines performance estimation problems, structured Lyapunov analysis and AI agents to turn numerical certificates into analytic convergence proofs. The authors claim tight bounds for specified Nesterov FGM variants and resolutions of conjectures from earlier optimization literature. They provide proof examples, prompts and evaluation records, with symbolic checks through SymPy.

Research relevance:

A practical domain-specific workflow for optimization researchers seeking exact inequalities and readable proofs from numerical evidence.

Claim status:
Available first-version preprint with analytic arguments and linked code. Conjecture resolutions are author claims; SymPy checks are reported computational validation, not Lean formalization or independent peer review.
Limitations:
Claims apply to the algorithm variants and assumptions stated in the paper. The workflow relies on substantial optimization-specific structure. Proofs, symbolic checks and evaluation runs were not independently reproduced.

Sources & further reading

Link to this entry
Solver Agent links an auditable AI workflow to Calabi–Yau geometry calculations Eliott Morgensztern, Cesar Fierro Cota and Alessandro Mininno Published: 3 sources

Solver Agent records assumptions, derivations and computations in a persistent ledger while coordinating specialized agents and separate checking agents. Its application gives claimed sufficient conditions for elliptically fibered Calabi–Yau fourfolds over projective threefolds with specified terminal cyclic quotient singularities, together with stringy Hodge and Euler corrections and toric examples.

Research relevance:

Relevant to algebraic geometry and mathematical physics, and useful as a public example of organizing lengthy AI-assisted calculations with inspectable research records.

Claim status:
Available preprint, public framework and linked reproducibility sessions. The geometric results and benefits of the workflow are author claims. Separate AI checking agents do not constitute independent mathematical scrutiny or kernel-checked formalization.
Limitations:
The stated cyclic quotient orders are 2, 3, 4 and 6, and the conclusions require the paper's geometric hypotheses. No Lean certification was established. The calculations, session records and software were not executed or independently validated.

Sources & further reading

Link to this entry
Mathathon redesign makes exposition and disclosed research artifacts central Mathathon organizers and a coalition of Caltech mathematicians Published: 1 source

A joint statement replaces the event's open-problem focus with 'Old Problems, New Proofs'. Participants will study difficult arguments, present their understanding, then develop an alternative proof or exposition over two months. Deliverables include an explainer and a repository containing supporting materials such as LLM conversations and visualization code; AI use must be disclosed and justified.

Research relevance:

A concrete model for mathematical digestion and accountable AI-assisted workflows, with explanation and inspectable provenance treated as research outputs.

Claim status:
Dated announcement of an event redesign and its intended deliverables, not evidence of completed mathematical results or demonstrated educational effectiveness.
Limitations:
The November event was still prospective on the target day. Examples in the statement explicitly include claimed proofs; mentioning them does not certify their correctness. This is a new operational announcement, distinct from the previously covered SAIR initiative.

Sources & further reading

Link to this entry
Coverage and limitations
  • Reconstructed the Paris civil day September 28, 2026 using public web searches and original dated sources. The two included arXiv submissions occurred at 17:59:12 and 18:00:00 UTC, within the requested window.
  • Read original announcements from FrenzyMath and Vals AI, their public repository documentation, both included arXiv abstracts and HTML papers, and the Mathathon statement on Terence Tao's blog. Repository pages reflect their current state and may contain later changes.
  • Consulted Tao's September archive and Xena. Confirmed Xena's official address, https://xenaproject.wordpress.com/, through Kevin Buzzard's Imperial webpage. Also consulted official websites for Scott Armstrong, Daniel Litt, Thomas Bloom, Boaz Barak, Lean, Epoch AI, Axiom and Harmonic.
  • Account identity checks were incomplete. Boaz Barak's official website links his Twitter account; other supplied handles were not all independently authenticated. Date-focused searches across the supplied names and handles did not provide comprehensive historical timelines. Direct access to the Lean and Project Numina X pages failed; indexed social snippets were treated only as leads.
  • Project Numina's website returned no readable text; Harmonic exposed limited content requiring JavaScript. Attempts to consult websites for Leonardo de Moura, Levent Alpöge and Sébastien Bubeck failed. Tao's Mathstodon and Buzzard's Bluesky archives were not consulted.
  • Excluded the Mathlib Phrasebook's September 28 build timestamp because it does not establish an original announcement date. Excluded the September 27 essay 'Doing math together in the age of AI', despite a September 28 aggregator timestamp, and older works shared in September 28 reading lists.
  • An AI4Math Chronicle Poincaré lead was visible only as an indexed snippet and failed to open; the item instead relies on FrenzyMath's original announcement. October 1 Thomson reporting was consulted as later commentary, not contemporaneous evidence. No proof was independently verified and no code or Lean was executed.

Requested coverage window: 2026-09-28T00:00:00+02:00 — 2026-09-29T00:00:00+02:00.

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

Archives 32
Older editions (2)