Lean for teaching

Stream: new members

[Johannes Riesterer]

Hello Everybody. Is there any material about how to use Lean and mathlib for an undergraduate lecture?

[Kevin Buzzard]

Can you ask this question in an appropriate thread, e.g. start a new one in the #Lean for teaching stream? This is a question about vectors.

[Kevin Buzzard]

@Johannes Riesterer

[Eric Wieser]

I'm starting to think that by disabling (no topic) we've made this type of mistake more common instead.

[Eric Wieser]

@Johannes Riesterer: you can edit your message above and change the topic name to move this to a new thread

[Johan Commelin]

@Johannes Riesterer Welcome! As Kevin pointed out, there is a #Lean for teaching stream where you can find some useful info.

[Johan Commelin]

Several people have taught courses using Lean. But I'm not sure there is a ready made package that you can use.

[Johan Commelin]

Do you have a specific direction you are interested in? Analyisis? Algebra? Discrete math? Type theory? Applications in computer science? Something else?

[Johannes Riesterer]

Thank you very much. And please excuse my clumsyness... it's the first time i am using zulip

[Kevin Buzzard]

Can you make your question much more precise? Is this a one-off lecture for UGs or part of an UG course? What level UGs? etc

[Johannes Riesterer]

multidimensional differentiation and integration - it is a course for computer scientists

[Johannes Riesterer]

and i thought nothing would motivate them more to learn proofs as programming :-) And i would love to get into the subject becuase i also think it is very interesting

[Johan Commelin]

Makes sense. Although experience suggests that learning Lean and maths at the same time seems pretty hard.

[Johan Commelin]

This is a bug. I would love to fix it.

[Kevin Buzzard]

Right -- my experience is that for students struggling with the material, introducing a computer proof system into the mix just makes things worse, because right now the learning curve is very steep

[Johannes Riesterer]

oh ok that sounds reasonable

[Johan Commelin]

Otoh, with CS students it might be a bit different. You might want to add it as an optional challenge.

[Johan Commelin]

One thing about mathlib: it is not developed with education in mind at all. It generally strives for the largest generality, and does not work out examples or special cases.

[Johan Commelin]

Integration theory is not developed for $\R$ first: it goes straight towards the Bochner integral. Something that 75% of working mathematicians have never even heard of.

[Johannes Riesterer]

oh ok. but it would be possible to go the "learning book" path? How much efford would it be?

[Johannes Riesterer]

for a lean newbie

[Johan Commelin]

Sure, that has been done. See e.g. the Mathematics in Lean book (which is only partly written, wip)

[Johan Commelin]

When are you planning to teach the course?

[Johan Commelin]

I would suggest to play with Lean for at least 1 semester before you dive into teaching with it.

[Johannes Riesterer]

it starts end of september

[Johan Commelin]

Hmm, then I would suggest that you play with lean, and maybe use it for another course somewhere in 2022.

[Johannes Riesterer]

ok that sounds like a plan :-)

[Johan Commelin]

I didn't have a CS background. It took me at least 6 months to get to the point that I would dare to teach with Lean :see_no_evil:

[Johan Commelin]

Situation is a bit better now. There is a lot more supporting material.

[Johan Commelin]

And maybe you have experience with other proof assistants? Or more CS background than I had :rofl:

[Johannes Riesterer]

well i have a lot of programming experience.... and i study Hott for some while now... i have a background as geometer and software developer. So it feels like the next step to do mathematics in such languages

[Johannes Riesterer]

and since i teach from time to time (lectureship only) mathematics for computer scientists this seems like a perfect match

[Johannes Riesterer]

at least perspectively

[Johannes Riesterer]

so thank you very much for your assessment.

[Johan Commelin]

I completely agree. And we need experiments like this, so that the system can become a better teaching tool!

[Johan Commelin]

Especially given your experience with HoTT and general programming experience, I think you should definitely try this, once you are comfy with Lean.

[Johannes Riesterer]

i will keep up with it

[Johan Commelin]

If you know a bit of French: here is a course on metric spaces and such, using Lean https://github.com/FredericLeRoux/LEAN_ESPACES_METRIQUES

[Johan Commelin]

Another popular thing, with CS students, is to go in the direction of software verification

[Johan Commelin]

See also https://lean-forward.github.io/logical-verification/2021

[Johannes Riesterer]

that helps a lot.... thank you.

[Anne Baanen]

I was just going to post that link :)

[Johannes Riesterer]

well i have to teach specific topics

[Johannes Riesterer]

so not too much freedom in selection of topics

[Patrick Massot]

It seems you still haven't found the Lean for teaching stream, you created a Lean for teaching topic in the new members stream.

[Patrick Massot]

(The conversations in Zulip have a 2-levels hierarchy: stream, topic). See in particular this recent topic for more pointers.

[Patrick Massot]

Including https://www.youtube.com/watch?v=mTLuON5eRZI&list=PLlF-CfQhukNnO8z3TcFcoKozif9gbl7Yt&index=23

[Eric Wieser]

(note that while you were able to move your message to a new topic to fix the initial Zulip mishap, only admins have the power to move topics between streams)

[Johannes Riesterer]

Thank you very much

[Johannes Riesterer]

very inspiring