3 ms·
Have you tried formalizing your ideas with Isabelle? It has a constraint solver and will often find counterexamples to false arithmetical propositions[1]. 1: h
by sudokuist 3y ago
Have you tried formalizing your ideas with Isabelle? It has a constraint solver and will often find counterexamples to false arithmetical propositions[1].
1: https://isabelle.in.tum.de/overview.html https://isabelle.in.tum.de/overview.html
- Nevermark 3y agoI have not, thanks for the tip.
- riku_iki 3y agocurious why you referred specifically on isabelle, which looks ancient and over engineered, there are many other tools and langs in this area. I am not criticizing, but curious about your opinion.
- c-cube 3y agoIsabelle is good at counter examples in ways few other proof assistants are. In general its automation is excellent, partly because it uses a less powerful logic (HOL instead of CIC; more expressive logics are harder to write automation for). It's not obsolete.
- mannykannot 3y agoI have not been able to figure out how that would help in the context of this discussion. As I see it, what’s very interesting here is that an LLM is able to do this.
- riku_iki 3y agoI think the point is that LLM is not right tool for deep reasoning, and isabelle and others are much better such tools, even community trying to apply LLM in this area following current wave of hype.