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).