# Zulip Chat Archive

## Stream: Lean for teaching

### Topic: Scott's course

#### Patrick Massot (Mar 05 2019 at 12:20):

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 (Mar 05 2019 at 12:21):

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 (Mar 05 2019 at 12:22):

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

#### Scott Morrison (Mar 05 2019 at 12:22):

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

#### Patrick Massot (Mar 05 2019 at 12:24):

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 (Mar 05 2019 at 12:25):

Yes.

#### Scott Morrison (Mar 05 2019 at 12:26):

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 (Mar 05 2019 at 12:27):

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

#### Kevin Sullivan (Mar 05 2019 at 16:13):

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 (Mar 05 2019 at 16:16):

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 (Mar 05 2019 at 17:38):

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

#### Patrick Massot (Mar 05 2019 at 17:39):

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 (Mar 05 2019 at 18:24):

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 (Mar 05 2019 at 21:20):

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 (Mar 05 2019 at 21:34):

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

#### Patrick Massot (Mar 05 2019 at 21:35):

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

#### Kevin Buzzard (Mar 05 2019 at 21:51):

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

#### Scott Morrison (Mar 05 2019 at 22:17):

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 (Mar 05 2019 at 22:37):

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

#### Kevin Buzzard (Mar 05 2019 at 22:40):

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 (Mar 05 2019 at 22:41):

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

#### Kevin Buzzard (Mar 05 2019 at 22:41):

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

#### Kevin Buzzard (Mar 05 2019 at 22:42):

That could even end up as a PR.

#### Kevin Buzzard (Mar 05 2019 at 22:42):

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 (Mar 05 2019 at 22:46):

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 (Mar 05 2019 at 22:48):

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 (Mar 05 2019 at 22:51):

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 (Mar 05 2019 at 22:53):

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 (Mar 05 2019 at 22:55):

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 (Mar 05 2019 at 22:57):

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 (Mar 05 2019 at 22:58):

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 (Mar 05 2019 at 23:00):

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 (Mar 05 2019 at 23:02):

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 (Mar 05 2019 at 23:03):

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 (Mar 05 2019 at 23:05):

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 (Mar 05 2019 at 23:06):

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 (Mar 05 2019 at 23:08):

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.

Last updated: Dec 20 2023 at 11:08 UTC