5 ms·
It's a pity that the author's high school didn't use geometry as the means of introducing the concept of mathematical proof. The classical high school two-colum
by dhosek 7y ago
It's a pity that the author's high school didn't use geometry as the means of introducing the concept of mathematical proof. The classical high school two-column proof is in many ways quite similar to the methods of Lean, albeit with a different structure.
- aadams 7y agoWill you provide links?
- lordnacho 7y agoDoes Lean allow you to put in geometric proofs? Say someone draws some circles and some lines and wants to prove that some property of the intersection points is true, eg that are always on the same straight line?
- h91wka 7y agoQuick search reveals that some people have encoded Euclid's axioms in Coq (Lean and Coq are based on roughly the same theory): http://geocoq.github.io/GeoCoq/ http://geocoq.github.io/GeoCoq/
- Smaug123 7y agoI greatly recommend Lockhart's Lament (https://www.maa.org/external_archive/devlin/LockhartsLament.pdf https://www.maa.org/external_archive/devlin/LockhartsLament....) which says exactly the opposite. 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.
- JadeNB 7y ago> 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.
- dhosek 7y agoAesthetically, 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.
- 0az 7y agoI personally credit my own geometry education, as much as I disliked it, with giving me the tools I needed to succeed in Calculus. That Calculus final involved proving part two of the FTC. Fun times. AP Calculus? It's much less helpful, in its computational focus.