4 ms·
Automated tools like Sledgehammer (Isabell/HOL) removes a lot of the manual work.
by mbrodersen 4y ago
Automated 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.