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 20, 2026Ecosystem

   AI writes along — responsibility stays human

   A new preprint estimates that 89% of English-language biomedical papers published in December 2025 in the open PubMed Central corpus show excess LLM-associated vocabulary. That is a population-level estimate of signs of writing or editing assistance, not proof that 89% of all research papers were written by AI. Nature reported the result while Nature Computational Science set out the necessary response: disclose material AI use, keep scholarly judgement and accountability human, and never treat generated data or citations as fact.

   SourcesarXiv:2608.10715NatureNature Computational Science

2. August 18, 2026Ecosystem

   A research diary makes the collaboration inspectable

   Haruhisa Enomoto accompanies a new representation-theory preprint with an essay about the work behind it. The preprint proposes an equidistribution conjecture for quotient-closed and submodule-closed subcategories, proves several cases and links a full Lean 4 formalization. Its record also names Fable 5 and GPT-5.6 Sol as collaborators. The essay documents the work unusually well. The conjecture and the individual contributions still need independent review.

   SourcesHaruhisa Enomoto — research essayarXiv:2608.18024

3. 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

4. July 23, 2026Benchmarks

   42 out of 42 — the Olympiad stops being a measurement

   At the 2026 IMO in Shanghai several frontier systems were officially graded a perfect 42/42, among them RedNote's dots-note 3.0 and Huawei's Celia, with models from OpenAI, Anthropic, Axiom Math and Moonshot AI reported at the same score. Seven of 666 human contestants managed full marks. Two years after a silver medal and one after gold, the contest has saturated.

   SourcesFrance 24South China Morning Post

5. July 2026Ecosystem

   Amazon makes the largest donation in the Lean FRO's history

   The Automated Reasoning group's grant is the biggest the Focused Research Organization behind Lean has received. In the same month Microsoft Research described using Lean, through the Aeneas toolchain, to verify the cryptography that ships in SymCrypt — the proof assistant mathematicians adopted is now load-bearing in production software.

   SourcesLean FRO

6. 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

7. June 14, 2026Formalization

   Fermat's Last Theorem: the blueprint keeps filling in

   Kevin Buzzard and Richard Taylor's blueprint for the Lean formalization was updated again. The project is not formalizing the 1995 argument but a twenty-first-century proof routed through Khare–Wintenberger and Kisin, and is funded by the EPSRC until September 2029 — a reminder that at this scale formalization is measured in years, not prompts.

   SourcesFLT repositoryBlueprint (PDF)

8. June 2, 2026Ecosystem

   Mathematicians set rules for AI in research

   The Leiden Declaration asks researchers, institutions, governments and industry to protect proof, attribution, transparency and independent verification as AI enters mathematics. It does not call for a ban: it asks people to disclose tool use, remain responsible for correctness and preserve open, humanly inspectable mathematics. The International Mathematical Union endorsed the declaration, and a Nature editorial endorsed both its process and conclusions.

   SourcesLeiden DeclarationNature

9. 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

10. 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

11. May 2026Ecosystem

    Mathlib takes the 2026 Demailly Prize for Open Science

    The citation calls the library "an exceptional contribution to the mathematical community" with "exceptionally broad structural significance" — infrastructure, not just a resource. The award was presented at the SMAI conference in early June. Mathlib now runs past 1.5 million lines.

    SourcesEPIGA — Demailly PrizeUniversité Paris-Saclay

12. April 27, 2026Formalization

    Sphere packing is formal in dimensions 8 and 24

    The Lean project Sidharth Hariharan and Maryna Viazovska started in March 2024 reached a sorry-free main theorem in February 2026, with the last stages closed by Math, Inc.'s autoformalization model Gauss — five days for dimension 8, and dimension 24's two hundred thousand-odd lines in about two weeks. A Fields-Medal proof from 2016 is now machine-checked end to end.

    SourcesEPFLIEEE SpectrumSphere-Packing-Lean

13. April 13, 2026Ecosystem

    Quanta maps the AI revolution in mathematics

    Quanta follows the shift from competition results to day-to-day research: systems search large spaces, suggest proof strategies, fill in details and translate arguments into formal languages. The examples also expose the unresolved part — credit, understanding, education and the difference between a checked formal proof and a plausible answer. It is a broad report on a changing practice, not evidence that every field or every model has crossed the same threshold.

    SourcesQuanta Magazine

14. November 10, 2025Formalization

    Quanta: turn proofs into checkable puzzles

    John Pavlus profiles Marijn Heule's work on SAT-based proof search: translate a statement into a tightly constrained logical problem, let a solver search, then check the resulting proof. It is a valuable counterpoint to fluent model output: a proof can be far too long to read line by line and still be mechanically checkable. The piece is an expert interview, not a benchmark of LLM capability.

    SourcesQuanta Magazine

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

1. An equidistribution conjecture for quotient-closed and submodule-closed subcategoriesHaruhisa EnomotoA fresh representation-theory preprint with several proved cases, a linked full Lean 4 formalization and an unusually explicit account of the human and AI collaboration. It remains a preprint, not peer review or a proof of the full conjecture.arXiv:2608.18024August 18, 2026
2. From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research FrontierEric Jiang, Xiao Liang, Yikai Zhang, Yingjia Wan, Mengting Li, Haikang Deng, Alexander K. Taylor, Justin Baker, Rushil Raghavan, Junyi Zhang, Ying Nian Wu, Andrea L. Bertozzi, Kai-Wei Chang, Raghu Meka, Matthew Sottile, Nanyun Peng, Amit Sahai, Terence Tao, Wei WangA UCLA-led account of what changes when language models stop solving exercises and start working where the answer is not known.arXiv:2607.07779July 10, 2026
3. First Proof Second BatchMohammed Abouzaid, Nikhil Srivastava, Rachel Ward, Lauren WilliamsTen research-level problems, methods, model attempts, human solutions, referee reports and logs in one public record. It is a high-quality capability evaluation, but only for its selected tasks and systems.arXiv:2606.18119June 16, 2026
4. LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean AutoformalizationYuanhe Zhang, Yuekai Sun, Taiji Suzuki, Jason D. Lee, Fanghui LiuShort proofs are solved. The open question is whether a system can hold a formalization together over days. This benchmark measures that.arXiv:2606.05400June 4, 2026
5. 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
6. Progress in Formalizing Sphere Packing in Dimension 8Sidharth Hariharan, Christopher Birkbeck, Seewoo Lee, Ho Kiu Gareth Ma, Bhavik Mehta, Auguste Poiroux, Maryna ViazovskaThe project report behind the formalization: modular forms, the Cohn–Elkies conditions, and where an autoformalization model took over.arXiv:2604.23468April 29, 2026
7. 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
8. Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative FormalizationBanri Yanahama, Akiyoshi SannaiNames the failure the kernel cannot catch: a proof that type-checks while the statement says something other than what was meant.arXiv:2604.16347 · AIPV 2026April 23, 2026
9. FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?Nikil Ravi, Kexing Ying, Vasilii Nesterov, Rayan Krishnan, Elif Uskuplu, Bingyu Xia, Janitha Aswedige, Langston NasholdGraduate-level statements, machine-checked answers: a benchmark that a convincing-sounding proof cannot pass.arXiv:2603.26996March 31, 2026
10. 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
11. Olympiad-level formal mathematical reasoning with reinforcement learningThomas Hubert, Rishi Mehta, Laurent Sartran et al.The AlphaProof paper shows why formal grounding matters: Lean checks the resulting proof term step by step. Its silver-medal-equivalent 2024 IMO result required multi-day computation and does not establish autonomous research-level mathematics in general.Nature 651, 607–613 (2026)November 12, 2025
12. Mathematical exploration and discovery at scaleBogdan Georgiev, Javier Gómez-Serrano, Terence Tao, Adam Zsolt WagnerA detailed account of LLM-guided evolutionary search on 67 problems, useful because it keeps proposals, automated evaluation and mathematical interpretation distinct. The authors' preprint still requires independent checking of each claimed result.arXiv:2511.02864November 3, 2025