MathGraph is a living, typed semantic hypergraph where axioms, definitions, theorems, proofs, transformations, countermodels, obstructions, and verification traces are represented as formal nodes. Every edge records a lawful continuation; an implication, specialization, generalization, rewrite, dependence, quotient, contradiction, proof step, or finite refutation that can be checked by a formal kernel.
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 not a static encyclopedia. Every accepted answer collapses into one of three terminal forms:
[1] a verified proof,
[2] a finite countermodel,
[3] a named obstruction.
MathGraph is built around traceability. Every accepted claim must either derive from a foundational seed of axioms and inference rules, reduce to a machine-checkable proof object, or collapse into a concrete counterexample or explicit obstruction. This makes MathGraph a lawful continuation engine: it explores mathematical possibility, eliminates invalid branches, preserves viable structures, and traces every survivor back to source law.
For AI, MathGraph acts as a reliability layer between language-model intuition and formal verification. A language model may propose routes, conjectures, proof sketches, transformations, or counterexamples, but MathGraph constrains those proposals through typed structure, proof obligations, finite model search, countermodel certificates, and Lean-verifiable artifacts. The result is not blind trust in AI output, but auditable reasoning chains whose truth can be inspected, reproduced, and verified.
MathGraph’s first practical testbed is the SAIR Mathematics Distillation Challenge (Stage 2): equational implication over finite magmas, where every answer must become either a Lean proof of implication or a finite magma countermodel certificate. Router intuition proposes a basin, the MathGraph kernel generates lawful continuations, constructors search for proof or countermodel certificates, Lean verifies the result, and 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.
MathGraph.org aims to become the verification layer for trustworthy AI: an open-core mathematical reasoning graph with enterprise APIs for proof traceability, automated verification, compliance reasoning, formal-methods workflows, and AI-assisted theorem, proof, and countermodel discovery.