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

Four dated October 6 announcements or publications: OpenAI releases a large manuscript collection, two AI-assisted preprints disclose formal proofs, and ScienceBench closes benchmark submissions. Proof correctness was not independently verified in this research.

Research updatesSelect an entry to read more

OpenAI releases 722 mathematical manuscripts with selected Lean artifacts and research-process disclosures OpenAI Published: 2 sources

OpenAI announced a public collection of 722 manuscripts grouped into 372 mathematical families, produced by an unreleased internal model. The repository provides manuscript navigation, supporting Lean materials and ten abridged reasoning summaries. OpenAI reports approximately 4,000 attempted problems and average compute per result equivalent to three hours of ChatGPT Pro thinking. This is a concrete artifact release beyond the September advisory-group announcement previously covered.

Research relevance:

Researchers can inspect manuscripts in their specialties, compare informal arguments with available formal statements, and study disclosed reasoning summaries. The family structure helps distinguish principal claims, consequences and alternative arguments.

Claim status:
Dated release announcement with publicly available manuscripts and selected formalization artifacts. OpenAI explicitly describes differing verification stages and acknowledges possible issues in unformalized results. Consultation with AGMAI does not constitute certification of individual proofs.
Limitations:
The collection was not audited theorem by theorem. Neither Lean builds nor correspondence between formal and intended statements were checked here. The model remains unreleased, and abridged reasoning summaries do not reproduce the full research process. The announcement supplies a calendar date but no precise Paris-window timestamp.

Sources & further reading

Link to this entry
AI-assisted preprint presents a second forest-unimodality proof with explicit formalization and review caveats Wei Li, Kevin Vallier and Tong Zhang Published: 3 sources

The preprint gives a second proof that every finite forest has a unimodal independence sequence, crediting an earlier proof by Zhang and Li. Its new route combines a hard-core-measure moment argument for forests with at least 25 vertices, finite arithmetic certificates and a counting argument for smaller forests. The contribution statement attributes the new mathematics and formal proofs to AI systems directed by Vallier. The accompanying Lean development proves the headline statement but uses a different certificate argument for the small-forest case.

Research relevance:

Useful for combinatorialists studying independence polynomials and for researchers examining how analytic arguments, finite certificates and AI-generated formal proofs fit together. The explicit account of proof provenance and trust assumptions provides an unusually concrete audit target.

Claim status:
Available provisional proof and public Lean package; successful builds and axiom audits are reported by the project. The October 6 contribution account reports no external referee review, no human review of the formalization, and no complete human review of the moment argument.
Limitations:
The final formal theorem reportedly depends on Lean.ofReduceBool and Lean.trustCompiler through 411 native_decide evaluations, extending the trusted base to the compiler. Parts of the written small-forest proof are not formalized because the formal proof takes another route. Builds were not reproduced here. This publication is a new proof presentation, not the first claimed resolution of Erdős Problem 993.

Sources & further reading

Link to this entry
Kasami preprint gives an AI-assisted proof of Carlet's cyclic-additive conjecture Gábor P. Nagy, Douglas S. McNeil and Attila Vajda Published: 3 sources

The authors claim the prescribed triple-count identity for derivative images of Kasami monomials over characteristic-two finite fields, for every admissible pair of parameters. Their argument translates a Fourier correction into twisted root counts, obtains nonnegativity using incidence geometry on the Fermat cubic, and forces equality through an exact average. They disclose sustained use of Claude and ChatGPT in developing the proof, and AI assistance including Aristotle in formalization.

Research relevance:

Relevant to finite-field combinatorics, APN functions and cryptographic constructions. The paper connects character sums and algebraic geometry while offering a case study of human-guided AI research with a reported formal counterpart.

Claim status:
An original dated preprint supplies an informal proof. The authors state that they reviewed the generated material and that the results were checked by the Lean kernel with Mathlib. They cite a Palomar record dated September 4; this digest reports the October 6 paper publication, not a newly completed formalization.
Limitations:
The claim concerns the Kasami family and its admissible parameters, not arbitrary APN functions. No independent proof assessment or Lean execution was performed here. The linked Palomar page exposed only its JavaScript loading shell, so its immutable record and verification restrictions could not be inspected. Earlier partial results and the formalization predate this publication.

Sources & further reading

Link to this entry
ScienceBench closes problem submissions while reconsidering research-mathematics benchmarking ScienceBench Published: 2 sources

ScienceBench's dated announcement says its current method of collecting benchmark problems has reached its limits and that submissions are closing while alternatives are explored. It also announces availability of version 2 of Benchmarks in Leipzig. The underlying paper was originally submitted June 4 and revised October 5; October 6 is the website announcement date.

Research relevance:

A practical change for mathematicians contributing research-level benchmark questions. It also signals that benchmark collection methods need reassessment as models become more capable on fixed problem sets.

Claim status:
Directly readable dated service announcement. The linked arXiv metadata independently establishes the paper's earlier original and revision dates. This is a workflow announcement, not a new theorem or an independent validation of model capability.
Limitations:
The announcement does not specify a replacement submission process or reopening date. Benchmark scores do not establish reliability on new open problems. The service's historical functionality was not tested, and no exact publication time was available.

Sources & further reading

Link to this entry
Coverage and limitations
  • Public web searches reconstructed October 6, 2026, rather than the latest news. Both included arXiv submissions have timestamps within the Paris civil day. OpenAI and ScienceBench display October 6 publication dates without precise publication times.
  • Read OpenAI's announcement and repository README, both mathematical preprints' original-version HTML, the forest-unimodality repository README, ScienceBench's dated announcement, and the Leipzig paper's arXiv metadata. Search aggregators supplied leads only; their indexing dates were not used as publication evidence.
  • Consulted Tao's blog, Antieau's original Hexagon announcement, Xena, Charton's blog, de Moura's blog, Windows On Theory, and official personal or institutional pages for Armstrong, Bloom, Litt, Barak, Kontorovich and Buzzard. Official links confirmed the supplied X handles for Armstrong, Charton, Barak and de Moura. Buzzard's Imperial page confirmed https://xenaproject.wordpress.com/ as the Xena blog.
  • X access was significantly limited: direct requests for Lean and several officially linked personal accounts failed, including explicit 403 responses. Buzzard's Bluesky profile also failed. Searches mentioning the supplied accounts did not provide a complete dated archive. Other supplied personal handles remain unverified against official links; indexed mirrors were not treated as certified identities or historical timelines.
  • Consulted official Lean, Axiom, Harmonic and Epoch AI websites. Project Numina's website returned no readable text. Alpöge's Harvard page returned no readable text; Bubeck's IAS page and Gowers's personal Cambridge page failed. These gaps prevent comprehensive account coverage.
  • Excluded Hexagon: Antieau's original announcement is dated October 5, although Tao cross-posted it October 6. Excluded the 3SUM/APSP preprint because its original submission was October 5. AIProver was first submitted October 4; an indexed October 6 update was insufficient to establish a substantive eligible announcement.
  • Read Bloom's October 6 guest post on changes to the Erdős problems website, but the linked original forum source was inaccessible and its original publication date could not be established. It was therefore excluded under the strict original-date rule.
  • The Kasami paper cites a September formalization record, and the forest paper describes earlier proofs and builds; these are distinguished from the October 6 publications. No supplied previous item was repeated. No source code was executed and no Lean build was run.

Requested coverage window: 2026-10-06T00:00:00+02:00 — 2026-10-07T00:00:00+02:00.

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

Archives 36
Older editions (6)