Research worth keeping up with

AI Research Newsletter.

Consequential AI research and releases, with the context that makes them matter.

A curated digest of work from across the field. Prepared with AI assistance and primary-source links; these are summaries of others’ research.

Daily · Up to three updatesSignal over volume

Mathematics

← All updates · 2 updates

AI-assisted proofs reach the optimal secretary guarantee for all linear matroids

Hamed Abdi, Kiarash Banihashem, MohammadTaghi Hajiaghayi, and Danny Mittal posted a proof of the strong matroid secretary conjecture for every linear matroid, establishing the optimal 1/e competitive guarantee for this broad class of online selection problems. The authors say GPT-5.6 Sol and GPT-6 Astra were essential to the construction and that they independently checked the resulting proofs; a second group subsequently posted essentially the same construction, also obtained with Astra.

Why it made the cut: This is a substantive theoretical advance with explicit researcher attribution of AI's role and corroboration from a separate expert group, rather than a model's unsupported claim to solve a problem. Both accounts are preprints, the full strong conjecture for arbitrary matroids remains outside the proved linear-matroid result, and the coincident constructions raise unresolved provenance questions without establishing that private conversations were shared.

First paper · Concurrent paper · Official research-group announcement

OpenAI publishes an AI-generated, Lean-formalized proposed solution to Navier–Stokes

OpenAI released a 166-page proof claiming that smooth, forced three-dimensional Navier–Stokes flow can develop unbounded velocity in finite time while retaining bounded kinetic energy—establishing alternatives C and D in the Clay problem statement. The company says an unreleased model more capable than GPT‑6 Astra found the construction through a roughly 10,000-agent effort, and it released the accompanying Lean 4 formalization; the extraordinary result still needs independent mathematical scrutiny and formal recognition.

Why it made the cut: If validated, this resolves a 90-year-old Millennium Prize problem and is direct evidence of a frontier AI system producing—and formally encoding—a major new mathematical result. The complete paper and checkable Lean repository make the claim unusually concrete, even as questions about priority and training-data provenance remain unresolved.

Paper (PDF) · Official announcement · Lean proof repository · Independent coverage (Nature)