Browse the watch

Open this edition →

Two major releases dominate the window: Axiom published a claimed complete 43.1-million-line Lean formalization of the classification of finite simple groups, and Anthropic released a second, reportedly independent AI-generated subexponential algorithm for 3-SAT with Lean artifacts. A new expert discussion also clarifies that OpenAI’s local-smoothing argument does not supersede the distinct Wang–Zahl Kakeya program. These are public, inspectable artifacts, but I did not execute Lean, verify any proof, or find completed independent mathematical scrutiny of the headline claims.

• Axiom releases a claimed complete Lean formalization of the classification of finite simple groupsAxiom Math; core contributors Dean Cureton, Vasily Ilin, Bhavik Mehta and Niels Voss, with additional mathematical and engineering contributors
• Anthropic publishes a second claimed AI discovery of a subexponential 3-SAT algorithm, with Lean artifactsClaude, Anthropic
• New discussion distinguishes OpenAI’s Kakeya consequences from the Wang–Zahl codimension-two programThomas Bloom, discussing work of Chun-Kit Lai, Yixuan Pang, Rahul Sethi and Chenjian Wang

Open this edition →

Five substantive developments were found in the 2026-10-24 to 2026-10-27 window. The most consequential are OpenAI’s public but not yet independently validated claims of a subexponential exact-counting algorithm refuting ETH and a proof of Euclidean local smoothing with consequences for Kakeya and restriction theory. Two new public Lean repositories formalize major results in stochastic PDE, while AGMAI issued recommendations about equal access to AI-generated research. Public artifacts exist for the mathematical and complexity claims, but correspondence between formal statements and the familiar conjectures still requires human review; the announced quantum-field-theory artifacts remain unavailable.

• OpenAI releases a claimed subexponential exact-counting algorithm that would refute ETHOpenAI
• OpenAI publishes claimed proofs of Euclidean local smoothing and major Kakeya consequencesOpenAI
• A new Lean development formalizes the critical two-dimensional KPZ-process paperScott Armstrong
• AI-assisted Lean library formalizes regularity structures and dynamical Φ⁴₃Scott Armstrong
• AGMAI recommends equal public access rather than lab-designated mathematical interpretersAdvisory Group on Mathematics and Artificial Intelligence

Open this edition →

No new substantive development in AI-assisted mathematical research was verified within the window from 2026-10-23T21:15:01.880495+02:00 to 2026-10-25T09:15:01.380738+01:00. The few collected X posts were either unrelated to mathematical research or linked to older material. Public searches and directly read official pages produced no qualifying new proof, counterexample, formalization, paper, code release, or research tool. Empty feeds are not evidence that no other activity occurred.

Open this edition →

One substantial new item met the editorial threshold: an eleven-author preprint constructs the critical two-dimensional KPZ process and gives an unusually detailed account of major AI contributions to the proof. The paper was submitted shortly before the window, but Scott Armstrong’s in-window post brought it to attention. No qualifying new Lean release or comparably substantial update was confirmed from the other monitored sources.

• Eleven authors present an AI-assisted construction of the critical two-dimensional KPZ processQuentin Berger, Francesco Caravenna, Jeremy Clark, Alexander Dunlap, Yu Gu, Ziyang Liu, Shuta Nakajima, Rongfeng Sun, Li-Cheng Tsai, Zuodi Xie and Nikos Zygouras

Open this edition →

Two substantive releases were rechecked: MathEconLib’s public Lean library and Anthropic–Theorem’s AI-assisted binary verification experiment. The latter’s public repository currently covers 60 entry points in 25 libraries, substantially less than the reported overall experiment. No additional item was established within the exact window.

• MathEconLib releases a broad Lean library for economic and political theoryMathEconLib contributors; support announced by Axiom Math
• Anthropic and Theorem publish Rocq artifacts from AI-assisted binary verificationAnthropic and Theorem

Open this edition →

Two substantive releases were found in the window: an unusually large AI-assisted Rocq verification experiment on compiled software, and the open-source release of a broad Lean library for economic theory. Both provide public artifacts, but neither was independently reproduced during this research.

• Anthropic and Theorem release Rocq artifacts from large-scale AI-assisted binary verificationKeane Lucas, Aengus Lynch, Luna Tong, Luke Champine, Zygi Straznickas, Dino Distefano, Harshikaa Agrawal, Evyatar Ben Asher, Ava Howell, Sami Jawhar, Chris Rohlf, Nickolai Zeldovich, Nicholas Carlini, Rajashree Agrawal, Jason Gross, and Theorem
• MathEconLib opens a broad Lean library for economic and political theoryMathEconLib contributors, with support announced by Axiom Math

Open this edition →

One substantive item appeared in the 2026-10-20 20:00 to 2026-10-22 08:00 Europe/Paris window. It concerns practical protections, infrastructure, credit, and research priorities for AI-assisted mathematics rather than a new theorem, proof, counterexample, or formalization. No qualifying update was found for the previously reported items.

• Tristan Buckmaster proposes privacy, open infrastructure, and revised credit for AI-assisted mathematicsTristan Buckmaster

Open this edition →

Three substantive developments were found in or plausibly within the narrow reporting window: an AI-assisted number-theory challenge, a new human exposition of an AI-generated argument, and an open-source reading tool for navigating long AI-generated papers. No new proof is treated as certified, and no Lean artifact was executed or independently checked.

• Tao proposes an AI-assisted challenge to extract explicit tenth-discriminant boundsTerence Tao
• Tao publishes a human-oriented sketch of the AI-generated Landau–Siegel-zero argumentTerence Tao
• Readable Intelligence releases paper maps and readable versions for AI-generated mathematicsReadable Intelligence

Open this edition →

One modest but potentially useful Lean-interface update appeared in the window. No new research theorem, proof, counterexample, paper, independently scrutinized result, or checked autoformalization was substantiated. Most monitored feeds were empty, and several access gaps prevent an exhaustive conclusion.

• A block-based “Integer Game” extends the experimental Visual Lean interfaceAlex Kontorovich (announcement; handle-to-person association not independently verified)

Open this edition →

One substantive proof-exposition lead and one research-practice essay merit attention. Green’s note is publicly readable, but its original publication date and independent validation remain unconfirmed. Social coverage is incomplete.

• Ben Green offers a five-page AI-assisted variant of the claimed Landau–Siegel zero argumentBen Green
• Francesco Maggi proposes disclosure standards and shared infrastructure for AI-assisted mathematicsFrancesco Maggi

Open this edition →

One substantive development was found in the 2026-10-16 20:00 CEST to 2026-10-18 08:00 CEST window: Shaoming Guo announced plans for a mathematics journal that would require Lean verification while rewarding explanatory understanding rather than priority. This is a publishing proposal, not a journal launch, a verified corpus, or evidence that Lean formalization alone settles semantic correspondence. No new proof, counterexample, paper, code release, or independently scrutinized formalization was established from the other supplied leads.

• Shaoming Guo announces plans for a journal requiring Lean-verified proofs and prioritizing understandingShaoming Guo; guest post hosted by Terence Tao

Open this edition →

Three substantive developments were found within the window: a detailed expert program for scalable, reusable autoformalization; the soft launch of an open mathematical AI workspace; and a visual interface for learning Lean. No new proof or counterexample was included because none could be substantiated from primary sources within the window.

• Lean experts propose a quality-controlled route to formalizing most of mathematicsJeremy Avigad, Kevin Buzzard, Johan Commelin, Rémy Degenne, Kim Morrison, Oliver Nash, and Adam Topaz
• SAIR soft-launches Open Math OS for collaborative mathematical AI workflowsTerence Tao and the Foundation for Science and AI Research
• Visual Lean introduces a drag-and-drop interface for the Natural Number GameAutumn Mapes

Open this edition →

One substantive update emerged from the window: Lean’s maintainers clarified the formal guarantees and practical limits of the verified checkers bundled with Lean 4.35. No new mathematical proof, counterexample, or independently scrutinized AI-generated result was found among the other supplied feeds.

• Lean’s maintainers clarify what its newly bundled “verified kernels” actually guaranteeLeonardo de Moura; Lean maintainers; Joachim Breitner and contributors

Open this edition →

One substantial new evaluation and one promising exposition update were found for 13–15 October 2026. First Proof reports expert-reviewed results on unpublished research problems; a supplied Bloom thread announces a shorter Egyptian-fraction proof exposition, whose PDF could not be retrieved.

• First Proof's third batch reports nine successful proofs out of ten, with exposition and attribution still laggingMohammed Abouzaid, Nikhil Srivastava, Rachel Ward and Lauren Williams
• Bloom announces a shorter exposition of the AI-generated Egyptian-fraction argumentThomas Bloom and Wouter van Doorn

Open this edition →

Lean 4.35 adds practical checks for AI-generated formalizations. Trellis reports completing a large Goldberg–Seymour formalization, with public artifacts and provenance qualifications. Two October 12 essays address making generated mathematics reviewable. These four items from today's earlier editions were rechecked; no additional substantive in-window result was established.

• Lean 4.35 adds project checking and comparison against separately specified theorem statementsLean development team
• Trellis reports completing a Goldberg–Seymour Lean formalizationWesley Pegden / Trellis project
• Roberts identifies cleanup and correspondence checks for AI-generated proof artifactsDavid Roberts
• Huiberts argues for accountable exposition and attribution in AI-assisted researchSophie Huiberts

Open this edition →

Lean 4.35 adds useful checks for AI-generated formalizations. Trellis reports completing a substantial Goldberg–Seymour formalization, with public artifacts and provenance qualifications. Two October 12 essays offer practical standards for making generated mathematics reviewable. Social coverage and independent proof scrutiny remain incomplete.

• Lean 4.35 integrates project checking and comparison against separately specified theorem statementsLean development team
• Trellis reports completing a Goldberg–Seymour Lean formalizationWesley Pegden / Trellis project
• Roberts identifies cleanup and correspondence checks for AI-generated proof artifactsDavid Roberts
• Huiberts argues for accountable exposition and attribution in AI-assisted researchSophie Huiberts

Open this edition →

Lean 4.35 adds practical checks for AI-generated proof artifacts. Trellis reports completing a large Goldberg–Seymour formalization, with public code and important provenance qualifications. Two October 12 essays address the work needed to make generated mathematics reviewable. Account and social coverage remains incomplete.

• Lean 4.35 integrates project checking and comparison against trusted theorem statementsLean development team
• Trellis reports completing a Goldberg–Seymour Lean formalizationWesley Pegden / Trellis project
• Roberts identifies cleanup and correspondence checks for AI-generated proof artifactsDavid Roberts
• Huiberts argues for accountable exposition and attribution in AI-assisted researchSophie Huiberts

Open this edition →

Two substantial October 12 contributions address the practical burden of assessing AI-generated mathematics. No new theorem, counterexample or tool release was sufficiently established within the requested window to include. Social and account-identity coverage remains incomplete.

• Roberts identifies concrete cleanup and correspondence checks for AI-generated proof artifactsDavid Roberts
• Huiberts argues that AI-assisted results require accountable exposition and attributionSophie Huiberts

Open this edition →

One substantive new research-workflow essay was found. No additional mathematical result, proof correction or tool release could be established within the supplied window without repeating previous items. Coverage remains incomplete.

• Harriss and Stange propose rigorous illustration as part of AI-assisted mathematical researchEdmund Harriss and Katherine E. Stange

Open this edition →

Two substantive items for October 9, 2026, 20:00 through October 11, 2026, 22:01 Europe/Paris: Armstrong and Loher announce five AI-assisted Lean developments, and Tao publishes his Math 2.0 lecture resource. Public primary sources support inclusion, but independent formalization scrutiny and social coverage remain incomplete.

• Armstrong and Loher announce five AI-assisted Lean developments in mathematical physics and hypoelliptic PDEScott Armstrong and Amélie Loher
• Tao publishes Math 2.0 slides outlining uses of AI that support mathematical understandingTerence Tao

Open this edition →

One substantive new resource was identified within October 9, 2026, 20:00 to October 11, 2026, 08:00 Europe/Paris: Terence Tao's Math 2.0 lecture slides. No additional proof, counterexample or formalization update was sufficiently substantiated for inclusion. Social coverage was significantly incomplete.

• Tao publishes Math 2.0 slides with concrete proposals for AI-assisted researchTerence Tao

Open this edition →

One substantive in-window item: Thomas Hales explains how mathematicians should assess the reliability of AI-assisted Lean formalizations. Significant social-access gaps limit this edition.

• Thomas Hales explains the checks needed to trust AI-assisted Lean formalizationsThomas Hales, guest post hosted by Terence Tao

Open this edition →

Today’s research: AlphaProof Nexus receives journal publication, with public research-level proof artifacts; LEVER optimizes proof-search cost and mathematical proof quality together; Argonaut Math claims a small refinement of OpenAI's quasi-Riemann zero-free boundary. Coverage remains incomplete; see the source notes below.

• AlphaProof Nexus receives journal publication, with public research-level proof artifactsGeorge Tsoukalas and collaborators
• LEVER optimizes proof-search cost and mathematical proof quality togetherNihal Jain, Shuangjie Yao, Begum Cicekdag, Zhuo Zhang and Suman Jana
• Argonaut Math claims a small refinement of OpenAI's quasi-Riemann zero-free boundaryArgonaut Math

Open this edition →

Public web research found substantive leads, but none could be reliably placed within October 8, 2026, 20:00:01 through October 9, 2026, 09:13:03 Europe/Paris. No items are included: older findings, previously covered results and developments with unresolved publication times were excluded. Significant access gaps prevent a confident no-news conclusion.

Open this edition →

Today's edition retains saved research entries alongside the latest refresh. Public web research found substantive leads, but none could be reliably placed within October 8, 2026, 20:00:01 through October 9, 2026, 09:13:03 Europe/Paris. No items are included: older findings, previously covered results and developments with unresolved publication times were excluded. Significant access gaps prevent a confident no-news conclusion.

• AlphaProof Nexus receives journal publication, with public research-level proof artifactsGeorge Tsoukalas and collaborators
• LEVER optimizes proof-search cost and mathematical proof quality togetherNihal Jain, Shuangjie Yao, Begum Cicekdag, Zhuo Zhang and Suman Jana
• Argonaut Math claims a small refinement of OpenAI's quasi-Riemann zero-free boundaryArgonaut Math

Open this edition →

Three substantive items: AlphaProof Nexus reaches journal publication, LEVER studies cost and proof quality during formal search, and Argonaut Math releases a claimed refinement of a zero-free region. Social-source coverage and independent verification remain limited.

• AlphaProof Nexus receives journal publication, with public research-level proof artifactsGeorge Tsoukalas and collaborators
• LEVER optimizes proof-search cost and mathematical proof quality togetherNihal Jain, Shuangjie Yao, Begum Cicekdag, Zhuo Zhang and Suman Jana
• Argonaut Math claims a small refinement of OpenAI's quasi-Riemann zero-free boundaryArgonaut Math

Open this edition →

Two substantive updates in the requested window: OpenAI withdrew three manuscripts and revised others; Scott Aaronson reported early expert scrutiny of the claimed Unique Games proof. Social-media coverage and account authentication remain incomplete.

• OpenAI withdraws three Hodge-related manuscripts and publishes proof repairsOpenAI
• Early scrutiny of the claimed Unique Games proof exposes substantial exposition workScott Aaronson, reporting observations by Dana Moshkovitz

Open this edition →

Two substantial updates were found for the requested window: OpenAI's release of research manuscripts and proof artifacts, and Thomas Bloom's changes to the Erdős Problems research workflow. Neither establishes that the advertised mathematical claims have received independent verification.

• OpenAI releases a large collection of mathematical manuscripts with supporting Lean artifactsOpenAI
• Erdős Problems changes how AI-generated proof claims are submitted and presentedThomas Bloom

Open this edition →

Reconstructed on 7 Oct 2026 · 16:52 CEST.

Four dated October 6 announcements or publications: OpenAI releases a large manuscript collection, two AI-assisted preprints disclose formal proofs, and ScienceBench closes benchmark submissions. Proof correctness was not independently verified in this research.

• OpenAI releases 722 mathematical manuscripts with selected Lean artifacts and research-process disclosuresOpenAI
• AI-assisted preprint presents a second forest-unimodality proof with explicit formalization and review caveatsWei Li, Kevin Vallier and Tong Zhang
• Kasami preprint gives an AI-assisted proof of Carlet's cyclic-additive conjectureGábor P. Nagy, Douglas S. McNeil and Attila Vajda
• ScienceBench closes problem submissions while reconsidering research-mathematics benchmarkingScienceBench

Open this edition →

Reconstructed on 7 Oct 2026 · 16:51 CEST.

Two dated contributions were established for October 5, 2026: an exposition of the Lyons–White result with a qualified AI formalization claim, and a proposal for evaluating research amid AI-driven publication growth. Social-media archival coverage remains incomplete.

• Axiom explains the Lyons–White exponent dichotomy and its qualified Lean formalizationColin Defant
• Pasquato proposes limiting publication-based evaluation to protect research qualityMario Pasquato

Open this edition →

Reconstructed on 7 Oct 2026 · 16:49 CEST.

Two substantive entries were located for October 4, 2026: a claimed AI-discovered Thue–Morse proof with public Lean artifacts, and specialist context for AI-assisted fluid singularity claims. Social-media archival coverage remains limited.

• Public AI-assisted Lean package claims the three Joshi–Rust Thue–Morse first-occurrence formulasdot (OpenAI), as credited in the package; submitted by ZestyDingo473
• Córdoba and Martínez-Zoroa explain the mathematical scope of fluid singularity claimsDiego Córdoba and Luis Martínez-Zoroa; guest post hosted by Terence Tao

Open this edition →

Reconstructed on 7 Oct 2026 · 16:47 CEST.

October 3, 2026: an AI-assisted combinatorics preprint supplies a proof and verification artifacts, while two mathematicians offer concrete guidance on research practice. Social-media archival coverage remains incomplete.

• AI-assisted preprint improves a lower bound for isosceles-free grid subsetsYukai Song
• Idrissi proposes research logbooks and separate credit for results and explanationsNajib Idrissi
• Taback reports useful AI assistance with lemma repair and paper organizationJennifer Taback

Open this edition →

Reconstructed on 7 Oct 2026 · 16:45 CEST.

Two substantive October 2 announcements were established: Meta's release of six AI-assisted mathematics papers and a correction exposing a circular hypothesis in a Collatz Lean development. Archival and social-media coverage remains incomplete.

• Meta releases six AI-assisted mathematics papers with disclosed human review and concurrent workMeta AI Research and collaborating mathematicians
• Collatz formalization erratum identifies a hypothesis equivalent to the large-cycle conclusionEric Merle

Open this edition →

Reconstructed on 7 Oct 2026 · 16:43 CEST.

Three substantive entries established for October 1, 2026: an account of AI-assisted operator-system research, a benchmark separating mathematical idea discovery from execution, and arXiv's response to AI-related submission growth. Coverage of the supplied social accounts remains incomplete.

• Van Suijlekom describes AI-assisted computations of operator-system K-theoretic invariantsWalter van Suijlekom
• The Missing Primitive tests whether models discover the organizing idea of a mathematical solutionShuo Xing, Zilin Dai, Chengyuan Qian, Fangzhou Lin, Wenjing Chen, Ping He, Pan Lu, Alvaro Velasquez, Mohit Bansal and Zhengzhong Tu
• arXiv introduces monthly submission limits in response to AI-related moderation pressureKat Boboris / arXiv

Open this edition →

Reconstructed on 7 Oct 2026 · 16:41 CEST.

September 30, 2026: an available preprint and code release study cheaper agent interaction with Rocq and Lean; Tao announces practical recommendations for AI-assisted theoretical research. Coverage of social-media archives and several primary-source leads remains incomplete.

• Evolved prover interfaces reduce reported proof-generation costs, with a Lean accuracy tradeoffJules Viennot, Guillaume Baudart, Marc Lelarge
• Tao highlights concrete proposals for adapting theoretical research to AITerence Tao; September 2026 Working Group

Open this edition →

Reconstructed on 7 Oct 2026 · 16:39 CEST.

Three substantive sources dated September 29, 2026: a reusable Lean research library, AGMAI release recommendations, and Rachel Webb’s account of AI in mathematical research. Social-media archival coverage remains limited.

• GenLimitLib organizes a research literature into reusable Lean developments and reports new mathematical findingsShuangping Li and Peng Zhang
• AGMAI specifies release standards for AI-generated mathematics that lacks human understandingAdvisory Group on Mathematics and Artificial Intelligence
• Rachel Webb describes choosing AI assistance around mathematical understanding and collaborationRachel Webb

Open this edition →

Reconstructed on 7 Oct 2026 · 16:37 CEST.

September 28, 2026: two substantial Lean formalization announcements, an optimization proof workflow, an agent framework applied to algebraic geometry, and a redesigned mathematical exposition initiative. Verification claims remain attributed to their authors.

• FrenzyMath announces an AI-assisted Lean formalization of the Poincaré conjectureFrenzyMath
• Vals AI publishes a claimed Lean proof of the seven-point Thomson problemHung Tran
• Peppy presents AI-assisted analytic proofs of tight optimization convergence boundsJaewook J. Suh, TaeHo Yoon, Edward Duc Hien Nguyen, Bicheng Ying and Shiqian Ma
• Solver Agent links an auditable AI workflow to Calabi–Yau geometry calculationsEliott Morgensztern, Cesar Fierro Cota and Alessandro Mininno
• Mathathon redesign makes exposition and disclosed research artifacts centralMathathon organizers and a coalition of Caltech mathematicians

Open this edition →

Reconstructed on 7 Oct 2026 · 16:34 CEST.

Three substantive sources dated September 27, 2026: an AI-assisted improvement in bounds for distinct zeta zeros, a reported Lean formalization of two-dimensional Navier–Stokes existence theory, and practical proposals for preserving research judgment in doctoral training. Social-media archival coverage remains limited.

• AI-assisted preprint improves the claimed lower bound for distinct zeta zeros to 83.699%Kristian Muri Knausgård
• AI-assisted Lean development formalizes a Galerkin construction for two-dimensional Navier–StokesWeinan Wang
• Jess Werk proposes departmental practices that reward understanding and verificationJess Werk

Open this edition →

Reconstructed on 7 Oct 2026 · 16:31 CEST.

Five substantive entries were identified for September 26, 2026: an AI-assisted polytope preprint, two dated Lean registry records, a reproducibility package for a nested recurrence, and an essay on research values. Archival social-media coverage remains incomplete.

• AI-assisted preprint gives counterexamples and bounds for cube-truncated Hadamard simplicesNikita Lebedev
• Dated Lean registry record claims Hamilton cycles in Cayley graphs of polylogarithmic degreeShengtong Zhang, formalization maintainer
• Erdős Problem #1220 receives a dated Lean record for non-provability in ZFCJi Ho Bae (JRTI)
• Padovan recurrence reproducibility package archives finite-state computations and Lean proofsBenoit Cloitre, Haobo Ma and Wenlin Zhang
• Ivan Corwin proposes evaluating AI use through the broader value of mathematical researchIvan Corwin

Open this edition →

Reconstructed on 7 Oct 2026 · 16:28 CEST.

Five substantive entries for September 25, 2026: an AI-assisted graph-pebbling proof, a registered ring-theoretic counterexample, reusable Lean analysis infrastructure, and two contributions on mathematical research and training. Formal verification claims are attributed to their sources; no proofs were independently verified and no Lean code was executed.

• AI-assisted preprint claims the tree-stacking formula, with a reported complete Lean formalizationJohn Fairfax-Ball
• Palomar registers a claimed AI-generated counterexample to left-right symmetry of PCI ringsVlad Tsyrklevich
• Locally convex space infrastructure receives a dated Lean registry recordBastiaan J. Braams
• PhD education summit releases practical recommendations for AI use in mathematical researchBryna Kra and Rachel Ward, presenting the summit recommendations
• Larry Guth explains the research values he wants preserved as AI changes mathematicsLarry Guth

Open this edition →

Reconstructed on 7 Oct 2026 · 16:27 CEST.

Three dated items for September 24, 2026: a benchmark for local formal reasoning in analysis, a Lean proof-checker benchmark release, and Amit Sahai’s proposal for expanding human mathematical expertise. Archival social-media coverage remains limited.

• ProofGap separates local formal reasoning from complete proof construction in analysisLihan Xie, Zhicheng Hui, Yingjun Lan, Zhehao Li, Xingzhi Qi, Siyue Huang, Jirui Liu, Chuxiao Zeng, Bohan Zhao and Qinxiang Cao
• Lean Kernel Arena archives its September proof-checker benchmark roundThe Lean Kernel Arena contributors; Joachim Breitner, editor
• Amit Sahai argues for expanding independent mathematical expertise alongside AI discoveryAmit Sahai

Open this edition →

Reconstructed on 7 Oct 2026 · 16:25 CEST.

Two substantive entries were established for September 23, 2026: a conditional Lean formalization in analytic number theory and a new essay on understanding and auditability in AI-assisted mathematics. Significant gaps remain in social-media and archival coverage.

• Fiori's short-interval zeta results receive a conditional Lean registry recordAndrew Fiori
• Schneider connects mathematical understanding with auditable AI research workflowsTapio Schneider

Open this edition →

Reconstructed on 7 Oct 2026 · 16:23 CEST.

Two substantive September 22 publications were established: Axiom's explanation of an earlier combinatorial result and its reported Lean workflow, and Martin Hairer's clarification of the independent mathematics advisory group's role. Archival social-media coverage remains incomplete.

• Axiom explains record-composition enumeration and its reported autonomous Lean proof workflowEvan Chen
• Hairer clarifies AGMAI's independence, advisory limits and publication prioritiesMartin Hairer

Open this edition →

Reconstructed on 7 Oct 2026 · 16:21 CEST.

Two substantive September 21 entries were established: a preprint on maintaining reusable Lean formalizations with AI agents, and a mathematics advisory-group announcement containing substantial but undocumented mathematical claims. Social-media archival coverage remains limited.

• Lean Pool preprint describes an AI-maintained archive of reusable formalized mathematicsVasily Ilin
• OpenAI announces an independent mathematics advisory group and claims over 100 problem resolutionsOpenAI

Open this edition →

Reconstructed on 7 Oct 2026 · 16:19 CEST.

One substantive September 20 assessment was established: scrutiny of the attribution and verification behind an AI-assisted social-choice result. No new theorem or completed formalization was securely dated to this day. Archival coverage remains incomplete.

• September 20 scrutiny separates an AI-assisted voting theorem from benchmark verificationVlad Makarov, Traictory

Open this edition →

Reconstructed on 7 Oct 2026 · 16:17 CEST.

No substantive entry could be established as originally published on September 19, 2026. Public web research was usable, but archival and social-media coverage was too limited to conclude that no relevant news occurred.

Open this edition →

Reconstructed on 7 Oct 2026 · 16:15 CEST.

Four substantive publications dated September 18, 2026 were identified: a claimed AI-assisted Conway proof, a candid Frankl-conjecture workflow report, an open mathematical-model initiative, and a proposal for rewarding mathematical explanation. Archival social-media coverage remains incomplete.

• Abramov publishes a claimed AI-assisted proof of Conway's refinement conjectureDan Abramov
• Hanson reports what worked and failed in an agent-based attack on Frankl's conjectureEric P. Hanson
• Tao announces SAIR's initiative for open mathematical models and research toolsTerence Tao and SAIR Foundation
• Sanderson proposes treating mathematical explanation as a research deliverableGrant Sanderson

Open this edition →

Reconstructed on 7 Oct 2026 · 16:13 CEST.

One substantial autoformalization preprint was published on September 17, 2026. A second dated preprint supplies a concurrent-discovery disclosure and corrects the chronology of an item in the previous digest. Archival social-media coverage remains limited.

• FormalFlow reports a Lean formalization of quantum soundness underlying MIP* = RESirui Lu, Ruixuan Deng, Yanqiao Zhu and Zhengfeng Ji
• Concurrent linear-matroid secretary preprint adds an AI-discovery disclosure and corrects the earlier chronologyKristóf Bérczi, Shaddin Dughmi, Vasilis Livanos, José A. Soto and Victor Verdugo

Open this edition →

Reconstructed on 7 Oct 2026 · 16:11 CEST.

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.

• AI-assisted preprint claims optimal secretary guarantees for linear matroids and a tight single-sample prophet inequalityHamed Abdi, Kiarash Banihashem, MohammadTaghi Hajiaghayi and Danny Mittal
• Bumpus describes using AI proofs as starting points for deeper research and learningBenjamin Merlin Bumpus

Open this edition →

Reconstructed on 7 Oct 2026 · 16:08 CEST.

Three substantive posts dated September 15, 2026 were established: Axiom's account of AI-assisted higher Dyson rank research and two essays on responsible mathematical research with AI. Archival social-media coverage remains limited.

• Axiom explains AI-assisted elliptic corrections for higher Dyson ranks and the scope of its Lean proofsKen Ono
• Henry Cohn identifies the technical debt of poorly explained AI-generated mathematicsHenry Cohn
• Ben Antieau proposes standards for ambitious AI-assisted research that researchers can understandBen Antieau

Open this edition →

Reconstructed on 7 Oct 2026 · 16:05 CEST.

Three substantive publications or updates dated September 14, 2026: practical advice from Pavel Etingof, a firsthand AI-assisted research account from Beni Bogoşel, and Emily Riehl’s discussion of mathematical explanation. No new theorem or formalization announcement was established for this day.

• Etingof adds a dated update on AI-assisted refereeing, formalization and research habitsPavel Etingof
• Bogoşel reports a research workflow combining notes, numerical code and directed AI agentsBeni Bogoşel
• Riehl argues that clarifying explanations remain central to mathematical researchEmily Riehl

Open this edition →

Reconstructed on 7 Oct 2026 · 16:03 CEST.

Three substantive publications dated September 13, 2026: a practical Lean agent workflow, Bryna Kra’s account of purported Nivat proofs, and Daniel Litt’s proposals for preserving mathematical expertise. No new theorem is certified by this digest.

• A practical Lean workflow lets coding agents iterate on build feedbackpandaman64
• Bryna Kra reports purported Nivat proofs and calls for accountable mathematical explanationBryna Kra
• Daniel Litt proposes evaluating mathematical understanding through defenses and sustained discussionDaniel Litt

Open this edition →

Reconstructed on 7 Oct 2026 · 16:02 CEST.

One substantive essay was established as published on September 12, 2026. No new mathematical result, proof artifact or research tool met the date and evidence requirements in the accessible material. Archival coverage remains incomplete.

• Manuel Rivera distinguishes AI's effects on mathematical understanding and the research professionManuel Rivera

Open this edition →

Reconstructed on 7 Oct 2026 · 15:59 CEST.

September 11, 2026: two dated Lean formalization registry records and a joint declaration on AI and mathematical research. Public social-media archives and direct access to the registry evidence were incomplete.

• Kolmogorov–Arnold superposition formalization receives a dated registry recordGeorge A. Constantinides
• Lean record reports a resolution of Gallardo’s polynomial-substitution conjectureBrandon Yates
• Fields medallists publish a joint declaration on AI and mathematical understandingJoint signatories, including Terence Tao

Open this edition →

Reconstructed on 7 Oct 2026 · 15:57 CEST.

One dated research-culture essay qualifies for September 10, 2026. No additional mathematical result or tool release was established for this day; archival and social-media coverage remains incomplete.

• Matt Baker examines how AI changes mathematical research, exposition and graduate trainingMatt Baker

Open this edition →

Reconstructed on 7 Oct 2026 · 15:56 CEST.

One dated update concerns the provenance of AI-assisted fluid-equation research. No new mathematical result or independently checked formalization was established for September 9 in the accessible sources. Archival and account-verification gaps limit this reconstruction.

• Alpöge’s account adds a provenance update to the AI-assisted fluid-equation disputeJulien Lausson, reporting statements by Levent Alpöge

Open this edition →

Reconstructed on 7 Oct 2026 · 15:54 CEST.

September 8, 2026: OpenAI released claimed AI-generated fluid blowup proofs and Lean artifacts; a separate Lean runtime bug report identified a concrete reliability issue. Archival social-media coverage remains incomplete.

• OpenAI releases claimed forced Navier–Stokes and unforced Euler blowup proofs with Lean artifactsOpenAI
• Lean runtime report exposes a constructor boundary bug affecting safe compiled codemufeedvh

Open this edition →

Reconstructed on 7 Oct 2026 · 15:51 CEST.

Two substantive sources dated 7 September 2026 concern AI-assisted fluid singularity research: smooth-forcing blowup constructions reported as Lean-formalized, and a PINN-generated candidate for unforced Euler blowup. Archival and timezone gaps limit reconstruction of the complete Paris civil day.

• Tao explains AI-assisted smooth-forcing blowup constructions and their reported Lean formalizationTerence Tao, discussing work by Levent Alpöge, Tristan Buckmaster and collaborators
• A physics-informed neural network proposes an unforced three-dimensional Euler singularity profileAnima Anandkumar, reporting joint work with Adarsh Ganeshram and Valentin Duruisseaux