4 ms·

No, I think you have a pretty good grasp of things. In the real world people do use more powerful tactics like ring to skip all the low-level algebraic manipula

No, I think you have a pretty good grasp of things. In the real world people do use more powerful tactics like ring to skip all the low-level algebraic manipulation (which I personally really enjoyed but can see others finding tedious). Your point about proof readability applies to interactive theorem provers generally. You can see a tradeoff here between Lean/Coq and more "literate" formal proof languages like TLA+, which has a prover called TLAPS (TLA+ Proof System). TLA+ proofs are written in a hierarchical style Lamport proposed in his paper How to Write a 21st Century Proof[0], and are readable by themselves. The BIG BIG tradeoff here is that when you're writing the proof in TLA+, it's very difficult to know what the prover is "thinking" and why it is stuck. Whereas with interactive provers you know exactly what the prover is "thinking" - the proof consists solely of instructions to manipulate those thoughts which you see on screen at all times! So at this time it seems there's a tradeoff between ease of writing a formal proof and ease of reading a formal proof. [0] https://www.microsoft.com/en-us/research/publication/write-21st-century-proof/ https://www.microsoft.com/en-us/research/publication/write-2...

uyt 6y ago
The algebra was tedious because for example, the very second thing you prove in the tutorial is that addition is associative. If you were teaching this to humans you would then immediately tell them that you now can omit parentheses because you have an algorithm to re-parenthesize however you want. But instead, for entire rest of the tutorial, you had to manually rewrite every single parenthesis yourself (with syntax that is pretty unergonomic for doing so too). I guess I found it a little disappointing that it's not easy to instruct it on how to fill in gaps so you can skip steps the same way you would in a human proof (which would only need a note saying that you're using associativity and parens are omitted thereafter, and any human reader will accept that as valid)

uyt 6y ago

The algebra was tedious because for example, the very second thing you prove in the tutorial is that addition is associative. If you were teaching this to humans you would then immediately tell them that you now can omit parentheses because you have an algorithm to re-parenthesize however you want. But instead, for entire rest of the tutorial, you had to manually rewrite every single parenthesis yourself (with syntax that is pretty unergonomic for doing so too). I guess I found it a little disappointing that it's not easy to instruct it on how to fill in gaps so you can skip steps the same way you would in a human proof (which would only need a note saying that you're using associativity and parens are omitted thereafter, and any human reader will accept that as valid)