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 · 10 linked sources Partial coverage

Five substantive entries for September 25, 2026: an AI-assisted graph-pebbling proof, a registered ring-theoretic counterexample, reusable Lean analysis infrastructure, and two contributions on mathematical research and training. Formal verification claims are attributed to their sources; no proofs were independently verified and no Lean code was executed.

Research updatesSelect an entry to read more

AI-assisted preprint claims the tree-stacking formula, with a reported complete Lean formalization John Fairfax-Ball Published: 3 sources

The preprint claims that the stacking number of every finite tree with at least two vertices equals the distance-and-degree estimator conjectured by Csernák and Soukup. Its proof combines recursive stackability messages, an explicit obstruction and weighted cancellation. The author discloses extensive AI assistance in mathematical exploration, Lean development and exposition. arXiv records the original submission at 13:34:53 UTC, within the Paris target day.

Research relevance:

A concrete combinatorial research claim with an available mathematical proof and reusable formal source, illustrating how structural arguments can replace bounded computational exploration.

Claim status:
An available preprint claims a proof. Its reproducibility section reports complete Lean formalization, standard axioms only, Palomar statement comparison and independent NanoDa kernel replay. These are source-reported checks, not checks performed for this digest.
Limitations:
The theorem concerns finite trees with at least two vertices; the singleton has a different threshold convention. Mechanical verification is distinct from human peer review, and no independent expert assessment was established.

Sources & further reading

Link to this entry
Palomar registers a claimed AI-generated counterexample to left-right symmetry of PCI rings Vlad Tsyrklevich Published: 2 sources

A registry record published at 06:45:47 UTC describes a countable domain that is left PCI and left V, but neither right Ore, right PCI nor right V. The submission claims negative answers to longstanding symmetry questions associated with Faith, Cozzens and Damiano. Its public repository supplies a paper and Lean development, explicitly disclosing that Claude wrote the material under human direction.

Research relevance:

A potentially significant counterexample in noncommutative ring theory, accompanied by formal statements and code that specialists can scrutinize.

Claim status:
Palomar lists the pinned artifact as registered. The repository claims a formal proof and says no human checked the mathematics beyond the challenge statements. Registration does not establish expert acceptance.
Limitations:
The compared statements cover the principal counterexample and two symmetry consequences; additional paper claims such as simplicity and left Noetherianity are not among those comparisons. September 25 is the registration date, not an established date of initial discovery. The digest did not rebuild or audit the artifact.

Sources & further reading

Link to this entry
Locally convex space infrastructure receives a dated Lean registry record Bastiaan J. Braams Published: 2 sources

Palomar records lean-LCS at 07:12:06 UTC. The entry compares 52 statements spanning locally convex spaces, duality, completeness, and closed graph and open mapping theorems, including results associated with Pták and De Wilde.

Research relevance:

Reusable formal analysis infrastructure could reduce the prerequisite work required for future research formalization and autoformalization projects.

Claim status:
A dated registration of classical mathematics, with the registry reporting proofs without sorry or additional axioms. This is formalization news rather than a new mathematical theorem.
Limitations:
The registration date does not establish when the library was first developed. AI involvement was not established from the consulted material. No Lean build or theorem-to-definition audit was performed.

Sources & further reading

Link to this entry
PhD education summit releases practical recommendations for AI use in mathematical research Bryna Kra and Rachel Ward, presenting the summit recommendations Published: 2 sources

A dated guest post releases the first draft of recommendations from the September 17–18 Harvard summit. The report advocates advisor-student discussions about particular AI uses, literacy in reading formal mathematical statements, and experimentation that supports understanding. It recommends regular assessments by multiple faculty instead of relying primarily on dissertation text.

Research relevance:

Practical guidance for research supervisors and graduate students deciding how to use numerical exploration, self-refereeing, autoformalization and proof generation while developing independent judgment.

Claim status:
An available draft recommendation report, announced September 25; the underlying meeting occurred September 17–18. This is guidance, not evidence of a theorem or measured workflow improvement.
Limitations:
The authors invite revision and feedback. Participants differed over which AI uses help or hinder development, and the report proposes no universal rule for research use.

Sources & further reading

Link to this entry
Larry Guth explains the research values he wants preserved as AI changes mathematics Larry Guth Published: 2 sources

MIT's departmental page dates Guth's essay to September 25. Motivated partly by AI developments, it describes mathematical understanding through connections between perspectives and emphasizes how confusion, failed approaches and admitting mistakes develop judgment. Examples from Fourier analysis connect this account to actual research practice.

Research relevance:

A research mathematician's account of intellectual development that helps frame decisions about which parts of mathematical work to delegate.

Claim status:
An available reflective essay, with its publication date supplied by MIT's official listing. It makes no new theorem or formalization claim.
Limitations:
The PDF itself has no visible publication date. This is a personal account of mathematical practice, not an empirical evaluation of AI tools or a detailed technical workflow.

Sources & further reading

Link to this entry
Coverage and limitations
  • Public web searches reconstructed September 25, 2026 in Europe/Paris. Original arXiv submission history and Palomar publication timestamps establish the dates of the technical entries; blog and MIT departmental dates establish the remaining entries. Search-index dates were not used as publication dates.
  • Read Tao's September archive and dated posts, MIT's AI Mathematics page and Larry Guth's essay, Harvard CMSA's summit report, the tree-stacking preprint, Palomar's machine-readable index, and public GitHub repository descriptions.
  • Consulted official or personal websites for Lean, Epoch AI, Axiom, Harmonic, Thomas Bloom, Daniel Litt, Scott Armstrong, Boaz Barak and Leonardo de Moura, plus Gowers's Weblog. Buzzard's Imperial webpage identifies https://xenaproject.wordpress.com/ as his Xena blog, which was also consulted. These checks did not authenticate every supplied social-media handle.
  • Date-specific indexed X searches covering the supplied individual and organization handles returned no results. No complete X timelines were read. Tao's Mathstodon and Buzzard's Bluesky histories were not consulted. Bubeck, Charton and Kontorovich's official websites were not consulted; an attempted Alpöge webpage returned an error. Coverage of these leads remains incomplete.
  • Project Numina's website returned no readable text. Palomar entry pages required JavaScript; the readable recent.json index supplied registration metadata, while attempted individual JSON records failed. Repository pages were read as public documentation, without executing source code.
  • Excluded ICIAM's original statement, whose official URL is dated September 24, despite Tao's September 25 announcement. Excluded older supplied entries and undated benchmark leads. A later October 5 retrospective led to a claimed September 25 zeta(2) record, but its primary GitHub page failed to open, so that claim was not included. These gaps prevent an exhaustive account of the day.

Requested coverage window: 2026-09-25T00:00:00+02:00 — 2026-09-26T00: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)