Zulip Chat Archive

Stream: general

Topic: a new world

Scott Morrison (Mar 26 2018 at 00:46):

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 (Mar 26 2018 at 00:47):

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

Scott Morrison (Mar 26 2018 at 00:53):

It feels like that moment before a tsunami.

Scott Morrison (Mar 26 2018 at 00:56):

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

Scott Morrison (Mar 26 2018 at 00:58):

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 (Mar 26 2018 at 06:39):

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 (Mar 26 2018 at 06:41):

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 (Mar 26 2018 at 06:42):

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

Kevin Buzzard (Mar 26 2018 at 06:42):

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

Last updated: Aug 03 2023 at 10:10 UTC