Acorn and the future of (AI?) theorem proving

It is a simple model, I think it's just a little dense NN with some hand-picked features. (https://github.com/acornprover/acorn/blob/master/python/mode...) Though Kevin has mentioned that, hopefully soon, we'll be able to have small-ish language models trained/fine-tuned on acornlib, but this requires some overhaul of the current approach to search.

> I wonder how they're going to keep it consistent over time (e.g., some proof steps suddenly becoming "unclear" after an update due to randomness of the ML model)

The idea (which I realize I didn't write about in the blogpost) is that each model iteration will be trained on `acornlib` along with previous traces. While it's possible that sometimes the model will fail to find a given proof for a fact (and therefore require some help when it didn't previously), the idea is that the model is learning both from its previous proofs and also new proofs that have been developed in the library since its previous training. In this sense, the model is constantly being "added" to and so should (ideally!) perform at least as well, as the acornlib gets larger.

> Sure, even Terence Tao would likely admit that formalizing proofs with Acorn is easier than with Lean, but formalizing existing/ongoing proofs is only part of the picture.

I think the point here is that, once the model gets good enough, you can just _write_ statements that you think might be true (and are, say, very nonobvious!) and then the Acorn engine would either automatically find a proof or give you a counterexample to the provided statement, which is much more akin to theorem proving with the computer.

> The best LLM provers + Lean combo right now can already crack IMO-level math, and what if they now write proofs in this more natural style?

For sure, my guess is LLM provers will find this style substantially "easier" though they do just fine at Lean, too.

> Will Acorn be better than Lean as an RL signal in this case?

I think this is the hope! The flywheel I think looks something like:

1. Train models using the standard library

2. Models can now discover new proofs of interesting facts and help in proving those more easily

3. Add those to the standard library + reasoning/proof traces

4. Train a new model on that

5. ???

6. Profit?

On the other hand, the `acornlib` (https://github.com/acornprover/acornlib) repo happily takes PRs that pass for many objects such as `Group`s (especially those in the standard library). so if there's something you're interested in proving, I would highly recommend just cloning it and proving it directly in the standard library and then PRing!