Scott's course

Stream: Lean for teaching

[Patrick Massot]

Attempting to prepare examples for my students was getting discouraging. Also they are already upset about not being able to find lemmas. :-)

What are you trying to teach?

[Scott Morrison]

I'm teaching a "special topics" course in our department (a nice Australian fellowship frees me from normal teaching duties for a while). We have 12 students, and we're ... trying to learn Lean. :-)

[Scott Morrison]

Here's assignment 1, which they are busy with at the moment: https://tqft.net/web/teaching/2019/ITP/assignment1.pdf

[Scott Morrison]

In fact, we are all hanging out here on Zulip, but we have a secret channel just for us. :-)

[Patrick Massot]

Ok, this is very different from what I'm doing. I may have put it in the wrong stream. This is really teaching Lean, not Lean for teaching

[Scott Morrison]

Yes.

[Scott Morrison]

I guess I'm less confident than you guys about Lean being ready for our mainstream courses (or rather, our mainstream courses being ready for Lean).

[Scott Morrison]

But I'm very very happy about the literate Lean programming tools you're building for pedagogical purposes.

[Kevin Sullivan]

Ok, this is very different from what I'm doing. I may have put it in the wrong stream. This is really teaching Lean, not Lean for teaching

Patrick,

What are you doing? FWIW, our aim isn't to teach Lean, per se, but to teach logic, proof, set theory, etc. Rather that a paper-pencil course using basic predicate logic and human checkers, we figured we'd teach them (they're early CS students) a more computational approach to logic, proof, checking, set theory (at least parts of it in Lean), etc. So it's Lean for teaching (discrete math), with teaching Lean as a necessary component.

[Kevin Sullivan]

Many of my early undergraduate students last semester (the first time we taught this) found it fairly rough going. One of the key points of friction is that students largely want to know how to get useful stuff done, and they don't see that learning DM using Lean, or that learning Lean, is going to help them in that regard. If they could just take a Javascript course, they'd be happy.

[Patrick Massot]

I can see you use Lean for teaching, my comment about teaching Lean was about Scott's course

[Patrick Massot]

I'm teaching an "introduction to proofs" course using Lean. You can see lecture notes of what I covered so far at https://www.math.u-psud.fr/~pmassot/enseignement/math114/ if you can read French

[Kevin Buzzard]

In fact, we are all hanging out here on Zulip, but we have a secret channel just for us. :-)

rofl I had noticed that there were a bunch of new people with anu email addresses and who weren't saying anything :-) We have an IC chat too.

[Kevin Buzzard]

The advantage of the private streams is that many of my students have 1000+ unread messages in the main chat, which they ignore, but they keep up to date with the IC chat because it's typically at a lower level. Occasionally someone asks something smart and I say "ask that in the main chat".

[Patrick Massot]

I can see private streams now gather 9% of the content https://leanprover.zulipchat.com/stats

[Patrick Massot]

Oh, and we just reached 500 active users. I really wonder what "active user" means

[Kevin Buzzard]

What year are these students in Scott? I think this looks like a fabulous course

[Scott Morrison]

Years 2, 3, and 4, with more or less a requirement that they got a great mark in our 2nd year abstract algebra course, and had seen some functional programming previously.

[Kevin Buzzard]

If you want to brainstorm ideas for future homeworks, feel free to get in touch.

[Kevin Buzzard]

I have been throwing out random exercises to mathematicians for a while, and one thing which sometimes goes down well is "let's make a new structure", e.g. let them import data.real.basic but nothing from data.complex, and then make the complex numbers from scratch and prove it's a field. This forces people to think about exactly what is needed. It's hard to start. You know that you want all the proofs to be "check on real and imaginary parts", but if you don't get the absolute basic stuff right then you're in trouble.

[Kevin Buzzard]

"Let's make a sheaf (of types on a topological space)" might be interesting, and it's probably harder to cheat.

[Kevin Buzzard]

"Let's make the quaternions"! AFAIK nobody has done that yet.

[Kevin Buzzard]

That could even end up as a PR.

[Kevin Buzzard]

You could look at the sort of stuff which Tom Hales wants in his FABSTRACTS -- I think he wrote a bunch of ideas down but a lot of them still need formalising.

[Kevin Buzzard]

Something which is harder than you want it to be is basic examples of groups of small order. Amelia Livingstone was doing the 2nd year group theory example sheets and on the first sheet one question was "true or false: if G is abelian then G is cyclic". To answer this in Lean you have to explicitly produce a non-cyclic abelian group. There are lots of ways to proceed so this is a nice question. However you construct it, you've got to prove it's not cyclic though! This kind of question is interesting. For some people they might end up exasperated that something so trivial is hard to do in Lean, but on the other hand others might start thinking "what is an actual good way of rigorously proving C_2 x C_2 is not cyclic".

[Kevin Buzzard]

You might want to scan that 2nd year abstract algebra course and see if there is anything which is not in mathlib yet. One structured homework, once they know what they're doing, could be to get that stuff in.

[Kevin Buzzard]

Quotients are hard; you need to know your out from your mk from your lift from your sound from your computational principle, and these are not words which are particularly familiar to mathematicians. But if you show them how to make quotient groups I bet they can make quotient rings.

[Kevin Buzzard]

An exercise I found particularly nice when I was teaching my 1st year course last term was proving that there was an equiv between equivalence relations on a type and partitions of the type, where a partition is a set of disjoint non-empty subsets whose union was the type. The proof is longer than you think.

[Kevin Buzzard]

Something which is easy in maths is proving that the sum of the first n odd numbers is n^2. Doing it in Lean is more of a challenge.

[Kevin Buzzard]

But thinking about how to do it taught me a lot about induction. https://xenaproject.wordpress.com/2018/03/30/proofs-by-induction/

[Kevin Buzzard]

At some point one has to think about the issue that there are some things which are really easy to do "in maths" but hard to do in Lean. I did not change my example sheet questions when I started integrating Lean into my teaching, but Patrick did.

[Kevin Buzzard]

One thing which was just as much fun in lean as in maths was basic questions about sups and infs. For example proving that if sup(S) = l then inf(-S)=-l, or if sup(S)=s and sup(T)=t then sup(S+T)=s+t. Those are a joy to do in Lean and should give satisfaction to beginners.

[Kevin Buzzard]

When I was a kid you could buy chicken mcnuggets in our local McDonalds in bags of 6 or 9, or a box of 20. I worked out the largest number that it was not possible to buy, and proved it in Lean. Proofs of this can go on for a very long time unless you know what you're doing.

[Kevin Buzzard]

Warning: nice little questions about number theory can be ferociously difficult for beginners, because subtraction is poorly behaved on nat, and passing between nat to int is hard.

[Kevin Buzzard]

This makes doing elementary number theory a lot harder than one might initially guess. I wrote https://github.com/leanprover-community/mathlib/blob/master/docs/extras/casts.md in an attempt to formalise some ideas of how to deal with this -- this is a long way from a mathematician's comfort zone. I lost count of the number of times I was asked last summer how to prove that a + b = c given the hypothesis that a + b = c, where there were random up-arrows in the hypothesis and/or the goal.

[Kevin Buzzard]

Proving that composite of injective functions is injective is easy, as is proving composite of surjective functions is surjective. But proving that a surjective function has a one-sided inverse is a nightmare if you don't know what you're doing; use choose!

[Kevin Buzzard]

Rolling your own limits of sequences and then proving that sum of limits is limit of sums, and product of limit is limit of products, is quite good fun.