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 glance2 entries · 3 linked sources Partial coverage

Two substantive October 2 announcements were established: Meta's release of six AI-assisted mathematics papers and a correction exposing a circular hypothesis in a Collatz Lean development. Archival and social-media coverage remains incomplete.

Research updatesSelect an entry to read more

Meta releases six AI-assisted mathematics papers with disclosed human review and concurrent work Meta AI Research and collaborating mathematicians Published: 2 sources

Meta released six papers developed with Muse Spark through its ordinary chat interface. Topics include Gaussian ellipsoid fitting, biharmonic nonlinear Schrödinger blow-up, group-theoretic and evolution-algebra counterexamples, optimization relaxations and arithmetic physics. Meta reports researcher guidance, a second group of mathematical reviewers and marked AI-drafted passages. It explicitly acknowledges earlier independent results for several problems.

Research relevance:

Provides research artifacts and a concrete collaboration workflow. Dinh's dated abstract claims finite-time blow-up in both time directions for radial, negative-energy H² solutions of the focusing mass-critical biharmonic nonlinear Schrödinger equation in dimensions N ≥ 2.

Claim status:
Dated primary announcement and publication abstract inspected. Meta reports mathematical review; this digest does not establish independent proof validation or formalization.
Limitations:
Full PDFs were not read. The PDE claim has radiality, energy and regularity restrictions. Concurrent work limits priority claims; Meta's count of five answered open questions should not imply five exclusive discoveries.

Sources & further reading

Link to this entry
Collatz formalization erratum identifies a hypothesis equivalent to the large-cycle conclusion Eric Merle Published: 1 source

An October 2 erratum corrects the scope of an AI-assisted conditional Lean development. The hypothesis DerivedLargeKBound was assumed rather than derived; under the stated computational hypothesis, it is equivalent to excluding the large cycles that the theorem purported to exclude. The author consequently limits the non-circular result to cycles with at most 1322 odd terms, still under two hypotheses. The April preprint retains the older statement.

Research relevance:

A concrete example of why a formally proved implication can provide little mathematical evidence when its hypotheses already contain the desired conclusion. It illustrates the need to audit theorem statements alongside proof terms.

Claim status:
Author-issued correction explicitly dated October 2 on the primary project website. Lean checking is reported by the author, not performed for this digest. The project does not claim to prove the Collatz conjecture.
Limitations:
The remaining result assumes BakerSeparation and a computational-verification hypothesis. The site reports that the main theorem was checked under Lean 4.27.0 and has not been rechecked since a subsequently fixed kernel bug; rechecking six shared files does not establish rechecking of that theorem. The current website is mutable.

Sources & further reading

Link to this entry
Coverage and limitations
  • Reconstructed October 2, 2026, using public web search and opened primary pages. Included dates are original announcement or correction dates; exact publication times were unavailable.
  • Read Meta AI Research's October 2 announcement and Leonard Dinh's dated publication page and abstract. The complete paper PDFs were not read, and no proofs or Lean developments were independently verified.
  • Read Collatz Lab's explicitly dated October 2 erratum on its current website. This is a living page, not an archived October 2 snapshot; its preprint dates from April 2026.
  • Consulted official UCLA and Imperial pages to check the Tao and Buzzard website leads, and opened Xena at https://xenaproject.wordpress.com/. Tao's October 2 archive could not be retrieved. Complete Mathstodon and Bluesky histories were not consulted.
  • Opened the Lean, Harmonic, Axiom and Epoch AI websites. The attempted Project Numina website could not be retrieved. These checks did not establish substantive October 2 announcements.
  • Searched the supplied personal and organizational X leads. No complete historical X timelines were available, and official-site confirmation of all supplied handles was not achieved. Indexed social-media mirrors with relative dates were excluded as evidence for this day.
  • MathsAI's dated report about mathematical statement scope was visible only in search results; its page could not be opened and the underlying preprint was not identified, so it was excluded.
  • An indexed Palomar subject page described an October 2 four-body formalization registration, but the direct registry entry could not be opened; it was excluded pending inspection of the original record.
  • Excluded older material with October 2 indexing or update dates, event listings without established publication dates, introductory tutorials and promotional summaries. No earlier supplied digest item was repeated.

Requested coverage window: 2026-10-02T00:00:00+02:00 — 2026-10-03T00: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)