News for hackers. Stuff that matters.

A comment on Doing a math assignment with the Lean theorem prover. Parent comment

Re:Doing a math assignment with the Lean theorem prover by JadeNB on Monday April 06, 2020 @05:53PM (#22798272)
> I didn't personally undergo "two-column proof" education, and learned what the phrase means from Lockhart's Lament itself, but it sounds miserable; I say this as an MMath who specialised in set theory and logic, and who has been side-project formalising maths in Agda for the last two years.

As a professional mathematician who did go through two-column proof, you're not the only one who finds them miserable. Personally, abstract algebra was what won me over to the beauty of proof (probably that old standby, the irrationality of sqrt(2), was the first); but everyone will find a different experience.

[ Parent | on HN ]
Re:Doing a math assignment with the Lean theorem prover by dhosek on Tuesday April 07, 2020 @11:46AM (#22804267)
Aesthetically, two-column proofs are miserable, but they have the advantage that the logic is very clearly laid out. There's no chance to hand-wave when every step of the proof needs to be explicitly justified.
[ Parent | on HN ]