After finishing Natural Number Game

Stream: general

[Andrew Helwer]

Any recommendations for where to go after finishing the Natural Numbers Game? I suppose there's the Real Numbers Game (https://github.com/ImperialCollegeLondon/real-number-game) which would be good since I don't have any experience using Lean with the real numbers. Might be able to dig up some of my old undergrad problem sets from calculus and formalize those. I think my large-scale goal is to start formalizing results in quantum information processing.

[Andrew Helwer]

P.S. I'd also like to say the NNG turned out to be my favorite puzzle game of the past few years, despite the lack of fancy graphics or non-mathematical narrative motivation! Absolutely incredible, truly.

[Kevin Buzzard]

rofl, that's really crazy. Thanks. Did you know that all of maths is a game like the natural number game? Lean has turned out to be my favourite puzzle game of the past few years. These other games like the real number game, the group theory game, the logic game (basic propositions, stuff like (P and Q) or (P and R) = P and (Q or R)), the integer game, ...) are all in half-written states because I'm currently teaching and dealing with admissions for a big PhD programme. Note that there is also plenty of potential for the natural number game 2, proving that every positive integer is uniquely a product of primes and so on. Even just stuff about odd and even numbers is quite fun.

If you want to play the perfectoid space game, then here are about 30 levels. But the maths involved is much more serious. It's just another thing on my pile of stuff to do (this is my area of research).

There are some maths challenges here, which are short and sweet.

Here are the example sheets from a short (8 hour) course I taught last term to 1st year maths undergrads: https://github.com/ImperialCollegeLondon/M40001_lean

It seems to me that there is loads of potential but we just have to find the time to do it. There is someone coming to Imperial for a 4 month "industrial placement"(!) who will work on some more games.

[Mario Carneiro]

@Kevin Buzzard You should write this kind of thing on the last level of NNG (or the victory screen if you have one)

[Kevin Buzzard]

When term is over I plan on fixing all the issues which have been reported; I'll add a note about this one.

[Patrick Massot]

Andrew, can you read French? If yes then I have more levels for you.

[Andrew Helwer]

Sadly I cannot; my Canadian high school French education was fairly rudimentary!

[Scott Morrison]

Surely (Lean French) < (math French) << (written French). :-)

[Kevin Buzzard]

i.e. "come on Patrick, please post the link anyway" :-)

[Patrick Massot]

Scott, the issue is the Lean files contain explanation in written French.

[Patrick Massot]

I still put an archive for Kevin at https://www.math.u-psud.fr/~pmassot/math114.tar.bz2. These are all the Lean files I used in my 2020 lectures so far. Everything you need to look at is in src. The file numbered 0 does not contain any exercise, it was shown on day one to give an idea of what Lean looks like, proving an early real analysis lemma (remember students had one semester of real analysis before my classes). Every other file contains a mixture of explanations, worked out examples and exercises. The lectures notes (with more details than what I actually discuss in class are at https://www.math.u-psud.fr/~pmassot/enseignement/math114. The file called dm.lean is something I asked them to do at home between files 03 and 04 (5 Lean exercises, including two they had to also write on paper). The file anatole1.lean is a special file I used last Friday on my student who did each of the other files in at most 15 minutes (it is not something I will cover with the other students).

[Kevin Buzzard]

Is the student interested in doing any more Lean? What kind of maths are they interested in?

[Scott Morrison]

My son this morning, playing the natural numbers game: "Induction is cool. I like induction."

[Kevin Buzzard]

I once said to Chris Hughes "isn't it funny that kids learn addition when they're about 6 but don't learn induction until they're about 16" and he said "they learn to count before they learn to add"

[Patrick Massot]

Scott, how old is your son?

[Scott Morrison]

He's 10

[Patrick Massot]

Nice. I should do a French translation of that game in order to try it on my oldest children.

[Scott Morrison]

Level 4 of multiplication would was pretty difficult for him.

[Scott Morrison]

But he seems to be getting it. He's just done an induction on the wrong variable, and is chanting "there's the annoying successor, how do I move the successor?!"

[Scott Morrison]

Okay, now Simon is teaching Mike Freedman how his proof of zero_mul worked.

[Kevin Buzzard]

rofl

[Patrick Massot]

I'll believe it only when I'll see Freedman here on Zulip :stuck_out_tongue_wink:

[Scott Morrison]

Mike was more impressed by Simon's proof of mul_assoc "it's obvious, they're both cubes with sides a, b, and c" than with zero_mul.

[Patrick Massot]

He is not ready for formal proofs.

[Patrick Massot]

(Mike I mean)

[Patrick Massot]

The story about Simon is indeed more impressive than the standard analogue for commutativity.

[Kevin Buzzard]

One can define addition and multiplication on nat in a completely different way, by first of all setting up a theory of cardinality of finite sets, and then defining addition to be "cardinality of disjoint union" and multiplication to be "cardinality of product". Then one really can give non-inductive proofs of things like mul_comm and mul_assoc of this form

[Mario Carneiro]

those exist in lean too, you know

[Mario Carneiro]

that's cardinal.mul_assoc

[Scott Morrison]

I’m curious about one design decision in the natural numbers game, @Kevin Buzzard. In the real world, we would carefully add @[simp] to each lemma as we go. I notice you don’t do this - in multiplication world all the lemmas about addition are available to simp, but for example in add_mul, simp can’t do mul_zero.

[Scott Morrison]

I understand the desire to not make levels too easy too early.

[Scott Morrison]

But on the other hand we need to show newcomers that proving in Lean is not _as_ tedious as it first appears, because the automation gets better and better as you go along.

[Kevin Buzzard]

Oh -- that's just because I don't understand simp :-/

[Kevin Buzzard]

I understand ring so I got that working, but I didn't want to teach simp because I didn't understand it myself.

[Kevin Buzzard]

Doesn't it work eventually -- I think I can show a+b+c+d+e=e+d+c+b+a by simp at the end of it. I think you're suggesting we should start earlier.

[Scott Morrison]

(And indeed, the very idea that it’s important that the mathematician themselves improves the automation as they go along —- even if just by marking lemmas with @[simp] — May be worth getting across to new users.)

[Scott Morrison]

yeah — you do point out that simp can do these things

[Scott Morrison]

but I’m wondering what the right pedagogical moment is for “it’s important that you make simp more powerful as you go!”

[Scott Morrison]

Oh dear. “Lean is busy” got stuck in the NNG, and so eventually I suggested to Simon that he reloads the page. That worked, but he’s really sad that all his proofs in earlier levels got lost. :-(

[Patrick Massot]

We really need some more energy put into this game, including some way to store data. People really like it so it would be worth the effort.

[Patrick Massot]

Regarding the simp discussion: it's not clear to me that this game is meant to teach Lean properly. I understand it as one possible fun introduction, but we don't expect people to start writing serious Lean code right after completing the game.

[Kevin Buzzard]

I think our first year undergraduates would also like the group theory game (which might appear within the next few months).

[Andrew Helwer]

How does simp work exactly? Does lean do some kind of breadth-first search applying all theorems tagged with [simp] to the goal, trying to maximize a similarity score?

[Scott Morrison]

No. simp traverses the expression, starting at the deepest parts of the expression, and tries to transform subexpressions using the simp lemmas.

[Scott Morrison]

It is entirely undirected --- if a simp lemma can fire, it will.

[Scott Morrison]

(The rewrite_search tactic, that Keeley and I wrote a while back back haven't ported to mathlib, does do edit distance based scoring of rewrites.)