I greatly recommend Lockhart's Lament (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.

> 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.

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.

I 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.

Does 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?

Quick 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/

Will you provide links?