4 ms·
This is a proof assistant, not an automated theorem prover. The user has to supply* the mathematics and the proof checker formally verifies whether or not the s
by 363849473754 5y ago
This is a proof assistant, not an automated theorem prover. The user has to supply* the mathematics and the proof checker formally verifies whether or not the steps are correct. It doesn’t have any creativity (that’s up to the mathematician).
*I should have clarified there is some proof generation, see the comment below by opnitro, but I meant the meat and potatoes of novel non-trivial proofs currently has to be supplied by the user.
- ajarmst 5y agoThanks for the clarification.
- opnitro 5y agoThat's not quite true. Many of these proof assistants support some level of automation and proof search. I haven't used Lean specifically, but it's quite common in Coq for projects to write proof search techniques specific to the problem domain and utilize them in their proofs.
- chriswarbo 5y agoTrue, and Isabelle can call out to automated provers (a mechanism called "sledgehammer"!)