 As noted earlier, the database "nat.mm" formalizes natural deduction.The Metamath Proof Explorer (with its database "set.mm") instead use a set of conventions that allow the use of natural deduction approaches within a Hilbert-style logic.Using the design ideas implemented in Metamath, Raph Levien has implemented very small proof checker, "mmverify.py", at only 500 lines of Python code.