## Stream: new members

### Topic: natural number game questions

#### Craig Citro (Dec 27 2019 at 04:34):

hi all! absolutely loving the natural number game (kudos @Kevin Buzzard). i had a few (largely silly) questions.

1. for adv proposition world, level 9, is there a way to beat it with only the tactics we know so far other than cc or tauto? in the second case, i spent a few minutes trying to figure out how to capitalize on having P \land \lnot P in hand before googling and discovering the contradiction tactic. was i missing a more "bare-handed" approach?

2. for adv proposition world, level 8, there's a "did you spot the import" comment at the end that's mysterious to me ... what import?

3. is there a github repo where the code for the game lives?

#### Craig Citro (Dec 27 2019 at 04:36):

... and a followup: how does one get inline expansion for latex here? ;)

#### Bryan Gin-ge Chen (Dec 27 2019 at 04:49):

1. You can do it using by_cases hq : Q, and exfalso (I guess that shows up in the next level though...) (edit: and you can replace exfalso by either using the term false.elim or by using cases H on a hypothesis H : false.)
2. I'm guessing Kevin was thinking of the line import tactic.finish in the source Lean file here and that paragraph was a subtle hint for you to try the finish tactic. Unfortunately, the import isn't visible in the generated HTML...

awesome, thanks!

#### Emily Riehl (Feb 21 2020 at 01:25):

Inspired by @Scott Morrison I returned to the natural numbers game this weekend and was delighted to see all the new tactics and new levels. I feel like I'm getting somewhere now. Thanks everyone.

#### Emily Riehl (Feb 21 2020 at 01:29):

Now here's my question: I'm stuck on mul_left_cancel in the advanced multiplication world. I'd like to prove (a !=0) -> (a b = a c) -> b = c by (strong) double induction on b and c. This should give me four cases, three of which involve the hypothesis that either b or c is zero. Then for the fourth the plan is to use add_left_cancel to conclude from the hypothesis

a (succ b) = a (succ c)

that

a b = a c.

Then the inductive hypothesis should give me b = c, whence succ b = succ c.

But I have no idea how to set up this double induction. The hint says to use revert but I don't see where it would help.

#### Scott Morrison (Feb 21 2020 at 01:34):

My guess is that you want a forall in the goal at the moment you invoke induction, and to achieve that you need to use revert.

#### Scott Morrison (Feb 21 2020 at 01:34):

Spoiler:

revert c,
induction b,
{ intro c, sorry, },
{ intro c, induction c,
{ sorry, },
{ sorry, } }


#### Scott Morrison (Feb 21 2020 at 01:35):

(I haven't actually tried doing the proof after that step, I'm just guessing that's the structure you wanted.)

#### Emily Riehl (Feb 21 2020 at 01:44):

Thanks @Scott Morrison . That did the trick.

Here's the full gory thing (spoiler below):

revert c,
induction b with x hx,
intro c,
rw mul_zero,
intro hyp,
symmetry at hyp,
have lem := eq_zero_or_eq_zero_of_mul_eq_zero _ _ hyp,
cases lem with p q,
exfalso,
exact ha p,
symmetry,
assumption,
intro c,
induction c with y hy,
intro hyp,
rw mul_zero at hyp,
have lem := eq_zero_or_eq_zero_of_mul_eq_zero _ _ hyp,
cases lem with p q,
exfalso,
exact ha p,
assumption,
intro hyp,
repeat {rw mul_succ at hyp},
have lem := add_right_cancel _ _ _ hyp,
have step := hx y lem,
apply succ_eq_succ_of_eq,
assumption,

#### Scott Morrison (Feb 21 2020 at 01:46):

Next you need some braces and indenting. :-)

Haha on point ;)

#### Scott Morrison (Feb 21 2020 at 01:46):

Ah, earlier I couldn't work out why ex_falso didn't exist... Apparently because it's exfalso, but by_contradiction.

#### Scott Morrison (Feb 21 2020 at 03:07):

@Kevin Buzzard, what do you think of adding a @[simp] lemma that says succ n = n + 1? In some of the later levels I find myself writing proofs that want to use this fact often.

#### Johan Commelin (Feb 21 2020 at 07:34):

@Emily Riehl Congrats!

#### Kevin Buzzard (Feb 21 2020 at 07:53):

This is a bad level. Without revert it's probably impossible and I do a really bad job of explaining how revert works. This needs to be fixed

#### Mario Carneiro (Feb 21 2020 at 08:21):

It can be done without revert if you use induction b generalizing c instead (which is the correct way to do inductions like this anyway)

#### Mario Carneiro (Feb 21 2020 at 08:22):

It's debatable, but I think it is a good teaching moment to explain what it means to generalize an argument in an induction. This came up in discussions at the meeting in bonn

#### Kevin Buzzard (Feb 21 2020 at 09:31):

I will get back to this game in a few weeks and update it. There are several minor changes I want to make

#### Ethan Horsfall (Feb 24 2020 at 20:31):

apologies if I am being useless; on question 8 of advanced addition world, and whenever I try to use succ_inj something goes wrong.

b n : mynat,
an : n + b = n → b = 0,
h : succ (n + b) = succ n
⊢ b = 0

I want to apply succ_inj to h by applying it to h with parameters n+b and b, but this always raises an error. When I've had problems like this on previious levels, I've used the 'have' tactic, but this also won't import because it seems to get confused by the parameter name n+b

#### Kevin Buzzard (Feb 24 2020 at 21:09):

does have h2 := succ_inj h work?

#### Kevin Buzzard (Feb 24 2020 at 21:11):

I guess you could just go backwards the way the computer scientists want you to do -- apply an and then apply succ_inj will presumably work.

#### Patrick Massot (Feb 24 2020 at 21:25):

It looks like the official solution

#### Ethan Horsfall (Feb 25 2020 at 10:29):

ah thank you that works ! i also hadnt realised there was an official solution set oops so thank you for that also

#### Ethan Horsfall (Feb 25 2020 at 10:29):

also really enjoying the game, so thanks for making it :)

#### Kevin Buzzard (Feb 25 2020 at 10:45):

I'm not sure it's officially documented anywhere that there's an official solution set :-)

#### Ethan Horsfall (Feb 25 2020 at 14:16):

when calling a function, such as succ_inj or mul_pos, how do you pass in arguments which themselves are functions?

For instance,
have f := mul_pos a b,

works but
have f := mul_pos succ(a) succ(b),
does not work, with the error message indicating that it expected something of type mynat, whereas it read s succ as a function from mynat to mynat.

thank you:)

#### Donald Sebastian Leung (Feb 25 2020 at 14:17):

You probably need to wrap succ(a) and succ(b) itself in parentheses, like so: have f := mul_pos (succ(a)) (succ(b))

#### Bryan Gin-ge Chen (Feb 25 2020 at 14:18):

The parentheses around a and b in succ(a) and succ(b) are unnecessary. Note that you can also take advantage of "dot notation" and write have f := mul_pos a.succ b.succ.

thank you both:)

#### Donald Sebastian Leung (Feb 25 2020 at 14:19):

You're welcome :smile:

#### Kevin Buzzard (Feb 25 2020 at 14:23):

I always put the parentheses in succ(a) in the natural number game because I felt it was less intimidating for mathematicians

#### Ethan Horsfall (Feb 25 2020 at 14:24):

yes I find that much more natural

#### Kevin Buzzard (Feb 25 2020 at 14:24):

However this shows a downside to this idea -- succ(a) looks like an irreducible gadget to a mathematician, but is apparently parsed as succ a and hence succ can fall off and be eaten by an earlier function.

#### Donald Sebastian Leung (Feb 25 2020 at 14:24):

@Ethan Horsfall FYI the notation for function application in (functional) programming differs from that in conventional mathematics, for example f(x) in mathematics could be simply written as f x in Lean

#### Ethan Horsfall (Feb 26 2020 at 16:31):

on the last level of advanced multiplication world, i have got it to the point where I have the hypothesis
c : mynat,
c_ih : ∀ (a : mynat), a ≠ 0 → ∀ (b : mynat), a * b = a * c → b = c, ###
a : mynat,
ha : a ≠ 0, ###
n : mynat,
g : a * n + a = a * c + a,
W : a * n + a = a * c + a → a * n = a * c
⊢ a * n = a * c → n = c ###

I have put ### by the remaining relevant propositions

which should be very simple as if we only look at c_ih and ha, the goal is just a restatement of this. but i cannot work out how to introduce the right variables into c_ih or revert the goal correctly. The propositions in the middle muddle it up when I use revert

#### Kevin Buzzard (Feb 26 2020 at 17:05):

Does exact c_ih a ha n work?

#### Kevin Buzzard (Feb 26 2020 at 17:06):

You can think of c_ih as a function, which takes as input a natural number a, a proof that it's not zero, and a natural number b, and returns a proof that ab=ac -> b=c.

#### Reid Barton (Feb 26 2020 at 17:12):

Also you should be able to apply c_ih and let Lean work out what additional arguments are needed.

#### Reid Barton (Feb 26 2020 at 17:13):

(either supplying them automatically or turning them into new goals)

#### Ethan Horsfall (Feb 26 2020 at 19:44):

thank you, that seems to have worked. the slightly weird thing is that it now just says 'no goals' instead of proof complete. viewing it as a function makes a lot of sense

#### Kevin Buzzard (Feb 26 2020 at 21:16):

?? I'm impressed :-) I thought Mohammad had managed to completely banish "no goals"!

#### Ethan Horsfall (Feb 27 2020 at 11:55):

Finished the game!!

#### Ethan Horsfall (Feb 27 2020 at 12:02):

is the official documentation the best place to go next?

#### Donald Sebastian Leung (Feb 27 2020 at 14:08):

Ethan Horsfall said:

is the official documentation the best place to go next?

That, or you could try Theorem Proving in Lean next which teaches you how to define your own functions, mathematical objects, etc. on top of proving theorems with tactics.

#### Bryan Gin-ge Chen (Feb 27 2020 at 14:19):

In addition to TPiL, I found the Logic & Proof book useful when I was learning Lean. I also like the Logical Verification notes.

#### Kevin Buzzard (Feb 27 2020 at 16:24):

If you're a mathematician then one thing you could try is to choose an arbitrary piece of elementary mathematics and try doing it in Lean, and ask when you get stuck. For me the route was: basic 1st year introduction to proof stuff, definition of a scheme, theorems about schemes, definition of a perfectoid space. Because there is no ideal book for mathematicians we have to forge our own path right now. I guess there are always the maths challenges if they're up your street. What are you looking for?

#### Kevin Buzzard (Feb 27 2020 at 16:25):

PS @Ethan Horsfall Mohammad says that if you can reproduce "no goals" then you should tell us how and he'll try and fix it ;-) He's just submitted his PhD thesis so I'm sure he has plenty of time on his hands :-)

#### Ethan Horsfall (Feb 27 2020 at 16:58):

I'm an undergraduate student. (actually, an undergraduate economist, but I just secured my switch to maths recently :) ). I'm in the fortunate position of mostly pursuing what I find interesting. for the 'no goals' every time I refreshed the page it would lose previous progress, so I may not be able to reproduce it

#### Kevin Buzzard (Feb 27 2020 at 17:37):

What maths do you know already?

#### Ethan Horsfall (Feb 27 2020 at 17:44):

i've covered https://dec41.user.srcf.net/notes/ all of part ia except dynamics and relativity, and ib linear algebra, markov chains, and partway through some others

#### Kevin Buzzard (Feb 27 2020 at 17:53):

Are you in Cambridge right now? You know they have a Lean meeting on Wednesday evenings?

#### Kevin Buzzard (Feb 27 2020 at 17:54):

If you want to help make the group theory game, the current state of it is here

#### Ethan Horsfall (Feb 27 2020 at 18:00):

I am in cambridge right now, and didn't know there was a lean meeting! i doubt i have enough experience to be much help but would be willing to try :)

#### Kevin Buzzard (Feb 27 2020 at 18:09):

Believe me, I'm sure you'll be welcome. @Edward Ayers is perhaps the person to talk to about it. Bring some friends ;-)

#### Kevin Buzzard (Feb 27 2020 at 18:09):

I'm at an Imperial meeting right now.

#### Edward Ayers (Feb 27 2020 at 18:15):

Hi @Ethan Horsfall I've added you to the secret Cambridge group. meetings are 15:00 to 18:00 on Wednesdays somewhere in the CMS room TBC. The meeting is for all skill levels, there are 3 or 4 people learning the natural numbers game. If anyone else wants to be added to the cambridge group then ask me. I think if you are a member of the group you can add new members?

#### Vaibhav Karve (Mar 02 2020 at 18:53):

Level 8 of the Advanced Proposition World says

Pro tip
Did you spot the import? What do you think it does?

I do not see any import though. What am I missing? Was it a mathlib import?

#### Kevin Buzzard (Mar 02 2020 at 18:59):

Let's look in the source code :-)

#### Kevin Buzzard (Mar 02 2020 at 19:01):

I seem to be importing finish

#### Kevin Buzzard (Mar 02 2020 at 19:01):

Does finish just finish the level in one move?

#### Kevin Buzzard (Mar 02 2020 at 19:02):

This looks like an outdated comment -- it is impossible to spot the import if you're playing the game because of the --hide

#### Kevin Buzzard (Mar 02 2020 at 19:03):

Looks like there was a commit where I hid the import, but didn't change the comment.

Cool. Thanks!

#### Simon Liesinger (Mar 09 2020 at 01:09):

@Kevin Buzzard , I noticed that the statement of pow_succ in the sidebar is wrong. it says that pow_succ (a b : mynat) : a ^ succ(b) = a ^ b * b, but I think it should be a^b*a

#### Kevin Buzzard (Mar 09 2020 at 07:23):

Yeah I know, it's on the list of things to fix. Thanks.

#### ohhaimark (Mar 09 2020 at 10:23):

How would one go writing a tactic that will select the first assumption in context that can be applyed to the goal?

and apply it

#### Anne Baanen (Mar 09 2020 at 10:26):

The spoilery way is to look at the implementation of the assumption tactic in core Lean:

meta def assumption : tactic unit :=
do { ctx ← local_context,
t   ← target,
H   ← find_same_type t ctx,
exact H }
<|> fail "assumption tactic failed"


#### Anne Baanen (Mar 09 2020 at 10:28):

Here, local_context gets the list of hypotheses, and target gives the goal type.

#### Anne Baanen (Mar 09 2020 at 10:30):

So instead of find_same_type, which finds the hypothesis with the exact same type as the goal, we could iterate over the local_context and try to apply each element in turn until it succeeds.

#### ohhaimark (Mar 09 2020 at 10:47):

Thanks. It somehow didn't occur to me to look at the definition of the basic tactics.

#### Kevin Buzzard (Mar 09 2020 at 10:47):

The best introduction we have to learning to write tactics in Lean is programming in Lean, which is a bit out of date but which does contain lots of juicy information. After that people just tend to ask in the chat.

#### Bryan Gin-ge Chen (Mar 09 2020 at 12:47):

The best introduction we have to learning to write tactics in Lean is programming in Lean,

I think the Logical Verification notes are also a good source (certainly less out of date).

#### Jasmin Blanchette (Mar 09 2020 at 13:08):

We're working on a 2nd edition. Keep an eye on the same URL, but with 2020 instead of 2019.

#### Patrick Massot (Mar 09 2020 at 16:51):

Recall we also have documentation in mathlib.

#### Scott Morrison (Mar 10 2020 at 01:45):

Do we know why sometimes we get stuck with "Lean is busy" in the natural numbers game?

#### Scott Morrison (Mar 10 2020 at 01:46):

It's happened to us again.

#### Scott Morrison (Mar 10 2020 at 02:20):

@Kevin Buzzard, I was just looking at the natural numbers game repo, and wondering about some a few things.

#### Scott Morrison (Mar 10 2020 at 02:20):

Are the src/my_solutions/ and src/solutions/ directories obsolete?

#### Scott Morrison (Mar 10 2020 at 02:21):

(The README currently suggests that if you wan to play the game in VSCode to use those directories, but they seem quite out of date relative to the src/game/ directory.)

#### Scott Morrison (Mar 10 2020 at 04:17):

It would be fun to be able to hack on this.

#### Kevin Buzzard (Mar 10 2020 at 07:18):

Yes I can quite believe that those directories are obsolete. I have no idea about any of the web issues. @Mohammad Pedramfar ?

#### Mohammad Pedramfar (Mar 12 2020 at 13:14):

Yes, the game maker only looks at the lean files specified in the game_config.toml file, which in this case are all contained in the game folder. The only other things that are needed are the files that are imported which, in this case, are contained in the mynat and tactic folder. The rest aren't needed.

#### Jiekai (Mar 26 2020 at 09:36):

Had a lot of fun with natural number game! Looking forward to more games.
The web game format works amazing. No setup hassle required at all.
Is real-number-game available on the web?

#### Kevin Buzzard (Mar 26 2020 at 11:13):

no, there is no real number game. Someone was coming to visit me in May and work on it but unfortunately this is now all up in the air. I should try and get a fan club together.

#### Jiekai (Mar 29 2020 at 03:50):

Inequality world Level 6

  cases hab,
cases hba,
rw hab_h at hba_h,
symmetry at hba_h,
have h00: (hab_w + hba_w) = 0 := eq_zero_of_add_right_eq_self _ _ hba_h,
cases hab_w,
{
rw hab_h,
refl, -- cursor here shows 'no goals'
},
{
}


#### Jiekai (Mar 29 2020 at 03:58):

Since the game does not introduces { ... }, I guess it is not an issue.

#### Kevin Buzzard (Mar 29 2020 at 09:22):

No goals is correct with the cursor there because you have finished the goal which you isolated

#### Kevin Buzzard (Mar 29 2020 at 09:23):

Oh -- but the point is that it doesn't say "proof complete" or whatever?

#### Jiekai (Mar 29 2020 at 10:09):

Yeah, guess "no goals" is okay

#### Jasmin Blanchette (Apr 03 2020 at 12:44):

Concerning the logical verification notes discussed on March 9, be aware that there's a new version now, available under "material" below:

https://lean-forward.github.io/logical-verification/2020/index.html#material


It's much better than the old book. Please tell anybody who's reading the old one to stop! ;)

#### Sara Fish (May 08 2020 at 06:20):

On "Advanced addition world" level 6, the instructions say that there is a three-line solution. I assume this intended solution is the following.

rw add_comm t a,


Using repeat, which has previously been introduced, this can also be done in two lines.

repeat {rw add_comm t},


Not sure whether this is worth briefly mentioning as an added challenge? Maybe this is trivial to point out, but I think the trick of using rw add_comm t is kind of cute here.

#### Kenny Lau (May 08 2020 at 06:46):

does it count as one line if you use ;to join the two lines?

#### Kenny Lau (May 08 2020 at 06:46):

what is the point?

Golf?

#### Kenny Lau (May 08 2020 at 07:08):

the two versions are essentially the same proof. It isn't like you simplified the proof.

#### Kevin Buzzard (May 08 2020 at 07:08):

Kenny can you beat 25 single rewrites for (a+b)^2?

#### Kenny Lau (May 08 2020 at 07:08):

what's the setting?

#### Kevin Buzzard (May 08 2020 at 07:09):

I can't remember, I just remember saying I did something in 27 and then someone telling me they could do 25

#### Kevin Buzzard (May 08 2020 at 07:09):

Maybe last level of power world?

#### Kenny Lau (May 08 2020 at 07:16):

  rw two_eq_succ_one,
rw pow_succ,
rw pow_succ,
rw pow_succ,
rw pow_one,
rw pow_one,
rw pow_one,
rw succ_mul,
rw one_mul,
rw mul_comm b a,
refl,


19 lines

#### Kenny Lau (May 08 2020 at 07:20):

of course there is also the one line rw {insert huge proof term}

#### Kevin Buzzard (May 08 2020 at 07:28):

In her paper on ring, Mahboubi claims that it takes 30 rewrites to prove the analogous result for (a+b)^3 but I asked her about it and apparently there's no concrete reference for this

#### Kevin Buzzard (May 08 2020 at 07:30):

The exact numbers probably depend on whether x^3=x(xx) or xx(x) etc

#### Shing Tak Lam (May 08 2020 at 07:32):

Kevin Buzzard said:

I can't remember, I just remember saying I did something in 27 and then someone telling me they could do 25

I think it was the last time the NNG was on r/math?

Also they did it in 18, not 25.

#### Kenny Lau (May 08 2020 at 07:33):

18 rewrites, so 19 lines

#### Kenny Lau (May 08 2020 at 07:33):

so the same as mine

#### Mario Carneiro (May 08 2020 at 07:36):

example (a b : ℤ) : (a + b) ^ 2 = a*a + 2*a*b + b*b :=


#### Kenny Lau (May 08 2020 at 07:37):

@Mario Carneiro we're using mynat

#### Kenny Lau (May 08 2020 at 07:37):

in the last level of power world

#### Mario Carneiro (May 08 2020 at 07:38):

I don't like these floating tactic scripts with no context

#### Johan Commelin (May 08 2020 at 07:38):

Isn't the topic title enough context?

#### Mario Carneiro (May 08 2020 at 07:38):

not to know what the problem is

#### Mario Carneiro (May 08 2020 at 07:39):

reading a tactic script is hard enough as it is, the type of the theorem is the main clue about what's going on

#### Mario Carneiro (May 08 2020 at 07:39):

these NNG examples are just unreadable

#### Kenny Lau (May 08 2020 at 07:39):

well if you Ctrl+A and Ctrl+C and Ctrl+V then you don't get the theorem

#### Mario Carneiro (May 08 2020 at 07:40):

I don't have the page up

#### Mario Carneiro (May 08 2020 at 07:40):

I don't know what the theorem looks like, I just guessed

#### Kenny Lau (May 08 2020 at 07:40):

https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=4&level=8

#### Mario Carneiro (May 08 2020 at 08:02):

lemma add_squared (a b : mynat) :
(a + b) ^ (2 : mynat) = a ^ (2 : mynat) + b ^ (2 : mynat) + 2 * a * b :=
begin
have : ∀ x:mynat, x ^ (2:mynat) = x * x := λ x, by rw [two_eq_succ_one, pow_succ, pow_one],
rw [this, this, this],
refl
end


#### Mario Carneiro (May 08 2020 at 08:06):

it would have been even better if I had add_four_comm : (a + b) + (c + d) = (a + c) + (b + d)

#### Mario Carneiro (May 08 2020 at 08:08):

or its less used cousin add_four_rotate_right : (a + b) + (c + d) = (a + c) + (d + b). In a real theorem prover you have all these things proven already

#### Kevin Buzzard (May 08 2020 at 09:16):

add42? Do you need add4n for 1<=n<=24?

#### Kenny Lau (May 08 2020 at 09:17):

presumably one of them is rfl

#### Alexandre Rademaker (Oct 20 2020 at 13:38):

hi @Kevin Buzzard, can we still play the game offline? I would like to have my solutions saved in my machine...

#### Kevin Buzzard (Oct 20 2020 at 16:42):

I thought that solutions were saved on your machine now? (but not transferrable between machines). You can clone the repo and edit the lean files directly, but note that they will all have solutions in.

#### Alexandre Rademaker (Oct 26 2020 at 11:28):

Hum, I don’t know how to find them. The browser is now showing all worlds as unsolved.

#### Kevin Buzzard (Oct 26 2020 at 11:47):

I'm really sorry, this is part of the set-up which I understand nothing about :-( My browser remembers my previous attempts shrug.

#### Bryan Gin-ge Chen (Oct 26 2020 at 13:51):

If I remember correctly, the save data is placed in your browser's local storage. It will get cleared if you clear your browser's cache for that site.

#### Bryan Gin-ge Chen (Oct 26 2020 at 13:53):

It woudn't be impossible to add a button that would download all the solutions as e.g. a ZIP file containing a bunch of Lean files. @Mohammad Pedramfar what do you think?

#### Julian Berman (Oct 26 2020 at 14:36):

@Alexandre Rademaker what browser are you on?

#### Julian Berman (Oct 26 2020 at 14:38):

On Firefox for me, if I go to Tools > Web Developer > Toggle Tools, and then click Storage and then Local Storage in the sidebar, I see an entry for https://wwwf.imperial.ac.uk, and if I click on it, I see what's a big blob of JSON but it has all my solutions in it. Do you see something similar?

#### Alexandre Rademaker (Oct 26 2020 at 15:51):

Safari, i will try to find the json

#### Alexandre Rademaker (Oct 26 2020 at 15:51):

But I am afraid I lost the data in the last update of the system

#### Kevin Buzzard (Oct 26 2020 at 15:53):

If you don't want to solve the levels again you can cheat by looking at the internal solutions here https://github.com/ImperialCollegeLondon/natural_number_game/tree/master/src/game

#### Mohammad Pedramfar (Oct 28 2020 at 12:16):

Bryan Gin-ge Chen said:

It woudn't be impossible to add a button that would download all the solutions as e.g. a ZIP file containing a bunch of Lean files. Mohammad Pedramfar what do you think?

It is possible to add a save and load button, so that the users can save their progress on their computer. However, saving the progress as editable lean files is slightly tricky, since the use might change some parts of the lean files that shouldn't be changed and then loading those files could be a bit problematic. I can add the option to save and load a save file that is not meant to be edited by the user though.

#### Bryan Gin-ge Chen (Oct 28 2020 at 15:06):

You could include comments telling the user to edit only within some part of the file.

#### Mohammad Pedramfar (Oct 29 2020 at 00:39):

That's possible, but for it to work, I might need to rewrite a good part of python code in javascript, the parts that handle lean files and turn in into a format that the game can use. Unless it's actually going to be used by a reasonable number of players, I'd rather not go through with it.
Especially since what the user can download will not be a single file, it will be a folder, containing several lean files and config files. Basically the repository that Kevin sent the link to.
Another point is that it's not straightforward for the player to recognize if they changed some part that they shouldn't have. Even adding a single space to the statement of a lemma can make the game treat it as a different lemma! (The reason for this behaviour is version control. If you're making the game and continuously updating it to fix typos and add/modify levels, you'd prefer the player's saves to not be reset with every single minor update. The way this game tracks problems through minor updates is by remembering the exact statement of lemmas. After a minor update, even if you rearrange levels, the saved data for an unchanged lemma will be remembered.) Of course this could be circumvented, by letting the player change the statement of the lemmas as well. But in that case, the player might as well just clone the Lean-game-maker and play the game on localhost!

#### Jon Eugster (Feb 03 2021 at 17:43):

Hi! (I've been looking at Lean 2 years ago but honestly forgot everything about it meanwhile)

I was going through the natural numbers game and encountered something weird: I thought my proof was correct seems to work and ends with "no goals.", but simultaneously it says "Invalid syntax" for an intermediate line which executes fine when going through with the cursor.

The line is the following

have q1 := eq_zero_or_eq_zero_of_mul_eq_zero a (succ c) (←h),


I suspect it's that I don't know yet how to properly plug in objects, I have h : 0 = a * succ c and I want to use

eq_zero_or_eq_zero_of_mul_eq_zero
(a b : mynat) (h : a * b = 0) :
a = 0 ∨ b = 0


to get something like q: a = 0 ∨ succ c = 0 (to get a contradiction).

I had the same problem with feeding a*c (a natural number) into a statement, so I'd really appreachiate an insight on how to do that! Thank you

This is Advanced Multiplication World Level 4, and my full code is

revert b,
induction c with c hc,

intros b h,
rw mul_zero at h,
rw mul_eq_zero_iff at h,
cases h,
exfalso, exact ha(h),
exact h,

intros b h,
cases b,
exfalso,
rw mul_zero at h,

have q1 := eq_zero_or_eq_zero_of_mul_eq_zero a (succ c) (←h),
cases q1,
exact ha(q1),
exact succ_ne_zero c q1,

repeat{rw mul_succ at h},
have q := hc b h,
apply succ_eq_succ_of_eq,
exact q,


#### Mario Carneiro (Feb 03 2021 at 17:44):

my advice is to ignore anything else lean says if it also says "invalid syntax"

#### Mario Carneiro (Feb 03 2021 at 17:45):

that means you have invalid syntax and everything else is lean trying to pick up the pieces and probably getting more confused

#### Mario Carneiro (Feb 03 2021 at 17:45):

in this case the issue is (←h), that's not an expression

#### Mario Carneiro (Feb 03 2021 at 17:45):

probably h.symm works in that position

#### Jon Eugster (Feb 03 2021 at 17:47):

It does, thank you! so \l is only used in combination with rw?

#### Jon Eugster (Feb 03 2021 at 17:50):

And regarding the other part, if I have h: a*c + a = 0 and I want to use

 add_left_eq_zero
{{a b : mynat}} (H : a + b = 0) : b = 0


to get a = 0, how do I do that?

I tried have h' := add_left_eq_zero (a*c) a h, is it the {{ that work differently than I expected?

#### Kevin Buzzard (Feb 03 2021 at 17:51):

The {{ }} brackets mean "Lean will supply these". Try have h' := add_left_eq_zero h. The point is that Lean can guess the other inputs after it sees the type of h so it doesn't want to bother the user with them.

#### Kevin Buzzard (Feb 03 2021 at 17:51):

Sorry, I don't ever explain {} brackets properly in NNG and this is a common question.

#### Jon Eugster (Feb 03 2021 at 17:54):

That makes sense, amazing!

The problem was again that I supplied either h: 0 = ... or ←h instead of h.symm.

Thank you both for the help!

#### Kevin Buzzard (Feb 03 2021 at 17:55):

Ps if you've finished with h then replace h := add_left_eq_zero h saves you from having to make a new hypothesis.

Last updated: May 08 2021 at 10:12 UTC