a new world

Stream: general

[Scott Morrison]

A student, to me earlier today: "I have been reading [some book], and to make sure I am really understanding it, I am implementing some of it in [a different interactive theorem prover]".

[Scott Morrison]

(Of course I have since tempted them into learning Lean.)

[Scott Morrison]

It feels like that moment before a tsunami.

[Scott Morrison]

Will students soon be asking for formalisations of our lecture notes, as well as latex'd lecture notes? :-)

[Scott Morrison]

When I explained that one of the wonderful things about Lean was that you could write new tactics in Lean itself, she was very excited, and started making plans to learn how to do this herself.

[Kevin Buzzard]

I had a student last November who had learnt some Lean at Xena, and I had been teaching some basic facts about congruence mod m in class, and then I taught them equivalence relations and proved that our previous results could be interpreted as saying that congruence mod m was an equivalence relation. The student typed up all the proofs of these facts in Lean and then found me and told me that they felt they really understood equivalence relations now. This was one of the stories that made me want to keep pushing Lean for mathematicians.

[Kevin Buzzard]

I have observed students typing up lectures in LaTeX -- this is normal now; 20 years ago it was unheard of. People develop tricks for being able to do it in real time. Why not a similar sort of thing in Lean? Get a rough idea down, fill in the details later.

[Kevin Buzzard]

You teach enough people how to do it and eventually you'll find someone who decides to have a go.

[Kevin Buzzard]

They'll be hell in class -- constantly asking about edge cases :-)