4 ms·
The tactics still require users to be aware of their existence and using them correctly (a non trivial mental load). And the resulting proof script is brittle a
by fspeech 4y ago
The tactics still require users to be aware of their existence and using them correctly (a non trivial mental load). And the resulting proof script is brittle and hard to read. This is what the essay attempted to improve over.
- mbrodersen 4y agoAutomated tools like Sledgehammer (Isabell/HOL) removes a lot of the manual work.
- fspeech 4y agoI have not used Sledgehammer but even with a SAT solver we still need to handle quantifier instantiations. And in case the SAT solver fails (I mean time-outs, not finding counter-examples) we won't get clues on how to fix it. SAT solvers work on CNF, which is very far from the deeply structured formulaes that math tends to generate.
- mbrodersen 4y agoI am not a working mathematician and don’t care about formalising mathematics. For the things I do care about (proving code correct) tools like Sledgehammer are awesome.