15. Trust and the audit

This document puts in one place what math2 trusts, what it checks, and the rules that do the checks. As in tamnd/arxiv, the audit is the real contract. A claim in the README, a status in the workspace or a number in a release is only as good as the rule that checks it. Each rule has a name and a state, and each rule writes into a committed report.

15.1 The trusted base

math2 states its trusted base explicitly. math2 believes that a statement at E5 is true if and only if all of these conditions are true:

1. Lean's kernel is sound for the type theory that it implements. We also require independent replay with lake check --paranoid. This replay checks again with nanoda, lean4lean and the verified con-leche and con-ron kernels (document 07.7). Thus the trusted base is "at least one of several independent kernel implementations is sound, and they agree", not "Lean's C++ kernel is sound". The kernel soundness bugs of 2026 (document 01) showed that this concern is not theoretical. They also showed that checkers which are out of date fail together. For this reason, the release records the version of each checker.
2. The standard axioms are consistent: propext, Quot.sound and Classical.choice, together with the type theory of Lean. This is equiconsistent with ZFC plus countably many inaccessible cardinals. That is a little more than ZFC, and much less than anything that mathematicians have doubts about.
3. The formal statement means what the informal statement says. This is the fidelity claim F2 or F3 (document 10). It is the weakest link. Each design decision about fidelity has the aim to make this link stronger.
4. The binding is the right declaration: the name, the Mathlib commit and the elaborated-type hash in the release manifest match what was built. The build checks this mechanically.

For E5, math2 trusts nothing else. Specifically, this includes:

• any model's output;
• the prover that found the proof;
• the implementation of any tactic, because its output is a term that the kernel checks;
• the m2 toolchain, except for the code that extracts declarations and hashes. That code is small and reviewed, and it has its own tests in math2-agent/trust/.

For E4, the trusted base is the certificate checker for that certificate kind (document 08.3), plus the runtime of the checker. For E3 and E2, it is the literature and the curators who read it. For E1, it is nothing.

15.2 How the audit runs

m2 audit                     # all planes, all rules, on the working tree
m2 audit -plane nodes        # one plane
m2 audit -rule G04           # one rule
m2 audit -changed            # only shards touched by the current diff (what PR CI runs)
m2 audit -release 2026.11    # the full pre-release audit

Each rule has one of five states, and the report shows all five:

math2 keeps n/a and pass separate for the same reason that tamnd/arxiv keeps them separate. If a rule passes because it had nothing to examine, the rule is not working. It should not look as if it works.

The report goes to reports/audit/<scope>.txt and reports/audit/<scope>.json. It is committed on main after each merge. The release report goes to reports/releases/<release>.txt.

$ m2 audit -plane formal -q
rule  state  checked   findings
F01   pass   41,203
F02   pass   41,203
F03   pass   41,203
F04   found  41,203    17
F05   pass   3,880
F06   n/a    0
...
41,203 bindings over 38,911 nodes, 17 soft findings, nothing failed

15.3 The rule catalogue

The letter tells the subject of the rule. Rules with the mark H are hard, and they block. Rules with the mark S are soft, and the audit reports them. The implementation of each rule is in tamnd/math2-agent/audit/<id>.go. With it is a fixture that triggers the rule and a fixture that does not.

T: tags and identity

S: schema

B: body

G: graph

F: formal

V: review and fidelity

C: computation

A: alignment

L: licence

P: provenance

R: release and reproducibility

X: agents

A merge is an agent PR when one of the new lines of its provenance logs is of an agent with no person. The runs of the PR are the runs that those lines name, and the audit reads their summaries in build/runs/. X01 checks each changed file, except the provenance logs, with agent.Permit for the role and the target of each run. A change passes when the set of one run allows it. X02 needs spend_usd and budget_usd in each summary. X03 counts the runs that started in the week that ends 7 days before the date of the HEAD commit, so that each PR had a week for review. A run is accepted when a provenance line on the branch names it. A role and a model with fewer than 5 runs in the week are not checked, and the threshold is 25%. X04 looks for a part of a field name that is a status word of S03, fidelity_reviews or reviews, in the lines of agents and in the fields of the nodes that an agent PR changes. It also fails an agent PR that changes a file below reviews/.

There are 65 rules. A new rule needs a fixture pair and a line in this table. Both must be in the same pull request.

15.4 Propagation when trust changes

Trust can change. The audit handles the events that change it:

• A conjecture is refuted. Some statements have a best alternative that uses the conjecture as: hypothesis. These statements do not change, because they are honest conditionals. Other statements have a proof that uses the conjecture not as a hypothesis. Each of these statements goes down to E1, gets a flag, and is in the list in the release notes. In that case, someone assumed an open conjecture and did not say so.
• A formal binding loses its declaration (a Mathlib rename without a deprecation alias). The binding is broken (F01 fails on the bump branch). The bump agent (document 07.9) proposes the rename from the deprecation data of Mathlib, and a person merges it. The node keeps its tag and its history in bindings.reg.
• A definition changes meaning underneath a review (F02). The review becomes stale. For that binding, the node goes down to F0, and E5 is not available. This stays true until someone reviews again, or until a second formalisation is proved equivalent.
• A kernel or checker bug is found. Some E5 nodes had their replay on the affected checker version. Each of these nodes runs again on a fixed version, or on the other checker only. The release that contained them gets an erratum. At some time, this has occurred in every proof assistant. Thus math2 has a plan for it and does not only hope that it will not occur.
• A model version is withdrawn (document 06.5, the withdrawal test). A generated PR quarantines its unreviewed output. An E5 status reached through that output does not change, because the kernel and the fidelity reviews carried that status, not the model.

15.5 What the workspace says

The status that a reader sees is a short phrase that the system generates from the evidence. It is never a checkmark. For example:

• "Proved in Lean (Mathlib), statement reviewed by 2 people. Classical. Replayed by 2 kernels."
• "Proved in refereed literature (3 sources, earliest 1871). Formal statement exists, unreviewed. No formal proof."
• "Claimed (preprint, 2026). Not reviewed. 1 agent-produced informal proof."
• "Open. Posed by Erdős (1975). Best known bounds: … (2025, formal)."

Each phrase has a link to the evidence that it summarises. A reader who wants to know why we believe something can follow the link down to the kernel replay log, the reviews, or the page number in the 1871 source.

Markdown · Source · Edit