Automated proving

Metamath is all about verifying proofs. Improved automation to help create those proofs is always welcome.

Existing Metamath tools already include some simple automation. For more information, see Metamath proof assistants.

This page points to information to help people implement improved automation for Metamath proofs, particularly using artificial intelligence (AI) and especially its subfield machine learning (ML).

The most relevant item today is Holophrasm, which can automatically generate Metamath proofs. See the paper "Holophrasm: a neural Automated Theorem Prover for higher-order logic" by Daniel Whalen and the related Github repo for Holophrasm.

Other potential items include:

• "Deep Learning for Symbolic Mathematics" (openreview.net). This uses a simple seq2seq model to do simple symbolic mathematics. There is a related HN discussion about this - many note that it sounds too good to be true.