teaching algebraic structures

Stream: Lean for teaching

[Rob Lewis]

I'm about to introduce my class to groups, rings, and fields. Mathlib's implementations have a lot of noise, for forgetful inheritance reasons. I don't want to introduce my students to this notion yet. So we'll start by defining group on our own, but very quickly I want all the group theorems in mathlib, so we'll have to switch.

How have others dealt with this dissonance? I'll tell them "there are a lot of fields you see when you #print group that you can really just ignore." But it's really ugly, and I don't think there's a clean way to see only the necessary fields of a structure, is there?

[Rob Lewis]

In particular, using the hole command to generate a skeleton structure shows you all the junk.

[Rob Lewis]

If you start with an empty structure { } the error messages "field ... was not provided" only cover the necessary stuff, which is good. But this isn't a great way to display it and it's annoying to have to go through them one by one.

[Kevin Buzzard]

I absolutely agree with you. I've only dealt with groups in one-off lectures, not in classes, and since the nsmul stuff appeared I've been rolling my own. You even see this problem with preorder, where using the hole command generates lt even though it's :=... and lt_iff_le_not_le even though it's ... . order_laws_tac. I would just switch, under the pretence that "we spent an hour proving theorems about groups but clearly we don't want to go through all x thousand lines of code in mathlib about group theory, oh by the way, here's a custom constructor I just made which enables us to make mathlib groups using exactly the same axioms as we used to make those hand-rolled groups last time"

[Johan Commelin]

Can meta programming detect which fields have default args?

[Kevin Buzzard]

you want to detect default args and args which are filled in with default tactics

[Kevin Buzzard]

"don't look at the definition of a group, it's not what you think it is" is no different to "don't look at the definition of a compact space, it's not something about open covers having finite subcovers despite the fact that this is the definition in every math textbook ever"

[Johan Commelin]

fair enough

[Filippo A. E. Nuccio]

@Kevin Buzzard When teaching your class last Spring (the formalising_mathematics repo), did this problem occur often? I am asking because I will need to teach a course next year and wanted to draw inspiration from yours.

[Kevin Buzzard]

My course was 8 independent short stories. So in the group theory short story I rolled my own groups and subgroups, and then we put them away and never used them again; later on when we needed groups I used mathlib's groups.

[Filippo A. E. Nuccio]

Ah OK, I see. And did you do a "pilot Episode 0" telling students the basics or was Episode 1 the true beginning, with them already in front of some Lean Code?

[Kevin Buzzard]

I demanded that everyone install Lean/VS Code etc beforehand, and then I just put episode 1 in front of them, and it was way way way too much material to cover in 2 hours. My current attempt on how to start a Lean course for mathematicians is here

[Kevin Buzzard]

I will be getting 1st years to beta test it next week

[Rob Lewis]

I'm ready to handwave it away for now, but some of my students will do math-y final projects and I don't want them to use a handrolled group for that. I trust them to figure it out more or less after I explain the handwaving. But this is a big-ish UI hiccup.

[Rob Lewis]

Metaprogramming can detect default tactics but not default args, afaik

[Filippo A. E. Nuccio]

Thanks! I have also seen you will be teaching in Term 2 to more advanced students. I guess I will try to steal a lot of ideas, is it allowed :angel: ?

[Rob Lewis]

We should definitely update that hole command to omit as many provided fields as we can detect.

[Kevin Buzzard]

@Rob: I've got used to it now. You roll your own natural numbers / groups / whatever, you maybe give them silly names like xena.group or my_group, you play around with them, and then you say "but of course we need 1000 lemmas so we're going to have to use mathlib's official ones now"

[Kevin Buzzard]

@Filippo I'm going to start preparing teaching materials for final year UGs in November and it will all be publically available.

[Filippo A. E. Nuccio]

Great! I will then ask for the link. I think that finding a balance in what you're currently discussing with Rob will be a hard point for a novice teacher.

[Kevin Buzzard]

@Rob the mantra I always push is "don't unfold -- use the API", but your audience will be different to mine; probably a bit less scared about computers but also I suspect far happier to take on board the idea that there can be more than one implementation of a structure and that it's not for them to worry about how the devs actually did it as long as they can use it.

[Filippo A. E. Nuccio]

Ah, one more question: from your experience, would you recommend having the students be in front of their PC trying to code 100% of the time, or would it be better to have some balance between me showing/coding/teaching "classically" and them trying/coding/getting frustrated?

[Adam Topaz]

Getting frustrated is the only way to learn (in my opinion)

[Filippo A. E. Nuccio]

I basically agree, but wouldn't you think that a bit of balance might help? I am happy I haven't been confronted to prismatic cohomology before simplicial one... But sure, you're right: a good deal of frustration helps.

[Adam Topaz]

The issue with groups is not just about the weird fields like gpow_..., but also because the first definition students see for groups is "A set $G$ with a binary operation such that blah blah blah". I introduced lean to a few of my group theory students this term, and the fact that $(-)^{-1}$ is defined as part of the data of a group was also confusing for them.

[Filippo A. E. Nuccio]

I see; do you have a public repo with your material?

[Adam Topaz]

there is no repo. I am not actually teaching any lean, this was just some optional components that some students found interesting.

[Adam Topaz]

Rob Lewis said:

We should definitely update that hole command to omit as many provided fields as we can detect.

Is this really a good idea? I would prefer to delete the fields myself if I want the default.

[Adam Topaz]

Is there a way to indicate that a certain field is optional?