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

Two substantive September 22 publications were established: Axiom's explanation of an earlier combinatorial result and its reported Lean workflow, and Martin Hairer's clarification of the independent mathematics advisory group's role. Archival social-media coverage remains incomplete.

Research updatesSelect an entry to read more

Axiom explains record-composition enumeration and its reported autonomous Lean proof workflow Evan Chen Published: 3 sources

Chen explains how counting alternating permutations by ordered record compositions refines the earlier Amdeberhan–Shareshian–Stanley enumeration by unordered record partitions. For a composition alpha, the count is a product of binomial coefficients and odd Euler zigzag numbers. The article connects this formula to noncommutative symmetric functions and reports that AxiomProver proved three supplied formulations without an informal proof or further guidance. It highlights the algebraic infrastructure needed to relate those formulations as a substantial part of the formalization.

Research relevance:

A concrete combinatorial example with a public paper and Lean artifacts, useful for studying how theorem formulation and supporting algebra affect automated proof production.

Claim status:
New dated exposition and workflow disclosure concerning an older result. The linked paper by Evan Chen, Michal Mogielnicki and Ken Ono was first submitted on July 14, 2026. Its abstract claims that AxiomProver produced and verified the results in Lean; a public artifact repository is available.
Limitations:
This is not a newly published theorem on September 22. The article says humans supplied the target statements, so autonomous proof generation should not be conflated with autonomous problem selection or discovery. Repository availability does not establish an independent audit of definitions, assumptions or correspondence with the informal theorem. No proof or Lean build was checked here.

Sources & further reading

Link to this entry
Hairer clarifies AGMAI's independence, advisory limits and publication priorities Martin Hairer Published: 3 sources

Following the previous day's advisory-group announcement, Hairer states that its nine members receive no compensation, deliberate without laboratory representatives, and obtain technical support from the Institute for Advanced Study. He describes its purpose as representing mathematical-community interests and improving the publication and dissemination of AI-generated research. Attribution, priority and human understanding are central concerns. He also acknowledges that laboratories may ignore the group's advice and that its members are not a representative sample of the community.

Research relevance:

Clarifies the institutional process surrounding AI-generated mathematical claims and the standards researchers should expect for explanation, attribution and dissemination.

Claim status:
First-person clarification by a group member, published September 22 and cross-posted by Terence Tao. This is a genuine update to the September 21 announcement, not an assessment certifying any mathematical result.
Limitations:
Independence and operating arrangements are reported by Hairer. The group has an advisory role rather than enforcement authority, and Hairer says its recommendations were still being developed. Membership does not establish independent proof scrutiny or formal verification of laboratory claims.

Sources & further reading

Link to this entry
Coverage and limitations
  • Reconstructed the Paris civil day September 22, 2026, using public web searches and original dated pages. Search-index and crawl dates were not treated as publication dates.
  • Read Axiom's September 22 article, its linked GitHub repository overview, and the underlying arXiv abstract and submission history. The mathematical preprint dates from July 14; the included item concerns the newly dated explanation and workflow disclosure.
  • Read Martin Hairer's September 22 article on Proofs and Prompts and its cross-post on Terence Tao's blog. Consulted Tao's September archive and the AGMAI website. Hairer's clarification adds information to the September 21 advisory-group announcement already supplied.
  • Consulted Xena and confirmed its address, https://xenaproject.wordpress.com/, through Kevin Buzzard's Imperial College webpage. Also consulted official or personal pages for Scott Armstrong, Daniel Litt, Boaz Barak, Thomas Bloom, Lean, Epoch AI and Harmonic, and Gowers's blog. These checks did not establish September 22 research announcements from those sources.
  • Official pages for Scott Armstrong and Boaz Barak provide social-account links; other supplied handles were not all independently authenticated. Grouped searches of several supplied X handles yielded no usable, originally dated September 22 posts. Indexed social-media mirrors with relative dates were treated only as leads. No exhaustive X access or historical timeline reconstruction was available; Tao's Mathstodon and Buzzard's Bluesky archives were not directly consulted.
  • Attempts to open pages for Alex Kontorovich, Leonardo de Moura and Sébastien Bubeck returned retrieval errors. Project Numina's homepage returned no readable text. Levent Alpöge's and François Charton's supplied account identities and day-specific activity remain unconfirmed.
  • Read NPR's reporting syndicated by Ideastream, originally published September 22 at 05:01 EDT. Its accessible text includes an update at 18:08 EDT, which falls on September 23 in Paris. Without an earlier snapshot, it was excluded as a separate item to avoid attributing potentially later text to the target day.
  • Excluded September 22 aggregations repeating the September 21 OpenAI announcement, the previously covered Lean Pool paper, and a graduate-education preprint whose original submission was September 19. Registry and search snippets were used for discovery, not as substitutes for dated primary publications. No proof was independently verified and no Lean code was executed.

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