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.