Thoughts on AI for theorem proving

#draft/aitp_thoughts/

---

Introduction and TOC

These are a set of notes which explore my thoughts on theorem proving and AI. They aren’t much more than personal notes which I’m sharing because they might be of greater interest. This of them as a (poorly written) series of blog posts. I didn’t have time to clean them up as much as I would have preferred.

I also want to clarify that I explore many ideas here. It’s difficult to say often where ideas come from. Half of my ideas come from reading papers in AI that have nothing to do with theorem proving, and saying “huh, wouldn’t it be great to do that in theorem proving as well?” Other ideas come from reading papers in the field and thinking of how to extend their works. Further, sometimes a conversation I have or a talk I see spurs lots of thoughts. For example, recent conversations with Lasse Blaauwbroek have made we question a lot of my thinking in this area. Also, conference talks, podcasts, etc. play a lot of roles in my thinking. For example, Szegedy has made a number of small comments in many of his public settings which have really spurred me to think about things more clearly.

It is likely the case that most of “my ideas” I explore here are not new. For lack of time I haven’t systematically tracked the literature to see if any of these have already been worked on. I’m likely missing out on talking about important related work at points, especially work of Josef’s Urban and his collaborators. I don’t see this as a document that should be cited, just like you wouldn’t cite a few off-hand remarks someone makes on a podcast, a talk, or in a blog.

In the end, I just want to help this field move forward, and if my thoughts here help, more the better. If not, at least they helped to clarify my thinking.

Summary of my thoughts on AI for theorem proving

[[Summary of my thoughts on AI for theorem proving]]

Broader Impact: Beyond the usual talking points

[[Broader Impact: Beyond the usual talking points]]

User stories: What is our goal, really?

[[User stories: What is our goal, really?]]

Auto-formalization: Let’s be realistic?

[[Auto-formalization: Let’s be realistic]]

SoTA trends in AI: Let’s embrace it!

[[Embracing new SoTA trends in AI]]

Learning Fast vs. Learning Slow: Can we have the best of both?

[[Fast vs. slow (online vs. offline) learning]]

*Proof Search: Why it’s not really working and what we can do about it

[[Search]]

*MathZero: What does zero mean?

*Benchmarks

*Tools and Environments

Models

Reinforcement Learning

Big ideas

Dump:

• Create library of little obvious theorems (lots of ways to do this)
• Challenges in RL if library changes
• Tree search benchmarks (with and without RL).
• What “product” are we building?
• Don’t forget related areas?
• Issues of data leakage in LLM
• Self supervision ideas