tamnd/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 M3. Each release v0.N.0 closes the code of one or more milestones:
Release v0.1.0 closes the code of M0: m2 new, m2 fmt, m2 check, m2 mint and m2 site build are written.
Release v0.2.0 closes the code of M1 and M2.
The code of M1 is the trust core. 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).
The code of M2 connects the graph to the world. 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 sameas id has the syntax of its system, with the crosswalk package. The align package and m2 align propose sameas, closeto 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. 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 msc package reads the topic map of MSC2020, and the coverage package and m2 coverage write the coverage report of each code.