Point your agent to mathgraph.org/agents

Start with a manifest, not a claim.

1. Read /llms.txt or /.well-known/mathgraph.json.
2. Fetch the short-lived /records/index.json catalogue and record the local fetch time.
3. Select an explicit record version and fetch its immutable JSON.
4. Validate the schema and both the canonical and transport digests.
5. Cite the permanent versioned page and content digest.

generated_at is publication time, not a response timestamp. Treat lifecycle state as fresh for at most max_age_seconds after your own fetch time, then re-fetch the catalogue.

Index source without promoting it into proof.

The Mathlib catalogue publishes real declaration occurrences and three closed-endpoint structural relations: DECLARES, IMPORTS_MODULE, and TYPE_REFERENCES. These are structural relations, never logical implication or semantic equivalence.

1. Independently pin the exact manifest and trust-policy digests. The exact Git commit is one chosen trust channel, not truth.
2. Hash the manifest bytes before parsing them.
3. Validate the catalogue ID and version plus the Mathlib repository, commit, tree, and Lean toolchain pins.
4. Fetch only manifest-listed search and shard paths, then verify every declared size and SHA-256 digest.
5. Recompute object and relation identities, require closed endpoints, and admit only the three declared structural relation types.
6. For an unsupported version, unknown critical extension, forged status, or missing endpoint: decline. Do not infer a nearby result.
7. Return the authority-free result below. Do not convert source indexing into verification or action permission.

Source status

SOURCE_INDEXED

Independent verification

NOT_CHECKED

Current applicability

NOT_CHECKED

Freshness

PINNED_HISTORICAL_SOURCE

Authority

NONE

Authorization

NONE

The exact public catalogue and trust policy were replayed by qualification run 38242539984 ↗, then committed at 7519de6a51e524caf70df51d37389ff42d430d43. A later regeneration run ↗ reproduced the catalogue publication with its own run-specific policy; it did not replay the public trust-policy bytes.

A digest served by the same origin detects changed bytes relative to a trusted pin; it does not authenticate a compromised origin or establish mathematical truth. Pin the manifest and trust-policy digests through an independently chosen channel. Repository authentication is a trust-policy choice, not mathematical truth.

Choose a module without expanding its authority.

Record 001 is an exact-scope consumption contract. Record 002 is a historical offline replay contract. They are independently usable and neither grants authority to browser or map exports: those presentation files declare authority: NONE.

Discover is a local advisory contract. Its real source-pack result is PARTIAL, with advisory_only: true, can_promote_truth: false, verification NOT_CHECKED, and FULL_REPLAY_UNAVAILABLE. Attention is allocation, not truth confidence.

Develop has one exact eight-state QUALIFIED_BOUNDED profile from same-owner implementation-independent replay. The Capability Family Compiler remains NOT_IMPLEMENTED. VDN / Lean remains an unqualified EXPERIMENTAL candidate.

The Capabilities registry has one qualified finite entry with exact contract, evaluation, receipt, and policy pins. Read the registry JSON and independently admit its policy and replay boundary. Reading the registry alone grants no trust. Current applicability is UNKNOWN; freshness, revocation, and supersession are NOT_CHECKED; action authorization is NONE.

External interoperability is unsigned correspondence only. An in-toto wrapper creates no qualification or authentication. Modules are independently usable; no autonomous loop or compulsory pipeline is provided.

Record 001 — exact source-scope match

An in-scope request must match the exact record ID, version, source pin, suite pin, and supported goal. This is a structured comparison—not an LLM judgment. Any mismatch or unsupported claim returns UNKNOWN.

{
  "record_id": "mg-l4yaml-source-check-20261010",
  "version": 1,
  "source_commit": "62bf7077910e888a0bc8adfc8e08a5f500ff3ca3",
  "external_suite_commit": "da267a5c4782e7361e82889e76c0dc7df0e1e870",
  "goal": "finite_parser_acceptance"
}

{
  "status": "WARRANTED_BOUNDED",
  "reason": "EXACT_SCOPE_MATCH",
  "truth_promotion": false
}

{
  "status": "UNKNOWN",
  "reason": "UNSUPPORTED_GOAL",
  "truth_promotion": false
}

Record 002 — offline dependency replay

This contract is different from record 001’s exact scope lookup. Download the immutable bundle, the separately supplied trust policy, and the standard-library Python consumer. Supply the expected policy digest through a trusted channel; the consumer validates typed claims, receipts, routes, withdrawals, and pins, then independently recomputes the seven historical outcomes.

The replay establishes a pinned historical snapshot. Current applicability remains UNKNOWN; freshness remains NOT_CHECKED. It does not rerun the original JPL Lean proof. This consumer and the earlier RealityGraph comparison are same-owner independent implementations, not outside-organization adoption.

The browser import report and knowledge-map download are presentation projections with authority NONE. They cannot be supplied as evidence to either independent consumer.

Snapshot digest

A digest is integrity, not authenticity.

The catalogue and record digest can detect changed bytes. If both arrive from a compromised host, the digest alone cannot authenticate that host or establish who published the replacement. Same-origin digests provide integrity relative to a trusted pin, not authenticity. The discovery manifest therefore links the committed catalogue source on GitHub as a second-origin provenance check, currently marked UNSIGNED_PROVENANCE_ONLY.

A future signature must name a key policy and authenticate a specific statement. It still would not establish semantic truth.

Canonical content SHA-256

Source pin

Suite pin

The static interface does not execute claims.

Whole-language YAML correctness, natural-language fidelity, generalization beyond the pinned cases, and newer source revisions remain UNKNOWN.