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

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

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

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

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