Acorn and the Future of AI Theorem Proving
Original: Acorn and the future of (AI?) theorem proving
Key topics
The theorem-proving landscape is abuzz with the emergence of Acorn, a newcomer that's generating excitement with its streamlined user experience. As commenters dug into Acorn's inner workings, they discovered that its "AI" prover relies on a relatively simple neural network with hand-picked features, rather than a cutting-edge model. While some users praised Acorn's potential, others noted that its library is still in its infancy compared to established players like Lean's mathlib. Despite this, the community is optimistic about Acorn's growth prospects.
Snapshot generated from the HN discussion
Discussion Activity
Light discussionFirst comment
4d
Peak period
3
90-96h
Avg / period
2
Key moments
- 01Story posted
Aug 30, 2025 at 12:06 PM EDT
4 months ago
Step 01 - 02First comment
Sep 3, 2025 at 5:47 AM EDT
4d after posting
Step 02 - 03Peak activity
3 comments in 90-96h
Hottest window of the conversation
Step 03 - 04Latest activity
Sep 3, 2025 at 12:54 PM EDT
4 months ago
Step 04
Generating AI Summary...
Analyzing up to 500 comments to identify key contributors and discussion patterns
Want the full context?
Jump to the original sources
Read the primary article or dive into the live Hacker News thread when you're ready.
To me the more intriguing question is: how would Acorn's "natural" interface cooperate with LM-based theorem provers? 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? Will Acorn be better than Lean as an RL signal in this case?
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!