Summer of Math Exposition

Really nice, we need more Lean content!

The importance one might assign to formalizing proofs in Lean. I wonder aboput the interaction of this with AI.

It made me feel confused. I began to want to understand how to use Lean to prove my own theorems, but it’s hard to gather how I could do that based on this one example.

The Lean programming language is really interesting and something that could definitely use some exposure!

This was a nice introduction to fundamental proof techniques and Lean.

A nitpick: The post assumes knowledge of De Morgan laws, which I don’t think is something a reader who is learning proof techniques for the first time will know.

I think the introduction to Lean is very cool, and I’m glad I got to learn about it since I’ve never heard of it before. However, I think the introductory part of the article where you describe how proofs work is incomplete, and isn’t enough for someone who doesn’t have any prior knowledge. If this article isn’t geared towards that group of people, then great, but by including an intro to proofs and not doing it full justice isn’t helpful. For example, you talk about logical equivalence of P implies Q to not Q implies not P in the contrapositive section. To someone who doesn’t know anything about formal logic, this is very confusing because you don’t into the truth tables and what not to show the two statements are logically equivalent. Additionally, I think the truth table for P implies Q can be sort of tricky to understand for a beginner, especially why if P is false then the implication is always true. So by skipping these steps and not breaking it down, the overall intro doesn’t properly teach the concept.

Neat introduction to proof assistants. More rationale for what they’re useful for (bigger proofs?) would be nice. Some small typos, e.g. ‘7th line’ actually referring to the fourth line of code

It would be nice to have syntax highlighting when quoting the code in the paragraphs. I still don’t quite get everything even though I have extensive programming experience, I guess formal proof languages are a different species. I’m interested in Lean so this article is squarely in my interest zone.

I’m sorry, I just had a feeling this is poorly written in general. Too many Lean concepts are introduced when you could have probably chosen a better proof example or more easier ones gradually building on top of each other. Maybe some classic proofs on number properties? The only Lean experience I had prior to reading this is basically going myself through the exercises in section 2.1 here (https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html#calculating), and I think I enjoyed it.

There are some grammatical errors.

I’ve spent a fair amount of time playing around with Lean; not an expert by any means, but reasonably confident with the ideas at least. With that context, I found the writeup quite enjoyable. However, there were a number of points when I had to rely on my my past knowledge to be confident in what you were saying.

For instance:

• The concept of “mode” was introduced but then mostly dropped. I don’t think a new user would know what to make of that.
• The word “tactic” shows up without any preamble about what a tactic is or does for us
• I feel like when you are forced to use unintuitive notation like “.1” then you should be a little apologetic. It’s not your fault, after all, but an acknowledgement that remembering which direction is 1 vs 2 is annoying, would a lot way toward connecting with the reader.

I know that these are generally not important for a first-time user to understand, but the point is that they won’t know that. I think you’re being intentional about not defining them (they are weirdly technical after all) but I worry that using these “insider words” will get folks hung up on minutae like this without realizing that in the end they’re not that important yet.

Two things I appreciated:

Part One (A) is a nice human touch that you wouldn’t find in a textbook. Some readers won’t like this but I think it’s wise to simulate the actual thought process you’d go through to prove a theorem, without sanitizing away the paths that didn’t work.

Personally, I really appreciated the link to the web version. It’s been obnoxious to install Lean on my computer and I keep having problems with it, so glad to know easier options exist.

V. Nice!