4 ms·

I played it recently. I spent almost a full day to finish all the worlds and then lost interest afterwards. I think I had expectations that it would be a lot l

• ahelwer 6y ago
  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)
• Cybiote 6y ago
  I originally intended to write what follows as its own comment but, although I used Coq instead of Lean and worked through a different set of exercises, your criticisms so closely mirrored mine, I decided to reply here instead, and point out promising paths to solutions. I too felt it a waste of time to prove things that were clearly "obvious". Of course, in math, some of the most frightening words to encounter are "obvious" and "trivial" but in this case it really was trivial, at the level of proving `a + b = b + a` while working with integers. Tactics like auto, tauto, ring and field help here and should be given more and earlier emphasis in teaching materials. Tactics like `auto` perform like the proof search you mention and others like ring and field make cleverer use of structure. To fill in the rest of the gap, a project like the Lean math library goes a long way. Not having to provide your own implementation of reals, differential forms or vectors over reals or complex numbers is incredibly useful. I was surprised by how difficult it was to find (I never did) a well maintained and documented library of basic common mathematical structures in Coq. The second major issue is Formal proofs without their contexts (something like a debugger variables watch list in regular type code), are incomprehensible to most. However, a project, https://plv.csail.mit.edu/blog/alectryon.html https://plv.csail.mit.edu/blog/alectryon.html, for Literate Formal proofs fully addressed that pain point for me. It's curious how the problem of tedium has a clear path to solution in the Lean community and the equally important flaw of write only proofs is being addressed within the Coq community. Returning to the issue of what is obvious, a vast amount of mathematical knowledge is tacit, buried in the minds of the respective communities of pure mathematicians. For everyone else, especially users who cannot themselves provide proofs, mathematical knowledge is very often like a Potemkin village. Superficial and artifice, understanding that falls apart upon close inspection. This divide plays no small part in how difficult it is to properly learn mathematics outside of a mathematics department. Formalizing undergraduate math is important because it provides a solid foundation that leads to deeper understanding of mathematics when taken in aggregate across all participants. Even pure mathematicians have gaps once they step outside their field of expertise.
  • fspeech 6y ago
    Actually there isn't much to understanding the tactics unless you want to use them similarly, just like you wouldn't bother looking into what "auto" has done. For understanding math it is a lot more important to understand the lemmas and why they are structured certain way, akin to understanding the API of programs. We can think of theorems as math's public API and lemmas the internal API for devs. In machine checked proofs lemmas often take on distinct flavors because how a human normally proves things may be hard to mechanize. Intead of tools for understanding tactics (granted, these could be useful for tacticians :) we really need tools to help us visualize structure of proofs. If I know how to write a lemma, tactical proof is rarely a blocking issue. Once it is checked the tactics become irrelevant. They were just there to convince the proof checker.