MathGraph.
MathGraph Check

Verification is not one bit.

MathGraph Check publishes source identity, machine observations, proof receipts, assumptions, and unknowns as separate facts. It does not turn every green sub-check into a universal “verified” label.

Local import workbench

Carry the evidence boundary with the record.

Import → Interpret → Check → Resolve → Explore → Export. This browser recognizes an exact local record and displays its existing qualified boundary. Its authority is NONE.

JSON local files only, at most 65,536 bytes. The one supported artifact is the unchanged L4YAML V1 record: 4,321 bytes. Changed, unsupported, or non-JSON bytes remain UNKNOWN.

Download the exact supported record.json, then select that local file below. There is no upload or URL input.

No proof, kernel, or source-suite execution takes place here. Exact byte recognition supplies integrity, not authenticity or warrant authority. Input contents are never parsed or executed; only a digest match unlocks the committed display data.

UNKNOWN — no local record has been recognized. Current applicability and freshness remain UNKNOWN.

Resolve selects the already qualified record-bound outcome only. An unsupported route remains UNKNOWN. The browser adds no resolution semantics.

Select a supported local file to begin. No imported evidence is shown yet.

The portable export is a read-only mathgraph.browser-recognition.v1 presentation, not an independent import result, proof, certificate, or input to the Python importer.

Supported local-record import paths and independent replay command

The browser supports only the exact downloaded record.json. The importer is available on main, while independent historical replay deliberately detaches at exact implementation commit 1204a1d267b6217c45c9b17f093cc3587450cf78. Run that pinned consumer only after reviewing the separate trust policy and its digest:

git clone https://github.com/metalogiclabs/mathgraph.git mathgraph-import-v1
cd mathgraph-import-v1
git checkout --detach 1204a1d267b6217c45c9b17f093cc3587450cf78

python3 -I -S scripts/mathgraph_import_v1.py \
  --record conformance/import_v1/fixtures/record.json \
  --policy conformance/import_v1/fixtures/trust-policy.json \
  --policy-sha256 944231afaf9d89e6f7dc77d9efbe80dcbd3fc76f8e8f260b32637a0f261faf65 \
  --goal finite_parser_acceptance

You may replace --record with the local path to that unchanged supported artifact. Keep the reviewed policy separate. This offline command does not execute the original proof, kernel, or source suite, check current applicability, or authorize actions.

Inspect the pinned independent consumer · Inspect the separately reviewed pinned policy · Independent result contract · Permanent supported record

Current capability

Pin a claim to the evidence that actually supports it.

Today, Check can publish an immutable record from a qualified evidence boundary and resolve only exact source-bound questions. New revisions and broader goals remain UNKNOWN until separately requalified.

Source identity

Implemented

Git objects + archived receipt hashes

Identifies exact repositories, commits, source blobs, toolchain, and publication digest.

Formal verification

Scoped replay

Named Lean proof objects

Replays only the explicitly named theorems and their recorded axiom boundary.

Finite executable evaluation

Warranted — bounded

Compiled parser + Lean #guard evaluation

Reports exact outcomes on exact decoded cases and controls; does not generalize to the whole language.

Statement fidelity

Unknown

No qualified interpretation service

Does not assert that an informal or normative source statement was translated completely or correctly.

Assumptions and semantic interpretation

Explicit boundary

Record fields + declared separator

Preserves assumptions and source-specific differences without promoting a preferred interpretation to truth.

Generalization

Unknown

No whole-domain theorem

A finite suite, content hash, or signature cannot establish correctness beyond the declared scope.

Requalification and revocation

Proposed lifecycle

Historic record remains immutable

Future state can mark a record superseded, stale, revoked, or requalified without rewriting its historic evidence.

Bounded example

The L4YAML record earns one narrow result.

48/48Decoded source casesMatched exact source labels
31Expected acceptancesPinned suite observations
17Expected rejectionsPinned suite observations
4Extra controls52 total Lean guards
Fail closed

Unsupported questions do not inherit nearby evidence.

Unknown

An incorrect source commit, a changed suite pin, a different record ID, or a broader goal such as whole-language correctness returns UNKNOWN. It is not a failed theorem and not an invitation to guess.

Current versus research

CapabilityMaturityBoundary
Immutable static evidence recordImplementedQualified L4YAML snapshot
Exact source-bound localhost resolverImplemented previewRead-only; no public hosted endpoint yet
Stable semantic object envelopeExperimentalQualified research candidate, not deployed V1
Automatic source-change requalificationProposedNo continuous watcher or revocation service