What TheoremPath asserts is correct

Current snapshot

Manifest generated 2026-05-02

The author-tagged set starts small. A page claim only enters the audit graph when an author wraps a numerical statement with a stable id and a verifiable formula. Most page math today is verified through the Lean theorem track or appears as a derived value inside a question; both of those rows carry the bulk of the audit signal. The author-tagged row grows as we annotate more pages.

Fetch the manifest

/audit/manifest.json — UTF-8 JSON, ~4.5 MB. Compressible to ~700 KB gzip. Stable schema (versioned at the top). Updated on every commit that touches the audit graph.

What it contains: ids, content hashes, status, method, reviewer, sourceRefs, lastVerifiedAt. What it does not contain: the underlying content text. Auditors who already have the rendered pages can verify by hashing their scrape; the manifest is the verification surface, not a content dump.

Schema and methods

Statuses: verified · unverified · needs-review · disputed · stale

Methods: computation · human-review · source-check · lean · test-case · llm-assisted-review

computation verification reuses a small whitelisted parser (no eval, no shell-out): arithmetic (+, −, *, /, ^), square root, log / ln / log2 / log10, exp, abs, min, max, identifiers drawn from a per-claim inputs map, and the constants e and pi. Function calls require parentheses. Each computation claim ships with the formula text, the input map, the expected value, and a tolerance; the verifier re-evaluates and compares.

How to file an audit report

1. Fetch the manifest. Find the claim id matching the surface you are reporting on.
2. If the claim is verified and you disagree, supply a verification artifact stronger than the recorded one (a Lean wrapper, a peer-reviewed source, or a counterexample with derivation). A bare prose disagreement against a verified claim is rejected by policy.
3. If the claim is unverified or needs-review, a normal report is welcome. Include the claim id, the proposed correction, and any sources.
4. Email [email protected] with subject prefix [audit]. If you also publish the report at a public URL, include that.

What the manifest does not cover

• Subjective editorial choices (page tier, module placement, difficulty rating). Disagreement here is a normal feature request, not an audit issue.
• Comparative judgements that depend on context the page authors weighted differently (best textbook, canonical proof style).
• Sister-section content (LinguisticsPath, ComputationPath, PhilosophyPath) is published with its own per-section audit manifest. Each follows the same schema described here; visit the relevant sister section for its current snapshot.