Metamath is a programming language created in 2005 by Norman Megill.
| #1726on PLDB | 20Years Old |
Metamath is a simple and flexible computer-processable language that supports rigorously verifying, archiving, and presenting mathematical proofs.
|- ph & |- ( ph -> ps ) => |- ps