# Zulip Chat Archive

## Stream: general

### Topic: After finishing Natural Number Game

#### Andrew Helwer (Mar 06 2020 at 18:07):

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 (Mar 06 2020 at 18:08):

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 (Mar 06 2020 at 18:20):

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 (Mar 06 2020 at 22:35):

@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 (Mar 06 2020 at 22:37):

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 (Mar 07 2020 at 15:54):

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

#### Andrew Helwer (Mar 07 2020 at 17:24):

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

#### Scott Morrison (Mar 07 2020 at 17:57):

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

#### Kevin Buzzard (Mar 07 2020 at 17:59):

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

#### Patrick Massot (Mar 07 2020 at 18:53):

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

#### Patrick Massot (Mar 07 2020 at 19:01):

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 (Mar 07 2020 at 19:03):

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

#### Scott Morrison (Mar 07 2020 at 20:58):

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

#### Kevin Buzzard (Mar 07 2020 at 21:00):

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 (Mar 07 2020 at 21:16):

Scott, how old is your son?

#### Scott Morrison (Mar 07 2020 at 21:21):

He's 10

#### Patrick Massot (Mar 07 2020 at 21:22):

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

#### Scott Morrison (Mar 07 2020 at 21:31):

Level 4 of multiplication would was pretty difficult for him.

#### Scott Morrison (Mar 07 2020 at 21:32):

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 (Mar 07 2020 at 21:56):

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

worked.

#### Kevin Buzzard (Mar 07 2020 at 21:57):

rofl

#### Patrick Massot (Mar 07 2020 at 21:58):

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

#### Scott Morrison (Mar 07 2020 at 22:04):

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 (Mar 07 2020 at 22:04):

He is not ready for formal proofs.

#### Patrick Massot (Mar 07 2020 at 22:05):

(Mike I mean)

#### Patrick Massot (Mar 07 2020 at 22:05):

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

#### Kevin Buzzard (Mar 07 2020 at 22:12):

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 (Mar 07 2020 at 22:38):

those exist in lean too, you know

#### Mario Carneiro (Mar 07 2020 at 22:39):

that's `cardinal.mul_assoc`

#### Scott Morrison (Mar 08 2020 at 16:57):

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 (Mar 08 2020 at 16:57):

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

#### Scott Morrison (Mar 08 2020 at 16:58):

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 (Mar 08 2020 at 16:58):

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

#### Kevin Buzzard (Mar 08 2020 at 16:58):

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 (Mar 08 2020 at 16:59):

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 (Mar 08 2020 at 16:59):

(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 (Mar 08 2020 at 17:00):

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

#### Scott Morrison (Mar 08 2020 at 17:00):

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 (Mar 08 2020 at 17:08):

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 (Mar 08 2020 at 17:31):

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 (Mar 08 2020 at 17:33):

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 (Mar 08 2020 at 17:43):

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

#### Andrew Helwer (Mar 08 2020 at 17:57):

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 (Mar 08 2020 at 17:57):

No. `simp`

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

#### Scott Morrison (Mar 08 2020 at 17:58):

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

#### Scott Morrison (Mar 08 2020 at 17:58):

(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.)

Last updated: May 13 2021 at 22:15 UTC