I’ve done most of the exercises in Logical Foundations (in Coq), and quite enjoyed the process. However:

I believe learning Lean has brought great clarity to my understanding of mathematical proofs. In a way it’s like the perfect scratch pad, focusing your mind on the goal while keeping track of all your assumptions and checking your thinking.

I can’t say I share this few. In my experience, mechanized proofs are overly verbose and at times more difficult than informal proofs (you can’t prove by contradiction, nor assume the principle of excluded middle; there’s some hoops to jump through!). In particular, while the proof in the article is certainly correct, it could quite easily be informally proven using geometric intuition.

Further (and the authors of LF caution against this), it’s easy to get caught up in the mechanical details of the proof, and hammer away at the keyboard transforming your goal until finally you get something that works. This approach does not at all elucidate the actual high-level reasoning behind the proof, neither to the creator of the proof, nor to others.

Either way, nice article! I’d look into the code highlighter; it seems like it treats multiplication as a comment delimiter :D

I think for me mechanized proofs really scratch my desire to have each transformation documented & checked… but I could see that getting annoying after a while! I agree with you there have been times where I’ve been lost in the middle of a more complicated proof, churning away without really thinking about what I’m doing. Translating existing informal proofs into formal language is a skill I still need to learn - lot of it is just inability to translate many handwavy proof constructs into Lean. For example, I think it would probably be difficult for me to translate the informal proof given at the start of the blog post into Lean.

I’ve talked with Leslie Lamport about Lean and he generally dislikes it (and interactive provers in general); he has an idea about how proofs should look, hierarchical in nature so you can see the high-level steps then recursively expand the proof steps to see all the lower-level proofs of those steps. Supposedly something like this is implemented in TLAPS (the TLA+ Proof System) but I haven’t yet managed to learn it.

I’ve done most of the exercises in Logical Foundations (in Coq), and quite enjoyed the process. However:

I can’t say I share this few. In my experience, mechanized proofs are overly verbose and at times more difficult than informal proofs (you can’t prove by contradiction, nor assume the principle of excluded middle; there’s some hoops to jump through!). In particular, while the proof in the article is certainly correct, it could quite easily be informally proven using geometric intuition.

Further (and the authors of LF caution against this), it’s easy to get caught up in the mechanical details of the proof, and hammer away at the keyboard transforming your goal until finally you get something that works. This approach does not at all elucidate the actual high-level reasoning behind the proof, neither to the creator of the proof, nor to others.

Either way, nice article! I’d look into the code highlighter; it seems like it treats multiplication as a comment delimiter :D

I think for me mechanized proofs really scratch my desire to have each transformation documented & checked… but I could see that getting annoying after a while! I agree with you there have been times where I’ve been lost in the middle of a more complicated proof, churning away without really thinking about what I’m doing. Translating existing informal proofs into formal language is a skill I still need to learn - lot of it is just inability to translate many handwavy proof constructs into Lean. For example, I think it would probably be difficult for me to translate the informal proof given at the start of the blog post into Lean.

I’ve talked with Leslie Lamport about Lean and he generally dislikes it (and interactive provers in general); he has an idea about how proofs should look, hierarchical in nature so you can see the high-level steps then recursively expand the proof steps to see all the lower-level proofs of those steps. Supposedly something like this is implemented in TLAPS (the TLA+ Proof System) but I haven’t yet managed to learn it.

Thanks for the tip about the code highlighter!

Just played through the first level of the mentioned Natural Number Game, excellent fun!