LeaTTa: A Machine-Checked Operational Semantics and Metatheory of MeTTa in Lean 4🔗

LeaTTa is a formalization of MeTTa, the language at the heart of OpenCog Hyperon  (Goertzel, 2021)Ben Goertzel, 2021. “Reflective Metagraph Rewriting as a Foundation for an AGI Language of Thought”. arXiv:2112.08272, carried out in the de Moura and Ullrich (2021)Leonardo de Moura and Sebastian Ullrich, 2021. “The Lean 4 Theorem Prover and Programming Language”. In Automated Deduction - CADE 28. interactive theorem prover. If you are a MeTTa developer, you can think of it as a machine-checked specification: every rule that fires, every type that is checked, every result that comes back is defined by Lean code that Lean's own kernel verifies. The formalization covers:

• the minimal interpreter;

• the standard library;

• the gradual type system;

• the published four-register operational semantics;

• the MeTTaIL formalization;

• a body of machine-checked metatheory: determinism, confluence of the deterministic fragment, type soundness, gradual-typing consistency, soundness and completeness of first-argument indexing, and a bisimulation connecting the kernel's rule-firing core to the published operational semantics of MeTTa at the level of which rules fire  (Meredith et al., 2023)Lucius Gregory Meredith, Ben Goertzel, Jonathan Warrell, and Adam Vandervorst, 2023. “Meta-MeTTa: an Operational Semantics for MeTTa”. arXiv:2305.17218.

Every theorem in this book is checked by Lean's kernel. The development contains no sorry, admit, native_decide, partial, or unsafe; the central axiom audit reports only the three standard classical axioms of Mathlib  (Community, 2020)The mathlib Community, 2020. “The Lean Mathematical Library”. In Certified Programs and Proofs (CPP 2020)., and the gradual-typing non-transitivity result depends on no axioms at all. The executable interpreter is validated against Hyperon's own test corpus (270/270 assertions). CI fails on root Lean/Lake warnings and on any unreviewed book warning; the only allowed book warning is the known upstream Verso v4.31.0 @[expose] warning.