4 ms·
Automated theorem proving is a concept that has been around for a long time already. Isabelle's sledgehammer strategy combines automatic theorem provers (E, Z3
by bramhaag 2y ago
Automated theorem proving is a concept that has been around for a long time already.
Isabelle's sledgehammer strategy combines automatic theorem provers (E, Z3, SPASS, Vampire, ...) and attempts to prove/refute a goal. In theory this seems fine, but in practice you end up with a reconstructed proof that applies 12 seemingly arbitrary lemmas. This sort of proof is unreadable and very fragile. I don't see how AI will magically solve this issue.
- gowld 2y agoWhat is a "fragile" proof?
- staunton 2y agoIt no longer works when some definition or other theorem changes slightly. Most of these proof assistants provide ways to write proofs that can slightly adjust and "plug together" the other theorems in the "obvious" way.
- harpiaharpyja 2y agoSo it's a brittle proof