math2-agent

README

math2-agent

This repository holds the toolchain and the research agents for Math 2.0. The content is in tamnd/math2.

Math 2.0 is a versioned knowledge graph of mathematics. The m2 command reads the node files in math2. It builds the Lean library, computes the status of each node, makes the graph and checks each change with the audit rules. Later milestones add search, an API, an MCP server, a research workspace and AI research agents.

Specification

The design is in spec/. It has 22 documents, 00 to 21. Issues, code and reviews refer to a section by its number, for example 04.5 or 15.3 S03.

The wiki at https://tamnd.github.io/math2 shows the spec, the milestones and each node.

Status

The project is at milestone M2. Release v0.1.0 closes the code of M0: m2 new, m2 fmt, m2 check, m2 mint and m2 site build are written. In M1, m2 audit runs the rules T01 to T06, S01 to S04, S09, B01 to B05, G01 to G10, F01 to F09, V01 to V04, R01 and R02. The rules G04, F01 to F05 and F07 to F09 read the files in build/ from the last m2 build. A rule skips when a file that it needs does not exist. The graph package derives the graph from the node files, with the AND-OR closure of spec 05.5, the CSR adjacency and the Parquet build format. The lean package drives M2Extract, a small Lean program that gives the type hash, the axioms, the formal dependencies and the deprecation of each bound declaration. It also runs the checks for degenerate statements of spec 10.4 on each bound theorem. m2 build runs lake build, runs M2Extract on each binding, replays each binding that needs it in six kernels, computes the status of each node and writes the graph, with a cache for each step. The status package computes the evidence level, the fidelity level and the flags of spec 04.7, and m2 status shows them. A review counts only when its reviewer has a record in registers/reviewers.reg and did not write the binding. F3 needs two reviewers with no shared affiliation. The release package makes the release manifest of spec 06.2 from a tree and its last build. It rebuilds the graph of a release from its commit (rule R01), and it rebuilds the .olean files and lists each file that is different (rule R02). m2 release cuts a release, writes its notes and verifies it, and the rules R03 to R05 check the notes, the restore drills and the pins. The first work of M2 is written: the store package puts the graph and the status of each node into one SQLite file, and m2 graph runs the neighbourhood, closure, reverse dependency, learning path and frontier queries on it. The synth package and bench/graph measure these queries on a synthetic graph. The ingest package and m2 ingest get pinned snapshots of external sources, apply the licence gate of spec 09.3 and write the records. The adapters of arXiv, zbMATH Open, Mathlib, the OEIS, Wikidata, the LMFDB, the Erdős problems, formal-conjectures, Palomar and the Stacks Project are written. The rules L01 to L04 check the licences. Rule A01 checks that each same_as id has the syntax of its system, with the crosswalk package. The align package and m2 align propose same_as, close_to and aligned edges to the records of a source, and a person accepts or rejects each proposal. The rules A02 to A04 check these edges over time. bench/align measures the precision and the recall of the aligner on labelled pairs. The bump package and m2 bump move the tree to a newer Mathlib release on a new branch. The report shows each other rule of spec 15.3 with the state skip and the reason "not written yet". m2 help shows the milestone that delivers each command. A command that is not written yet exits with code 3 and names its milestone. It does not exit with code 0, because a command that does nothing and exits with code 0 looks like a command that worked.

Milestone	Dates	Result
M0, the skeleton	Nov to Dec 2026	Both repositories, the node schema, m2 new, m2 fmt, m2 check and the public wiki.
M1, the seed and the trust core	Jan to Mar 2027	About 2,000 seed nodes, m2 build, m2 audit, the checker stack and release 2027.03.
M2, the graph meets the world	Apr to Jun 2027	External sources, alignment, the monthly Mathlib bump and monthly releases.
M3, open to readers	Jul to Sep 2027	Search, the read API, the MCP server, the workspace and the computational engine.
M4, fidelity at scale	Oct to Dec 2027	The review tool, statement autoformalization and write access through the API.
M5, the research engine	Jan to Jun 2028	The research agents, the orchestrator, budgets and the weekly agent report.

Each milestone has a tracking issue with the label milestone. The tracking issue has the exit criteria and a list of sub-issues.

Install

You need Go 1.27 or later.

go install github.com/tamnd/math2-agent/cmd/m2@latest

You can also download a binary from the releases page. Each archive has a build provenance attestation. To verify an archive, run this command:

gh attestation verify m2_v0.1.0_linux_amd64.tar.gz --repo tamnd/math2-agent

Commands

Command	What it does	Milestone
m2 new <kind>	Make a node file with a provisional id.	written
m2 fmt	Make front matter canonical and change aliases to tags.	written
m2 check	Check schema, body and links on the working tree. This does not use Lean.	written
m2 mint	Change the provisional ids to tags before merge, and add the tags to registers/tags.reg. m2 mint -seed gives tags that start with 0 to the nodes of the M1 seed.	written
m2 site build	Build the wiki: a static site for people and agents.	written
m2 build	Build the derived data: Lean, extraction, replay, status, graph and store. Search comes later.	written
m2 audit	Run the audit rules and write the report to reports/.	written
m2 status <tag>	Show the computed status of a node and the evidence for it.	written
m2 graph	Run a graph query: neighbourhood, closure, reverse dependencies, path or frontier.	written
m2 ingest <source>	Get a pinned snapshot of an external source and write its records. -snapshot HASH uses a recorded snapshot again.	written
m2 align <source>	Propose crosswalk edges to an external source. m2 align queue, accept, reject and confirm show the proposals and record the decision of a person.	written
m2 bump	Make a branch that moves Lean and Mathlib to the next release, rebind the renamed declarations and write the bump report.	written
m2 release	Cut a release with its manifest, levels and notes, write the release notes, or rebuild a release from its manifest.	written
m2 search <query>	Search the knowledge graph.	M3
m2 serve	Serve the API, the MCP server and the workspace.	M3
m2 compute	Run or verify a computation.	M3
m2 prov	Show or change provenance.	M3
m2 review <tag>	Review a formal statement against its informal statement.	M4
m2 autoform <tag>	Make a formal statement for a node.	M4
m2 agent run <role>	Do one agent run.	M5
m2 orchestrate	Run the job scheduler.	M5

The wiki

m2 site build makes the wiki at https://tamnd.github.io/math2 from a math2 working tree and the spec. The math2 repository runs it on each push to main and each night, and GitHub Pages serves the result.

go run ./cmd/m2 site build -content ../math2 -spec spec -out _site
python3 -m http.server -d _site 8000

Each node gets a page with an infobox, its links and its backlinks. KaTeX renders the math in the browser with the macros of math2. Each page also has a copy for programs: node/<TAG>.md, api/node/<TAG>.json, api/nodes.json, llms.txt and llms-full.txt. A build with no -date flag gives the same bytes each time.

To preview the site with the local server above, set -url http://localhost:8000.

The build

m2 build makes the derived data of a math2 working tree in build/. Run it in the root of the tree. It needs elan for the Lean steps.

m2 build                # all the steps
m2 build -only lean     # only lake build
m2 build -json          # write the manifest as JSON
m2 build -no-sandbox    # run the checkers without the sandbox, for example on macOS

The steps are lean, extract, replay, status, graph and store. The lean step gets the Mathlib cache and runs lake build in lean/. The extract step runs M2Extract on each formal declaration and adapter that a node names, and on each declaration with the attribute @[m2 "TAG"]. It writes build/extract.json. The replay step checks each binding that passes each check of E5 except the replay, and writes build/replay.json. The status step computes the evidence level and the fidelity level of each node from the nodes, build/extract.json, build/replay.json and the reviews in reviews/, and writes build/status.json. The graph step writes the graph as Parquet to build/graph/. The store step writes the graph, the status of each node and the aliases to the SQLite file build/store.db, for m2 graph. A tree without lean/ has only the status, graph and store steps.

build/manifest.json records the Lean toolchain, the Mathlib commit, the hash of each checker program of the toolchain, and the input hash and output hash of each step. When the inputs of a step and its files do not change, the step does not run again. The output hash of the build covers extract.json, replay.json, status.json, graph/ and store.db.

The replay of a proof

The replay package checks a formal declaration again, outside the process that elaborated it (spec 07.7). It writes a challenge module that states the declaration again from its record, with sorry as the proof. It exports the challenge and the module of the declaration with leanexport, and runs lake comparator --paranoid on the two exports. The declaration passes when it has the statement of the challenge, uses only the standard axioms, and each kernel of the toolchain accepts it. The kernels are leanchecker, leanchecker-paranoid, lean4lean, nanoda_bin, con-leche and con-ron. A check takes about 20 seconds for a declaration that imports Mathlib.

The comparator runs the checkers in a bwrap sandbox, and bwrap needs Linux. On macOS, m2 build -no-sandbox runs the checkers without the sandbox. A replay without the sandbox does not give E5, and m2 status gives the reason. E5 also needs two kernels that accept the proof. Two builds of the same commit give the same output hash (rule R01).

The status of a node

m2 status shows the status of a node from the last m2 build. It reads build/status.json. Give a tag, an alias or an m2:// URI.

m2 status 3C53TD
m2 status lagrange-theorem-groups
m2 status m2://lean/Subgroup.card_subgroup_dvd_card
m2 status -json 3C53TD

The output gives the evidence level, the fidelity level, the flags, the statement hash, each item of evidence, each Lean binding with its type hash, its axioms, its reviews and its replay, and one reason for each decision. For an E5 result, it also gives the checker versions. A tag that is not in the build exits with code 1.

Graph queries

m2 graph runs a query on build/store.db from the last m2 build. Give each node as a tag, an alias or an m2:// URI. Put the flags before the nodes. Each query takes -json.

m2 graph neighbourhood D2SB01           # the nodes and the edges at most 2 edges from the node (Q2)
m2 graph closure 3C53TD                 # the best alternative, its trust profile and its axioms (Q3)
m2 graph closure -measure size 3C53TD   # the alternative with few nodes, not the least depth
m2 graph rdeps m2://concept/group       # the nodes that need the node, and the nodes that use it (Q4)
m2 graph path group 3C53TD              # the shortest learning path through definitions (Q5)
m2 graph frontier -msc 11               # the formal statements with no kernel proof (Q6)
m2 graph frontier -open -topic T0NT01   # the open problems and the statements that bound them (Q7)

m2 graph neighbourhood takes -hops N. m2 graph frontier also takes -evidence E1. A node that needs the node loses each alternative when the node is false. A node that uses the node uses it in at least one alternative. The learning path goes from from to to through the uses edges that end at a definition and the defines edges.

Ingest

m2 ingest gets a snapshot of an external source through its bulk channel, records the snapshot in manifests/sources.yaml and writes the records to build/records/<source>.jsonl. The import manifest manifests/ingest/<source>.yaml names the snapshot, the adapter and the hash of the records. Thus two imports of the same snapshot give the same bytes, and anyone can check it.

m2 ingest arxiv                        # a new snapshot from the bulk channel of the source
m2 ingest arxiv -snapshot blake3:...   # the recorded snapshot again, from the cache or from its URL
m2 ingest zbmath -url 'https://oai.zbmath.org/v1/?verb=ListRecords&metadataPrefix=oai_zb_preview&set=11'
m2 ingest mathlib                      # the declarations of Mathlib at the commit that lean/lake-manifest.json pins
m2 ingest lmfdb -url 'https://www.lmfdb.org/api/nf_fields/?degree=i2&disc_abs=py{"$lte":1000}'

These sources have an adapter now:

Source	Package	Bulk channel	Licence	What a record keeps
arxiv	ingest/arxiv	the metadata plane of tamnd/arxiv, one JSONL file for each month	CC0 metadata; each paper has the licence of its last version	the mathematics papers only: title, authors, categories, MSC codes, DOI and the ax:// locator. No text.
erdosproblems	ingest/erdosproblems	the git archive of teorth/erdosproblems, data/problems.yaml	Apache 2.0	each problem: the number, the status and its date, the formal status, the prize, the OEIS sequences, the tags, the short name and Paul Erdős as the person who posed it (rule G06). No statement text, because the data file has none.
formal_conjectures	ingest/formalconjectures	the git archive of google-deepmind/formal-conjectures, the Lean files under FormalConjectures/	Apache 2.0	each theorem with a category attribute, except the category test: the full Lean name, the docstring as the text, the category, the AMS classes, the Lean statement, the link to a formal proof, the title and the links of the module docstring, and the Erdős, OEIS, MathOverflow and Wikipedia ids that the links name. The URL is the line of the theorem at the commit of the snapshot.
lmfdb	ingest/lmfdb	a URL of the API of the LMFDB, with a table and filters. The default is the elliptic curves over Q of conductor at most 100	CC BY-SA 4.0	each object: the path of its page as the id, such as EllipticCurve/Q/11.a2, the label as the title and the table as the kind. The adapter knows the tables ec_curvedata and nf_fields.
mathlib	ingest/mathlib	M2Extract in the Lake project lean/ of the tree, at the pinned commit of Mathlib	Apache 2.0	each declaration of Mathlib: kind, module, the hash of the canonical type, the constants that the value uses, the docstring as text and the link to the documentation.
oeis	ingest/oeis	https://oeis.org/names.gz, the names of all sequences	CC BY-SA 4.0	each sequence: the A-number and the name as the title. No other text.
palomar	ingest/palomar	the listing of the Palomar registry API, order=registered&trust=all	CC0	each registered result at the newest version of its entry: the entry id, the title, the abstract as the text, the authors, the arXiv categories, the MSC classes, the Lean names of the theorems, the repository and commit that the registry checked, the trust level and the time of registration.
stacks	ingest/stacks	the git archive of stacks/stacks-project, tags/tags, chapters.tex and the LaTeX of the chapters	GFDL 1.2 or later: link only	each tag: the kind, the title of the part, chapter, section or named statement, the label, the chapter, the section and the file and line. The URL is the page of the tag. The text of the statement and its proof gives the fingerprints of rule L02, and the licence gate drops the text.
wikidata	ingest/wikidata	the SPARQL service of Wikidata, one query for each crosswalk property	CC0	each item with an id in nLab, MathWorld, ProofWiki, the Encyclopedia of Mathematics, the MSC, the OEIS, Mathlib, the LMFDB knowls, the House of Graphs or the Erdős problems: the QID, the English label as the title and the ids in the other systems.
zbmath	ingest/zbmath	the OAI-PMH interface of zbMATH Open, oai_zb_preview	CC BY-SA 4.0	each document: title, authors, MSC codes, Zbl number, DOI, the source as the locator and the ids of the references. No review text.

The formal-conjectures adapter reads the Lean files as text and does not build them, because the project pins its own Mathlib. It skips comments and strings, follows the namespaces and takes each theorem and lemma that has a category attribute. The snapshot of 25 October 2026 (commit 49ba26b) gave 4,652 statements: 1,602 open research problems, 2,816 solved research problems and 234 textbook results. 2,773 of them name an Erdős problem.

The Palomar adapter follows the cursor of the listing with one request each second. When the registry changes during a fetch, the API answers 409 Conflict and the adapter starts again from the first page. When the listing abbreviates an entry, the adapter gets the complete record of the entry. The snapshot of 25 October 2026 (revision 517) gave 760 results in 43 seconds. 117 of them name a directory in their repository, and 85 entries have more than one version.

The Stacks adapter reads the LaTeX as text, one line after the other, and joins each tag in tags/tags to its label. It does not compute the numbers of the book, such as Lemma 26.4.2, because the numbers come from the LaTeX build and the adapter cannot check them. The snapshot of 25 October 2026 (commit a04446e) gave 21,446 tags in less than 5 seconds: 12,587 lemmas, 3,299 sections, 1,721 definitions, 688 equations, 449 examples, 440 items, 386 exercises, 330 propositions, 214 theorems, 124 situations, 116 chapters, 35 subsections, 9 parts, 1,043 remarks and 5 lists of remarks. The records keep no text, only the fingerprints. With these records, rule L02 passes on the nodes of math2 and fails on a node that copies the statement of tag 01IS.

When the bulk channel is a git repository, the snapshot is the git archive that GitHub gives for the branch, and the catalogue records the commit from the archive. An adapter uses ingest.FetchArchive and ingest.WalkArchive for this. A snapshot that has more than one file, such as an OAI-PMH harvest, is the files one after the other, compressed with gzip. The zbMATH adapter fails when the number of records is not the size of the list that zbMATH Open gives. The full zbMATH harvest has more than four million documents, so give a set to harvest one MSC class.

The Mathlib adapter downloads nothing. It runs M2Extract on the .olean files of the tree, so run m2 build first. The catalogue records the commit of Mathlib with the snapshot. When the tree moves to a new tag of Mathlib, run m2 ingest mathlib again to get the records of the new tag. At the commit 56a0058 of Mathlib, for Lean 4.35.0, the adapter gives 358,102 records in less than 5 minutes on a laptop. Of these, 90,326 have a docstring. The snapshot is 50 MB.

The Wikidata adapter gives the crosswalk that Wikidata has now. On 2026-10-25 it gave 12,302 items in less than 30 seconds. MathWorld has the most ids (6,840) and nLab is next (4,348). Only 115 items have a Mathlib id. The adapter does not ask for the items with a defining formula, because most of them are single numbers and the query does not end in the 60 seconds that the service gives it.

The LMFDB adapter gets the labels one page of 100 after the other, with a pause of 2 seconds between the pages. The LMFDB asks automated clients to use its bulk downloads for large slices, and it answers with a captcha when it gets too many requests. Thus give a filter that selects a small slice. When the answer is not JSON, the adapter stops with an error.

Each source has an access class: open, share-alike-nc, verbatim, gfdl or record (spec 09.3). The licence gate stores the text of an item only when its class is open. For the other classes it keeps the record, the locator and the fingerprints of the text. The fingerprints cannot give the text back. The audit uses them to find copied text:

Rule	What it checks
L01	Each source names a licence and a class that agrees with it. Each import manifest names a recorded snapshot. The records agree with the manifest and store only the text that their class allows.
L02	No node body copies text from a source that is not open.
L03	Each share-alike source has an attribution line, and a node that uses its text names the item in sources or same_as.
L04	A node body that is similar to an item that it cites. A person checks it.

L02 to L04 need the records in build/records/. When they do not exist, the rules skip. Each source has an adapter in the package ingest/<source>. An adapter whose bulk channel has more than one file also implements ingest.Fetcher. To add a source, write the adapter, register it with ingest.Register, import its package in cmd/m2, and ask a maintainer to approve the class in manifests/sources.yaml.

Alignment

m2 align <source> compares each node with the records of a source and proposes edges. Run m2 ingest <source> first. The aligner does not change a node. It writes the proposals to queues/align/<system>.jsonl, and a person decides on each one.

m2 ingest wikidata
m2 align wikidata                     # write the proposals to queues/align/wikidata.jsonl
m2 align wikidata -n                  # show the proposals and do not write them
m2 align queue                        # all proposals, the node with the most dependents first
m2 align accept -by github:octocat 3f9a0c12b7de
m2 align accept -by github:octocat -note "The record is the finite case only." 8e01d2c4a9b3
m2 align reject -by github:octocat 5c7e2b90d1fa
m2 align confirm -by orcid:0000-0002-1825-0097 3C53TD wikidata

The aligner gives a score from 0 to 1 to each candidate record. It uses four channels:

Channel	What it compares
id	The node and the record have the same id in a third system, or the record names the Mathlib declaration of the node. The Wikidata records connect the systems, thus a node with an nLab id finds its OEIS sequence through the Wikidata item that has both ids. When only one record matches by id, its score is 1.
name	The names and the aliases, in lowercase and without accents. An equal name gives 1. Otherwise the score is the share of the rare words that the two names have in common.
formula	The formulas in $...$, without space and braces. This channel counts only when both texts have formulas.
embedding	The cosine of the vectors of the two texts. The default embedder hash/1 hashes the words, the word pairs and the character trigrams. It is in the binary, and it calls no service. A program can give a different align.Embedder.

A node gets a same_as proposal when the best record has a score of at least 0.9 (-threshold), the next record is at least 0.05 lower (-margin), and the node has no value for the system yet. Each other record with a score of at least 0.75 (-close) gives a close_to proposal. When two nodes match one record, the aligner proposes close_to for both, and it proposes in queues/dedup.jsonl that the two nodes are one node. A record of arXiv or zbMATH Open is a paper, and it gives an aligned proposal with the locator of the paper. The aligner skips retired nodes, the edges that the nodes have already and the edges that a person rejected.

m2 align accept writes the edge into the node in canonical form, and it removes the proposal from the queue. A close_to edge needs a note that tells how the node and the record differ. An aligned edge needs -match: exact, stronger, weaker, variant or partial. An accepted duplicate does not change the nodes, because a curator merges or retires the nodes in a separate pull request. Only a person decides. The -by flag takes orcid: and an ORCID iD, or github: and a GitHub login, and the command refuses an agent or a bot. Each decision is one line of registers/crosswalk.reg, with the hash of the record at the time of the decision. m2 align confirm records that a person checked a same_as value that was in the node already.

Rule	What it checks
A02	A same_as value that an agent wrote, as the provenance log in prov/ shows, has the decision of a person within 90 days.
A03	Each same_as value is still in the latest records of its system. When a person decided on the value, the record still has the hash that it had at the time of the decision. The rule reads build/records/, and it does not use the network.
A04	No duplicate proposal in queues/dedup.jsonl waits for more than 30 days.

On the nodes of math2 and the Wikidata records of 25 October 2026, the aligner proposes two same_as edges: Q505798 for Lagrange's theorem, through its Mathlib declaration, and Q83478 for the node Group. Both are correct. The other sources give no proposals for the seed nodes.

The Mathlib bump

m2 bump moves the tree to the newest release tag of Mathlib (spec 07.9). It never picks a release candidate. The command needs a git working tree with no changes, and it does these steps:

1. It builds the tree with the old pins, if the last build is not of the pinned Mathlib commit. This build gives the type hash of each binding before the bump.
2. It makes the branch bump/<tag>. It writes the tag into lean/lakefile.toml and the toolchain of the tag into lean/lean-toolchain, and it runs lake update mathlib.
3. It builds the tree with the new pins and puts each change of a binding into one kind: deprecated (the @[deprecated] attribute names the new declaration), renamed (the old declaration is gone, and one declaration has its type hash), refactored (the type hash changed), lost (no declaration or more than one has the type hash) or broken (Lean reports an error in the Math2 code).
4. It writes the new names of the deprecated and renamed declarations into the node files, and records each rename and refactor in registers/bindings.reg. A rename keeps the author of the binding. Then it builds again and runs the audit.
5. It writes the report to reports/bump/<date>.md and commits it on the branch. The report counts the breaks by kind, gives the time to green, lists the nodes whose fidelity level went down, and lists the Math2 declarations that Mathlib now has with the same type hash.

The exit code is 0 when the build and the audit pass with the new pins. It is 1 when they do not. The branch and the report are there in both cases, thus a workflow can open a pull request for each bump. m2 bump -master builds Mathlib master as an early warning. Do not merge such a branch. m2 bump -n shows the tag of the bump and stops.

Releases

A release of math2 has a name, YYYY.MM for the monthly release or YYYY.MM.N for a patch release (spec 06.2). It has three files in manifests/releases/ and a git tag:

File	What it has
YYYY.MM.yaml	The manifest: the commit, the pins, the hash of each artefact, the counts and the rebuild check.
YYYY.MM.levels	The evidence level and the fidelity level of each live node. The notes of the next release read it, thus they need no build of an old commit.
YYYY.MM.md	The release notes. A person writes the summary. m2 release notes writes the other sections.

A cut has two runs of m2 release cut:

1. The first run builds the tree, writes the three files and commits them. The name is the month of today, or the next patch release when the month has a release. The manifest must pin one stable Lean toolchain and one Mathlib commit.
2. A person writes the summary of the notes. On a second machine, m2 release verify -oleans DIR -record RUNNER NAME rebuilds the graph and the .olean files from the commit and writes the result into the manifest. With -against DIR, it also lists each .olean file that is different, and a person writes the reason of each one.
3. The second run checks that only the files of the release changed after the commit of the manifest, runs the full audit, and makes the tag when the audit passes. Push the tag with git push origin NAME.

m2 release notes FROM..TO writes the notes of TO again and keeps its summary. Without FROM, it uses the release before TO. The notes have these sections: the counts that changed with the cause of each change, the topics whose number of nodes changed, the nodes that moved evidence level, the conjectures and problems that a statement resolves now, the retired nodes with their successors, and the bindings that a Mathlib rename or refactor changed.

Rule	What it checks
R01	The graph rebuilds from the commit of the manifest to the same hash.
R02	The .olean files rebuild to the same hash, or the manifest gives the reason of each different file.
R03	The counts table of the notes gives each count that changed since the release before, with the same numbers and a cause.
R04	The last restore drill in reports/restore/ passed, and it is not older than one quarter at the last release.
R05	The manifest pins one stable Lean toolchain and one full Mathlib commit, the Lake project of the commit has the same pins, and the last bump report to that commit is green.

Benchmarks

bench/graph measures the latency of the queries Q1 to Q7 on a synthetic graph from the synth package, and compares the 95th percentile with the targets of spec 05.6. The test runs with 20,000 nodes in CI. The bench workflow runs it each week with 1 million nodes and puts the table in the summary of the run. To run it at reference scale (5 million nodes), use a machine with at least 24 GB of memory and 6 GB of free disk:

go test ./bench/graph -run TestLatency -nodes 5000000 -timeout 2h -v -report bench.md

On a Mac with 10 cores and 24 GB, with 5,001,118 nodes and 16,225,859 edges, each query meets its target:

Query		p50	p95	target p95
Q1	resolve an identifier	0.15 ms	1.2 ms	5 ms
Q2	neighbourhood, 2 hops	5.5 ms	10 ms	20 ms
Q3	dependency closure (median 682,066 nodes)	24 ms	33 ms	100 ms
Q4	reverse dependencies	1.0 ms	132 ms	200 ms
Q5	prerequisite path	3.4 ms	12 ms	100 ms
Q6	status slice	94 ms	230 ms	500 ms
Q7	open-problem frontier	8.7 ms	144 ms	200 ms

The store file has 2.9 GB. Open takes 37 seconds, and the heap after Open has 2.6 GB. The store keeps in memory only the uses, proves and defines edges, the kind and the evidence level of each node, and the axioms of the bindings. The other data stays in SQLite.

bench/align measures the precision and the recall of m2 align on labelled pairs (spec 17.3.3). Each line of bench/align/pairs.tsv is an item of one source, a record of a second source, and the label same or different. The file has the ids only, and no text of a source. The first pairs come from the exact matches that the sources state: the OEIS, Mathlib and Erdős problem ids of the Wikidata items, and the Erdős problem of each main theorem of formal-conjectures. The decisions of people in registers/crosswalk.reg of math2 add more pairs. The evaluation turns off the id channel, because the ids are the labels. The hash of the item puts each pair in the dev split or the test split. Only the threshold is fitted, on the dev split. Without flags the test runs on small records in testdata. To run it on the records of the sources:

go test ./bench/align -root DIR -v -report align.md

DIR is a tree with the records from m2 ingest in build/records. On the records of 2026-10-26, with 1,361 pairs, the test split at the default threshold 0.90 gives:

Sources	Items	Proposals	Correct	Wrong	Precision	Recall
formal_conjectures → erdosproblems	621	603	603	0	1.000	0.971
mathlib → wikidata	96	36	33	3	0.917	0.344
wikidata → erdosproblems	3	1	1	0	1.000	0.333
wikidata → oeis	350	47	44	3	0.936	0.126
all	1,070	687	681	6	0.991	0.636

The precision of all the pairs is 0.991, thus the default threshold meets the target of 0.98. The precision of mathlib → wikidata and of wikidata → oeis is less than 0.98. Most wrong proposals in the dev split are a near name of a different thing: Stirling numbers of the first kind has more than one OEIS sequence, and the Mathlib PowerSeries is the formal power series, not the power series. A threshold does not remove these errors, because their score is 1. The fitted threshold is 0.83. On the test split it gives the precision 0.972, thus the default stays at 0.90. The pooled dev split is mostly formal-conjectures pairs, and these do not tell the threshold for the other sources.

The pairs do not cover all the sources yet. The Stacks project, the LMFDB, zbMATH, arXiv and Palomar state no exact matches that the bench can read: Wikidata has no Stacks property, the adapter does not read the zbMATH property, the LMFDB knowl values are not object ids, and the snapshot has no arXiv records for the Palomar papers. Pairs for these sources come from the decisions of people in crosswalk.reg.

Rules that the toolchain keeps

1. The files in tamnd/math2 are the truth. Each database, index and site comes from these files, and you can make it again from them.
2. The build computes the status of each node. No person and no agent writes a status.
3. Only the Lean kernel and the certificate checkers can give the levels E4 and E5. A model can propose a proof. A model cannot accept a proof.
4. A formal statement must agree with its informal statement. This agreement is a separate level, F0 to F3. Only a person can give F2 or F3.
5. Each write is a pull request against tamnd/math2. The audit is the gate.
6. Each agent run has a run record. Each run has a person or a schedule that is responsible for it.
7. Each release pins the Lean toolchain, the Mathlib tag, the container images, the model ids and the prompt versions.

Build and test

make build    # writes bin/m2
make test     # runs the tests with the race detector
make lint     # runs golangci-lint

CI runs the same checks on each pull request. It also runs govulncheck, CodeQL, OpenSSF Scorecard, a smoke test of the binary, actionlint and zizmor.

Layout

cmd/m2/   the m2 binary
align/    the aligner: candidates, scores, the curation queues and the register of decisions (spec 05.3, 05.4 and 16.3)
audit/    the audit rules of spec 15, with a fixture pair for each rule
bench/    the benchmarks: bench/graph measures the graph queries of spec 05.6, and bench/align measures the precision of the aligner
bump/     the Mathlib bump: the pins, the breaks of a bump, the renames and the bump report (spec 07.9)
build/    the steps of m2 build, their cache and the build manifest
check/    the fast rules of m2 check: schema, body and links
crosswalk/ the syntax of the ids of each external system of same_as (spec 05.3)
cli/      the command table
format/   the canonical form of m2 fmt and the change from aliases to tags
graph/    the graph of spec 05: edges, closure, cycles, CSR and Parquet
ingest/   the adapters of the external sources, the licence gate, the snapshots and the import manifests (spec 09)
lean/     M2Extract, its Lake package and the Go package that drives it
node/     read node files, write the canonical form and compute the content hash
release/  the release manifest, the levels and the notes of spec 06.2, and the rebuild checks R01 and R02
replay/   the replay of a declaration in the comparator and the independent kernels
schema/   check front matter against the node schema
site/     build the wiki
store/    the serving store: the graph and the status of each node in SQLite, and the queries of spec 05.6
status/   the evidence level, the fidelity level and the flags of each node (spec 04.7), and the reviews
synth/    synthetic graphs for the benchmarks
tag/      tags, provisional ids, the tag register and the alias register
uri/      m2:// URIs
spec/     the specification

Each directory except cmd/, bench/ and spec/ is a Go package that other programs can import. For example, a bot can use github.com/tamnd/math2-agent/node to read and format node files. The packages follow the conventions of the Go standard library, and go doc shows an example for each main function.

The full layout arrives with the milestones. The plan has these parts: compute, search, api, mcp, orchestrator, agent, prompts/, images/ and web/.

Contribute

Read CONTRIBUTING.md. To report a security problem, read SECURITY.md.

Licence

Apache-2.0. Refer to LICENSE.