News from the edge of what is proved

Newest first. Every entry links the primary source first — the wiki, the blueprint, the abstract — and the reporting second.

1. August 3, 2026Erdős problems

   Quanta asks why the Erdős problems are falling

   A long piece on the acceleration that began in late 2025 — literature-search models first, then formalization systems, then autonomous provers — and on the argument it started inside the community about credit, verification, and what a proof is for.

   SourcesQuanta MagazinePhysics World

2. June 30, 2026Erdős problems

   The Erdős register grades how much the machine actually did

   Terence Tao's community wiki sorts every AI contribution into four classes of primary work — standalone, alongside the literature, building on it, in collaboration with humans — plus secondary roles like literature search and formalization, and colour-codes outcomes down to "incorrect" and "unverified". Eleven disclaimers accompany the table. It is the closest thing the field has to an audited ledger.

   Sourceserdosproblems wikierdosproblems.com

3. May 26, 2026Erdős problems

   Erdős #90 falls twice in six days

   An internal OpenAI model produced a standalone solution to the planar unit-distance problem on 20 May. Claude Mythos produced another, independently, on 26 May. The register records both as primary contributions with no human argument in the loop. The construction reportedly leans on algebraic number theory to beat the square grid — a question open since 1946.

   Sourceserdosproblems wikiNature

4. May 3, 2026Erdős problems

   A method the literature missed for ninety years

   Tao, Jared Duker Lichtman and six co-authors resolved Erdős Problem #1196 on primitive sets. The idea that carried it — bounding Erdős sums via Markov chains with von Mangoldt weights — was suggested by output from GPT-5.4 Pro and, the authors note, appears to have been overlooked since Erdős's seminal 1935 paper. This is the collaboration mode that is hardest to dismiss: the machine supplied a direction, the people supplied the proof.

   SourcesWhat's new (Tao)arXiv:2605.00301

The papers behind the headlines. Titles and author lists are reproduced as published; the line underneath says why it is on this list.

1. Primitive sets and von Mangoldt chains: Erdős Problem #1196 and beyondTerence Tao, Jared Duker Lichtman, Boris Alexeev, Kevin Barreto, Yanyang Li, Liam Price, Jibran Iqbal Shah, Quanyu TangThe resolution of #1196, written up with an explicit account of which step came from a model and which from the authors.arXiv:2605.00301May 3, 2026
2. QED: An Open-Source Multi-Agent System for Generating Mathematical Proofs on Open ProblemsChenyang An, Qihao Ye, Minghao Pan, Jiayuan ZhangAn open-source counterweight to the closed systems that produced this year's headlines — the pipeline is inspectable.arXiv:2604.24021April 24, 2026
3. Resolution of Erdős Problem #728: a writeup of Aristotle's Lean proofNat SothanaphanA human reading of a machine's Lean proof — the genre this year invented, and the one that decides whether such proofs enter the literature.arXiv:2601.07421January 13, 2026