2 ms·
What 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
by robinzfc 7y ago
What 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.