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

Two substantive publications were established for September 16, 2026: an AI-assisted preprint on matroid secretary algorithms and a practical essay on turning AI-generated proofs into mathematical understanding. Archival coverage of the supplied social accounts remains incomplete.

Research updatesSelect an entry to read more

AI-assisted preprint claims optimal secretary guarantees for linear matroids and a tight single-sample prophet inequality Hamed Abdi, Kiarash Banihashem, MohammadTaghi Hajiaghayi and Danny Mittal Published: 3 sources

The authors give a 1/e-competitive ordinal secretary algorithm for every linear matroid, using constraints on expected intersection dimensions and finite linear programs. They also claim a tight 1/2 single-sample prophet guarantee for arbitrary matroids and a reduction yielding a 1/64 secretary guarantee. Their acknowledgments describe GPT Sol 5.6 and especially GPT Astra interactions as essential to the results, and say generated proofs were subsequently formalized in Lean and checked by the authors.

Research relevance:

A concrete example of AI-assisted research in combinatorial optimization, with a public mathematical manuscript and explicit attribution of model involvement in both discovery and formalization.

Claim status:
Available preprint with mathematical proofs; Lean checking is reported by the authors. A later September 17 manuscript by Bérczi, Dughmi, Livanos, Soto and Verdugo reports concurrent discovery of the linear-matroid result through ChatGPT-6 Astra and an essentially identical approach. That later disclosure was not available on the target day.
Limitations:
The 1/e theorem concerns linear matroids, not all matroids. The later concurrent paper does not independently certify every result in this preprint. No proof was verified or Lean executed for this digest, and no independent formal replay was established.

Sources & further reading

Link to this entry
Bumpus describes using AI proofs as starting points for deeper research and learning Benjamin Merlin Bumpus Published: 1 source

Bumpus describes receiving a quick ChatGPT proof of a lemma, then spending most of a day finding an explanation that made the result transparent. He proposes consulting an LLM after conventional literature review and treating its output as material to understand and improve. For learning and teaching, he describes asking AI to expose gaps through increasingly difficult questions and adversarial lecture preparation, including exercises around space-complexity theorems.

Research relevance:

Offers concrete research habits for using generated arguments while continuing to develop conceptual explanations and mathematical judgment.

Claim status:
Dated first-person workflow report and opinion essay; no new theorem or formalization is released.
Limitations:
The lemma and interaction transcript are not supplied, and the educational benefits are anecdotal. An unnamed colleague's purported conjecture resolution is mentioned without enough evidence to report it as a mathematical result. Later comments are outside the target edition.

Sources & further reading

Link to this entry
Coverage and limitations
  • Public web search was used to reconstruct September 16, 2026, the Paris civil day. The included preprint was submitted at 17:43:06 UTC, within the requested window; the essay explicitly displays September 16. Search-index and crawl dates were not treated as publication dates.
  • Read the original arXiv abstract and HTML manuscript of On the Strong Matroid Secretary Conjecture and Beyond, Benjamin Merlin Bumpus's dated essay, Tao's September archive, the Xena homepage, and Axiom's blog index. Also consulted official websites for Lean, Epoch AI, Harmonic, Daniel Litt, Thomas Bloom, Boaz Barak, Leonardo de Moura and François Charton.
  • Identity checking was incomplete. Boaz Barak's official website links directly to @boazbaraktcs; Kevin Buzzard's Imperial webpage establishes https://xenaproject.wordpress.com/ as his Xena blog. Other supplied handles were not all independently authenticated through official outbound links. Indexed X profiles and third-party mirrors were treated only as leads.
  • No exhaustive X archive was available. Barak's linked Twitter page returned 403; the Liouville–Goldbach announcement could not be fetched. Bubeck's website returned 502; attempted Armstrong and Kontorovich pages were inaccessible; Alpöge's Harvard page and Project Numina's homepage yielded no readable text. Tao's Mathstodon and Buzzard's Bluesky histories were not consulted.
  • Read the current Four Color Theorem and Liouville–Goldbach GitHub repositories, but their commit-history pages could not be fetched. Later registries attribute releases to September 16; an original dated announcement or historical release record was not established, so both leads were excluded.
  • Stellar Colosseum appeared in a September 16 news archive, but its original arXiv submission was September 14, so it was excluded. The indexed Zenodo record titled Lean verification 16sept26 was published September 17 and was excluded. Previously supplied fluid-equation announcements and September 15 essays were not repeated.
  • The September 17 concurrent matroid paper was read only as explicitly later context. This digest does not certify proofs, report executed Lean checks, or infer that inaccessible sources contained no news.

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