Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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.

view this post on Zulip waldo (Oct 26 2019 at 19:18):

yeah sure

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 19:18):

@waldo did reloading the page help?

view this post on Zulip waldo (Oct 26 2019 at 19:18):

still getting the lean is busy

view this post on Zulip waldo (Oct 26 2019 at 19:18):

what browser are you using?

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 19:19):

It works for me on Chrome

view this post on Zulip Tim Hosgood (Oct 26 2019 at 19:21):

and it works for me on Firefox

view this post on Zulip Bryan Gin-ge Chen (Oct 26 2019 at 19:21):

Do you see any strange messages in your browser console?

view this post on Zulip waldo (Oct 26 2019 at 19:21):

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

view this post on Zulip waldo (Oct 26 2019 at 19:21):

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

view this post on Zulip Bryan Gin-ge Chen (Oct 26 2019 at 19:22):

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

view this post on Zulip waldo (Oct 26 2019 at 19:22):

maybe I have changed some privacy settings..

view this post on Zulip waldo (Oct 26 2019 at 19:22):

latest firefox but privacy settings on (cookies mainly)

view this post on Zulip Tim Hosgood (Oct 26 2019 at 19:22):

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

view this post on Zulip waldo (Oct 26 2019 at 19:23):

I have to go, let's speak later

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 19:23):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 19:25):

so I suspect the javascript is not running

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 19:26):

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

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 22:54):

does the natural number game work for you on chrome?

view this post on Zulip waldo (Oct 26 2019 at 22:56):

you mean level 4 world 1?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip waldo (Oct 26 2019 at 22:59):

in edge the lean interperter was busy all the time

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip waldo (Oct 26 2019 at 23:01):

are you a mathmetician kevin?

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 23:01):

right.

view this post on Zulip waldo (Oct 26 2019 at 23:01):

or you programmed the lean interperter?

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip waldo (Oct 26 2019 at 23:03):

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

view this post on Zulip Bryan Gin-ge Chen (Oct 26 2019 at 23:04):

probably zero work had to be done

Heh, depends on your definition of zero...

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 23:04):

what was that talk?

view this post on Zulip 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

view this post on Zulip waldo (Oct 26 2019 at 23:04):

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

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 23:05):

Lean 3 does not. Lean 4 will.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip waldo (Oct 26 2019 at 23:10):

:D

view this post on Zulip 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.

view this post on Zulip waldo (Oct 26 2019 at 23:11):

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

view this post on Zulip Mario Carneiro (Oct 26 2019 at 23:11):

what do you mean exactly?

view this post on Zulip Mario Carneiro (Oct 26 2019 at 23:12):

lean isn't about "computation" per se

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip waldo (Oct 26 2019 at 23:14):

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

view this post on Zulip 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)

view this post on Zulip waldo (Oct 26 2019 at 23:15):

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

view this post on Zulip Mario Carneiro (Oct 26 2019 at 23:15):

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

view this post on Zulip waldo (Oct 26 2019 at 23:15):

it's all theoretically

view this post on Zulip waldo (Oct 26 2019 at 23:15):

who is actually leading the talks here

view this post on Zulip waldo (Oct 26 2019 at 23:15):

the challenge, lean the language

view this post on Zulip waldo (Oct 26 2019 at 23:16):

lean is by microsoft researches or am I wrong?

view this post on Zulip 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?)

view this post on Zulip 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

view this post on Zulip waldo (Oct 26 2019 at 23:18):

mathlib is a lean lbirary for math proofs?

view this post on Zulip Mario Carneiro (Oct 26 2019 at 23:18):

yes

view this post on Zulip 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

view this post on Zulip waldo (Oct 26 2019 at 23:19):

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

view this post on Zulip Mario Carneiro (Oct 26 2019 at 23:19):

go for it!

view this post on Zulip waldo (Oct 26 2019 at 23:19):

Where do we stand today?

view this post on Zulip waldo (Oct 26 2019 at 23:19):

is there a roadmap?

view this post on Zulip waldo (Oct 26 2019 at 23:19):

what are the limitations of lean currently?

view this post on Zulip waldo (Oct 26 2019 at 23:19):

how is cog compared to lean?

view this post on Zulip 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

view this post on Zulip waldo (Oct 26 2019 at 23:20):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 26 2019 at 23:21):

which is a bit backward from the usual pedagogy

view this post on Zulip waldo (Oct 26 2019 at 23:21):

is it just to get things go faster?

view this post on Zulip waldo (Oct 26 2019 at 23:21):

so we can go for more hard stuff?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 26 2019 at 23:23):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 26 2019 at 23:25):

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

view this post on Zulip waldo (Oct 26 2019 at 23:25):

is this the right stream?

view this post on Zulip Mario Carneiro (Oct 26 2019 at 23:25):

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

view this post on Zulip waldo (Oct 26 2019 at 23:26):

right stream to talk about is I mean

view this post on Zulip waldo (Oct 26 2019 at 23:26):

nvm, I'll go throught the game

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 26 2019 at 23:27):

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

view this post on Zulip 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,
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,

view this post on Zulip 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,
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,

view this post on Zulip Kevin Buzzard (Oct 27 2019 at 00:18):

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

view this post on Zulip Kevin Buzzard (Oct 27 2019 at 00:21):

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.

view this post on Zulip 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.

view this post on Zulip 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,.

view this post on Zulip Kenny Lau (Oct 27 2019 at 01:59):

let b := f a

view this post on Zulip 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.

view this post on Zulip Jesse Michael Han (Oct 27 2019 at 02:10):

let is the user-facing version of tactic.pose

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Emily Riehl (Oct 29 2019 at 12:32):

Thanks. I wasn't reading carefully enough.

view this post on Zulip 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".

view this post on Zulip Kevin Buzzard (Oct 29 2019 at 12:34):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 29 2019 at 15:42):

@Emily Riehl Welcome on the chat :smiley:

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Oct 29 2019 at 18:17):

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

view this post on Zulip 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 :-/

view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 29 2019 at 18:20):

@Kevin Buzzard maybe put that link there

view this post on Zulip Kenny Lau (Oct 29 2019 at 18:22):

btw you have 4 PRs now

view this post on Zulip Kevin Buzzard (Oct 29 2019 at 18:28):

I do?

view this post on Zulip Kevin Buzzard (Oct 29 2019 at 18:28):

Thanks for letting me know!

view this post on Zulip Kenny Lau (Oct 29 2019 at 18:28):

no problem

view this post on Zulip 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.

view this post on Zulip 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! :)

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Oct 30 2019 at 22:46):

I am systematically removing all these worlds

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Oct 30 2019 at 22:47):

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

view this post on Zulip Michael Barz (Oct 30 2019 at 22:48):

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

view this post on Zulip Kevin Buzzard (Oct 30 2019 at 22:48):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Oct 30 2019 at 23:46):

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

view this post on Zulip Kevin Buzzard (Oct 30 2019 at 23:46):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Oct 30 2019 at 23:47):

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

view this post on Zulip Kevin Buzzard (Oct 30 2019 at 23:47):

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

view this post on Zulip Kevin Buzzard (Oct 30 2019 at 23:47):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 30 2019 at 23:54):

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

view this post on Zulip 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

view this post on Zulip 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,
{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},

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Lynn (Nov 01 2019 at 01:28):

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

view this post on Zulip Lynn (Nov 01 2019 at 01:28):

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

view this post on Zulip Lynn (Nov 01 2019 at 01:32):

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

view this post on Zulip Kevin Buzzard (Nov 01 2019 at 08:54):

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

view this post on Zulip Kevin Buzzard (Nov 01 2019 at 10:11):

Fixed in v1.03

view this post on Zulip 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.

view this post on Zulip vrs (Nov 01 2019 at 20:28):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip vrs (Nov 01 2019 at 20:33):

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

view this post on Zulip Johan Commelin (Nov 01 2019 at 20:34):

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

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Nov 01 2019 at 20:35):

As Johan says, conv might help.

view this post on Zulip 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,

but I get the answer

rewrite tactic failed, lemma lhs is a metavariable

view this post on Zulip vrs (Nov 01 2019 at 21:09):

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

view this post on Zulip Kevin Buzzard (Nov 01 2019 at 21:09):

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

view this post on Zulip Kevin Buzzard (Nov 01 2019 at 21:10):

succ_inj will prove that your goal implies a hypothesis.

view this post on Zulip Kevin Buzzard (Nov 01 2019 at 21:10):

You need to show that your hypotheses imply the goal

view this post on Zulip Kevin Buzzard (Nov 01 2019 at 21:11):

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

view this post on Zulip Antoine Chambert-Loir (Nov 01 2019 at 21:12):

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

view this post on Zulip 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

view this post on Zulip 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
```

view this post on Zulip 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.

view this post on Zulip 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 !

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 01 2019 at 22:01):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip vrs (Nov 02 2019 at 01:20):

use is magic

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 02 2019 at 12:28):

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

view this post on Zulip 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},
repeat {rw add_mul},
repeat {rw mul_add},
simp,

view this post on Zulip Kevin Buzzard (Nov 02 2019 at 14:07):

Did you look at the spoiler on Twitter?

view this post on Zulip Kevin Buzzard (Nov 02 2019 at 14:07):

It's even easier than that :D

view this post on Zulip vrs (Nov 02 2019 at 14:07):

yes but ring was never introduced was it?

view this post on Zulip Kevin Buzzard (Nov 02 2019 at 14:07):

indeed it wasn't.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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(a+b)^2 is trivial" [at the start] to "a lot goes into this actually" to "oh no, it is trivial after all".

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip vrs (Nov 02 2019 at 14:17):

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

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 02 2019 at 14:26):

@Antoine Chambert-Loir

view this post on Zulip 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.

view this post on Zulip 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".

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Nov 02 2019 at 15:07):

This is not something I can say anything about.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip pyon (Nov 02 2019 at 15:58):

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

view this post on Zulip Kevin Buzzard (Nov 02 2019 at 19:50):

You could try the perfectoid space game

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 02 2019 at 19:52):

Alternatively you could try the levels I just wrote this afternoon

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip pyon (Nov 02 2019 at 20:09):

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

view this post on Zulip Kevin Buzzard (Nov 02 2019 at 20:11):

lemme get world 5 up, hang on.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 02 2019 at 22:05):

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

view this post on Zulip Kevin Buzzard (Nov 02 2019 at 22:06):

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

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?"

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 04 2019 at 02:37):

apply h

view this post on Zulip pyon (Nov 04 2019 at 03:08):

Thanks!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip 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},
  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?

view this post on Zulip Johan Commelin (Nov 05 2019 at 05:02):

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

view this post on Zulip Johan Commelin (Nov 05 2019 at 05:05):

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

view this post on Zulip Kevin Buzzard (Nov 05 2019 at 07:16):

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

view this post on Zulip Kevin Buzzard (Nov 05 2019 at 07:17):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 {...}.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 06 2019 at 07:06):

What Bryan said.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 06 2019 at 08:40):

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

view this post on Zulip Kevin Buzzard (Nov 06 2019 at 08:41):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 07 2019 at 07:03):

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

view this post on Zulip Kevin Buzzard (Nov 07 2019 at 07:03):

You could play the beta version next

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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 ?

view this post on Zulip 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

view this post on Zulip Rob Lewis (Nov 10 2019 at 14:45):

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

def x :  := by library_search

view this post on Zulip Chris Hughes (Nov 10 2019 at 14:46):

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

view this post on Zulip 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

view this post on Zulip Chris Hughes (Nov 10 2019 at 14:50):

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

view this post on Zulip Rob Lewis (Nov 10 2019 at 14:52):

No, nothing so reasonable.

view this post on Zulip Kevin Buzzard (Nov 10 2019 at 14:53):

for int you get 1, for rat it fails.

view this post on Zulip Kevin Buzzard (Nov 10 2019 at 14:54):

Oh of course, it depends heavily on imports

view this post on Zulip 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!

view this post on Zulip 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)))))).

view this post on Zulip Bryan Gin-ge Chen (Nov 13 2019 at 03:28):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 18:15):

Thanks!

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 18 2019 at 18:28):

i.e. what is your maths proof?

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 19 2019 at 07:15):

There is also induction a generalizing b for this pattern

view this post on Zulip 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...? -.-

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 20:01):

Do you want a hint @yuppie ?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 20 2019 at 16:15):

what manual?

view this post on Zulip Mario Carneiro (Nov 20 2019 at 16:16):

It should be in the mathlib tactic docs

view this post on Zulip Michael R Douglas (Nov 20 2019 at 16:38):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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=).

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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,
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?

view this post on Zulip Kevin Buzzard (Dec 06 2019 at 10:26):

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

view this post on Zulip Kevin Buzzard (Dec 06 2019 at 10:26):

Then you can prove it using hc

view this post on Zulip Kevin Buzzard (Dec 06 2019 at 10:27):

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

view this post on Zulip 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 ;-)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 06 2019 at 10:46):

Apply hb then use (d+c)

view this post on Zulip 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.

view this post on Zulip 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