alt Hacker News> Reconfiguring existing proofs in ways that have been tedious or obscured from humans,
To a layman, that doesn't sound like very AI-like? Surely there must be a dozen algorithms to effectively search this space already, given that mathematics is pretty logical?
Replies
Legend2440 • yesterday at 1:22 AM
The issue with traditional logic solvers ('good old-fashioned AI') is that the search space is extremely large, or even infinite.
Logic solvers are useful, but not tractable as a general way to approach mathematics.
➕ show 1 reply
AndrewKemendo • yesterday at 12:27 AM
Define laymen here
The fact of how you use the term AI tells me that you are a representative of laymen so what precisely are you trying to define?
It might be helpful to understand the term artificial intelligence first:
I actually know about this a bit since it was part of what I was studying with my incomplete PhD.
Isabelle has had the "Sledgehammer" tool for quite awhile [1]. It uses solvers like z3 to search and apply a catalog of proof strategies and then try and construct a proof for your main proof or any remaining subtasks that you have to complete. It's not perfect but it's remarkably useful (even if it does sometimes give you proofs that import like ten different libraries and are hard to read).
I think Coq has Coqhammer but I haven't played with that one yet.
[1] https://isabelle.in.tum.de/dist/doc/sledgehammer.pdf