A manageable topic for beginners

Stream: new members

[Byung-Hak Hwang]

Hello,

I'm planning to give a tutorial on Lean 4 (though I'm still a beginner myself).
The audience will consist of undergraduate and first-year graduate students.
I'd like to demonstrate how to use Lean for formalization in 1.5 to 2 hours.
I'll be writing Lean code on the screen, and the audience will follow along on their laptops.
So, I'm looking for a suitable topic to formalize.
If there is a topic (e.g., the Pythagorean theorem) that is manageable for beginners, please let me know.

[Julian Berman]

I think there's https://github.com/PatrickMassot/GlimpseOfLean which is intended for around that time frame. You can find some discussion of it in the #Lean for teaching stream as well. On the math side I think people will say to pick a topic that your audience knows well and for which the Lean code looks close to the math they know (rather than some vast generalization of it).

[Kevin Buzzard]

Patrick's Glimpse is definitely a good choice; I've also used my own repo https://github.com/ImperialCollegeLondon/formalising-mathematics-2024 and gone through some of the early sections (e.g. section 5 on groups is suitable for this sort of tutorial). One trick I'd recommend is to rehearse what you're going to go through so that you're less likely to get stuck when presenting.

[Byung-Hak Hwang]

Julian Berman 말함:

I think there's https://github.com/PatrickMassot/GlimpseOfLean which is intended for around that time frame. You can find some discussion of it in the #Lean for teaching stream as well. On the math side I think people will say to pick a topic that your audience knows well and for which the Lean code looks close to the math they know (rather than some vast generalization of it).

Thank you for your suggestion. I'll check them.

[Byung-Hak Hwang]

Kevin Buzzard 말함:

Patrick's Glimpse is definitely a good choice; I've also used my own repo https://github.com/ImperialCollegeLondon/formalising-mathematics-2024 and gone through some of the early sections (e.g. section 5 on groups is suitable for this sort of tutorial). One trick I'd recommend is to rehearse what you're going to go through so that you're less likely to get stuck when presenting.

Thank you! Patrick's, and yours notes seem very useful. I'll check them carefully.