Using the design ideas implemented in Metamath, Raph Levien has implemented what might be the smallest proof checker in the world, mmverify.py, at only 500 lines of Python code.
•
The original natural deduction system (due to Gerhard Gentzen), which uses an extra stack, is an example of a system that cannot be implemented with Metamath.