Math 2.0: specification

Math 2.0 is a versioned, executable, verifiable and navigable knowledge system for all of mathematics. It has four parts:

• a knowledge graph of concepts, statements, proofs, objects and problems;
• a formal engine and a computational engine, which make claims checkable;
• AI research agents, which extend and maintain the graph under human review;
• a workspace, where people search, explore, explain and collaborate.

Two repositories hold the work. This follows the tamnd/arxiv pattern:

The date of this specification is 2026-10-25. Document 01 is its evidence base. Document 01 gives the state of the field on that date.

Documents

The corpus sub-spec

The directory corpus/ holds the corpus sub-spec, K00 to K15. It says how math2 gets each definition, theorem, proof and example from public sources and from what models know, and how each node becomes ready for a course, a book or an article. It adds to this spec and changes it in the places that its README lists. Its phases P0 to P5 come after the milestones of document 19.

Reading order

• Overview, in about 20 minutes: 02, then 03, then 19.
• Content contributors: 04, then 05, 10 and 16.
• Toolchain implementers: 03, 04, 05, 06 and 07, then 11, 15 and 20. Then 08, 09, 12 and 14 as necessary.
• Agent work: 11, 12, 10 and 17.
• Reviewers of the design: 01 first, then 15 and 21. 01 is the evidence. 15 and 21 show where the design could be wrong.

The diagram, box by box

The architecture diagram has eight boxes. This table gives the location and the specification of each box:

Three supporting parts apply across all the boxes: search (14), autoformalization and fidelity (10), and the audit (15).

Settled decisions

These decisions are settled. To change one, open a PR to this file. Link the PR to a measurement or an incident that shows the decision is wrong. Undecided items are in 21. When an open question in 21 is settled, move it here with its PR link.

Architecture (03.5)

1. Files in git are the truth. Every database, index, embedding and site is derived from these files. Each of them can be rebuilt (05.1, 06.1).
2. Status is computed, never asserted. No one, person or agent, writes an evidence level. The build derives it from the evidence (04.7).
3. Only the kernel and certificate checkers referee E4 and E5. Models produce candidates, never verdicts. LLM judges triage. They never raise status (15.1).
4. Fidelity is a separate axis. Each F-level is bound to the type hash of the Lean statement. Only people raise an F-level to F2 or above (04.7, 10).
5. Every byte has provenance. Every agent run has a run record and a responsible person or schedule (06.5, 11.6).
6. Tags are permanent. A tag is never reused or deleted. Retirement keeps the tag and points to its successor (04.3).
7. Every write is a pull request, and the audit is the gate. The API has no other write path (11.1, 15).
8. Each release pins everything: the Lean toolchain, the Mathlib tag, container image digests, model ids and prompt versions (06.2).
9. Link, do not copy. math2 holds external records as locators and metadata only, unless the licence allows more (16.5, 16.6).
10. There is one URI space, m2://, and it is inside the ant URI space (04.4).

Formal stack (07)

11. Releases are calendar-versioned YYYY.MM. A release is cut each month. Patch releases are YYYY.MM.N. Each release pins a Lean stable release and one compatible Mathlib revision. This revision is normally its v4.X.Y tag (06.2, 07.1).
12. The Math2 Lean package uses the module system only (07.2).
13. Proofs are checked by lake check --paranoid, plus comparator against the bound statement, plus math2's own type-hash check. Each E5 result records the checker versions (07.7).
14. Axioms are limited to propext, Quot.sound and Classical.choice. A proof that uses native_decide or implemented_by is not E5. At best it is E4 under a named axiom class (07.5).
15. Lean declaration names are time-scoped aliases, not identities (05.3).
16. Defer to Mathlib and do not duplicate it. Send general-purpose material upstream. math2 holds the bindings and the material that is out of scope for Mathlib (07.3, 16.5).

Content and licences (16.6)

17. There are three licence zones: prose CC BY-SA 4.0, code Apache-2.0, metadata CC0.
18. Source rules:
    • Link GFDL sources (the Stacks Project). Never copy them.
    • For arXiv papers under the default licence, store only metadata and locators.
    • Do not store MSC descriptions (CC BY-NC-SA).
    • Take Stack Exchange content per post through the API, with attribution.
19. No raw embedding vectors are served (14.4). The API returns neighbours and scores. It is still open whether embeddings of open-class text can ever be published. This is 21 Q-14.

Agents and process

20. Agent PR volume is capped by measured review throughput (11.5).
21. Novelty verdicts are never "new". The best verdict for an explore claim is "no prior result found by the documented search" (17.5).
22. No autonomous target selection for research. People choose explore targets and campaigns. Agents rank within them (12.5). 21 Q-10 asks whether to relax this rule later. Until then, this rule applies.
23. Node count is not an axis of progress. Problems solved is also not an axis. The axes are in 02.3.
24. Disclosure is generated, not written by hand. m2 prov disclose produces AGMAI-style disclosure text and Palomar formalization.yaml from run records (16.5).

Conventions

• Section references have the form 07.7 (document 07, section 7), 05.6 Q5 (a numbered query) or 21 Q-11 (an open question).
• Tags are 6 characters of Crockford base32 (0-9 A-Z without I L O U), for example 7K3QX2. Tags that start with 0 belong to the M1 seed. A provisional id is ~ followed by 8 hex characters (e.g. ~3fa94c01). Use a provisional id only before merge. The merge bot rewrites it to a tag (04.3).
• URIs have the form m2://TAG, m2://[email protected] (at a release), m2://TAG@<commit> or m2://TAG#formal (a section). Aliases such as m2://concept/compact-space or m2://lean/<decl> resolve to tags. Never store an alias as a reference (04.4).
• Evidence levels:
  • E5 kernel-checked
  • E4 certified computation
  • E3 refereed
  • E2 standard
  • E1 claimed
  • E0 open
  • E⊥ refuted
• Fidelity levels: F0 bound but unchecked; F1 passes the machine battery; F2 one human review of this exact statement hash; F3 two independent reviews, or a second independent formalization proved equivalent (04.7, 10).
• Coverage levels: C0 to C4 (18).
• Model ids: claude-haiku-5-5, claude-sonnet-5-5, claude-opus-5-5 and claude-fable-5-1, plus open-weight provers. Each release pins all of them (12.3).
• Confidence tags in 01: [P] primary, [S] secondary, [U] unverified.
• Normative language: "must" and "never" state requirements. "Should" states the default. Do something different only for a documented reason. Measurements tune the numbers marked as targets. These numbers are not promises.

Note on inputs

The original request referred to two images. Only the second image arrived. It is the eight-box architecture diagram. This specification follows that diagram exactly (03.1). If the first image showed something that this specification does not cover, raise it as a new item in 21.

Markdown · Source · Edit