MeTTaMath is a project to import the Metamath library into MeTTa. MeTTa is a programming language designed to be the development and cognitive language for AGI systems. The core of MeTTa is pattern matching and rewriting. This aligns naturally with Metamath's core inference rule of variable substitution, making integration conceptually elegant.
Every core function called after parsing in the read() function is implemented in MeTTa, which includes verify(), treat_step, add_d, etc. The project currently processes Metamath .mm files during Python parsing, adding relevant information to MeTTa spaces, and proceeding to do verification in MeTTa. The implementation passes the metamath tests that it can run in a reasonable amount of time. Full MeTTa pasring may be done once MORK is fully integrated, speeding it up a lot.
- mmverify-utils.metta - Contains the MeTTa implementations along with utility functions
- mmverify.py - The original Python Metamath verifier by Raph Levien, modified with MeTTa integration code
- examples/ - Contains examples of MeTTa interpretation of Metamath statements and their output
This is a Metamath verifier written in Python, originally by Raph Levien.
Metamath is a formal language and an associated computer program (a proof checker) for archiving, verifying, and studying mathematical proofs. The set of proved theorems using Metamath is one of the largest bodies of formalized mathematics. Multiple Metamath verifiers (written in different languages by different people) are used to verify them, reducing the risk that a software defect will lead to an incorrectly verified proof.
For a quick introduction to Metamath and its goals, see the video Metamath Proof Explorer: A Modern Principia Mathematica.
For more information about Metamath, see the Metamath website.
You can also get the (physical) book about Metamath; see: Metamath: A Computer Language for Mathematical Proofs by Norman Megill & David A. Wheeler, 2019, ISBN 9780359702237.
This software is free-libre / open source software (FLOSS) released under the MIT license.