LLM generation of proofs in FLT project?

Stream: Machine Learning for Theorem Proving

[Kevin Buzzard]

This weekend I put together the first part of a long exercise in the FLT project, whose goal it is to define a certain kind of modular form from scratch. At the time of writing we haven't got as far as defining the modular form yet, but we have made some new types (rings) ZHat and QHat, and I've proved some API for them in LaTeX and stated it all in Lean but some proofs are missing in Lean. The exercise is a connected component in the blueprint with about twenty nodes, not connected to the large FLT component (ignore the small connected components in top right).

example.png

Now many of those Lean theorems were written by Github copilot (possibly including one which was originally completely wrong FLT#56). The 12 blue nodes represent situations where the statement of the theorem is written in Lean and LaTeX, and the proof is written in LaTeX but sorried in Lean. I did not try running my LaTeX proofs through any LLM to see how good they were at writing proofs of these "basic" number-theoretic statements.

I would imagine that there will be many more times in the FLT project when there is suddenly some strong correspondence between a LaTeX blueprint file and a Lean file, except that there are places where the LaTeX has a proof and the Lean has a sorry. The example above is saying that this LaTeX file and this Lean file correspond in a strong way, and the question is how many sorries can an LLM remove autonomously, possibly after some interaction with a Lean server.

[Kevin Buzzard]

PS on looking through the Lean code I suddenly remembered that an LLM wrote that proof and got it right first time.