## Stream: new members

### Topic: natural number game (https://tinyurl.com/natgame1234)

#### Kevin Buzzard (Oct 26 2019 at 19:18):

@waldo @Tim Hosgood @Emily Riehl maybe it's sensible to talk about the natural number game in a separate thread.

yeah sure

#### waldo (Oct 26 2019 at 19:18):

still getting the lean is busy

#### waldo (Oct 26 2019 at 19:18):

what browser are you using?

#### Kevin Buzzard (Oct 26 2019 at 19:19):

It works for me on Chrome

#### Tim Hosgood (Oct 26 2019 at 19:21):

and it works for me on Firefox

#### Bryan Gin-ge Chen (Oct 26 2019 at 19:21):

Do you see any strange messages in your browser console?

#### waldo (Oct 26 2019 at 19:21):

yeah, it fails to compile the wasm (web assembly)

#### waldo (Oct 26 2019 at 19:21):

i'm happy to see that sites actually usign web assembly

#### Bryan Gin-ge Chen (Oct 26 2019 at 19:22):

What about on Firefox? What version of Firefox are you using?

#### waldo (Oct 26 2019 at 19:22):

maybe I have changed some privacy settings..

#### waldo (Oct 26 2019 at 19:22):

latest firefox but privacy settings on (cookies mainly)

#### Tim Hosgood (Oct 26 2019 at 19:22):

hmm, I'm also on the latest Firefox and have pretty harsh privacy settings too

#### waldo (Oct 26 2019 at 19:23):

I have to go, let's speak later

#### Kevin Buzzard (Oct 26 2019 at 19:23):

@Mohammad Pedramfar told me that the Lean server stuff he was doing was tested in Chrome

#### Tim Hosgood (Oct 26 2019 at 19:24):

I know this probably isn't causing the problem, but I didn't realise at first that only things before your cursor were getting evaluated, and being halfway through a line could give funny output

#### Bryan Gin-ge Chen (Oct 26 2019 at 19:24):

For what it's worth, I just get a blank page if I try to open the game in a "private window", but in a normal tab with cookies etc. allowed it works fine for me.

#### Kevin Buzzard (Oct 26 2019 at 19:25):

I think waldo's problem is that he is always seeing "Lean busy". I can easily replicate this -- if I just compile the project and then don't run an http server and open the local index.html with a browser then it just sits there saying "Lean busy"

#### Kevin Buzzard (Oct 26 2019 at 19:25):

so I suspect the javascript is not running

#### Kevin Buzzard (Oct 26 2019 at 19:26):

but honestly take my musings with a large pinch of salt.

#### Bryan Gin-ge Chen (Oct 26 2019 at 19:49):

It's impossible to diagnose what's causing this without the console output, unfortunately. I would like to know whether it's something that should be addressed "upstream" in my lean-web-editor or lean-client-js-browser forks.

@waldo when you get back, could you open your web console in Firefox and refresh the page? This is what I see:
Screenshot-2019-10-26-15.42.22.png

Make sure that the XHR and Requests options are selected. You can either copy+paste the text here or upload a screenshot.

Also, out of curiosity, does https://leanprover-community.github.io/lean-web-editor work for you? (If not, I'd be interested to see the logs for that as well.)

#### waldo (Oct 26 2019 at 22:53):

The github you linked indeed work,
now when I returned I can see that it works on chrome

#### Kevin Buzzard (Oct 26 2019 at 22:54):

does the natural number game work for you on chrome?

#### waldo (Oct 26 2019 at 22:56):

you mean level 4 world 1?

#### Kevin Buzzard (Oct 26 2019 at 22:57):

@Mohammad Pedramfar I just looked at Bryan's screenshot above and I am a bit confused. The files he's reporting as not being able to see -- e.g. vs/loader.js -- they are there, but -rw--r--r-- so my guess is that he can't see them because there's no +x. Is this a problem with our set-up?

#### Bryan Gin-ge Chen (Oct 26 2019 at 22:57):

@Kevin Buzzard there's no issues in my screenshot. That's me refreshing when everything worked fine.

#### Kevin Buzzard (Oct 26 2019 at 22:58):

@waldo I mean that when you came here you said you were getting "Lean is busy" all the time. Are you still getting that or is the game working for you now?

#### Bryan Gin-ge Chen (Oct 26 2019 at 22:58):

The "source maps" not being found is fairly normal. They're useful for debugging, but most deployed web apps don't provide them.

#### Kevin Buzzard (Oct 26 2019 at 22:58):

@Bryan Gin-ge Chen your screenshot looks to me like it contains 404 errors but those files are present, they're just not +x.

#### waldo (Oct 26 2019 at 22:59):

the game works in chrome(after enabling cookies) :D, in edge it didn't, and in firefox it didn't load (no cookise enabled)

#### waldo (Oct 26 2019 at 22:59):

in edge the lean interperter was busy all the time

#### waldo (Oct 26 2019 at 23:00):

in chrome I think it started that way but I got home now and it seems to work so who knows

#### Kevin Buzzard (Oct 26 2019 at 23:00):

Ok, I just wanted to check it was working for you. I don't even know what a cookie is, @Mohammad Pedramfar did all the web work, I just wrote the Lean code. But Bryan knows what he's talking about as well, I'm pretty sure Mohammad used Bryan's work.

#### waldo (Oct 26 2019 at 23:01):

are you a mathmetician kevin?

right.

#### waldo (Oct 26 2019 at 23:01):

or you programmed the lean interperter?

#### Mario Carneiro (Oct 26 2019 at 23:02):

the lean JS compilation was first done by Gabriel Ebner, but I think Bryan done a lot of work since to update it for the community version

#### Kevin Buzzard (Oct 26 2019 at 23:02):

I did this bit: https://github.com/ImperialCollegeLondon/natural_number_game (100% Lean code) and Mohammad did this bit: https://github.com/mpedramfar/Lean-game-maker (possibly 0% Lean code)

#### waldo (Oct 26 2019 at 23:03):

It's truley amazing that it actually uses web assembly,
probably zero work had to be done (because Lean is pretty minimal, same as webassembly)

#### waldo (Oct 26 2019 at 23:03):

The goal of the game is get students familliar with lean?

#### Bryan Gin-ge Chen (Oct 26 2019 at 23:04):

probably zero work had to be done

Heh, depends on your definition of zero...

#### waldo (Oct 26 2019 at 23:04):

I've seen a talk latley about someone who wants to move all paper proofs to lean so they can be verified by computer automatically insteadof humans, but I found this chat throught the IMO grand challenge

#### Kevin Buzzard (Oct 26 2019 at 23:04):

what was that talk?

#### Mario Carneiro (Oct 26 2019 at 23:04):

because Lean is pretty minimal

I'm curious what definition of "minimal" leads you to that conclusion

#### waldo (Oct 26 2019 at 23:04):

if lean already uses llvm (which it's probably is)

#### Kevin Buzzard (Oct 26 2019 at 23:05):

Lean 3 does not. Lean 4 will.

#### Mario Carneiro (Oct 26 2019 at 23:05):

but it can be compiled with clang via llvm so emscripten is doing most of the heavy lifting for the WASM build

#### Kevin Buzzard (Oct 26 2019 at 23:06):

The goal of the game is get students familliar with lean?

Right. I want to teach young mathematicians how to use theorem provers because I am convinced that they (theorem provers) should play a bigger role in the future of mathematics.

#### Kevin Buzzard (Oct 26 2019 at 23:06):

And you can blame Mario for this, because without him I would have given up a long time ago before I even learnt how to use Lean.

#### waldo (Oct 26 2019 at 23:09):

I never used lean so I mainly guess
anyway the usage of lean is for used for computation from my understaing (and not relaying on the OS from processes, threading etc)
I agree that the future is for automatically verified theorems (and even come up with new theorems and proofs)

#### Kevin Buzzard (Oct 26 2019 at 23:10):

I agree that the future is for automatically verified theorems (and even come up with new theorems and proofs)

Great, you're hired. When can you start?

:D

#### Kevin Buzzard (Oct 26 2019 at 23:11):

We've done 0.001% of maths so far, so you have a lot to choose from.

#### waldo (Oct 26 2019 at 23:11):

When mathematicians will give up on their computation power to this of course

#### Mario Carneiro (Oct 26 2019 at 23:11):

what do you mean exactly?

#### Mario Carneiro (Oct 26 2019 at 23:12):

lean isn't about "computation" per se

#### Mario Carneiro (Oct 26 2019 at 23:12):

you can use it like a programming language, but the main thing the people around here care about is proving mathematical theorems, that may not "have computational content" so to speak

#### waldo (Oct 26 2019 at 23:13):

I mean that professors currently getting paid for lower computation power(their brains), rather than levering computers (and lean) to improve their productivity
I have the feeling that I exaggerate everything I say today so don't take me too seriously please

#### waldo (Oct 26 2019 at 23:14):

I haven't explored lean at all, care to explain what do you mean?

#### Mario Carneiro (Oct 26 2019 at 23:14):

aha. Well that's actually a hard thing to do; currently human mathematicians far outstrip computers in effectiveness (although they aren't quite doing the same things)

#### waldo (Oct 26 2019 at 23:15):

yeah, humans are more specialized for human things that defenitly true

#### Mario Carneiro (Oct 26 2019 at 23:15):

the IMO grand challenge in part is intended to narrow the gap

#### waldo (Oct 26 2019 at 23:15):

it's all theoretically

#### waldo (Oct 26 2019 at 23:15):

who is actually leading the talks here

#### waldo (Oct 26 2019 at 23:15):

the challenge, lean the language

#### waldo (Oct 26 2019 at 23:16):

lean is by microsoft researches or am I wrong?

#### Mario Carneiro (Oct 26 2019 at 23:16):

the IMO grand challenge is lead by Leo de Moura (MSR) and Daniel Selsam (not sure, MSR?)

#### Mario Carneiro (Oct 26 2019 at 23:17):

mathlib is lead by the people you will find on this chat, a hodgepodge of mathematicians and computer scientists around the world

#### waldo (Oct 26 2019 at 23:18):

mathlib is a lean lbirary for math proofs?

yes

#### Mario Carneiro (Oct 26 2019 at 23:19):

it's actually a lot more than that, it's basically a "standard library" of sorts for lean 3

#### waldo (Oct 26 2019 at 23:19):

If I provide proofs for the entire calclus will I remmbered besides Cauchy? :joy:

go for it!

#### waldo (Oct 26 2019 at 23:19):

Where do we stand today?

#### waldo (Oct 26 2019 at 23:19):

what are the limitations of lean currently?

#### waldo (Oct 26 2019 at 23:19):

how is cog compared to lean?

#### Mario Carneiro (Oct 26 2019 at 23:20):

on calculus, we have general derivatives but we haven't done real (calc 1 style) derivatives yet, or derivatives of basic functions like exp

#### waldo (Oct 26 2019 at 23:20):

what do you mean general derviatives? defeinition but iwthout proof?

#### Mario Carneiro (Oct 26 2019 at 23:20):

mathlib has a bourbaki style approach where we start from the abstract notion and work our way to the concrete

#### Mario Carneiro (Oct 26 2019 at 23:21):

which is a bit backward from the usual pedagogy

#### waldo (Oct 26 2019 at 23:21):

is it just to get things go faster?

#### waldo (Oct 26 2019 at 23:21):

so we can go for more hard stuff?

#### Mario Carneiro (Oct 26 2019 at 23:21):

it is to unify developments so we don't have to redo stuff later when we care about e.g. multivariate derivative

#### waldo (Oct 26 2019 at 23:22):

I think it may be good to leave gaps, and maybe we'll be able to leverege computer to get to the result by itself

#### Mario Carneiro (Oct 26 2019 at 23:22):

we have derivatives on normed vector spaces, producing a linear map called the derivative, but the calc 1 style derivative is a number, not a linear map

#### Mario Carneiro (Oct 26 2019 at 23:23):

leveraging the computer to get the result by itself is mostly wishful thinking at this point

#### Mario Carneiro (Oct 26 2019 at 23:23):

it may well happen in the near term but lean today is not going to impress you if you are hoping for that

#### waldo (Oct 26 2019 at 23:24):

that ok, I just wander if putting efforts into lean is the right thing, that why I ask for caomprsions to other languages and whether there is a roadmap

#### waldo (Oct 26 2019 at 23:25):

is this the right stream?

#### Mario Carneiro (Oct 26 2019 at 23:25):

it's pretty decentralized, people work on the stuff that interests them

#### waldo (Oct 26 2019 at 23:26):

right stream to talk about is I mean

#### waldo (Oct 26 2019 at 23:26):

nvm, I'll go throught the game

#### Mario Carneiro (Oct 26 2019 at 23:27):

The mathlib paper may be able to answer your questions about overview and comparison to other languages

#### Mario Carneiro (Oct 26 2019 at 23:27):

https://leanprover-community.github.io/papers/mathlib-paper.pdf

#### waldo (Oct 27 2019 at 00:14):

World 2 level 2, I'm still not sure how to write proper lean, but I trust lean to test my proof so even if it's not optimized and not coherent enough (for me at least as a user) I still know it works
The solution:
induction c with d cd,
induction b with e be,
refl,
refl,
rw cd,
refl,

#### Kevin Buzzard (Oct 27 2019 at 00:17):

You can quote Lean code if you put it between   . Even better, put  lean  at the top and    at the bottom. Then it looks like this:

induction c with d cd,
induction b with e be,
refl,
refl,
rw cd,
refl,


#### Kevin Buzzard (Oct 27 2019 at 00:18):

I note that you used induction hypothesis cd but you never use be in your proof.

#### Kevin Buzzard (Oct 27 2019 at 00:21):

The roadmap is that people just do what they feel like doing, but generally I encourage people to work on undergraduate maths degree level stuff which isn't already there, because it's the path of least resistance.

#### Emily Riehl (Oct 27 2019 at 01:54):

Beginner question: does lean have something like "pose" in coq? Say I have a term a : A and a function f : A -> B (maybe proven in a previous lemma). I'd like to give a name to a term in B to do something complicated with later and add it to my givens. In coq I'd type something like "pose b := (f a)." At the moment, I'm feeding very long composite terms into the exact tactic.

#### Bryan Gin-ge Chen (Oct 27 2019 at 01:59):

I don't know Coq, but I suspect you're looking for have. In tactic mode, you would write have b := f a,.

#### Kenny Lau (Oct 27 2019 at 01:59):

let b := f a

#### Reid Barton (Oct 27 2019 at 02:01):

Use let if you will need to use the definitional equality of b and f a, otherwise have (for example if b is the proof of a proposition). I'm not sure which one pose is.

#### Jesse Michael Han (Oct 27 2019 at 02:10):

let is the user-facing version of tactic.pose

#### Emily Riehl (Oct 29 2019 at 02:47):

Thanks. Now I'm stuck on world 3 level 11. In the first line I wrote

split,


to split the iff into implications but I got a "tactic failed" error. What am I doing wrong?

#### Kenny Lau (Oct 29 2019 at 02:50):

@Emily Riehl the goal doesn't start with iff (in Polish notation, which is the internal representation in Lean)

#### Emily Riehl (Oct 29 2019 at 12:32):

Thanks. I wasn't reading carefully enough.

#### Kevin Buzzard (Oct 29 2019 at 12:34):

Professional category theorist:"I am stuck. No, wait -- I'm not reading carefully enough". Me: "I need to make this better, so people can't not read carefully enough".

#### Kevin Buzzard (Oct 29 2019 at 12:36):

Note also that some error messages are being incorrectly suppressed in the version online at the minute. This is a bug which has been chased down and squashed but has not made it upstream.

#### Johan Commelin (Oct 29 2019 at 15:42):

@Emily Riehl Welcome on the chat :smiley:

#### Alain Muller (Oct 29 2019 at 17:25):

Hi. I am in the process of learning lean. After going through the first 4 sections of theorem proving with lean, I decided to play the natural number game to learn about tactics. I just finished it and I enjoyed it very much. I was stuck at some points but managed to find some explanations about some tactics in the documentation that were not explained during the process of the game.

#### Kevin Buzzard (Oct 29 2019 at 18:17):

Yeah, I'm afraid v1.0 is a bit rubbish :-/

#### Kevin Buzzard (Oct 29 2019 at 18:18):

but I'll get there in the end :D Given the choice between organising an open day for potential PhD students and playing with the natural number game, I know which one I would rather be doing, but unfortunately I also know which one I have to be doing :-/

#### Kevin Buzzard (Oct 29 2019 at 18:19):

Alain, if you want to leave some rude comments about where you got stuck and how bad the documentation was at these points, feel free to do so at https://github.com/ImperialCollegeLondon/natural_number_game

#### Kenny Lau (Oct 29 2019 at 18:20):

@Kevin Buzzard maybe put that link there

#### Kenny Lau (Oct 29 2019 at 18:22):

btw you have 4 PRs now

I do?

#### Kevin Buzzard (Oct 29 2019 at 18:28):

Thanks for letting me know!

no problem

#### Mohammad Pedramfar (Oct 30 2019 at 15:14):

Mohammad Pedramfar I just looked at Bryan's screenshot above and I am a bit confused. The files he's reporting as not being able to see -- e.g. vs/loader.js -- they are there, but -rw--r--r-- so my guess is that he can't see them because there's no +x. Is this a problem with our set-up?

There's no problem with Bryan's screenshots. As he said, the missing files are debugging tools. They're not necessary.

#### Mohammad Pedramfar (Oct 30 2019 at 15:17):

the game works in chrome(after enabling cookies) :D, in edge it didn't, and in firefox it didn't load (no cookise enabled)

Edge and IE are always different! I'm glad it's working now. I haven't had any problems with firefox before, if you have the screenshots of console output, I might be able to figure out what's going on.
I'm glad it's finally working! :)

#### Michael Barz (Oct 30 2019 at 22:46):

Here's another question about the game, regarding world 2, level 9; I've reached a point where I have as a hypothesis that P -> Q and I want to prove R -> Q. There is a previous lemma which shows that R -> P, although I'm confused as to how I can express in Lean "use the lemma to prove R -> P, then R -> P -> Q and so R -> Q"

(more particularly, for an inductive step, I have the induction hypothesis that b + a = c + a --> b = c, and my goal is succ(b+a) = succ(c+a) --> b = c, which I want to demonstrate by applying succ_inj to show that succ(b+a) = succ(c+a) --> b+a = c+a)

#### Kevin Buzzard (Oct 30 2019 at 22:46):

I am systematically removing all these worlds

#### Kevin Buzzard (Oct 30 2019 at 22:47):

I have spent some time trying to understand what exactly needs to be taught to a mathematician in order for them to be able to do these worlds without getting totally confused

#### Kevin Buzzard (Oct 30 2019 at 22:47):

@Michael Barz you need to know about intro and have and apply.

#### Michael Barz (Oct 30 2019 at 22:48):

Okay, thanks! I'll look into have, as it's the one I am unfamiliar with

#### Kevin Buzzard (Oct 30 2019 at 22:48):

http://wwwf.imperial.ac.uk/~buzzard/xena/html/source/tactics/tacticindex.html#basic-tactic-list

#### Kevin Buzzard (Oct 30 2019 at 22:49):

I need to take the relevant tactics from there, explain them carefully, and put them into the game.

#### Kevin Buzzard (Oct 30 2019 at 22:49):

Until I've done that (hopefully some time tomorrow) and until Mohammad has written the python code which makes the web game from the Lean file (hopefully also not too long), I think it's best that we just stay away from functions.

#### Kevin Buzzard (Oct 30 2019 at 22:50):

But what you need to learn about is this stuff: http://wwwf.imperial.ac.uk/~buzzard/xena/html/source/ch1_and_or_props/prop_exercises.html

#### vrs (Oct 30 2019 at 23:27):

hi, I'm a noob and I'm very confused about world 2 level 10 - I get the impression that it's supposed to be three lines, but rw add_comm a, rw add_comm b, exact add_left_cancel, complains about "invalid type ascription" and I suspect a more exact match than what I have is needed, so what is my misunderstanding here?

#### Reid Barton (Oct 30 2019 at 23:31):

add_left_cancel takes a b c as explicit arguments. I'm not sure what the game has taught you so far, but you can either specify them explicitly or use apply instead of exact

#### vrs (Oct 30 2019 at 23:40):

ahah so what I had to do was rw add_comm a, rw add_comm b, apply add_left_cancel,, while going from http://wwwf.imperial.ac.uk/~buzzard/xena/html/source/tactics/apply.html I would've expected that apply would reduce my goal to a = b and not solve it outright

#### Reid Barton (Oct 30 2019 at 23:46):

I see. I agree you wouldn't expect apply to work here based on that description.

#### Kevin Buzzard (Oct 30 2019 at 23:46):

I might have broken the default explicit/implicit argument thing.

#### Reid Barton (Oct 30 2019 at 23:47):

You were probably expected to intro the hypothesis, then rewrite the hypothesis, and then apply add_left_cancel and finally provide the rewritten hypothesis.

#### Kevin Buzzard (Oct 30 2019 at 23:47):

I'm trying to figure out what my users like best.

#### Kevin Buzzard (Oct 30 2019 at 23:47):

The users are currently not expected to be able to solve those levels at all.

#### Kevin Buzzard (Oct 30 2019 at 23:47):

That's why I'm removing them for a bit.

#### vrs (Oct 30 2019 at 23:52):

sample solutions would be nice, I got most of the way on my own but occasionally I feel I did something super ugly and awkward and there has to be an elegant way

#### vrs (Oct 30 2019 at 23:53):

also they'd teach me about how to use certain tactics properly, in an "oh you can do that?" way

#### Mario Carneiro (Oct 30 2019 at 23:54):

if you want to see solutions, asking here is an easy way to have an "oh you can do that?" moment

#### Mario Carneiro (Oct 30 2019 at 23:54):

If I heard correctly, the solutions are also available from the source code for the game

#### Kevin Buzzard (Oct 30 2019 at 23:55):

That is true, for example you can see my solution to 2-10 here:

https://github.com/ImperialCollegeLondon/natural_number_game/blob/master/src/game/world2/level10.lean

#### vrs (Oct 30 2019 at 23:57):

oh that is in fact very much what my 2-9 solution looked like!

intro,
induction a with d hd,
{apply hd, rw ← eq_iff_succ_eq_succ, rw ← succ_add, rw ← succ_add, exact a_1},


#### Lynn (Nov 01 2019 at 01:16):

hey, the mul_succ axiom as it's presented at the start of world 3 looks a little off: a * succ(b) = a * b + b

#### Alex J. Best (Nov 01 2019 at 01:27):

Wow, fortunately the one that is actually introduced behind the scenes is correct, if you put  have := mul_succ, in the proof box you can see this : ∀ (m n : mynat), m * succ n = m * n + m is what is really added

#### Lynn (Nov 01 2019 at 01:28):

I see there's a github repo, so I'll make a pull request!

#### Lynn (Nov 01 2019 at 01:28):

ah, https://github.com/ImperialCollegeLondon/natural_number_game/pull/15 is way ahead of me.

#### Lynn (Nov 01 2019 at 01:32):

:thought: 3 * 5 = 15, 4 * 7 = 28, 5 * 9 = 45 passed 3/3 test cases :check_mark:

#### Kevin Buzzard (Nov 01 2019 at 08:54):

Ha ha I need to get my act together! Thanks @Lynn

Fixed in v1.03

#### Kevin Buzzard (Nov 01 2019 at 10:12):

Most stuff in the bar on the left is generated automatically, but the axioms themselves are not in the game levels, they're else where in some behind the scenes files with the definitions, so I had to do them manually.

#### vrs (Nov 01 2019 at 20:28):

now that I know how useful apply is, the first two levels of power world are oneliners

#### Johan Commelin (Nov 01 2019 at 20:30):

apply is cool. I hope in some of the next levels refine will be unlocked. It's even better.

#### vrs (Nov 01 2019 at 20:32):

what kind of frustrates me is that I can't rw at a very specific position only, I was going to throw rw \l one_mul b at w3l6 (I think) but it replaced all instances of b instead of just the rightmost one

#### vrs (Nov 01 2019 at 20:33):

or maybe there is a way but I already forgot it again

#### Johan Commelin (Nov 01 2019 at 20:34):

There is a way, but it takes a bit more typing

#### Johan Commelin (Nov 01 2019 at 20:35):

There is a so-called conv-mode that allows you to "zoom in" on the expression, before calling rw

#### Bryan Gin-ge Chen (Nov 01 2019 at 20:35):

As Johan says, conv might help.

#### Antoine Chambert-Loir (Nov 01 2019 at 21:08):

I am stuck at world 2, level 2.
I brought Lean to the goal:

case mynat.succ
a b c1 : mynat,
hc1 : a + b + c1 = a + (b + c1)
⊢ succ (a + b + c1) = succ (a + (b + c1))

and I expected to conclude with

rw succ_inj,

rewrite tactic failed, lemma lhs is a metavariable

#### vrs (Nov 01 2019 at 21:09):

conv did help, but turned out that I would've needed mul_comm either way

#### Kevin Buzzard (Nov 01 2019 at 21:09):

@Antoine Chambert-Loir you are going the wrong way.

#### Kevin Buzzard (Nov 01 2019 at 21:10):

succ_inj will prove that your goal implies a hypothesis.

#### Kevin Buzzard (Nov 01 2019 at 21:10):

You need to show that your hypotheses imply the goal

#### Kevin Buzzard (Nov 01 2019 at 21:11):

succ_inj is a red herring. I am consdering removing it from the game completely.

#### Antoine Chambert-Loir (Nov 01 2019 at 21:12):

Oh yes! Sorry... but I'm stuck anyway. :-)

#### Kevin Buzzard (Nov 01 2019 at 21:13):

In fact the fact that you are even asking this question makes it clear that I should do this. I will introduce it at the place where the users know the tactics to be able to use it (e.g .apply). New levels to come but here's a sneak preview:

https://github.com/ImperialCollegeLondon/natural_number_game/tree/master/src/game/function_world

#### Johan Commelin (Nov 01 2019 at 21:15):

@Antoine Chambert-Loir Aside: you can get syntax highlighting on the chat using the following mark-up

lean
code goes here



#### Kevin Buzzard (Nov 01 2019 at 21:15):

Well, the hint is that the result you need is mathematically trivial now, all you need to do is to sub in. You have been misled by succ_inj, because you are only just getting used to thinking about laying maths out formally in this way, and the set-up has led you to the incorrect conclusion that succ_inj needs to be used in some way. It's much easier than that.

#### Antoine Chambert-Loir (Nov 01 2019 at 21:19):

Thanks, I needed to go back to World 2 Level 2 to be reminded to use rw on the induction hypothesis

rw hc1,


I is not clear to me what it does.
But I can rush to level 3 !

#### Johan Commelin (Nov 01 2019 at 21:27):

rw takes an equality h (or an iff) and searches the goal for occurences of the left-hand-side of h. If it finds them, it replaces them with the right-hand-side of h.

#### Johan Commelin (Nov 01 2019 at 21:27):

With rw h at foo, you can do the same thing at hypothesis foo instead of the goal

#### vrs (Nov 01 2019 at 22:00):

I find myself not really looking at the theorems themselves anymore, just thinking in terms of rewrite rules. is this common?

#### Kevin Buzzard (Nov 01 2019 at 22:00):

Yes! some people have said to me that it's kind of amazing that you can just prove the theorems by following your nose.

#### Kevin Buzzard (Nov 01 2019 at 22:01):

But I am working on a Friday night treat for you which you might find harder.

#### vrs (Nov 01 2019 at 22:03):

also I agree that the inequalities have been very confusing in their presence in the lower worlds. together with an exfalso, they might be useful, but I didn't quite pick up how that worked from just the prover output

#### Marc Huisinga (Nov 01 2019 at 22:07):

it's common and can be a curse as well. sometimes you stop thinking entirely and turn into a human unification algorithm - the terminator.
occasionally, when i get stuck and regain conciousness, i feel lost and unsure about how to continue the proof that my robo-self has started.

#### vrs (Nov 02 2019 at 01:20):

use is magic

#### vrs (Nov 02 2019 at 01:22):

it becomes clearer when you know that rw le_def at ⊢, can be elided and the same will happen (respectively, use implies rw), but still

#### Antoine Chambert-Loir (Nov 02 2019 at 11:20):

World 3/Level 9, is this it ?
It took me some minutes to solve it, and I had to use the rw tactic with the theorems reversed,

rw ← mul_assoc b,
rw ← mul_assoc,
rw mul_comm a,
refl,


This is very funny, because mul_assoc and mul_comm can be viewed as permutations, and this exercise is more or less about writing a given permutation as a word in them.

#### Kevin Buzzard (Nov 02 2019 at 12:28):

Yes, and of course there are algorithms which will do this.

#### vrs (Nov 02 2019 at 14:06):

4.8 is fairly easy with stuff introduced in the game:

rw one_eq_succ_zero,
repeat {rw pow_succ},
repeat {rw pow_zero},
rw ← one_eq_succ_zero,
rw succ_mul,
repeat {rw one_mul},
simp,


#### Kevin Buzzard (Nov 02 2019 at 14:07):

Did you look at the spoiler on Twitter?

#### Kevin Buzzard (Nov 02 2019 at 14:07):

It's even easier than that :D

#### vrs (Nov 02 2019 at 14:07):

yes but ring was never introduced was it?

#### Kevin Buzzard (Nov 02 2019 at 14:07):

indeed it wasn't.

#### Kevin Buzzard (Nov 02 2019 at 14:08):

although there was quite a painful period last night when it was secretly being introduced into the game :D

#### vrs (Nov 02 2019 at 14:08):

in fact I spoilered myself with the github source instead of the tweet and just went "whaat, unfair" (not in a bad way, I mean I expect the source to be ahead of what I've learned so far)

#### Kevin Buzzard (Nov 02 2019 at 14:08):

If ring sees a^b it expects a to be in the ring and b to be one of Lean's nats.

#### Kevin Buzzard (Nov 02 2019 at 14:10):

Sure it's unfair. But there's a message. If you are doing something boring then you shouldn't be doing it, you should be automating it. I make people look at a "trivial" thing (every schoolkid knows that (a+b)^2=a^2+b^2+2ab) and then I get people to prove it in Lean, when they discover what a complete pain it is because it's obvious that it can be done but it's boring, and then they discover that actually it's easy after all.

#### Kevin Buzzard (Nov 02 2019 at 14:11):

so it's a real voyage of discovery: in the space of playing the game they go from "expanding $(a+b)^2$ is trivial" [at the start] to "a lot goes into this actually" to "oh no, it is trivial after all".

#### vrs (Nov 02 2019 at 14:13):

my experience with 4.8 was, it was a lot of writing but fairly straightforward, while stuff like add_right_cancel and add_left_cancel felt much more hard-won

#### vrs (Nov 02 2019 at 14:15):

my biggest a-ha moment was early in the game when I realized I could do rw hd and not just rw stuff_in_the_left_bar

#### vrs (Nov 02 2019 at 14:17):

it may be aesthetic preference but every time I had to pull out induction it felt 'harder'

#### vrs (Nov 02 2019 at 14:20):

the extra addition levels were fun in a dwarf-fortress way and made me look up more advanced tactics

#### vrs (Nov 02 2019 at 14:21):

something that'd be neat would be zachtronics-like scoreboards displaying "x % of players completed this in y instructions"

#### Kevin Buzzard (Nov 02 2019 at 14:25):

World 3/Level 9, is this it ?
It took me some minutes to solve it, and I had to use the rw tactic with the theorems reversed,

rw ← mul_assoc b,
rw ← mul_assoc,
rw mul_comm a,
refl,


This is very funny, because mul_assoc and mul_comm can be viewed as permutations, and this exercise is more or less about writing a given permutation as a word in them.

So the simplifier asks for mul_left_comm, I suppose, so it can do a proof like this:

attribute [simp] mul_assoc mul_comm mul_left_comm

example (a b c d e : ℕ) : (((a*b)*c)*d)*e=(c*((b*e)*a))*d := by simp

example (a b c d e : ℕ) : (((a*b)*c)*d)*e=(c*((b*e)*a))*d := begin
repeat {rw mul_assoc},
rw mul_left_comm b,
rw mul_left_comm a,
rw mul_left_comm a,
rw mul_comm d,
rw mul_left_comm a,
end


Here's a link to the Lean Web Editor if you want to examine the proof yourself.

#### Kevin Buzzard (Nov 02 2019 at 14:26):

The combinatorics becomes much easier with mul_comm and mul_left_comm because after all the applications of add_assoc you can swap arbitrary adjacent pairs of elements. I guess this is turning into the proof that associativity and commutativity can indeed be used to do all the things which mathematicians assume follow from associativity and commutativity.

#### Kevin Buzzard (Nov 02 2019 at 14:26):

@Antoine Chambert-Loir

#### Kevin Buzzard (Nov 02 2019 at 14:28):

my experience with 4.8 was, it was a lot of writing but fairly straightforward, while stuff like add_right_cancel and add_left_cancel felt much more hard-won

You are absolutely right. The thing is with those hard levels is that I decided that a poor explanation was worse than no explanation at all. Those lemmas like add_right_cancel, which are functions not equalities, need a completely different set of tactics which need to be introduced properly first for the user to have any chance at all. Yes, there are some far more interesting levels coming.

#### Kevin Buzzard (Nov 02 2019 at 14:30):

something that'd be neat would be zachtronics-like scoreboards displaying "x % of players completed this in y instructions"

@Mohammad Pedramfar is this even feasible? Mohammad basically said very early on in the project "OK so we can either have people log in or not, and if they log in we can keep all their game data and do all sorts of things, but it will take me X days to learn how to do it" (for some value of X which was positive) and I said "Euclid the game doesn't have logins, so let's just go for it now while I don't have teaching, and let the user have access to all the levels".

#### Kevin Buzzard (Nov 02 2019 at 14:32):

With Project Euler you can do all sorts of things with the stats, but they have a login system. Of course if there's any CS-minded person who wants to change the tooling etc then they should feel free to work with Mohammad, who is currently writing his maths Phd up (which has nothing to do with natural numbers, he does dynamical systems of some sort) and doing this on the side.

#### Kevin Buzzard (Nov 02 2019 at 14:35):

the extra addition levels were fun in a dwarf-fortress way and made me look up more advanced tactics

I decided that for every person like you there are 10 people giving up and I needed to do it properly.

#### vrs (Nov 02 2019 at 14:43):

you could store the gamestate including proofs in the browser (localstorage), then you wouldn't have to store any on the server and logins would be unnecessary if you don't mind the % stats being not completely accurate, biggest downside would be you'd still have to come up with a mechanism that handles world changes in a way that keeps most of one's gamestate intact

#### vrs (Nov 02 2019 at 14:47):

the software engineer in me wonders whether optimizing for verification time would be worthwhile (proofs that are efficient to check make things more interactive down the road)

#### Kevin Buzzard (Nov 02 2019 at 15:07):

This is not something I can say anything about.

#### Marc Huisinga (Nov 02 2019 at 15:21):

even now verification can become very slow when abusing certain tactics too much, to the degree where the "interactive" in ITP vanishes.
afaik this will get better in lean 4 because lean will spend less time re-verifying things when adding stuff to a proof.

#### Kevin Buzzard (Nov 02 2019 at 15:43):

We don't have this issue in the natural number game because we are only doing simple things. It would not surprise me if there were some cool tools to produce various incarnations of a proof term.

#### pyon (Nov 02 2019 at 15:58):

What's the next step in learning Lean after playing the natural number game?

#### Kevin Buzzard (Nov 02 2019 at 19:50):

You could try the perfectoid space game

#### Kevin Buzzard (Nov 02 2019 at 19:52):

https://github.com/leanprover-community/lean-perfectoid-spaces/issues/33 I think there's 38 levels there, and when we're done the collectible is a non-empty perfectoid space, the first example of its kind in any theorem prover.

#### Kevin Buzzard (Nov 02 2019 at 19:52):

Alternatively you could try the levels I just wrote this afternoon

#### Johan Commelin (Nov 02 2019 at 19:58):

@pyon If you are looking for things do in Lean... there is a lot of low-hanging fruit. But it would be best to share a bit of your background knowledge and interests. The perfectoid space game is a rather big leap from that nat.nr.game, I would say.

#### Kevin Buzzard (Nov 02 2019 at 19:59):

Yes, this is a much more sensible reply. Are you a professor of computer science or an undergraduate mathematician? The answers are very different.

#### Kevin Buzzard (Nov 02 2019 at 20:03):

If you have a computer science background then you might like Theorem Proving In Lean. If you have a maths background then you might prefer dipping into Logic and Proof. I learnt Lean by finding simple maths questions and trying to solve them in Lean. Here are the example sheets I set my undergraduates: https://github.com/ImperialCollegeLondon/M40001_lean . But if all you have is the natural number game then these levels are too difficult. I'm currently trying to get a new world 5 together, I'll post a beta link when I'm done.

#### Kevin Buzzard (Nov 02 2019 at 20:03):

The new world 5 will teach you how to manipulate functions in Lean using intro, exact and apply.

#### Bryan Gin-ge Chen (Nov 02 2019 at 20:08):

There's also now Logical Verification in Lean (scroll to "materials") which is also CS focused. My impression is that it's a little easier than Theorem Proving in Lean, but take that opinion with a grain of salt since I knew a lot more Lean when I started reading Logical Verification than I did when I read TPiL.

#### pyon (Nov 02 2019 at 20:09):

@Johan Commelin @Kevin Buzzard Undergraduate mathematician. And thanks for the references!

#### Kevin Buzzard (Nov 02 2019 at 20:11):

lemme get world 5 up, hang on.

#### tirima (Nov 02 2019 at 21:41):

World 3/Level 9, is this it ?
It took me some minutes to solve it, and I had to use the rw tactic with the theorems reversed,

rw ← mul_assoc b,
rw ← mul_assoc,
rw mul_comm a,
refl,


@Antoine Chambert-Loir you don't need backward rewriting. You could do rw [mul_comm b (a*c), mul_assoc, mul_comm c], refl.

#### Antoine Chambert-Loir (Nov 02 2019 at 22:04):

Where can I get information about the syntax of rw ?
Up to now, I used it in the same way 1st year univ student to proof — throw in whatever looks plausible and pray for it to work.

#### Kevin Buzzard (Nov 02 2019 at 22:05):

Does the description of the tactic in the drop-down menu on the left not help?

#### Kevin Buzzard (Nov 02 2019 at 22:06):

I have just actually rewritten the description of the tactic in v1.07beta

#### Bryan Gin-ge Chen (Nov 02 2019 at 22:24):

Ordinarily, putting the cursor in the name of a tactic should show the docstring in the web editor's info window (top right), but it looks like Kevin's modifications have somehow disabled them. Anyways, this is what it says for rw:

tactic rw
An abbreviation for rewrite.

OK, not so helpful, but this is what it is for rewrite:

tactic rewrite
rewrite e applies identity e as a rewrite rule to the target of the main goal. If e is preceded by left arrow (← or <-), the rewrite is applied in the reverse direction. If e is a defined constant, then the equational lemmas associated with e are used. This provides a convenient way to unfold e.

rewrite [e₁, ..., eₙ] applies the given rules sequentially.

rewrite e at l rewrites e at location(s) l, where l is either * or a list of hypotheses in the local context. In the latter case, a turnstile ⊢ or |- can also be used, to signify the target of the goal.

This chapter of "Theorem Proving in Lean" is another good reference on "core" tactics (including rw).

#### Kevin Buzzard (Nov 02 2019 at 23:05):

I have documented all the tactics I use in a drop down menu on the left. Are people not seeing this? How should I be making this information easy to spot?

#### rory (Nov 02 2019 at 23:10):

What I'm guessing is that, not all tactics is in the drop down menu at every level(although that's the purpose). Level 1 mentioned rw, but rw is not explained in the drop-down menu in the first level.

#### Bryan Gin-ge Chen (Nov 02 2019 at 23:13):

I don't think rw is used in 1-1, only refl. I only see rw mentioned in this sentence:

Now click on "next level" in the top right of your browser to go onto the second level of tutorial world, where we'll learn about the rw tactic.

#### matt rice (Nov 02 2019 at 23:49):

when playing with this, wondering why 2-5 pointing me off towards one_eq_succ_zero, when there seems to be a much simpler way, is that supposed to be for the 1 + n case perhaps?

#### Kevin Buzzard (Nov 03 2019 at 00:04):

I should think you can prove it with refl, but I haven't introduced the idea of definitional equality (mathematicians only have one kind of equality and don't like thinking about all these other weird kinds with formal definitions) so people have to take stuff apart because they don't know any other way.

#### Kevin Buzzard (Nov 03 2019 at 00:55):

First draft of my attempt to teach intro, apply, exact now available at http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game_beta/ in world 5.

#### Kevin Buzzard (Nov 03 2019 at 00:57):

The purists will be wincing. 9 levels of constructing data in tactic mode. I think mathematicians might like this approach better than having to come to terms with the fact that implication is a function. Next level is going to be proposition world and it will just basically be the same levels again but with type Prop, so the mathematician user learns Propositions-as-Types or whatever it's called by it slowly dawning on them that they're doing the same level twice but thinking about it in two different ways.

#### Chris Hughes (Nov 03 2019 at 01:05):

I find term mode statements so difficult to read. I think this is much more readable.

theorem add_comm' (a b : ℕ) : begin
apply eq,
apply ((+) : ℕ → ℕ → ℕ),
apply a,
apply b,
apply ((+) : ℕ → ℕ → ℕ),
apply b,
apply a,
end


#### Kevin Buzzard (Nov 03 2019 at 19:46):

That would be a great pub quiz question: "These following standard theorem statements are constructed in tactic mode! What are their names?"

#### Kevin Buzzard (Nov 03 2019 at 19:48):

OK so I have function world (9 levels of manipulating sets and elements using intro, apply) and proposition world (9 levels of manipulating propositions and proofs using intro, apply) up at the beta link at http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game_beta/ if anyone is desperate for more levels.

#### pyon (Nov 04 2019 at 02:32):

Given a goal Q and a hypothesis h : P -> Q, is there some way to use h to reduce the goal to proving P?

#### pyon (Nov 04 2019 at 02:32):

Phrased differently, I want to know if there is a way to solve level 9 from world 5 step by step, rather than constructing a single large term.

#### Mario Carneiro (Nov 04 2019 at 02:37):

apply h

Thanks!

#### Mohammad Pedramfar (Nov 04 2019 at 06:43):

something that'd be neat would be zachtronics-like scoreboards displaying "x % of players completed this in y instructions"

Mohammad Pedramfar is this even feasible? Mohammad basically said very early on in the project "OK so we can either have people log in or not, and if they log in we can keep all their game data and do all sorts of things, but it will take me X days to learn how to do it" (for some value of X which was positive) and I said "Euclid the game doesn't have logins, so let's just go for it now while I don't have teaching, and let the user have access to all the levels".

Right now the game is a static webpage, the browser just downloads some files and runs the game. If we want the server to collect game statistics then we need a dynamic webpage. It's not theoretically difficult but it would take me some time to learn about it. The same is true with passwords and logins. The page needs to become dynamic.

#### Mohammad Pedramfar (Nov 04 2019 at 06:48):

you could store the gamestate including proofs in the browser (localstorage), then you wouldn't have to store any on the server and logins would be unnecessary if you don't mind the % stats being not completely accurate, biggest downside would be you'd still have to come up with a mechanism that handles world changes in a way that keeps most of one's gamestate intact

It's possible to save the gamestate in the browser, but then it will only give you statistics about yourself which is not necessarily useful. Saving the gamestate can be useful in order to remember the progress, so that you can continue the game another day. However, this is not a priority now since the game is constantly being updated and with any change, all the previous saved data in the browser will be lost.

#### Kevin Buzzard (Nov 04 2019 at 07:55):

Given a goal Q and a hypothesis h : P -> Q, is there some way to use h to reduce the goal to proving P?

This is the point of world 5 level 4.

#### Kevin Buzzard (Nov 04 2019 at 07:57):

I write all this text in the levels, and then younger viewers (like my 17 year old son) say "there are so many _words_!" and only read some of them. It's difficult. Younger people are more happy to watch a youtube vid. There should be a video version with no text at all and just the levels, where you watch the vid, get a "take home message", do the level and press on. No reading words necessary!

#### Bhavik Mehta (Nov 04 2019 at 11:04):

It's possible to save the gamestate in the browser, but then it will only give you statistics about yourself which is not necessarily useful. Saving the gamestate can be useful in order to remember the progress, so that you can continue the game another day. However, this is not a priority now since the game is constantly being updated and with any change, all the previous saved data in the browser will be lost.

Is it possible to do something like http://incredible.pm/, where progress is saved but when the game is updated, we hold on to old progress?

#### Luis O'Shea (Nov 05 2019 at 03:13):

I solved World 3/Level 5 with

lemma mul_assoc (a b c : mynat) : (a * b) * c = a * (b * c) :=
begin
induction c with d hd,
repeat {rw mul_zero},
refl,
end


but @Kevin Buzzard says "2) Did you know you can do rwa [hd, mul_add]? (I learnt that trick from Ken Lee)". How do I use that hint?

#### Johan Commelin (Nov 05 2019 at 05:02):

@Luis O'Shea rwa means rw followed by assumption.

#### Johan Commelin (Nov 05 2019 at 05:05):

That said, I don't see exactly what Kevin means with the hint

#### Kevin Buzzard (Nov 05 2019 at 07:16):

I think hint (2) is supposed to be read in conjunction with hint (1).

#### Kevin Buzzard (Nov 05 2019 at 07:17):

  induction c with d hd,
repeat {rw mul_zero},
repeat {rw mul_succ},
-- no refl!


#### Kevin Buzzard (Nov 05 2019 at 07:32):

I have no idea why repeat {rw mul_zero} doesn't need a refl. This is I guess a bug in the game. I have modified some tactics to behave differently but I didn't modify repeat. I don't know if it tries refl at the end of things.

#### Kevin Buzzard (Nov 05 2019 at 07:32):

In real Lean, rw tries to close the goal by refl at the end so you often don't need to write it. I decided this was confusing for the mathematician user and made them write all of them by disabling this.

#### Luis O'Shea (Nov 06 2019 at 04:49):

In my haste to solve the level I had not even noticed the missing refl after repeat {...}.

#### Luis O'Shea (Nov 06 2019 at 05:01):

In @Kevin Buzzard's post why can I not replace rwa [hd,mul_add] with rw [hd,mul_add],assumption? In fact what assumption does rwa use to close the goal?

#### Bryan Gin-ge Chen (Nov 06 2019 at 05:06):

It might have to do with the way that Kevin modified rw so that it doesn't automatically apply refl at the end. My guess is that rwa doesn't have that modification so it still applies the usual refl, which closes the goal.

#### Bryan Gin-ge Chen (Nov 06 2019 at 05:19):

Inspecting the code here supports my guess. The proofs in the natural number game use tactics from the "less_leaky.interactive" namespace instead of the usual tactic.interactive namespace. rw is defined in the less_leaky.interactive namespace to be rw' (a modified version which doesn't apply refl at the end) but rwa isn't directly defined there, so the usual rwa (which applies refl) gets copied into less_leaky.interactive by copy_decls.

What Bryan said.

#### Miguel Raz Guzmán Macedo (Nov 06 2019 at 07:50):

Hello all.
I thoroughly enjoyed the natural number game, but couldn't defeat the final boss.
Is there an answer sheet somewhere?
I couldn't get the twitter hint either, but I did have fun trying and I would recommend it as a tutorial starting point for all interested in Lean.

#### Kevin Buzzard (Nov 06 2019 at 08:40):

The Twitter hint just shows how to solve it using automation.

#### Kevin Buzzard (Nov 06 2019 at 08:41):

There's a proper proof involving a dozen or more rewrites though

#### Mohammad Pedramfar (Nov 07 2019 at 02:37):

I write all this text in the levels, and then younger viewers (like my 17 year old son) say "there are so many _words_!" and only read some of them. It's difficult. Younger people are more happy to watch a youtube vid. There should be a video version with no text at all and just the levels, where you watch the vid, get a "take home message", do the level and press on. No reading words necessary!

If the videos exist on youtube, it's probably not to hard to implement that.

#### Mohammad Pedramfar (Nov 07 2019 at 02:45):

It's possible to save the gamestate in the browser, but then it will only give you statistics about yourself which is not necessarily useful. Saving the gamestate can be useful in order to remember the progress, so that you can continue the game another day. However, this is not a priority now since the game is constantly being updated and with any change, all the previous saved data in the browser will be lost.

Is it possible to do something like http://incredible.pm/, where progress is saved but when the game is updated, we hold on to old progress?

That's an interesting website! If the updates are done in a way that the old levels don't change, I suppose that would be possible.

#### Lucas Allen (Nov 07 2019 at 03:52):

This is a fun game.

On world 3 level 5, the proof is below the lean editor window. It says "induction c with d hd, refl, repeat {rw mulsucc}, -- a * b * d + a * b = a * (b * d + b) rwa [hd, muladd], -/".

also, on world 2 level 4 I couldn't hear the boss music.

#### Kevin Buzzard (Nov 07 2019 at 07:03):

@Mohammad Pedramfar apparently there's a problem with the boss music

#### Kevin Buzzard (Nov 07 2019 at 07:03):

You could play the beta version next

#### Kevin Buzzard (Nov 07 2019 at 07:04):

natural_number_game_beta I think it is. Or something even more secret at natural_number_game_diags

#### Mohammad Pedramfar (Nov 07 2019 at 18:07):

It's possible to save the gamestate in the browser, but then it will only give you statistics about yourself which is not necessarily useful. Saving the gamestate can be useful in order to remember the progress, so that you can continue the game another day. However, this is not a priority now since the game is constantly being updated and with any change, all the previous saved data in the browser will be lost.

Is it possible to do something like http://incredible.pm/, where progress is saved but when the game is updated, we hold on to old progress?

I introduced this game to a friend of mine who's teaching logic now. He says thanks! :D

#### Mohammad Pedramfar (Nov 07 2019 at 18:08):

Mohammad Pedramfar apparently there's a problem with the boss music

We can solve that. Something like this : https://www.youtube.com/watch?v=-bzWSJG93P8 ?

#### Kevin Buzzard (Nov 10 2019 at 12:07):

I find term mode statements so difficult to read. I think this is much more readable.

theorem add_comm' (a b : ℕ) : begin
apply eq,
apply ((+) : ℕ → ℕ → ℕ),
apply a,
apply b,
apply ((+) : ℕ → ℕ → ℕ),
apply b,
apply a,
end


I find numerals so difficult to handle. I think this is much more readable.

def x : ℕ :=
begin
right,
right,
right,
left,
end

#print x -- 3


#### Rob Lewis (Nov 10 2019 at 14:45):

You're just duplicating something that's already in mathlib.

def x : ℕ := by library_search


#### Chris Hughes (Nov 10 2019 at 14:46):

I get x = 1100 when I do that. How interesting

#### Rob Lewis (Nov 10 2019 at 14:47):

@Scott Morrison A quiz: without checking, what's the type of y?

def y := by library_search


#### Chris Hughes (Nov 10 2019 at 14:50):

Is it Π {α : Sort *}, α → α ?

#### Rob Lewis (Nov 10 2019 at 14:52):

No, nothing so reasonable.

#### Kevin Buzzard (Nov 10 2019 at 14:53):

for int you get 1, for rat it fails.

#### Kevin Buzzard (Nov 10 2019 at 14:54):

Oh of course, it depends heavily on imports

#### Kevin Buzzard (Nov 12 2019 at 00:11):

The extra addition and multiplication worlds (which were there in v1.0 and removed in v1.06) are back in the current stable version of the natural number game, v1.09. I'm hoping users will find these a lot easier than last time around!

#### Lucas Allen (Nov 13 2019 at 03:19):

Level 9 of function world can be solved using solve_by_elim,

example (A B C D E F G H I J K L : Type)
(f1 : A → B) (f2 : B → E) (f3 : E → D) (f4 : D → A) (f5 : E → F)
(f6 : F → C) (f7 : B → C) (f8 : F → G) (f9 : G → J) (f10 : I → J)
(f11 : J → I) (f12 : I → H) (f13 : E → H) (f14 : H → K) (f15 : I → L)
: A → L :=
begin
intro,
solve_by_elim {max_rep := 8},
end


I figured since lean is a computer game, I'd create a file called hotkeys.lean with some personalized tactics not suitable for mathlib. One of these tactics is just solve_by_elim with the addition that it spits out an exact statement just like library_search. Using this, the line solve_by_elim {max_rep := 8} can be replaced by exact f15 (f11 (f9 (f8 (f5 (f2 (f1 a)))))).

#### Bryan Gin-ge Chen (Nov 13 2019 at 03:28):

Neat! There was some discussion on this example last week in this thread.

#### Lucas Allen (Nov 13 2019 at 03:43):

Oh I see, the { max_rep := 8 } part of solve_by_elim unfortunately is just something the user needs to know at this stage. I remember typing max_reps a couple of times and wondering why it wasn't working. It's explained in the doc string though.

#### Bryan Gin-ge Chen (Nov 13 2019 at 04:09):

I certainly didn't know about the max_rep option (I must have missed it at the bottom of the docstring). The fact that it's set to 3 by default should probably be added to the docstring / tactics doc.

#### Kevin Buzzard (Nov 13 2019 at 07:35):

I'll update the level! Thanks. I had not understood from the original conversation that this could be done.

#### agro1986 (Nov 14 2019 at 13:51):

Hi all, just wanna drop by to say thanks for making the fun game! Finished the addition and multiplication world and will try the others :)

#### agro1986 (Nov 16 2019 at 17:08):

Btw found a small typo on Proposition World level 3: exact l(j(h(P))) should be small case p.
If PRs are OK, I sent one here :) https://github.com/ImperialCollegeLondon/natural_number_game/pull/31

Thanks!

#### yuppie (Nov 18 2019 at 17:31):

I also need help for Advanced multiplication world, Level 4, mul_left_cancel. I started like this:

revert,
induction a,
exfalso,
exact ha(refl 0),
repeat {rw succ_mul},


and the goal is something like this:

case mynat.succ
b c a_n : mynat,
a_ih : a_n ≠ 0 → a_n * b = a_n * c → b = c,
ha : succ a_n ≠ 0
⊢ a_n * b + b = a_n * c + c → b=c


Somehow I would need to make a distinction whether a_n is 0, 1 or something else. Some kind of proof by cases or induction starting at 1 or something similar. Or am I going into a completely wrong direction? Am I still confined to constructive argumentation?

I am really addicted to the natural number game. Keep up the good work!

#### Kevin Buzzard (Nov 18 2019 at 18:20):

You can do cases a_n with a and it will split into the two cases a_n=0 and a_n=succ(a). On the other hand it might be worth thinking a bit about precisely what you want to prove by induction here.

#### Kevin Buzzard (Nov 18 2019 at 18:28):

i.e. what is your maths proof?

#### Lucas Allen (Nov 18 2019 at 21:59):

I struggled with mul_left_cancel for hours. I eventually cheated and looked at the answer on github. The trick is to start the proof with revert b or revert c, so that when you do induction and then cases the variable in the induction hypothesis isn't changed to succ something.

#### Luis O'Shea (Nov 19 2019 at 01:06):

I also found the use of revert in the proof of mul_left_cancel tricky (although KB added a very explicit hint to the game around v1.09b). Looking around in other examples I found various uses of revert which are not critical (i.e., can be easily done without revert). This was the first proof which truly used (IMO).

#### Luis O'Shea (Nov 19 2019 at 01:09):

As it happens I think it's an interesting issue since I think mathematicians don't clearly distinguish between statements like "n is natural number implies 2n is even" and "for all natural numbers n, 2n is even". That makes revert (as used in mul_left_cancel) slippery, but interesting. (At least this is how I see it.)

#### Luis O'Shea (Nov 19 2019 at 01:55):

For example in M1F example sheets/S0101.lean the first proof (of M1F_Sheet01_Q01a_is_F) uses revert in an inessential way: instead of revert H2,norm_num you can say norm_num at H2,assumption. However revert can not be eliminated from the proof of mul_left_cancel so easily, if at all.
As a beginner I think it would be useful to see another simple but "essential" use of revert.

#### Kevin Buzzard (Nov 19 2019 at 07:14):

You have to be clear what you're proving by induction. Is it ok if b is fixed like in associativity of addition (the inductive step uses the same b) or does the thing you're proving by induction need to be a claim that for all b something is true

#### Mario Carneiro (Nov 19 2019 at 07:15):

There is also induction a generalizing b for this pattern

#### yuppie (Nov 19 2019 at 19:39):

Ok I thought I was having trouble with lean but as Kevin pointed out I agree that I didn't have a math plan. Wait, how do you even prove b+b=c+c \implies b=c? Is this even true...? -.-

#### Kevin Buzzard (Nov 19 2019 at 20:01):

I'm glad to see that I'm causing some mini crises :-) Surely they taught you this proof in school? Funny how stuff gets skipped over :D

#### Kevin Buzzard (Nov 19 2019 at 20:01):

Do you want a hint @yuppie ?

#### yuppie (Nov 19 2019 at 20:14):

Do you want a hint yuppie ?

Thanks a lot, but not yet. I want to think about it for some while. I might come back to you in a few days when I'm desperate.

#### Michael R Douglas (Nov 20 2019 at 16:14):

I too struggled with mul_left_cancel, and eventually gave up and looked at the solution.
It uses the tactic congr which is not explained in the text (or even in the manual I was looking at ).
But it can be replaced with apply succ_eq_succ_of_eq.
Anyways I agree that we should see a simpler example of the need for revert.

what manual?

#### Mario Carneiro (Nov 20 2019 at 16:16):

It should be in the mathlib tactic docs

#### Michael R Douglas (Nov 20 2019 at 16:38):

https://leanprover.github.io/reference/tactics.html

#### Elvorfirilmathredia (Nov 20 2019 at 17:36):

I too struggled with mul_left_cancel, and eventually gave up and looked at the solution.

I didn't know there are solutions, where can I find them?
I just finished mul_left_cancel and thus the whole game but I'm new to lean and would like to see other solutions as well

#### Bryan Gin-ge Chen (Nov 20 2019 at 18:08):

You can find Kevin's solutions in the natural_number_game repo here. mul_left_cancel in particular is here.

#### Mario Carneiro (Nov 24 2019 at 15:18):

@Kevin Buzzard @Mohammad Pedramfar would it be possible to have the current level in the URL, so that people can link to levels? Currently it is always on the top level URL http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ . I think there are JS commands for updating the URL even in a "single page application" like this.

#### Bryan Gin-ge Chen (Nov 24 2019 at 15:27):

The easiest way might be to store / read the level name in a "hash parameter" (like how the lean-web-editor puts the code in the URL behind #code=).

#### Kevin Buzzard (Nov 24 2019 at 18:43):

I'm just the guy who writes the levels, so I have no idea. I was talking to my education specialist post-doc Athina and she said that for teaching students about about continuous functions it would be nice to have some little graphics apps with stuff you can pull to change epsilon and delta etc and I suspect this might be pretty tough in the current set-up which made me wonder if moving to observable would be better

#### Bryan Gin-ge Chen (Nov 24 2019 at 19:09):

I don't think there's any need to move things to Observable. It shouldn't be hard to embed illustrative interactive graphics that are written "as usual" using D3 or some other JS graphics library into the current game. If you want to have those graphics communicate with Lean code in some way then some of the code I wrote for the Lean Observable notebooks might come in handy as a reference, but you could still add such gadgets to the game without having to rewrite it in a different framework.

If you have some specific graphics ideas in mind, feel free to post a description here and I or someone else might take a stab at it.

#### Mohammad Pedramfar (Nov 25 2019 at 15:12):

Kevin Buzzard Mohammad Pedramfar would it be possible to have the current level in the URL, so that people can link to levels? Currently it is always on the top level URL http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ . I think there are JS commands for updating the URL even in a "single page application" like this.

That's a good idea. I'll implement it this weekend.

#### Mohammad Pedramfar (Nov 25 2019 at 15:12):

The easiest way might be to store / read the level name in a "hash parameter" (like how the lean-web-editor puts the code in the URL behind #code=).

Yeah, that's what I was thinking

#### Mohammad Pedramfar (Nov 25 2019 at 15:19):

I don't think there's any need to move things to Observable. It shouldn't be hard to embed illustrative interactive graphics that are written "as usual" using D3 or some other JS graphics library into the current game. If you want to have those graphics communicate with Lean code in some way then some of the code I wrote for the Lean Observable notebooks might come in handy as a reference, but you could still add such gadgets to the game without having to rewrite it in a different framework.

If you have some specific graphics ideas in mind, feel free to post a description here and I or someone else might take a stab at it.

I agree. It should be easy to import independent javascript graphics into the game. I'll try to look into your Observable codes, it's probably not too difficult to import/copy the same codes that you used there as well.

#### Julian Gilbey (Dec 05 2019 at 15:29):

As it happens I think it's an interesting issue since I think mathematicians don't clearly distinguish between statements like "n is natural number implies 2n is even" and "for all natural numbers n, 2n is even". That makes revert (as used in mul_left_cancel) slippery, but interesting. (At least this is how I see it.)

I also had fun trying to do this problem. I think it goes something like this. How do we prove ab=ac => b=c by induction? Well, let's try induction on b. Let us say we know the result for b=k and want to show it for b=k+1. More precisely, we know that ak=ac => k=c and we want to show that a(k+1) = ac => k+1 = c. But we can't possibly do that; we can expand the antecedent to get ak+a = ac, but even knowing that ak=ac => k=c doesn't get us anywhere. The problem is that c has a fixed value.

Instead, we have to prove a slightly different result, namely: "for all c, ab=ac => b=c". Now our induction hypothesis becomes "for all c, ak=ac => k=c" and we want to prove "for all c, a(k+1)=ac => k+1=c". We can now deal with the two possible cases for c, namely c=0 and c=m+1; the first leads to false => false (as a and k+1 are both non-zero), and the second gives a(k+1)=a(m+1) => k+1 = m+1, which can be reduced to ak=am => k+1=m+1. Since we know ak=am => k=m from our induction hypothesis, we can then deduce k+1=m+1.

#### Julian Gilbey (Dec 06 2019 at 09:20):

Hmm, I'm stuck on Inequality level 16. Here's where I've got to:

lemma lt_aux_two (a b : mynat) : succ a ≤ b → a ≤ b ∧ ¬ (b ≤ a) :=
intro h,
cases h with c hc,
split,
use succ c,
exact hc,
intro hb,
cases hb with d hd,
rw hd at hc,
have hb := not_succ_le_self b,
sorry


At this point I have the very helpful state:

a b c d : mynat,
hd : a = b + d,
hc : b = succ b + (d + c),
hb : ¬succ b ≤ b
⊢ false


I really want to turn hc into succ b ≤ b, so I want to do some sort of exists introduction, essentially saying "hc is my proof that succ b ≤ b", but I have no idea how to do so. (Of course, once I have this, then I just apply hb to it to close the goal.)

Any suggestions?

#### Kevin Buzzard (Dec 06 2019 at 10:26):

How about have hc' : succ b <= b,?

#### Kevin Buzzard (Dec 06 2019 at 10:26):

Then you can prove it using hc

#### Kevin Buzzard (Dec 06 2019 at 10:27):

Alternatively just work backwards, apply hb and then work on your new goal

#### Julian Gilbey (Dec 06 2019 at 10:32):

Ah, nice, thanks! I'd completely forgotten that you could introduce new goals with have! I'm gradually getting the hang of this ;-)

#### Kevin Buzzard (Dec 06 2019 at 10:45):

I think your next move should just be apply hb. Did you do that function level where you just do have have have and go forwards but then there's this other proof where you go apply apply apply and go backwards?

#### Kevin Buzzard (Dec 06 2019 at 10:46):

Thinking backwards is important because it tells you how to start writing your function, as opposed to what to put at the end of it

#### Kevin Buzzard (Dec 06 2019 at 10:46):

Apply hb then use (d+c)

#### Luis O'Shea (Dec 08 2019 at 20:26):

@Julian Gilbey, another approach to proving lt_aux_two is to use the transitivity of "≤" (le_trans); see spoiler for full proof.

#### Julian Gilbey (Dec 13 2019 at 12:08):

Julian Gilbey, another approach to proving lt_aux_two is to use the transitivity of "≤" (le_trans`); see spoiler for full proof.

Ah, that's a nice idea, thanks! With that hint, I recreated exactly your solution myself.

Last updated: May 16 2021 at 21:11 UTC