Metamath is a computer language and associated computer programs for archiving, verifying, and studying mathematical proofs.