8 ms·
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 neu
by aSanchezStern 3y ago
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 it currently seems to lack as compared to the state of the art.
- Vetch 3y agoAh you're right. That makes sense. The autocomplete, informal proofs, translation or autoformalization, reference, search, feedback interactive assistant use-cases do seem promising though.
- jychang 3y agoWhen do you think we’ll have something that can do “verify this proof of the ABC conjecture” and it would check the proof?
- aSanchezStern 3y ago1979 :) https://en.wikipedia.org/wiki/Logic_for_Computable_Functions https://en.wikipedia.org/wiki/Logic_for_Computable_Functions
- schoen 3y agoIf the proof is written in a formal language, we have that now! Even several directly competing efforts (for better and worse). https://www.cs.ru.nl/~freek/100/ https://www.cs.ru.nl/~freek/100/ Some people greatly hope that fully formal proofs become a routine part of math research and communication in the future.