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 example, mmj2 will automatically fill in some proof steps if you prefix a step with "!". 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
• OpenAI has created a number of Metamath proofs (the first ones were revealed in March 2020). See set.mm and search for "OpenAI". Their papers and models are not yet public; we eagerly await them!
• This Metamath mailing list discussion about using machine learning to create proofs

There is a very large literature about automated proofs in general. For example:

• "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.

There's a large set of information about using AI/ML systems, and it's being added to constantly. Here are some links:

• AI Canon - some basic background information
• How To Finetune GPT Like Large Language Models on a Custom Dataset
• Open-Source vs. OpenAI. 8 Best Open-Source Alternatives to GPT - warning, it confuses "open source" with "available"
• 512MB Large language models
• https://github.com/bentoml/OpenLLM
• Fine-Tuning Llama-2: A Comprehensive Case Study for Tailoring Models to Unique Applications