A high-performance experimental proof checker for Lean 4, developed by Metalogic Labs.
MathGraph builds on:
The checker is used as a testing bed for kernel performance, soundness testing and differential testing. It is evaluated in the Lean Kernel Arena, including accept/reject tests and large Lean environments such as mathlib.
The core conversion algorithm is closure-based, with additional implementation-level optimisations.
This remains an experimental kernel implementation and is not a replacement for Lean's official kernel.