35 ms·
> Automated theorem checking is typically very difficult for any nontrivial theorem I'm not sure this is true -- I thought the whole idea of these theorem syst
by andrewla 8y ago
> Automated theorem checking is typically very difficult for any nontrivial theorem
I'm not sure this is true -- I thought the whole idea of these theorem systems was to make the kernel of the proof system as simple as possible (to allow a manual proof, or at least high confidence of correctness).
If your program can produce an instance of a type, and it type-checks, then it true. Type inference can be tricky, and a lot of what makes the systems usable is the fact that you can omit types and allow the compiler to infer them, but a fully-expressed typed proof outline is enough to quickly verify correctness of the proof.
- throwawaymath 8y ago> but a fully-expressed typed proof outline is enough to quickly verify correctness of the proof. Yes, implementing that is the difficult part. I'm not saying it's infeasible - I'm saying it's very difficult. Writing provably correct software is also very difficult. This kind of theorem checking is becoming more common for theorems in e.g. combinatorics, but it's still very uncommon due to the added effort.
- danharaj 8y agoEncoding a proof to check it is the hard part.
- deleted 8y ago[deleted]