Math 2.0

Math 2.0: the corpus specification

The main spec (the files 00 to 21 in the parent directory) says how math2 holds, checks and serves mathematics. This sub-spec says how math2 gets the mathematics: each definition, theorem, proof and example that a person can find in a public source, and what models know, as nodes that people can read and machines can check, ready to go into a course, a book or an article (K2.1).

The corpus sub-spec adds to the main spec and changes it in a small number of named places. Where the two disagree, this sub-spec is the newer text, and the change is listed in "Changes to the main spec" below. The main spec files are not edited by this sub-spec. A change becomes part of them in the same pull request that implements it.

This sub-spec was written on 2026-10-26. Its evidence base is K01, which reflects the sources as of that date.

Documents

# Document What it settles
00 README (this file) index, reading order, settled corpus decisions, conventions, the rules that the corpus adds
01 Research the method, the findings that change the plan, the corrections to the main spec, what could not be verified
01a Part A: reference works encyclopedias, wikis, databases, problem lists and Q&A sites: sizes, licences, channels
01b Part B: literature and books literature indexes, full text, extraction projects, open textbooks, syllabi, theorem lists
01c Part C: formal libraries formal libraries, translation between systems, formal and informal datasets
01d Part D: model generation error rates, projects at scale, memorization, the law on model output, provider terms, cost
01e Part E: representation and packaging formats, levels of explanation, exercises, book and course formats, notation
02 The goal the goal in one sentence, items, writing levels W0 to W3, formal outcomes, what the corpus must not do, the reference scale
03 Identifiers tags of ten characters, the check character, sharding, one space for nodes and inventory rows
04 The inventory mentions and rows, clustering, outcomes, which declarations and objects become nodes, measuring what is missing
05 Human sources the source document, licence reading, public domain, reference works, textbooks, literature, curricula, exercise banks, adapters, import order
06 Formal sources intake classes, the libraries, Mathlib, libraries that AI wrote, other systems, crosswalks, datasets, informalization
07 Machine generation what models are for, the four new roles, generation from what models know, the write job, the model register, configurations, provider terms
08 The node card the house style, front matter, the card of each kind, proofs in steps, explanations at levels, exercises, schema changes
09 Quality the gates before merge, sanity checks, the copy check, source confirmation, what people check, sample audits, reader reports
10 Structure and notation the taxonomy, curricula, the notation register, conventions, names and languages
11 Packaging the volume file, linearization, editorial text, outputs, the pack check, licence, editions, the Lean companion
12 Pipeline and operations the stages of an item, jobs, priority, batches, review capacity, cost, measurement, commands and libraries
13 Law and ethics the three zones, copyright in model text, copies, human sources, the EU AI Act, provider terms, disclosure, questions for a lawyer
14 Roadmap phases 0 to 5 with entry and exit criteria, what runs all the time, the people that the phases need
15 Open questions OQ01 to OQ60, each with the way to settle it and the phase that it blocks

Reading order

  • Overview: K02, then K14, then the settled decisions below.
  • Before an importer is written: K05 or K06, then K04, K13 and K15.
  • Before agents write nodes: K07, K08 and K09, then K12.
  • Before a volume is built: K08, K10 and K11.
  • Reviewers of the design: K01 first, then K09, K13 and K15. K01 is the evidence; K09, K13 and K15 are where the design could be wrong.

How the corpus relates to the main spec

The corpus uses the objects of the main spec and adds no new box to its architecture:

The corpus needs The main spec gives The corpus adds
a place for each item nodes and kinds (spec 04) the inventory as a register of rows (K04), the exercise node (K8.7)
sources the record plane and licence classes (spec 09) the source document, licence reading, the public-domain rule (K05), intake classes (K06)
writers agent roles and run records (spec 11, 12) four new roles, the model register, generation from what models know (K07)
checks the audit and the status levels (spec 15) the copy check, source confirmation, sample audits, new rules (K09)
readers the workspace and explanations at levels (spec 13) the node card (K08), the notation register (K10), volumes and the pack check (K11)

Settled corpus decisions

These decisions are settled. A change to one of them is a change to this file and to the document that it names, in one commit, with the reason.

  1. Tags have ten characters. Nine random characters and one check character, from Crockford base32. The tags of six characters that exist are frozen and stay valid (K03).
  2. Nodes and inventory rows share one identifier space. A row identifier is never a node tag (K3.6, rule T08).
  3. The inventory is the denominator. The corpus is complete when each row has an outcome. The open count is the number of rows with no outcome, and its target is zero (K04).
  4. No row from models alone. A mention that a model gave becomes a row only when a source that people wrote confirms it (rule I03).
  5. The licence class decides what the corpus takes from a source. Only open text enters the prose zone. share-alike-nc, gfdl and record give records, locators and links. verbatim gives short quotations only (K5.1, K13.4).
  6. The licence is read at the source. An aggregator does not change a licence. The licence is read again at each snapshot, and the reading has a date and a person (K5.2.1).
  7. Public domain means the US and the EU. A work is open as public domain only if it is in the public domain in both (K5.2.3).
  8. Each formal library has one intake class: bind, crosswalk, link, evaluate or exclude (K6.2). Benchmarks evaluate roles; they are not sources (K6.8).
  9. Models write; they never decide what is true. Models never raise a status, and a judge is of a family other than the writer's (K07, rule X09). This keeps settled decision 3 of the main spec.
  10. The copy check runs against a reference corpus, not only against the cited sources. No restricted text is in the context of a write job (K9.4, K7.5).
  11. The prose zone stays CC BY-SA 4.0, with a notice that the licence applies only where copyright subsists. The provenance says which sections software wrote (K13.2). This keeps settled decision 17 of the main spec.
  12. The exercise is a node. Its text is in the prose zone. Its Lean statement and its reference solution are in the code zone, Apache-2.0 (K8.7, K13.1).
  13. One notation register. Each macro has one meaning in its scope, and the LaTeX macros and the KaTeX map are generated from the register (K10.4).
  14. A volume adds no mathematics. Each definition, statement, proof and example in a volume is a node, and glue states no mathematics (K11).
  15. Review capacity sets the speed. Agent work is capped by what people can review, not by the cost of the models (K12.5).
  16. Phases have entry and exit criteria, not dates (K14).

Conventions

  • Numbering. Corpus documents are K01 to K15, and their sections are K2.1, K2.2 and so on. A reference to "spec 09" or "spec 9.3" is to the main spec. A reference to "settled decision 17" is to the list in the main README.
  • Rules. A rule has an id in the families of the main spec 15, and H (hard: the audit fails) or S (soft: the audit reports). The rules in this sub-spec are proposed. They become part of the audit when m2 audit implements them, and the main spec 15 lists them in the same pull request.
  • Not settled. Where the sources disagree or a fact is not known, the text says "not settled" or names the question in K15, and it takes the safe course (K15.1).
  • Facts and dates. Each fact from the research has a URL and the date of reading in K01. A figure that a later reading changes is changed in the corpus document and in the part of K01, in the same commit (K1.6).
  • Style. The text follows ASD-STE100 Simplified Technical English.

Rules that the corpus adds

Rule H/S Checks Where
T06 H changed: a tag has six or ten characters K3.8
T08 H the tag register and the inventory register have no value in common K3.6, K3.7
T09 H each tag of ten characters has a valid check character K3.7
T10 H no tag of six characters is minted after the cut-over commit K3.7
I01 H each inventory value in a node points to a row whose outcome is node or member with the tag of that node K4.9
I02 H each row with the outcome node or member points to a live node, or to a retired node with a successor K4.9
I03 H no row has only mentions from models K4.9
I04 H each outcome that a rule gave names a rule in schema/outcomes.v1.yaml K4.9
I05 S a deferred row whose date has passed K4.9
I06 S an MSC code at two digits whose estimated recall is below 90% K4.9
L05 H each agent-written body has a clean copy check result. Soft until the calibration is done K9.9
L06 H each item from a source with a licence for each item records the licence of the item K13.9
L07 S a node with a takedown report older than two working days that is not quarantined K13.9
L08 H each source document has the required fields, and each mention names a source K5.14
L09 H a source with a choice of licences has an election K5.14
L10 H a public-domain source of the open class is public domain in the US and the EU K5.14
L11 H a mention with text comes from a snapshot whose licence was read on or before the snapshot date K5.14
L12 S a source whose licence was last read more than twelve months ago K5.14
F10 H each mention from a library records the library, the pin, the declaration, the intake class and the licence of the item K6.12
F11 H no section holds text from a library of class link, evaluate or exclude, or from an item whose licence is not open K6.12
F12 H each library source document has authored, and each mention copies it K6.12
F13 S a binding to an ai or mixed declaration whose F2 review does not cover the definitions that its statement uses K6.12
P05 H each source that an agent added resolves to a record, and the record matches the claim K9.9
P06 S a source with locator_unconfirmed older than 180 days K9.9
X05 H an agent-written statement or proof has the results of the sanity checks in its run record K9.9
X06 S a stratum whose error rate is near its threshold K9.9
X07 S a theorem that a body names that resolves to no node and has no source K9.9
X08 H each field that an agent wrote names a model in the model register K7.10
X09 H each judge verdict is from a model of a family other than the writer's K7.10
N01 H each macro in a body has a register entry in scope, or the node defines it K10.7
N02 H two entries with the same glyph in overlapping scopes are the same macro, or list each other in conflicts K10.7
N03 S a curriculum puts a member before one of its prerequisites K10.7
N04 S a node uses a non-default option of a convention and does not say so K10.7
N05 S a concept with no specializes edge and no topic other than its MSC code K10.7
N06 H each macro has one denotes, and the macro files are the output of the register K10.7
N07 S a symbol in a notation field that no register entry has as introduced_by K10.7

The pack check of a volume (PC1 to PC10, K11.6) is not an audit rule. It runs when a volume is built, and a volume that fails it is not published.

Changes to the main spec

Main spec Change Where
00, 04.3, 04.4, 04.5, 05.1, 06.4, 06.7, 15.3, 20.1 tags of ten characters, the shard key, the inventory register; rules T08 to T10 K3.7
04.9 the new edges, sections and fields of node.v1; the exercise kind in node.v2 K8.9
1.7, 9.2, 9.3, 9.6, 16.6 figures and licences of sources, including Kerodon as record K1.4, K5.13
1.7, 9.4 figures of formal libraries K6.11
9.1 adapters are importer/<source> K5.11
12 the roles enumerate, write, informalize and exercise K7.3
15 the rules above this file
16.6 the zone of the Lean part of an exercise is the code zone K13.1

Markdown · Source · Edit