Earlier quoted context omitted.
Oh, I think you might misunderstand what I'm comparing it to. The other tools, like Proverbot9001, are exactly the NNUE scenario you describe, where a small neural network guides a search procedure to find proofs; they are more effective at finding formal proofs than Llemma. For other tasks, like non-formal proof generation, Llemma has novel results as far as I know; it's just in terms of producing formal proofs that…
When do you think we’ll have something that can do “verify this proof of the ABC conjecture” and it would check the proof?
Llemma: An Open Language Model for Mathematics
51–52 of 52 posts