Browse the watch

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