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 items today for automated proving with Metamath are:

• 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.
• "Learning to Prove Theorems by Learning to Generate Theorems" by Mingzhe Wang, Jia Deng

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.