MathGraph.
Source-pinned verification evidence

Knowledge you can verify. Capabilities you can build on.

Search real mathematical objects, follow exact source-backed connections, and inspect what independent evidence does—and does not—establish.

Explore source-pinned mathematics, inspect independently qualified evidence, and discover what remains unresolved. Start with the published Mathlib slice and reproducible verification cases; arbitrary repository or proof submission is not currently hosted.

This is a 13-module slice of Mathlib, not all of Mathlib. Search includes source-indexed declarations, separately qualified records, and bounded capabilities; indexing is not independent proof checking.

Inspect real evidenceUnderstand the protocol
Published network snapshot

Substantial source coverage. Deliberately separate evidence.

Every number below is derived at build time from validated, versioned contracts. They are not added into a single adoption or verification total.

2,345Indexed declarationsPinned Mathlib source occurrences
1Qualified bounded resultUnique independently admitted Check result
3,578Typed source-backed relationsStructural and qualified-evidence relations
4External source projectsAllowlisted repository identities
1Qualified reusable capabilityRegistry entry with bounded replay

Source structure: DECLARES 2,345 · TYPE_REFERENCES 1,224 · IMPORTS_MODULE 2

Evidence structure: EVIDENCE_FOR 4 · WITHDRAWS 3

Exact external project identities
Three ways in

Follow the outcome you need.

  • Explore knowledge

    Inspect source-pinned records and their declared relations. Keep unknowns in view.

    Discover is advisory: it allocates attention, not truth confidence.

  • Verify a claim

    Recognize the supported local record, inspect the historical receipt, and replay the independent consumer.

    Check preserves source scope. Resolve replays a bounded historical dependency graph.

  • Build on a capability

    Inspect one independently replayable finite capability and the precise conditions for reuse.

    Develop has a qualified finite profile. The Capability Family Compiler remains unimplemented.

The modules exchange evidence at different maturity levels. There is no autonomous loop or hosted execution service.

Real source → bounded result

Pinned parser source. Bounded evidence.

The L4YAML example checks an exact revision of publicly available third-party Lean 4 code against decoded YAML-suite cases, preserving the scope of its proof and parser receipts.

Source
nasa-jpl/L4YAML at 62bf7077910e888a0bc8adfc8e08a5f500ff3ca3
Suite
yaml/yaml-test-suite at da267a5c4782e7361e82889e76c0dc7df0e1e870
Finite observation
48/48 decoded cases matched; 31 accept, 17 reject. 52/52 Lean guards include 4 additional controls.
Historical receipt
Inspect the normalized native parser run. Whole-language correctness, statement fidelity, and generalization remain UNKNOWN.

mathgraph.l4yaml.48-case-qualification EVIDENCE_FOR jpl.l4yaml.finite_parser_acceptance · source pointer /derivation/routes/3/evidence/0

This typed relation is copied from the qualified record projection. It does not generalize the finite observation or establish a new proof.

Independent check of public third-party code. No affiliation or endorsement implied. The site displays published receipts; it does not rerun the original JPL Lean proof.

A real mathematical object

Open a declaration. Follow what its source actually says.

Real.rpow is one exact declaration occurrence in the pinned Mathlib catalogue—not a MathGraph-verified theorem.

Declaration
Real.rpow · definition
Module
Mathlib.Analysis.SpecialFunctions.Pow.Real
Source pin
d13f23b723b8a846827a245b89c10fc7d3f11612
Source status
SOURCE_INDEXED
Independent verification
NOT_CHECKED

Inspect exact source, statement, omissions, and replay →

Rendered declaration type
Real → Real → Real

Statement digest 0d4222242bb169ad0bbda1f344df403b005d93fb54c8c3e5d10e4395ea38fb1d. The hash protects bytes; it does not establish truth or semantic equivalence.

Declared objects and relations

Presentation projection · authority NONE · not a certificate, proof, or verifier

Position and proximity organize this view only. Every arrow repeats an exact structural relation whose logical implication and semantic equivalence flags are false.

Filter declared relation types

3 of 3 objects · 3 of 3 relations · omitted: 0 objects, 0 relations

This page is capped at 6 objects and 10 relations. Counts preserve the complete one-hop selected scope, including named omissions.

Incoming

Selected occurrence

Outgoing

    Display-only traversal

    Follow only the currently displayed declared arrows. This is not proof search, verification or support closure.

    No traversal requested.

      Declared relation list

      1. Mathlib.Analysis.SpecialFunctions.Pow.RealDECLARESReal.rpowdirected · implication false · equivalence false · authority NONE
      2. Real.rpow_eq_powTYPE_REFERENCESReal.rpowdirected · implication false · equivalence false · authority NONE
      3. Mathlib.Analysis.SpecialFunctions.Pow.RealDECLARESReal.rpow_eq_powdirected · implication false · equivalence false · authority NONE

      Visual projection

      The diagram is drawn from the same bounded payload after JavaScript loads. The semantic lists remain the accessible source of exact links and relation labels.

      Enable JavaScript to draw the visual projection.

      Download displayed subgraph

      Export kind PRESENTATION_PROJECTION · authority NONE · semantics READ_ONLY_SOURCE_STRUCTURE. It is not an evidence receipt and grants no action authority.

      Explore this declaration in the catalogue → · Inspect canonical objects and declared relations

      Source relations such as DECLARES and TYPE_REFERENCES support navigation; they are not dependency proofs. Unlike documentation or theorem-search tools, MathGraph also links separately qualified records to exact evidence, scope, and historical changes.

      Bounded capability

      Reuse starts with explicit conditions.

      QUALIFIED_BOUNDED

      One finite representation-refinement profile has independent bounded replay.

      Exactly the eight ordered 3-bit states; deterministic Boolean policies on observational cells; the fixed five named refinements and all 256 Boolean one-bit refinements; discovery bit0 AND parity and reuse bit0 OR parity.

      Assumptions stay attached:

      • The carrier is exactly the ordered 3-bit Boolean cube.
      • Policies are total deterministic Boolean functions of the declared observations.
      • Source-distinct reuse means two different target functions in the same owned source; it is not external adoption.

      Current applicability: UNKNOWN. Freshness: NOT_CHECKED. Action authorization: NONE.

      Same-owner implementation-independent qualification does not establish external adoption. The Capability Family Compiler remains unimplemented; no universal invention theorem is claimed.

      Inspect the capability registry → · Read the finite replay boundary

      The edge of the record

      See what resolves—and what does not.

      The record warrants an exact, finite observation. The same deterministic matcher returns UNKNOWN as soon as the record identity, version, pins, or goal leave that boundary.

      1. ImplementedSource identityTwo exact Git commits.
      2. Warranted — bounded48/48 decoded cases31 accept · 17 reject
      3. Warranted — bounded52/52 Lean guardsCases plus 4 controls.
      4. UNKNOWNBeyond the pinned boundaryWhole-language correctness · Statement fidelity · Generalization
      Three fixed requests

      Try the boundary, without pretending to run arbitrary claims.

      Exact pinned observation
      Requestfinite_parser_acceptance
      Warranted — boundedEXACT_SCOPE_MATCH
      Wrong source pin
      Requestfinite_parser_acceptance
      UNKNOWNSOURCE_PIN_MISMATCH
      Unsupported whole-language claim
      Requestwhole_language_correctness
      UNKNOWNUNSUPPORTED_GOAL

      These are precomputed from the same exact-match function used by the isolated consumer test. No visitor input is executed.

      Point your agent to MathGraph →

      Independent verification

      Inspect the checker. Choose the trust policy.

      A result is useful when you can trace its source, scope, assumptions, and verifier.

      The local Python importer validates the supported record and replays its historical receipt under a separate pinned policy. The browser only recognizes exact bytes and presents existing evidence. Neither step reruns the original proof or establishes current applicability.

      Obtain consumer and policy pins through a separately trusted channel. Same-origin hashes protect byte integrity; they do not authenticate a publisher.

      Independent dependency replay instructions · Agent consumption contract · Read the protocol

      Executable quick start

      Import the supported record locally.

      Clone the repository and detach at exact implementation commit 1204a1d267b6217c45c9b17f093cc3587450cf78. With Python available and the separately pinned policy and consumer reviewed:

      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

      The result uses mathgraph.import-result.v1. Historical bounded receipt validation leaves proof, kernel, and source-suite replay NOT_PERFORMED; freshness NOT_CHECKED; and current applicability UNKNOWN. It authorizes no action.

      Inspect the pinned independent consumer · Inspect the separately reviewed policy · Developer setup and consumers →

      Long-term direction

      Portable evidence across systems.

      MathGraph aims to connect mathematics, scientific workflows, software verification, and machine-generated claims through reusable evidence.

      Today’s foundation is finite and explicit: a source-indexed mathematical catalogue, source-pinned records, a historical dependency replay, one qualified finite capability, and a local record workflow. Broader source adapters, capability compilation, continuous requalification, and hosted resolver or MCP services remain future work. These examples do not establish universal support.