Verification-Memory & World Model for AI Reasoning
from mathgraph import Kernel
kernel = Kernel(seed="mathlib4")
trace = kernel.prove("forall x : R, x^2 >= 0")
trace.verify() # returns Lean-verified proof or countermodel
MathGraph is an open-source verification memory layer for AI systems.
Verifiers decide what is true. MathGraph remembers how truth was proved, refuted, blocked, and reused.
It is designed to move beyond “does this look right?” and ask a harder question:
MathGraph represents claims, definitions, proofs, transformations, countermodels, obstructions, and verification traces as typed objects in a reasoning graph.
Every accepted edge records a lawful continuation: an implication, rewrite, specialization, dependency, quotient, contradiction, proof step, or finite refutation that can be inspected, replayed, and checked.
The result is not just a record of answers, but reusable verification memory: a system that learns from every proof, failure, obstruction, and refutation so future reasoning becomes cheaper, sharper, and more trustworthy.
MathGraph is not a static encyclopedia of mathematical facts. It is a verification-native system where every accepted claim must collapse into one of three terminal forms:
[1] a verified proof - the claim is supported by a formal proof, trusted import, or verifier-backed artifact.
[2] a finite countermodel - the claim is refuted by a concrete finite structure and witness.
[3] a named obstruction - the system cannot yet resolve the claim, but can identify the structural reason or residual basin blocking progress.
MathGraph is built around traceability and verifier boundaries.
A language model, search process, or human can propose a route, conjecture, proof sketch, transformation, or counterexample. MathGraph constrains that proposal through typed structure, proof obligations, finite model search, countermodel certificates, replayable evidence, and formal verification where available.
The goal is not to trust generated reasoning.
The goal is to convert generated reasoning into auditable structure.
In MathGraph, every durable result must either derive from accepted foundations, reduce to a machine-checkable proof or verification artifact, collapse into a concrete counterexample, or be honestly named as an obstruction.
This makes MathGraph a lawful continuation engine: it explores mathematical possibility, eliminates invalid branches, preserves viable structures, and records what survives as reusable verification memory.
For AI systems, MathGraph acts as a reliability layer between language-model intuition and formal verification.
Language models are powerful generators of possible reasoning. But generation is not verification. A fluent answer may still be wrong, incomplete, or impossible to reproduce.
MathGraph sits after generation and asks:
The result is not blind trust in AI output, but auditable reasoning chains whose assumptions, transformations, failures, and certificates can be inspected and reused.
MathGraph is built for a world where AI systems do more than generate answers.
They propose claims, search for proofs, invent definitions, produce counterexamples, explore routes, and uncover patterns across large spaces of mathematical and logical possibility.
But open-ended generation is not discovery.
Discovery begins when a system can explain what it found, why it matters, how it was checked, where it failed, and how the result can be reused.
MathGraph turns every verification attempt into structured memory.
A proof becomes a reusable route.
A counterexample becomes a refutation pattern.
A failed attempt becomes a named obstruction.
A repeated proof shape becomes a motif.
A useful abstraction becomes a compression of future search.
This lets AI systems move from isolated answers to cumulative discovery.
Instead of merely asking whether a claim is true, MathGraph asks:
In this sense, MathGraph is not only a verification layer. It is a discovery-structure layer: a system for turning proofs, failures, countermodels, routes, abstractions, and obstructions into reusable reasoning infrastructure.
MathGraph’s first practical testbed is the SAIR Mathematics Distillation Challenge: equational implication over finite magmas, where every answer must become either a Lean proof of implication, a finite magma countermodel certificate, or a named obstruction.
Router intuition proposes a basin. The MathGraph kernel generates lawful continuations. Constructors search for proof or countermodel certificates. Lean verifies the result. Failures become named obstructions that improve the graph.
The same architecture can support trustworthy reasoning in science, engineering, law, medicine, finance, and safety-critical systems: any domain where decisions depend on explicit assumptions, valid inference, regulatory constraints, and verifiable chains of consequence.