4 ms·
We need to develope tools that can automatically fill small gaps (ones left as errors in the essay), because the point of having mechanized proofs is to not hav
by fspeech 4y ago
We need to develope tools that can automatically fill small gaps (ones left as errors in the essay), because the point of having mechanized proofs is to not have gaps. Then practitioners can write lemmas and let the computers do the checking.
- reuben364 4y agoIn the proof assistants I'm familiar with, such as Lean and Coq, you can write tactics which generate proofs for a goal and potentially produce more subgoals. However there isn't a "one size fits all" tactic for these gaps. One area that is being explored is ML for generating proofs, but training data is limited.
- fspeech 4y agoThe 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.
- mbrodersen 4y agoDafny is a great example of what you are talking about. It automated most of the proving. However you still need to figure out the key invariants.