Hacker News Reader

Comment by outlace | Hacker News Reader

For those on the fence about learning Lean or some other theorem prover: I highly recommend it if you want to self-learn math. Learning math from a textbook is rather dry and often doesn’t come with solutions.

Lean essentially gamifies learning math and you always know if you got the right answer. Moreover, unlike written math which is rife with ambiguous notation (unless you’re an expert), math in a theorem prover like Lean is always unambiguous.

View on HN

I'm learning lean with that intent (to self learn mathematics). I get distracted trying to learn how to do better proof automation and tactic golf.

Also, since I don't see anyone mentioning so it far: there is a currently fairly active Zulip chat for the lean prover. They have been quite helpful for me getting started.

I'm planning to learn Agda for this very reason. Have you looked at Agda or other proof checkers?

What about Lean made you decide to use it for this project? The Tactics system?

Yes I've played with Agda before Lean. I found documentation for Agda to be sparse, maybe it's improved since then. Also, it was kind of a pain to get it setup. Lean was extremely easy to get running, works beautifully with VSCode, has great documentation and a helpful community. It's a "sexy" language and set of tooling compared to Agda and Coq (and I'm of the opinion aesthetics matter). It also feels more well-supported with the backing of Microsoft Research behind it.

You are not really learning how to make proofs though, you are learning how to make specifications. There is an important difference. It is one thing to "prove by induction that this loop will end" and another completely to write a specification for the compiler to find a proof for you. It comes down to the fundamental concept of computability. You won't learn true proving if you don't at least attempt to work through e.g. Cantor or Epsilon-Deltas.

It is my understanding that Lean can formalize essentially all of mathematics, whether it's an epsilon-delta proof or otherwise. Not all proofs are computations, which is why some constructs must be labeled `noncomputable` but nonetheless the typer checker can verify the proof is valid.

I hope so. Because otherwise you are not learning real mathematics, just rote memorization. It is not good because that is the mathematical equivalent of a code monkey.

You learn maths, and also formal specification -- an almost wholly different field -- and ultimately enough engineering to ensure your proof checks finish before the heat death of the universe (itself hastened thereby).

Automation of epsilon-delta proofs is in its infancy. Currently with an interactive theorem prover like Lean, you type in the proof yourself, so it's pretty much exactly the same as doing it on paper, except that you can't make a mistake. For example here is a website giving a proof of the squeeze theorem

http://wwwf.imperial.ac.uk/~buzzard/docs/lean/sandwich.html

and if you click on a line in the proof, and then on a little grey rectangle, you will see the state of Lean's brain at that point in the proof. But the proof is just the normal proof and a student writing the proof in Lean has to just write the normal proof, but in Lean's language rather than in mathematical English.

> It is one thing to "prove by induction that this loop will end" and another completely to write a specification for the compiler to find a proof for you.

Lean is an interactive proof assistant, not an ATP. If you're actively using Lean (or for that matter any other proof assistant), you're definitely "learning how to make proofs". Induction-based proofs, specifically, are notoriously hard to automate.

Reply on news.ycombinator.com