 It has a "prove" command that enables users to enter a proof, along with mechanisms to search for existing proofs.The Metamath program can convert statements to HTML or TeX notation;
for example, it can output the modus ponens axiom from set.mm as