Zulip Chat Archive

Stream: Lean for teaching

Topic: Two workshops

Patrick Massot (Mar 06 2023 at 15:17):

I don't think there have been any announcement here, but there will be two events about teaching using a proof assistant, and Lean in particular: https://sites.google.com/view/learning-maths-with-lean2/ and https://pat2023.icube.unistra.fr/

Martin Dvořák (Mar 06 2023 at 16:13):

It isn't in Lean 2, is it?

Adam Topaz (Mar 06 2023 at 16:14):

I assume that it's 2 as opposed to https://www.lboro.ac.uk/departments/maths-education/events/2022/learningmathematicswithlean/

Sebastian Ullrich (Mar 06 2023 at 16:25):

According to the website title it's actually Lean -2, which I'm assuming is the new version supporting homotopy type theory

Kevin Buzzard (Apr 18 2023 at 13:02):

The learning maths with Lean workshop starts in an hour, at 2023-04-18T15:00:00+01:00 . Today we'll have @Gihan Marasingha at 2023-04-18T15:15:00+01:00 , then me at 2023-04-18T15:45:00+01:00 , then @Rob Lewis at 2023-04-18T16:30:00+01:00 and finally @Jeremy Avigad at 2023-04-18T17:00:00+01:00 . Note that the times on the website are in GMT, which is not the current UK time zone, we're right now in BST=GMT+1.

Eric Wieser (Apr 18 2023 at 13:23):

Will these talks be recorded?

Kevin Buzzard (Apr 18 2023 at 13:26):

IIRC I signed something which usually means "yes"

Alex J. Best (Apr 18 2023 at 13:28):

I asked the organisers and was told "yes we are planning to record the talks and post a link to the recordings on the event website."

Kevin Buzzard (Apr 18 2023 at 14:03):

Apparently they will be up on youtube "very soon"

Kevin Buzzard (Apr 19 2023 at 14:06):

Today at the second Learning Maths with Lean conference we have:

@Athina and Paola Iannone talking about their observations of students playing #nng at 2023-04-19T15:15:00+01:00 ,

then some students from Imperial and Exeter reporting on having survived lectures by Gihan and me at 2023-04-19T15:45:00+01:00 ,

then @Kitty Yan and @Gila Hanna talking about "Proving with the Lean theorem prover: The case of transitivity of implication" at 2023-04-19T16:30:00+01:00 ,

and finally @Heather Macbeth talking about her course; her title is " A "calculation-heavy" introduction to proof, with support from Lean" and she's at 2023-04-19T17:00:00+01:00 .

Adam Topaz (Apr 19 2023 at 15:52):

Kevin Buzzard said:

Apparently they will be up on youtube "very soon"

Does anyone have a link handy to this youtube page? (Even if the lectures have not yet been posted, it would be useful to have.)

Kevin Buzzard (Apr 19 2023 at 16:00):

I'm not sure it exists yet.

Kevin Buzzard (Apr 19 2023 at 16:00):

(the lectures haven't even all happened yet)

Kevin Buzzard (Apr 20 2023 at 14:17):

Today starts with @Patrick Massot right now 2023-04-20T15:15:00+01:00

Kevin Buzzard (Apr 20 2023 at 15:35):

Then @Phil Wood at 2023-04-20T15:45:00+01:00, and after that it's students sharing their experiences.

Pietro Monticone (Apr 20 2023 at 16:48):

Kevin Buzzard said:

Apparently they will be up on youtube "very soon"

I've just asked:

Where will the recorded talks be published? Do you have a YouTube channel I can subscribe to already?

They replied:

We will add them to the Southampton Education YouTube channel but we will email everyone when the talks are uploaded

The YouTube channel they mentioned should be this one.

Kevin Buzzard (Apr 20 2023 at 16:57):

As a bonus, @Dan Velleman is speaking at I think 2023-04-20T20:00:00+01:00 on his Lean translation of "how to prove it". Zoom link available at https://emap.fgv.br/en/event/how-prove-it-lean

Last updated: Dec 20 2023 at 11:08 UTC