Did not know about Acorn and it was an interesting read! However, I did a bit of digging and haven't found further details on how Acorn's internal prover "AI" works (saying it is an "ML" model makes me think it's some sort of oldschool model like random forests, but not sure yet). Though whatever it is, 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).
I'm also not sure how this prover really fits in the AI proof scheme. 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.
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?
Definitely looks like a smoother experience than using Lean from this presentation. I guess their library is less fleshed-out than mathlib at the moment but that can only grow I suppose (hence acorn??). Will be curious to see how it develops
3 comments
[ 2.8 ms ] story [ 16.0 ms ] threadTo 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?