[oggy]

AI can be very useful in practice for theorem proving WITHOUT proving "big new theorems" or inventing new mathematics. Right now, what makes theorem proving an extremely expensive undertaking is making proof search work. AI could help immensely by improving the search.

The process of proving things in provers like Lean, HOL or Coq is interactive; roughly, the theorem you want to prove is your starting goal, and you apply tactics to transform the proof goal until the goal becomes the boolean value true. The Platonic ideal of this process is that you provide the main, "creative" steps of the goal transformation, and the tactics discharge the rest automatically. In practice, however, for the process to work, you need to carefully state your theorems in a certain way, and you need an enormous amount of tacit knowledge about how the internals of the tactics, as well as of the libraries of already proved facts that you can use. These things take years of practice to build up. I think it unlikely that theorem provers will see a significant uptake until the tactics (i.e., proof search) improve massively.

This is where I hope AI could step in. There are many challenges, obviously. The training data sets are relatively modest; when I looked a few years ago, the publicly available Isabelle theories, for example, amounted to a few hundred thousand proved theorems, which is a minuscule corpus compared to what something like GPT-3 uses. Then, how do you represent the input, just characters, or do you need more structure? Can you can leverage something like reinforcement learning? How do you could set the training process up? On the other hand, compared to chat bots, the quality of the resulting AI system would be much easier to quantify (success rate on a benchmark of new theorems).

There's already work in this area, but I'm not aware of any grand successes yet. I hope to see much more work on this in the near future. I've been dabbling in it myself a while ago while I was still in academia, but other priorities have taken precedence in the past couple of years.