4 ms·
If you're using a proof assistant, you can't just write something like "X clearly follows from Y" or "Z is left as an exercise to the reader": you have to speci
by logicchains 7y ago
If you're using a proof assistant, you can't just write something like "X clearly follows from Y" or "Z is left as an exercise to the reader": you have to specify every step, even if they're steps a human reader would easily figure out themselves.
- robinzfc 7y agoWhat logicchains says above is true in some sense but of course it depends on the degree of automation a given theorem proving environment provides. In Isabelle a proof may consist of the keyword "using" followed by a list o 9-10 theorems and it may be accepted if the list is complete (in some sense).
- logicchains 7y agoThat's definitely true, but unfortunately I think the set of things "left to the reader" is way larger than the set of things Isabelle can figure out by itself, even with Sledgehammer.
- lonelappde 7y agoOf course you can! You can put any axioms (a claim that a conjecture is true is an axiom) you want in a proof assistant. What you cannot do is not say those things but still rely on them in your proof.