Hacker News Reader

Comment by outlace | Hacker News Reader

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.

View on HN

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.

Reply on news.ycombinator.com