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

Stream: new members

[Kevin Buzzard]

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

[waldo]

yeah sure

[Kevin Buzzard]

@waldo did reloading the page help?

[waldo]

still getting the lean is busy

[waldo]

what browser are you using?

[Kevin Buzzard]

It works for me on Chrome

[Tim Hosgood]

and it works for me on Firefox

[Bryan Gin-ge Chen]

Do you see any strange messages in your browser console?

[waldo]

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

[waldo]

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

[Bryan Gin-ge Chen]

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

[waldo]

maybe I have changed some privacy settings..

[waldo]

latest firefox but privacy settings on (cookies mainly)

[Tim Hosgood]

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

[waldo]

I have to go, let's speak later

[Kevin Buzzard]

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

[Tim Hosgood]

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]

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]

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]

so I suspect the javascript is not running

[Kevin Buzzard]

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

[Bryan Gin-ge Chen]

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]

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

[Kevin Buzzard]

does the natural number game work for you on chrome?

[waldo]

you mean level 4 world 1?

[Kevin Buzzard]

@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]

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

[Kevin Buzzard]

@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]

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]

@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]

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]

in edge the lean interperter was busy all the time

[waldo]

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

[Kevin Buzzard]

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]

are you a mathmetician kevin?

[Kevin Buzzard]

right.

[waldo]

or you programmed the lean interperter?

[Mario Carneiro]

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]

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]

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]

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

[Bryan Gin-ge Chen]

probably zero work had to be done

Heh, depends on your definition of zero...

[waldo]

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]

what was that talk?

[Mario Carneiro]

because Lean is pretty minimal

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

[waldo]

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

[Kevin Buzzard]

Lean 3 does not. Lean 4 will.

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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]

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]

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?

[waldo]

:D

[Kevin Buzzard]

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

[waldo]

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

[Mario Carneiro]

what do you mean exactly?

[Mario Carneiro]

lean isn't about "computation" per se

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[waldo]

it's all theoretically

[waldo]

who is actually leading the talks here

[waldo]

the challenge, lean the language

[waldo]

lean is by microsoft researches or am I wrong?

[Mario Carneiro]

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

[Mario Carneiro]

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

[waldo]

mathlib is a lean lbirary for math proofs?

[Mario Carneiro]

yes

[Mario Carneiro]

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

[waldo]

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

[Mario Carneiro]

go for it!

[waldo]

Where do we stand today?

[waldo]

is there a roadmap?

[waldo]

what are the limitations of lean currently?

[waldo]

how is cog compared to lean?

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

which is a bit backward from the usual pedagogy

[waldo]

is it just to get things go faster?

[waldo]

so we can go for more hard stuff?

[Mario Carneiro]

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

[waldo]

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]

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]

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

[Mario Carneiro]

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

[waldo]

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

[Mario Carneiro]

@Kevin Buzzard is a better person to ask for the roadmap

[waldo]

is this the right stream?

[Mario Carneiro]

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

[waldo]

right stream to talk about is I mean

[waldo]

nvm, I'll go throught the game

[Mario Carneiro]

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

[Mario Carneiro]

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

[waldo]

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,
rw add_zero,
rw add_zero,
rw add_zero,
rw add_zero,
refl,
rw add_succ,
rw add_zero,
rw add_zero,
rw add_succ,
refl,
rw add_succ,
rw add_succ,
rw add_succ,
rw cd,
refl,

[Kevin Buzzard]

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,
rw add_zero,
rw add_zero,
rw add_zero,
rw add_zero,
refl,
rw add_succ,
rw add_zero,
rw add_zero,
rw add_succ,
refl,
rw add_succ,
rw add_succ,
rw add_succ,
rw cd,
refl,

[Kevin Buzzard]

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

[Kevin Buzzard]

Kevin Buzzard is a better person to ask for the roadmap

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]

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]

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]

let b := f a

[Reid Barton]

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]

let is the user-facing version of tactic.pose

[Emily Riehl]

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]

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

[Emily Riehl]

Thanks. I wasn't reading carefully enough.

[Kevin Buzzard]

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]

I hope to return to this game over the weekend. Thanks for your feedback Emily.

[Kevin Buzzard]

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]

@Emily Riehl Welcome on the chat :smiley:

[Alain Muller]

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]

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

[Kevin Buzzard]

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]

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]

@Kevin Buzzard maybe put that link there

[Kenny Lau]

btw you have 4 PRs now

[Kevin Buzzard]

I do?

[Kevin Buzzard]

Thanks for letting me know!

[Kenny Lau]

no problem

[Mohammad Pedramfar]

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]

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]

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]

I am systematically removing all these worlds

[Kevin Buzzard]

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]

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

[Michael Barz]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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

[Reid Barton]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[vrs]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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

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

[Lynn]

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]

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]

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

[Lynn]

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

[Lynn]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Fixed in v1.03

[Kevin Buzzard]

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]

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

[Johan Commelin]

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

[vrs]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Bryan Gin-ge Chen]

As Johan says, conv might help.

[Antoine Chambert-Loir]

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,

but I get the answer

rewrite tactic failed, lemma lhs is a metavariable

[vrs]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

succ_inj will prove that your goal implies a hypothesis.

[Kevin Buzzard]

You need to show that your hypotheses imply the goal

[Kevin Buzzard]

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

[Antoine Chambert-Loir]

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

[Kevin Buzzard]

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]

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

```lean
code goes here
```

[Kevin Buzzard]

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]

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]

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]

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

[vrs]

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

[Kevin Buzzard]

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]

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

[vrs]

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]

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]

use is magic

[vrs]

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]

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]

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

[vrs]

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},
repeat {rw add_mul},
repeat {rw mul_add},
simp,

[Kevin Buzzard]

Did you look at the spoiler on Twitter?

[Kevin Buzzard]

It's even easier than that :D

[vrs]

yes but ring was never introduced was it?

[Kevin Buzzard]

indeed it wasn't.

[Kevin Buzzard]

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

[vrs]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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

[vrs]

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

[vrs]

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

[Kevin Buzzard]

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]

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]

@Antoine Chambert-Loir

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

This is not something I can say anything about.

[Marc Huisinga]

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]

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]

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

[Kevin Buzzard]

You could try the perfectoid space game

[Kevin Buzzard]

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]

Alternatively you could try the levels I just wrote this afternoon

[Johan Commelin]

@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]

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]

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]

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

[Bryan Gin-ge Chen]

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]

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

[Kevin Buzzard]

lemme get world 5 up, hang on.

[tirima]

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]

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]

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

[Kevin Buzzard]

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

[Bryan Gin-ge Chen]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

apply h

[pyon]

Thanks!

[Mohammad Pedramfar]

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]

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]

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]

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]

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]

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},
  rw [mul_succ, mul_succ, mul_add, hd],
  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]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Luis O'Shea]

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]

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]

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.

[Kevin Buzzard]

What Bryan said.

[Miguel Raz Guzmán Macedo]

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]

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

[Kevin Buzzard]

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

[Mohammad Pedramfar]

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]

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]

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]

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

[Kevin Buzzard]

You could play the beta version next

[Kevin Buzzard]

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

[Mohammad Pedramfar]

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]

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]

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]

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

def x : ℕ := by library_search

[Chris Hughes]

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

[Rob Lewis]

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

def y := by library_search

[Chris Hughes]

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

[Rob Lewis]

No, nothing so reasonable.

[Kevin Buzzard]

for int you get 1, for rat it fails.

[Kevin Buzzard]

Oh of course, it depends heavily on imports

[Kevin Buzzard]

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]

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]

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

[Lucas Allen]

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]

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]

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

[agro1986]

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]

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

[Kevin Buzzard]

Thanks!

[yuppie]

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]

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]

i.e. what is your maths proof?

[Lucas Allen]

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]

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]

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]

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]

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]

There is also induction a generalizing b for this pattern

[yuppie]

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]

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]

Do you want a hint @yuppie ?

[yuppie]

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]

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.

[Mario Carneiro]

what manual?

[Mario Carneiro]

It should be in the mathlib tactic docs

[Michael R Douglas]

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

[Elvorfirilmathredia]

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]

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

[Mario Carneiro]

@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]

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]

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]

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]

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]

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]

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]

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]

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,
rw [succ_add, ← add_succ] at hc,
split,
  use succ c,
  exact hc,
intro hb,
cases hb with d hd,
rw hd at hc,
rw [add_assoc, add_succ, add_succ, ← succ_add] 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]

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

[Kevin Buzzard]

Then you can prove it using hc

[Kevin Buzzard]

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

[Julian Gilbey]

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]

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]

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]

Apply hb then use (d+c)

[Luis O'Shea]

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

[Julian Gilbey]

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.