Successes of machine learning in formal theorem proving

Question

Attempts to apply machine-learning (as opposed to hand-crafted automation) to formal theorem proving are still in their infancy.

Still, there have been some successes. GPT-f found some proofs that were shorter than existing proofs in the Metamath library, and were accordingly accepted there.

Are there other applications of machine-learning to constructing proofs in any proof assistant that attained a success of at least this magnitude - i.e. finding somewhat better versions of existing proofs, if not entirely new proofs?

"Better" can be measured by whatever standards that proof assistant's community usually uses to evaluate proofs, i.e. a shorter proof might not count if it is less readable or less maintainable.

Answer 1

Only a bit more than two months ago, a new formula for Kazhdan-Lusztig polynomials was found by Google's deep learning subsidiary: DeepMind (the same machine-learning company that wrote AlphaGo to beat humans at the board game Go). This formula is presented as Theorem 3.7 in the above-linked paper, and the authors conjectured in the same paper that the formula gives the right answer for any hypercube decomposition (which they indeed checked computationally for all of the Bruhat intervals up to $S_9$, which turned out to be more than a million of them). This conjecture which they computationally found to be very likely true, implies the combinatorial invariance conjecture for symmetric groups, which has been unproven since it was first formulated the 1980s.

The proof of Theorem 3.7 is given in Sections 4-5 of the above-linked-paper, but and is very much a "pen-and-paper" proof, but the theorem itself was discovered amidst the training of machine learning models to predict Kazhdan-Lusztig polynomials from Bruhat graphs, in Nature (2021) "Advancing mathematics by guiding human intuition with AI" which was only published about 2 months ago (Fig 3 shows which hypercube edges are the most important ones as determined from a saliency analysis, and these turned out to be precisely the edges related to the new theorem). Carlo Beenakker called this "the first significant advance in pure mathematics generated by artificial intelligence" in the highest-voted answer to "Breakthroughs in Mathematics in 2021" on MathOverflow (an answer on which you were the first to write a comment!).

Overall, the combinatorial invariance conjecture for symmetric groups remains unproven, but machine-learning helped to discover a "Lemma" which is very likely to be a part of the proof. I would call this a major "success of machine learning in theorem proving", but about this part of your question:

"Are there other applications of machine-learning to constructing proofs in any proof assistant that attained a success of at least this magnitude - i.e. finding somewhat better versions of existing proofs, if not entirely new proofs?"

I hope I'm wrong, but even for proofs done by theorem provers without machine learning, the ones I know were not for entirely new proofs but for finding somewhat better versions of existing proofs. In the case I described above, a new proof would rely on a Lemma which the saliency analysis (a machine learning technique borrowed from the computer vision community) was able to help find.

Answer 2

The group at OpenAI has recently published a new paper, among other problems they have been able to prove two questions from the International Mathematical Olympiad. Isabelle's Sledgehammer has been able to find solutions to some of these examples as well, and they of course have been proved by many people already.

I guess it's open for debate whether the proofs found by GPT-f are better than the ones found by ATP or constructed by humans, but at least Kevin Buzzard finds some of the proofs quite surprising.