education

Stream: new members

[Notification Bot]

This topic was moved by Bryan Gin-ge Chen to #Lean for teaching > education

[Daniel Ever]

thanks! I didn't see #Lean for teaching in my list, will investigate.

as for using Lean to learn proofs, I feel that there's a point where having all the previous assumptions in a simple list with a functional simplifier will speed up the learning process significantly. As far as I can judge that comes as soon as the student wants to really understand why different properties for operations with limits (and then derivatives) hold. Classical proofs are very long and nonintuitive at first, so while you try to figure out what does epsilon stand for you already forget what you were trying to prove. Lean allows tracking the goals at every step which is a huge advancement .

When it comes to linear spaces, things tend to pile up much quicker and greatly benifit from a well thought organizing. Anyway, thanks for your input!

[Kevin Buzzard]

Can you delete this message and repost in the new thread?