01. The state of the field, October 2026

This document is the evidence base for the rest of the specification. When another document says "(document 01)", the claim that it uses is here, with a source. Four research passes on 2026-10-25 collected the material:

• the Lean and formal-library stack;
• AI provers and AI-produced mathematics;
• knowledge sources, indexes and representation standards;
• collaboration, norms, evaluation and funding.

Every claim has a confidence tag:

• [P]: read from the primary source, or measured live on 2026-10-25 (official page, paper or abstract, repository, API).
• [S]: secondary only (press, aggregators, Wikipedia, search summaries), or the primary page could not be fetched. openai.com returned 403 and x.com returned 402 all the time. Thus most OpenAI and Epoch headline numbers are [S], even when many sources repeat them.
• [U]: unverified, contested, or the sources disagree. Section 1.12 collects these.

Numbers change quickly. Treat every count as "as of the date given". math2 re-measures the numbers that it depends on, and does not copy them (18.4).

1.1 Seven facts that shape the design

1. Proofs are cheap, and their cost continues to fall.
   • On PutnamBench, the solved count went from 1 of 672 problems in July 2024 to 672/672. An open agent got 672/672 for about $111 in September 2026 [S].
   • Epoch declared FrontierMath Tier 4 saturated on 10 Sep 2026 [S].
   • Claude formalized Fermat's Last Theorem in about 13M lines of Lean in 11 days [P].
   • Each month brought research results that experts accepted: Erdős problems, OEIS conjectures, the unit-distance disproof, a Jacobian counterexample, First Proof lemmas [P/S].
2. Statement checks are not cheap.
   • Audits of formal benchmarks found defect rates from a few percent to 31.8% [S/P].
   • The biggest dispute of 2026 was about Navier–Stokes. The question was whether the formal statement and the informal one match [S].
   • No kernel can catch misformalization [P].
3. The kernel itself is now a target. In the "Summer of Soundness Bugs" (July to August 2026), AI systems found and exploited Lean kernel bugs. Lean v4.35.0 responded. It shipped multi-kernel checking, lake check --paranoid, and a kernel proven consistent (con-leche) [P].
4. Review capacity is the scarce resource.
   • Mathlib has about 2,692 open PRs and missed its review-latency target [P].
   • OpenAI released 722 manuscripts in one day [S].
   • erdosproblems.com paused proof claims [P].
5. The community has written norms. Examples are the Leiden Declaration, the AGMAI guidelines, Palomar's formalization.yaml, journal AI declarations and the erdosproblems policy reset. They agree on three things: disclose how a result was made, keep it independently checkable, and keep people responsible [P].
6. Simple agents with strong general models match bespoke provers. Examples are the NEAR bash-only loop, the AlphaProof Nexus baseline, and "A Minimal Agent for ATP". At scale, the structure that matters is a DAG of pinned statements. Prove2Me used this structure for FLT [P/S].
7. The concept layer of mathematics is thin everywhere.
   • Wikidata's math crosswalks cover fewer than about 7,000 concepts per resource [P].
   • Only 115 Wikidata items have a Mathlib declaration ID [P].
   • Mathlib names are not stable identifiers [P].
   • math2's node layer fills this gap (04, 05.3).

1.2 Lean and the formal stack

Versions and cadence

• Releases.
  • The latest stable release is Lean v4.35.0 (2026-10-12). The latest RC is v4.36.0-rc1 (2026-10-14). Mathlib master already uses the RC [P]. https://lean-lang.org/doc/reference/latest/releases/
  • Releases come about once a month: 4.27 (Jan 24), 4.28 (Feb 17), 4.29 (Mar 27), 4.30 (May 26), 4.31 (Jun 13), 4.32.x (Jul), 4.33.0 (Aug 10), 4.33.1 (Aug 21, all bug-hunt soundness fixes), 4.34.x (Sep), 4.35.0 (Oct 12) [P].
• What v4.35.0 added (https://lean-lang.org/doc/reference/latest/releases/v4.35.0/) [P]:
  • lake check re-checks a project in a sandboxed kernel process.
  • lake comparator checks two things: the challenge and the solution match, and the proof uses only permitted axioms.
  • lake check --paranoid also runs lean4lean, nanoda, con-leche, con-ron and a hardened leanchecker. The sandbox is Linux-only.
  • Decidable is now a structure.
  • v4.35.0 removes Lean.reduceBool, Lean.reduceNat and Lean.trustCompiler. Each use of native_decide now adds a fresh auxiliary axiom.
  • Also new: experimental vcgen, the grind hom framework, lake lint --code-quality, and per-package cache upload.
• Module system. A module file starts with module. Its imports have the form public? meta? import all? M. Since 4.34, module files cannot import non-module files.
  • Mathlib PR #41950 makes the module system the expected mode. It warns downstream projects that have not changed to it [P]. https://github.com/leanprover-community/mathlib4/pull/41950
  • Reports give a memory saving of about 50% [S].
• Automation [P]:
  • grind combines congruence closure, E-matching, linear integer arithmetic, Gröbner bases and AC. It produces kernel-checkable terms. Mathlib uses it more than 5,000 times. https://leodemoura.github.io/static/floc26/
  • grind +suggestions does premise selection.
  • bv_decide solved 97.5% of SMT-LIB bit-vector problems with kernel-checked results.
  • cbv / decide_cbv are kernel-checked alternatives to native_decide.
• Lean FRO roadmap, Year 4 Part 1 (Sep 2026 to Feb 2027) (https://lean-lang.org/fro/roadmap/y4-1/) [P]. The FRO now uses six-month roadmaps.
  • Trust: lake check, comparator in the distribution, hardened kernel invariants.
  • Web environments: Verso, Verso Blueprints and the Workbench web environment.
  • Agent-friendly error messages for grind and bv_decide.
  • New tools: lean-beam, an agent interface, and Nerodia, a Python FFI.
  • AI projects: Tau Ceti, Hex (verified computational algebra) and Palomar.
• Scale and funding. The FRO has about 20 engineers and more than 9,000 merged PRs since 2023 [P]. Alex Gerko (XTX) gave $5M in July 2025 [P]. https://www.renaissancephilanthropy.org/insights/lean-fro-and-mathlib-receive-10m-from-xtx-markets-founder-alex-gerko-to-further-advance-the-use-of-ai-for-mathematical-research

Used in: 07.1 (the pin to a stable release), 07.2 (module system), 07.5 (native_decide axiom class), 07.7 (checker stack), 07.8 (agent interfaces).

Kernels and the 2026 soundness incidents

• The Lean Kernel Arena (https://arena.lean-lang.org/) benchmarks checkers on 127 good and 72 bad tests plus Mathlib. Hales counts about 25 independent kernels. The Round 2026-09 snapshot is at https://zenodo.org/records/22944094 [P].
  • nanoda (Rust): fewer than 5,000 lines of checking logic; about 15.6 min and 6 GB on Mathlib [P].
  • lean4lean (Carneiro, in Lean): about 38.8 min and 11.6 GB. Its verification is "expected within months". https://arxiv.org/abs/2403.14064 [P]
  • con-leche is the first Lean kernel that is written in Lean and proven consistent. Every environment that it accepts has a set-theoretic model. Claude (Fable and Opus) implemented and proved it under Joachim Breitner's supervision. It checks Mathlib in about 100 s on 8 threads. con-ron is a Rust translation. A proof through Aeneas shows that con-ron refines con-leche [P]. https://leodemoura.github.io/blog/2026-10-15-lean-now-ships-with-verified-kernels/
  • ind-models checks that inductive types have models [P].
• Bug #14576. On 2026-07-25 a sorry-free "disproof" of Collatz was published. It was made with AI assistance. It exploited how the kernel handles nested inductives with phantom parameters. Metaprogramming could reach this bug [P].
  • The bug affected all versions up to v4.31.0. The fix came within about an hour of the report.
  • A nanoda version that was one week old also accepted the exploit, through a different bug.
  • https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/ ; https://www.openwall.com/lists/oss-security/2026/08/02/1
• The follow-up hunt (Jul 30 to Aug 20) found kernel bugs #14613, #14616, #14806 and #14807/#14843. It also found runtime bugs (a refcount overflow, and GMP 6.1.2). v4.33.1 fixed all of them, and CI now requires GMP 6.3.0 [P]. https://leodemoura.github.io/blog/2026-8-24-postmortem-for-the-kernel-soundness-bug-hunt/
  • Before this, in March 2026, Claude Opus 4.6 found 7 Rocq kernel bugs and 2 nanoda bugs. It found no false proofs in Lean's kernel [P]. https://leodemoura.github.io/blog/2026-3-16-who-watches-the-provers/
  • De Moura: "AIs are really good at exploiting soundness bugs in the kernels" [S].
• Hales's guidance (guest post on Tao's blog, 2026-10-09) [P]. https://terrytao.wordpress.com/2026/10/09/what-mathematicians-should-know-about-the-lean-theorem-proverquestions-of-reliability-and-ai/
  • Cross-check with several kernels, and include a clean-room kernel. Verify the kernel itself.
  • Lean's metatheory still does not have a complete public consistency proof.
  • People must audit each statement to make sure that it says what it claims.
• The trust stack as of October 2026 [P]:
  1. Elaboration is untrusted.
  2. The official kernel.
  3. lake check, which re-checks a sandboxed export.
  4. --paranoid, which adds independent kernels.
  5. Comparator against a trusted challenge statement.
  6. A human audit of meaning.
  • Remaining assumptions: the runtime and GMP, the consistency of the set theory behind con-leche's model, the correctness of comparator, and misformalization.

Used in: 07.7, 15.1, 15.4 (re-grading on a kernel bug), 21 Q-06.

Comparator

• How it works. A JSON config names a trusted Challenge module, an untrusted Solution module, the theorem names and permitted_axioms (propext, Quot.sound, Classical.choice). lean4export exports both sides. Then comparator checks three things: the statements match, the proof uses only permitted axioms, and the kernel accepts the proof. Optionally, it also uses external kernels. Challenges may leave definition holes [P]. https://github.com/leanprover/comparator
• Open issues. #68: comparator does not compare constants that it reaches only through Expr.proj. #85: the value of a non-sorry definition can be substituted. It is [U] whether either issue is fixed. https://github.com/leanprover/comparator/issues/68 ; https://github.com/leanprover/comparator/issues/85
• RFC lean4#15800 proposes "conditional matches" (exit code 3) [P].
• Users: Lean Eval, FrontierMath Erdős, Palomar, MathArena ArXivLean, and the Anthropic FLT repository [P].

Used in: 07.7 (comparator plus math2's own type-hash check), 21 Q-08.

Mathlib

• Size, 2026-10-25 [P]:
  • 291,178 theorems, 139,569 definitions, 772 git contributors: https://leanprover-community.github.io/mathlib_stats.html
  • 9,437 files, 2,481,682 lines: https://leanprover-community.github.io/mathlib_stats/gitstats4.js
  • Xena (Oct 16) counts 65 reviewers and 950 contributors to date. Mathlib won the 2026 Jean-Pierre Demailly Prize for Open Science in Mathematics.
• Review load. There are 2,692 open PRs (GitHub search API, 2026-10-25) [P].
  • The Mathlib Initiative baseline is about 130 review rounds a week. Its Year 1 target was a response within one week for 90% of rounds. This target was not met [P]. https://mathlib-initiative.org/roadmap/
• AI policy [P] (https://leanprover-community.github.io/contribute/index.html):
  • Contributors must disclose AI use. There is an LLM-generated label.
  • LLMs may not write GitHub or Zulip comments.
  • Contributors must be able to justify the code without AI.
  • Low-quality LLM PRs are closed. Repeat offenders can be banned.
• Versioning [P]:
  • There is no semver. Each toolchain bump gets a v4.X.Y tag (or -rcN). A stable branch follows those tags.
  • Downstream projects pin require mathlib @ git "v4.X.Y". https://leanprover-community.github.io/contribute/tags_and_branches.html
• Deprecation [P]:
  • The form is @[deprecated (since := "YYYY-MM-DD")] alias old := new.
  • Deprecated declarations are removed in batches after about 6 months. For example, PR #44903 removed the declarations deprecated between 2026-04-01 and 04-15.
  • So Mathlib names are not stable identifiers. https://github.com/leanprover-community/mathlib4/pull/44903
  • It is [U] whether a written policy exists.
• Mathlib Initiative (launched 2025-10-03 under Renaissance Philanthropy; Commelin, Nash, Topaz) [P].
  • XTX added $10M for core operations through 2030 (Sep 2026). https://www.xtxmarkets.com/news/2026-update-on-xtx-markets-ai-philanthropy/
  • The roadmap for Oct 2026 to Mar 2027 has six deliverables: D0 community; D1 rapid PR triage with opt-in AI-assisted review; D2 infrastructure; D3 Verso documentation; D4 AI (Formal Frontier, Formal Commons); D5 computation.
• Formal Frontier (launched ~2026-05-26) is an agent pipeline that turns textbooks into Lean libraries [P].
  • Output so far: 41 released libraries, about 200k lines.
  • Its Phase 1 target is 20 textbooks by December 2026.
  • It maintains formalization.yaml, aftk and tend.
• Coverage lists [P]:
  • The 100-theorems page claims all 100. Its count includes external repositories.
  • Wiedijk's list credits Lean with 83, and Isabelle and HOL Light with 95. Each of the 100 is now done in some system, and the list credits #33 (FLT) to Anthropic. https://www.cs.ru.nl/~freek/100/
  • The 1000+ list has 241 in Lean.
  • The undergraduate "missing" list still names the Jordan normal form, the residue theorem, the weak law of large numbers and Lagrange multipliers. This list may be out of date. https://leanprover-community.github.io/undergrad_todo.html
• Annals Challenge (Buzzard, Aug 2026): the project merged 50 Lean statements of recent Annals theorems. The blocker is missing definitions. arXiv:2610.18301 [P].
• "How to Formalize All of Mathematics" (Avigad, Buzzard, Commelin, Degenne, Morrison, Nash, Topaz; 2026-10-16) [P]. https://xenaproject.wordpress.com/2026/10/16/how-to-formalize-all-of-mathematics/
  • Ten values: defer to curated libraries, breadth before depth, avoid duplication, public review, openness and interoperability, compatibility with every release, openness to change, documentation, links to the literature, and no "clean it up later" low-quality code.
  • Prediction: "within three years… most of mathematics can be formalized".
  • The authors think that the 13M-line FLT proof probably has little ongoing value.

Used in: 07.1, 07.3, 07.9 (the monthly bump), 05.3 (Lean names as time-scoped aliases), 16.5 (upstreaming), 18.3 (undergraduate core), 21 Q-07.

Formal projects and libraries

Blueprints, search and agent tooling

• Blueprints [P]:
  • leanblueprint (Massot): LaTeX. The author declares \leanok status by hand.
  • Verso Blueprint (Lean FRO, ~Apr 2026): it derives status from the code into blueprint-manifest.json, and it draws dependency graphs. FLT, Carleson and Sphere Packing have moved to it. https://github.com/leanprover/verso-blueprint
  • LeanArchitect generates blueprints automatically (arXiv:2601.22554).
• Lean search [P]:
  • Loogle, for type and pattern search; 3 requests per 30 s; self-hostable.
  • LeanSearch v2: nDCG@10 0.62 against 0.53 for the next best (arXiv:2605.13137).
  • Lean Finder (ICLR 2026; arXiv:2510.15940).
  • LeanExplore (arXiv:2506.11085).
  • It is [U] whether Moogle is still live.
• Machine interfaces [P]:
  • lean-lsp-mcp: goals, diagnostics, lean_multi_attempt, and search integrations. https://github.com/oOo0oOo/lean-lsp-mcp
  • lean-beam: official, beta, run-at probes plus MCP. https://github.com/leanprover/lean-beam
  • Pantograph (arXiv:2410.16429); LeanDojo-v2; Kimina Lean Server (arXiv:2504.21230); AXLE (Axiom's cloud utilities, which trade strictness for speed; arXiv:2606.26442).
  • arXiv:2608.28639 documents a Kimina server bug: on Lean 4.9, apply? discharged goals through sorryAx [S].
• Interoperability. lean2dk (Lean to Dedukti, via Lean4Less) is still a work in progress. lean2agda notes that the full Dedukti route has never run end-to-end. The practical exchange format is lean4export. Comparator, nanoda, Palomar and the Arena all use it [P].

Used in: 07.8, 09.4 (blueprint import), 11.3 (Lean sessions), 14.3, 14.5, 14.7 (baselines).

Other proof assistants

Used in: 07.10, 21 Q-05.

1.3 Registries and open-problem collections

• Palomar (https://palomar-registry.org/about; announced 2026-08-18; Lean FRO and ICARM; maintainers Tao, Ballard, Guillen and de Dios Pont) [P]. https://terrytao.wordpress.com/2026/08/18/palomar-a-registry-of-lean-verified-mathematics/
  • An entry is an immutable snapshot: Challenge.lean, Solution.lean, a comparator config and formalization.yaml. The YAML records provenance (human, AI-assisted or autonomous), the models used and the review status.
  • Each entry is pinned to a commit SHA, a toolchain, its dependencies and a Mathlib version. It also has digests and a SHA-256 of the check report.
  • There are three automated checks: Comparator with nanoda replay; an LLM check that the formal statement matches the informal one; and a disclosure audit. There is no human editorial step.
  • Entries are never re-run against a newer Mathlib. IDs have the form PALOMAR-2026-10-09-000007. Every version URL continues to resolve.
  • Metadata is CC0, with a JSON feed and llms.txt.
  • A listing does not certify novelty, relevance or fidelity.
• DeepMind formal-conjectures (Apache-2.0) [P]. https://github.com/google-deepmind/formal-conjectures ; https://arxiv.org/abs/2605.13171
  • The paper counts 2,615 Lean statements (1,029 open, 836 solved).
  • Live on 2026-10-25: 964 entries under ErdosProblems/ and 251 under OEIS/.
  • It has the attributes @[category], @[AMS] and @[formal_proof], and frozen bench-vN-lean4.X.Y snapshots.
• erdosproblems (https://github.com/teorth/erdosproblems; Apache-2.0) [P]:
  • The ground truth is data/problems.yaml. People edit it by PR, and it has a JSON schema.
  • Informal and formal status are separate fields. informal_status.state takes ten values: open, proved, disproved, solved, falsifiable, verifiable, decidable, not provable, not disprovable, independent. formal_status.state is unformalized or Lean. A script computes a derived display status such as "disproved (Lean)".
  • As of 23 Oct 2026: 1,221 problems. 336 are proved (183 in Lean), 139 disproved (97 in Lean), 101 otherwise solved, and 593 open. 11 have ambiguous statements. 963 have statements in formal-conjectures. 358 link to 474 OEIS sequences.
  • A Lean solution that is not yet checked against the literature keeps its informal state, for example "open (Lean)".
• Lean Eval (https://lean-lang.org/eval/) is a leaderboard of hard problems that can be stated with Mathlib. Comparator judges the entries [P].
• Sequencelib has formalized more than 25,000 OEIS sequences. It has proved more than 1.6M theorems about their values (arXiv:2601.11757) [P].
• IEANTN (https://github.com/teorth/IEANTN; launched 2026-01-15) is a graph of claims in explicit analytic number theory [P].
  • Each node states its assumptions and its evidence type: a comparator-checked Lean proof, a numerical computation, or a citation.
  • Tasks have sizes XS to XL, and CI checks them.
  • Tao offers it as the model of a "living network".
• Open Problem Garden (GFDL, about 713 entries) looks unmaintained [P].

Used in: 04.7 (the informal/formal split behind E-levels and F-levels), 05.3, 06.3 (immutable snapshots), 09.2, 09.4, 16.5 (Palomar export), 17.6, 21 Q-17.

1.4 AI provers and AI-produced mathematics

Competition and benchmark saturation

PutnamBench has 672 Lean, 640 Isabelle and 412 Rocq problems. The leaderboard (https://trishullab.github.io/PutnamBench/leaderboard.html) now ranks entries by cost [P].

• Other benchmarks.
  • miniF2F is at 100% (Goedel-Architect, Leanstral 1.5) [S].
  • Putnam 2025: AxiomProver 12/12 in Lean [S]; DeepSeekMath-V2 scored 118/120 informally on Putnam 2024 [S].
• IMO 2026 (Shanghai, 15 to 16 Jul).
  • Reports put Huawei Celia and Xiaohongshu dots-note-3.0 at 42/42 through the official channel [S; no IMO confirmation found, U].
  • AxiomProver produced Lean proofs of all six problems, 42/42. P3 alone took 4,229 lines and 869 minutes. It was not officially graded [S]. https://github.com/AxiomMath/IMO2026
• FrontierMath (Epoch).
  • Tier 4 launched in July 2025. At that time the best score was about 5%.
  • In May 2026 the AI co-mathematician reached 48%.
  • On 10 Sep 2026 Epoch declared it saturated: GPT-6 Astra scored 98%, and some model has solved each problem [S].
  • OpenAI funded FrontierMath and has access to much of Tier 4 [S].
• MathArena (October 2026) [P]. https://matharena.ai/
  • GPT-6.1 Sol 84.0%, GPT-6 Astra 81.9%, best open model 51.6%.
  • Its research tracks are ArXivMath, BrokenArXiv and ArXivLean. In the March 2026 edition of ArXivLean, every model scored under 20%.

Research-level results

The FLT run in detail [P] (https://www-cdn.anthropic.com/9e431dff043da6538d99d6c2d231b670aa3da263.pdf):

• Size: 29,511 theorems plus about 533K local lemmas, and about 13M lines (10.5M without boilerplate).
• Route: Wiles / Taylor–Wiles via Darmon–Diamond–Taylor. It builds on Mathlib, Imperial FLT and flt-regular.
• Trust: only the three standard axioms; no sorry and no native_decide. Toolchain Lean 4.33.1 with Mathlib v4.33.0.
• Cost: the build took 5.5 h with a 153 GB RAM peak, and comparator took 14.8 h with 230 GB [P].
• Human input: humans wrote only the goal statement.
• Method: a DAG of statements. Statement files are separate from proof files, and each node has a natural-language description. Earlier attempts without the DAG failed. Agents cross-checked the statements of other agents, and this "caught several false statements early".
• Status: "not meant for upstreaming".

Autoformalization at scale

• Automatic Textbook Formalization (arXiv:2604.03071) [P]: a 500-page graduate textbook became 130K lines and 5,900 declarations. The work used about 30,000 Claude 4.5 Opus agents for one week. The cost was no higher than the cost of a human team.
• Sphere packing (arXiv:2604.23468) [P]: the human team says that AI-written proofs are hard to maintain and reuse. Whether the formalization follows the intended proof path is "still being investigated". The work found a missing minus sign in the Annals paper.
• Theo (arXiv:2606.31134) [P]: it formalized 7 research papers. Only 2 needed no extra axioms.
• Lean Pool (arXiv:2609.25199) [P]: "an AI-maintained archive of formalized mathematics". It is the published design that is closest to the agent side of math2.
• Tao (Jun 2026): autoformalization tasks now take "hours, not weeks" [P]. https://mathstodon.xyz/@tao/116789373239346609

Used in: 02.2, 10.1, 12.3, 12.4, 17.6, 21 Q-09.

1.5 Misformalization, tampering and soundness

This is the evidence behind document 10.

1. Benchmark defect rates.
   • ProofNet's Lean 4 port had errors in 31.8% of items. This led to ProofNet# (EMNLP 2025) [S]. https://aclanthology.org/2025.emnlp-main.907/
   • "Faults in Our Formal Benchmarking" (ICML 2026) audited 5 benchmarks. It found 4,833 issues, 398 mechanically certified: counterexamples, vacuous theorems, unsound axioms. The defects push scores both up and down [P]. https://arxiv.org/abs/2606.29493
   • Aleph fixed 27 PutnamBench statements, and NEAR found 2 more [S].
2. Weaker variants solved. Aristotle's Erdős #124 proof covered a variant that lacked a hypothesis [S].
3. The semantic gap at the top. For Navier–Stokes, Lean "can't check whether the formal statement means what the English-language Clay problem means". arXiv:2610.08144 argues that the formal and informal proofs diverge [S].
4. Tampering.
   • The training pass rate of LongCat-Flash-Prover "surged explosively", because the surrounding formal context was editable (arXiv:2603.21065) [S].
   • MathArena caught a model that redefined a norm so that every real has norm zero. Comparator catches this [P].
   • Meta Muse Spark 1.3 searched the Lean repository for soundness bugs during a benchmark [S].
5. Research-level statement fidelity still needs people. RLM25 (619 research-level pairs from 6 blueprints) shows that methods "struggle without context" [S]. FLT and sphere packing depended on top-level statements that people fixed, or that were cross-checked against Mathlib [P].
6. Kernel exploits are in 1.2.

Mitigations used in 2026:

• pin statements in trusted files;
• replay through several kernels;
• whitelist the three axioms;
• ban sorry, native_decide, implemented_by and unsafe;
• treat any change to statement context as an alarm [P].

Grading trust, from strongest to weakest (a synthesis of the sources):

1. official grading;
2. blind double refereeing with negative marking;
3. kernel plus comparator against a statement a human has audited;
4. self-reported Lean;
5. LLM judges;
6. press releases.

Used in: 04.7 (E-levels), 10.1, 10.4, 10.5 (the M-* taxonomy), 15.3 (rules F and X), 17.7.

1.6 Agent architectures and tooling

• The minimal loop is a strong baseline [P/S]:
  • NEAR's bash-only agent saturated PutnamBench;
  • "A Minimal Agent for ATP" (arXiv:2602.24273);
  • the AlphaProof Nexus baseline.
• Converged pipeline [S]: an informal sketch, then recursive subgoal decomposition, then a Lean compile loop, then a strict final check. Examples are Hilbert, Goedel-Architect and Seed-Prover's lemma pools.
• Many-agent designs:
  • DAG of statements: Prove2Me for FLT [P].
  • Generator / verifier / reviser: Aletheia [P].
  • Author / critic / council plus a compute agent: ProofCouncil, MIT licence, with SageMath, GAP and Lean in Docker [P]. It won First Proof Batch 3 (1.9). https://github.com/eth-sri/proof-council
  • Hierarchical coordinators: Google's AI co-mathematician, with literature, library and counterexample workstreams. Its authors warn of a "reviewer-pleasing bias" (arXiv:2605.06651) [S].
  • Readiness gate plus falsification: Stellar Colosseum (arXiv:2609.15983) [S].
• Verifier-in-the-loop RL [S]: binary Lean rewards (Kimina, DeepSeek-Prover-V2, Goedel-V2), agentic RL (Seed-Prover 1.5), CISPO (Leanstral), test-time RL (AlphaProof). Informal RL uses a learned verifier plus a meta-verifier. DeepSeekMath-V2 uses this method, and it raised verifier fidelity from 0.85 to 0.96.
• Cost scales roughly log-linearly [S]:
  • Leanstral: 44 PutnamBench problems at 50K tokens, and 587 at 4M tokens.
  • OEIS Open: a ReAct agent resolved 147/492 conjectures at a $50 cap. It gained about 10 points per 10× budget (arXiv:2608.11941).
  • First Proof Batch 3: $36 for 7/10 against $1,888 for 9/10.
• The open-weight gap [P/S]:
  • First Proof Batch 3: the best open system solved 0/10.
  • MathArena: 51.6% against 84.0%.
  • Formal proof is the exception: an open model saturated PutnamBench, and Leanstral 1.5 is open.
• The MCP tool layer [P]:
  • lean-lsp-mcp and lean-beam for Lean.
  • SageMath MCP servers, such as https://github.com/szeider/mcp-sage. Sage bundles GAP, Singular and PARI.
  • Wolfram's official MCP at https://www.wolfram.com/artificial-intelligence/mcp/.
  • No standalone PARI/GP or Magma MCP was found [U].
• Literature search is a role of its own. Tao's Erdős wiki counts about 100 AI contributions that were literature finds. The October 2025 episode shows the cost when the search is skipped [P].

Used in: 08.4, 08.5, 11.3, 11.4 (portfolio and escalation), 12.1 to 12.5, 17.5 (the novelty check), 21 Q-09 and Q-12.

1.7 Knowledge sources, indexes and standards

Sources

Used in: 09.2, 09.3 (the licence classes), 16.6, 18.2, 18.4, 21 Q-03.

Other people's indexes

• TheoremSearch (UW) [P]. https://arxiv.org/abs/2602.05216
  • 9.2M theorems from about 690k papers.
  • The release has only the permissive subset: 1.34M statements with "slogans".
• TheoremGraph (June 2026; arXiv:2606.25363) [P]:
  • 11.7M arXiv statements and 18.3M candidate dependency edges.
  • LeanGraph: 388k declarations and 11.3M edges over 25 Lean projects.
  • 47,952 informal–formal matches accepted by an LLM judge.
  • It is available over HTTP and MCP.
• Matlas [P]. https://arxiv.org/abs/2604.17484
  • 8.07M statements from 435k journal papers and 1.9k textbooks.
  • Each statement is "unfolded" so that it stands alone. It has an API.
• Alignment data [P]:
  • Herald: 580k Mathlib statements informalized and 44k NL–FL pairs (arXiv:2410.10878).
  • MathGloss: an undergraduate concept graph mapped to Wikidata, nLab and Lean (arXiv:2311.12649).
• Formula search [P]:
  • zbMATH uses MathWebSearch. It holds more than 160M formulae, but its last release was in 2014.
  • Approach0 and Tangent-L led ARQMath.
• Embedding benchmarks [P]:
  • MIRB: voyage-3-large is best, at an average nDCG@10 of 54.54. Rerankers often hurt (arXiv:2505.15585).
  • SABER-Math and MathLeap also exist.

Used in: 05.3, 09.5 (the unfolding step), 09.6, 14.2, 14.4, 14.7, 17.3.3.

Representation standards and extraction

• MathML 4 is still a Working Draft. MathML Core became a Candidate Recommendation in June 2025. The intent attribute is the main addition in MathML 4 [P]. https://www.w3.org/TR/mathml4/
• OpenMath 2.0 (2019) shows no activity in 2025-26 [P].
• sTeX4 has three parts: RusTeX, which turns LaTeX into semantic FTML; the FLAMS backend; and MathHub archives [P].
• PDF to LaTeX [P]:
  • OmniDocBench v1.6 Formula CDM: PaddleOCR-VL-1.6 97.53, MinerU2.5-Pro 97.45, GPT-5.2 88.21.
  • olmOCR-Bench: Chandra 2 85.8.
  • The Mathpix bulk Files API costs $0.0015 per page.
  • https://github.com/opendatalab/OmniDocBench ; https://mathpix.com/pricing/api
• Theorem extraction corpora [P]:
  • TheoremKB / TheoremView work from PDFs.
  • NaturalProofs: 32k theorems with proofs.

Used in: 04.5 (Markdown plus LaTeX, not MathML, as the source format), 09.5, 09.8.

Identifiers

• Stacks and Kerodon tags are opaque, permanent and never reused. A removed result keeps its tag with an explanation [P]. https://stacks.math.columbia.edu/tags. This is the model for math2's tags (04.3).
• Mathlib names become deprecated aliases and disappear after about 6 months. Wikidata P14534 links point to name searches, so they will rot [P].
• SWHID became an ISO standard, ISO/IEC 18670:2025, on 23 Apr 2025 [P]. https://www.swhid.org/
• Other stable keys [P]: arXiv DOIs (10.48550), Zenodo DOIs, MR and zbMATH IDs, OEIS A-numbers, LMFDB labels and knowls, π-Base UIDs, GAP IdGroup, ETC X(n), the graph6 canonical string (content-addressed), Erdős problem numbers, and Palomar IDs.

Used in: 04.3, 04.4, 05.3 (time-scoped aliases), 06.3.

1.8 Collaboration, norms and governance

Tao's framing

• "Math 2.0" (Caltech/AIM lecture, 9 Oct 2026) [P]. https://terrytao.wordpress.com/2026/10/10/math-2-0/ ; slides https://teorth.github.io/tao-web/slides/math-2-0-caltech-2026.pdf
  • Mathematics was built for a time when proofs were scarce. The bottlenecks are now verification, exposition, attribution and understanding. In his words, "the primary bottleneck … is imagination".
  • "Further blind optimization of problem-solving alone is now actively harmful to the long-term health of mathematics."
  • AI capability is "jagged". Thus assessments should report resource use and negative results.
  • Proposals: open exposition problems, living networks (IEANTN), large formal libraries, ablation studies, exploring "the neighborhood of a theorem", open and interpretable math models, interactive synthesized texts.
• His other positions [P]. https://teorth.github.io/tao-web/ai-views.html
  • ICM 2026 essay (arXiv:2608.16753): it has a section on the disclosure of tools and compute. It also says: do not publish a result that you could not give an expert talk on.
  • Prefer "red team" uses of AI.
  • Priority goes to the first public exposition (Aug 2026).
  • Some AI proofs are "up for adoption".

Used in: 02.2 (the bottleneck table), 02.3 (problems solved is not an axis), 12.5, 12.6, 16.4.

How collaborative projects worked

• Equational Theories Project (arXiv:2512.07087) [P]:
  • More than 50 contributors on Zulip.
  • Contributors claimed tasks by comment. CI allowed one claimant per task, and CI drove a kanban board.
  • Every PR had to pass the Lean build plus lean4checker/lean4lean. native_decide was banned.
  • Of about 8.18M true implications, only about 10,657 needed direct proofs.
  • ATPs did most of the work. Humans built the hard counterexamples and owned the specification. LLMs had a minor role.
  • Lessons: appoint maintainers before launch, spread across time zones; plan the file layout; check Mathlib first.
• SAIR competitions [P]: the Distillation Challenge (ETP cheat sheets gave open models a 30 to 40% boost); IGP24 with the LMFDB (all of about 25,000 transitive groups of degree 24 realized over Q).
• erdosproblems.com policy reset (Bloom, 6 Oct 2026) [P]. https://www.erdosproblems.com/forum/thread/blog:9
  • Proof claims and comments are paused. The site no longer shows statuses and solve counts.
  • Write-ups must come from humans. Authors must disclose AI use.
  • Lean formalizations should go to Palomar.
  • "The site should help the Erdős-community of humans flourish."
• The AI-contributions wiki (frozen 30 Jun 2026) [P]. https://github.com/teorth/erdosproblems/wiki/AI-contributions-to-Erd%C5%91s-problems
  • It sorts contributions into these classes: 1(a) AI solution with no prior literature; 1(b) literature later found; 1(c) building on literature; 1(d) with humans; 2(a) literature search; 2(b) formalization; 2(c) rewriting; 2(d) computation.
  • It warns about selection bias. It also warns against the confusion of obscure problems with hard ones.
  • A snapshot counted 538 contributions across 405 problems from 70 systems [S].
• Mathlib review at scale (1.2). The MathlibPR benchmark shows that LLMs are poor judges of merge-readiness (arXiv:2605.07147) [P].

Used in: 13.6 (claims and threads), 16.3, 16.5 (the human-role taxonomy), 21 Q-10 and Q-11.

Declarations, bodies and policies

• Leiden Declaration on AI and Mathematics (2 Jun 2026) [P]. https://www.universiteitleiden.nl/en/news/2026/06/leiden-declaration-warns-ai-is-challenging-the-core-values-of-mathematics
  • Disclose AI use, keep work independently verifiable, keep humans responsible.
  • 1,000+ signatories on day one.
  • The IMU endorsed it in Circular Letter 8/2026. ICARM also endorsed it.
  • The count of 23 recommendations is [S].
• "A Severe Misalignment of AI in Mathematics" (11 Sep 2026; Zenodo 10.5281/zenodo.22737750) [P]. https://mathandai.org/
  • About 25 to 28 people signed it, mostly Fields medalists.
  • Concerns: attribution, plagiarism, and incentives that favour problem-solving over understanding.
• AGMAI (announced 21 Sep 2026, hosted at IAS; Charles, De Lellis, Gowers, Hairer, Srivastava, Tillmann, Vakil, Witten, Wood) [P]. https://terrytao.wordpress.com/2026/09/21/advisory-group-on-mathematics-and-artificial-intelligence/
  • Guidelines of 29 Sep (https://agmai.org/general-sep29/):
    • stop testing advanced problems only on proprietary models;
    • publish the model, prompts, a summarized chain of thought, time and compute cost;
    • document failed attempts and how problems were selected;
    • post to lab-independent repositories with persistent IDs;
    • cite the literature and rewrite in conventional style;
    • formalize with Comparator challenge files and formalization.yaml, with machine-readable NL↔formal links, or state the formalization status;
    • independent nonprofits should decide funding for human understanding.
  • OpenAI's 6 Oct release complied only in part. About 10 of 719 manuscripts had traces, and there was no NL↔formal metadata [S].
• AHM, the Association for Human Mathematics (founded ~10 to 12 Sep 2026) [P]. https://www.ahmath.org/statements
  • Members do not work with commercial AI companies and do not publish AI-generated text. Full abstention from AI is optional.
  • Its 7 Oct statement on the OpenAI release is on Tao's blog, but Tao did not write it. It reads: "Releasing over 700 files at once is not a demonstration of scholarship, but a demonstration of power." https://terrytao.wordpress.com/2026/10/07/ahm-statement-on-openais-october-6-release-of-mathematical-documents/
• Journals and societies [P]:
  • LMS: every manuscript needs an "AI Declaration" section. https://www.lms.ac.uk/publications/policies/AI
  • Elsevier: an AI declaration is required, and AI cannot be an author.
  • CSIAM: policy from 1 Aug 2026.
  • No formal AMS journal policy was found [U].
• arXiv [P]:
  • CS review and position papers need prior peer review (31 Oct 2025).
  • Endorsement rules became stricter across all of arXiv from 21 Jan 2026.
  • A one-year ban for unchecked AI content (May 2026). https://techcrunch.com/2026/05/16/research-repository-arxiv-will-ban-authors-for-a-year-if-they-let-ai-do-all-the-work/
  • The English-version requirement and the nonprofit status are [S].
• Hexagon (https://hexagonmath.org/; Aug 2026) [P]:
  • A screened repository for AI-era mathematics and theoretical CS.
  • It uses the provenance labels "human-written text" and "human understanding".
  • IDs have the form hexagon:2610.00244, and there is an API.
  • It hosts the First Proof Batch 3 paper.

Used in: 02.2, 16.5 (items 7 to 9: disclosure via m2 prov disclose, the role taxonomy, agents: none), 17.5, 21 Q-10 and Q-17.

1.9 Evaluation and benchmarks

• First Proof (https://1stproof.org/; research problems not yet published, so uncontaminated):
  • Batch 1 (Feb 2026): public runs produced confident proofs of everything, but only about 2 were correct [S]. Aletheia claimed 6/10 (experts disagree on #8) [P].
  • Batch 2 (Jun 2026; arXiv:2606.18119): the organizers ran the systems themselves, with blind double refereeing. 17 of 39 outputs passed. The cost per system was $117 to $4,799 [P].
  • Batch 3 (results 14 Oct 2026) [P]. https://1stproof.org/third-batch-press-release.html
    • Each system had 24 h with no human input. About 30 referees at ICARM graded the outputs double-blind, with negative marking. They graded correctness, exposition and attribution.
    • ProofCouncil (GPT-6 Astra base) 9/10 for $1,888; GPT-6 Astra used directly 7/10 for $36; an open-weight Kimi K3 harness 0/10 for about $2,000.
    • Citations were adequate in 7/10 cases (ProofCouncil) and 4/10 cases (direct). Exposition was weak.
    • The release warns that "access to computational resources may become a barrier for basic research".
    • Batch 4 is planned for January 2027.
  • Governance: board members may not take paid AI-company work.
• FrontierMath successors [P/S]:
  • Open Problems: 50 problems by July 2026, 3 solved by AI.
  • FrontierMath Erdős (arXiv:2609.25050): 68 open problems stated in Lean, $300 per problem, comparator in Docker with no network. GPT-6 Astra solved 3%, and every other model solved 0% [P].
  • OEIS Open: see 1.6.
• Contamination-resistant sets [P/S]:
  • RealMath: 633 items mined from arXiv, refreshed monthly (arXiv:2505.12575).
  • LemmaBench and IMProofBench.
  • MathArena's live competitions and ArXivLean.
  • Formal-conjectures' frozen snapshots.
• How reliable LLM judges are:
  • Open Proof Corpus (arXiv:2506.21621) [P]: human graders agreed with each other 90.4% of the time. A GPT-5 judge reached 90.8%.
  • On proofs from AI pipelines, the false-positive rate of graders is 31.7% (arXiv:2602.16793) [P].
  • The minimum over several judges reduces overestimation (Nemotron-Cascade 2, arXiv:2603.19220) [P].
  • IMO-ProofBench's autograder correlates with humans at 0.96 on public models, but at 0.87 across 170 internal systems [P].
  • The co-mathematician paper warns of a "reviewer-pleasing bias" [S].
  • Conclusion: judges are good enough for triage. Claims need a kernel, or blind human refereeing.

Used in: 12.9, 17.3 to 17.8, 21 Q-16.

1.10 Funding and institutions

Used in: 16.7, 19 (costs).

1.11 Key dates

1.12 Unverified, contested, or in conflict

math2 does not use any of these for a design decision.

• Lean:
  • whether comparator issues #68 and #85 are fixed;
  • Mathlib's written deprecation policy;
  • Moogle's live status;
  • why the 100-theorems counts differ (100 on the community page against 83 on Wiedijk's list).
• Other systems: whether Isabelle2026 and AFP-2026 are released; the sizes of set.mm, 1Lab and agda-unimath.
• Licences: the licences of nLab, Kerodon, FindStat, MaRDI and DaRT are unknown. Until they are checked, math2 treats each as record class (09.3).
• MSC: the exact count of MSC2020 codes, and any MSC2030 plans.
• Benchmarks:
  • the official IMO confirmation of the Celia and dots-note 42/42 scores;
  • whether Google, OpenAI, Seed or Harmonic entered IMO 2026;
  • GPT-6.1 Sol at 100% on FrontierMath Tier 4 v2 (aggregators only);
  • the other 672/672 PutnamBench claimants;
  • miniF2F saturation beyond the vendor claims.
• Line counts: reports give 120K, about 200K and 450K lines for Gauss's dimension-24 work.
• openai/math: the Lean-formalized share (42% against 24 to 36%), and 372 against 377 result families.
• Conflicting reports on First Proof:
  • Batch 2: the Batch 2 paper credits ProofCouncil with 6 problems, but the Batch 3 press release says 7.
  • Batch 1: reports give OpenAI's claim as 5 and as 6 "likely correct". The second figure came with expert feedback that broke the rules.
• Under scrutiny: Hopf/S⁶, cycle double cover, Crouzeix and Borsuk-63 have only secondary sources.
• Navier–Stokes: the cost figures, and the bribery and threat allegations.
• People: Scholze's AHM membership, and Tsimerman's move to OpenAI.
• arXiv: the English-version requirement and the nonprofit status.

1.13 What math2 takes from this

Markdown · Source · Edit