Natural Number Game : Feedback from a Newbie

Stream: general

[Ian Allen]

As the Game is intended to introduce new people to Lean(4?), and I am a new person here both to the community, to lean, and to the subject matter of foundational mathematics required for theorem proving, I thought I would contribute with some feedback from my perspective. I'm playing as I go and I will edit in comments in progressive order, indexed to match the game page number so numbers might be skipped.

0. What a great idea.
It looks fun and the advantages to reading a multi-hundred page manual (which I will need to do eventually anyhow) are obvious with respect to onboarding new members.

1. RFL
A) Easy enough. I am left wondering precisely what the tactic is based on. Is it the basic functionality of the = sign? What does "reflexivity" mean in this context? I feel that the RFL tooltip is somewhat lacking, and could be improved with at least a link to more specific information, perhaps pointing inside the manual or other learning resource, if not more explicitly defined in the tooltip itself.

B) In the tooltip at the bottom, it ends with, "...and who cares what the definition of addition is)." I think I care. I feel like I am supposed to care if I am here. I believe the people who created this game definitely care. I know this is a joke, but I only mostly think I get it and I find it confusing to the learning process. As much as I love a good joke, I feel it should be followed up with an explanatory comment that we will be getting to addition later (assuming this is the joke), or at least a short comment about why we don't care about what addition is.

C) When I beat the level, I get a "level completed!" line. But I don't think I get to see what LEAN will actually do; I am pretty certain it is not that. For consistency, I would suggest the game level ends the same way in the tutorial as in the main program, with the addition of the essentially "you win!" comment line to keep it thematic with a game.

2. RW
A) Linguistically, math is as much a spoken language as say English, and the two should be interchangeable within vocabulary. It seems strange to me that I use RW[h] instead of RW[y] in this context, though I imagine there is a very good reason for that, probably related to multiple functions with y as a parameter.

3. Numbers
A) I read the page, looked at the problem, and immediately typed in "1 = succ 0". I got "no goals left; This probably means you solved the level with warnings or Lean encountered a parsing error." I don't see a warning, unless you count that statement, so I must have caused a parsing error? At any rate, the game doesn't suggest to me what I should do next.

B) I managed to reset the level by going back and forward. This time I followed the instructions exactly. RW is still strange due to an incomplete understanding of the programming context. Will it always rewrite the left hand side of the formula as found in the "need to prove" line? When I tried to double check how this works, I found the tooltips for the various succ formulas no longer worked - I can click and it brings up a now empty tooltip.

4. Rewriting Backwards
A) Ah hah! The very first sentence "If h is a proof of X = Y then rw [h] will turn Xs into Ys." should be in the RW page, however, just to make it abundantly clear to anybody who doesn't immediately get the syntax.
B) I solved this one in only two lines. When do I get my bonus points?

5. Adding Zero
A) Addition rears its ugly head and we turned our tails and fled instead... No just kidding, that was a joke and a cultural reference. Ha ha ha! And now for something completely different: How does RW select the add_zero function by parameter, is it always by lowest letter case first? What if I had wanted to only rewrite the c statement, instead? Can I include a parameter pointer in the RW command?

6. Precision Rewriting
A) Just in the nick of time. I like the flow of this tutorial for the most part; from now on I will do the subsequent page before commenting on the previous. I am however getting tired of keystrokes. On the assumption that brackets always immediately follow an RW input, shouldn't that autocomplete after typing RW? Spare your users tedium; above all things, time is precious.

7. Add_Succ
A) Confusion. RW[one_eq_succ_zero] got me ...+succ... in my goal line, but RW[add_succ] does nothing despite being the clear tip from the directions. Also in this case, there is no response output from the program after user input, which breaks a game-design principle. Can I personalize LEAN so that it responds with "I'm sorry Dave, I'm afraid I can't do that." when I give it pointless inputs?

B) There seems to be some kind of update hangup causing me problems. I went back and forward and the problem resolved itself in that I can see my commands went thru and I had gotten to succ n = succ n. Here however, I tried RFL as the obvious choice, and got the infamous "no goals left possible parsing error.." message. I seem to be at an impasse.

C) Impasse resolved. While unable to see the response outputs, I had attempted an invalid command and got a pink warning message. I had however the correct goal line of succ n = succ n. The system would not accept RFL until I had gone back and resolved the warning message by "retrying" the previous successful command and thereby erasing the warning. This is not at all clear to the new user.

8. 2+2 = 4
A) Good news, everyone! I have proven that 2+2 = 4, but only for very certain, rare values of 2, and I need you all to travel to Death Planet 42 in the Galaxy of Agonizing Pain to get me some of those 2's.

B) There is a command called "nth_rewrite". For consistency and less tedium, why not call this "nth_RW"?

This game is fun. I ended up proving this with succ(succ(succ(succ 0)))) so I think the next step is to naturalize the language so I can intuitively do this in fewer steps. Lucky for me, the computer doesn't mind one way or the other. Maybe a bonus points mini-game where the game hints that you can do better (what is the inverse of succ?) until you finally unlock the mathematically proven minimal number of steps required in a proof, would be a nice learning motivator.

[Jon Eugster]

Thanks for the feedback! I'll just pick out the things that concern lean4game (and not the NNG content)

1) lean itself in the infoview just shows "no goals", I believe. So the current behaviour of showing "level completed" is likely already exactly what you suggest should happen, isnt it?

3a, 3b, 7a, 7b: These seem all to be referring to similar bugs which are already resolved, and will be there once NNG is updated to v4.6.0 at the end of the month lean4game#177, lean4game#121

6a) We found autocomplete extremely unuseful, since by default it suggests anything in Lean, also things way outside the game's scope. But for sure, if somebody worked on a better autocomplete or some drag-n-drop feature, that would be most welcome

7c) From your description, I cannot fully understand the bug, if you could write an issue at the link above with an exact reproduction (i.e. step-by-step what you entered for that level), that would be helpful.

Likewise for the NNG-content, I think it would be helpful to add your ideas as an issue at https://github.com/leanprover-community/NNG4

[Ian Allen]

Jon Eugster said:

7c) From your description, I cannot fully understand the bug, if you could write an issue at the link above with an exact reproduction (i.e. step-by-step what you entered for that level), that would be helpful.

Well, I did I believe the following:
Got to the point where I had "succ n = succ (n + 0)" but could not see this line due to update problem.
Typed in something like "RW [add_succ n 0] trying to use parameters and got an unseen "tactic rewrite failed" error.
Went back, then forward to force the update. Saw that I had that error but that underneath I was now on the goal succ n = succ n.
Was unable to use RFL until I clicked "retry" on the line above the error, clearing the error, then returning to succ n = succ n thru correct command entry, at which point RFL was accepted.

As far as the autocomplete feature, I meant only a restricted implementation that fills what i would call "syntax characters" in the programming language. So if you type in RW it would give you the brackets and only the brackets, and possibly place your cursor inside of them. Thats assuming that there are no commands that continue after starting with RW, other than arguments inside the brackets.

[Ian Allen]

Ok now I have a technical question. I am in stage 11/11 in Implication World.

"intro" gives me
Assumptions:
a: succ (succ 0) + succ (succ 0) = succ (succ (succ (succ (succ 0))))
Goal:
False

"apply zero ne succ" then gives me
Assumptions:
a: succ (succ 0) + succ (succ 0) = succ (succ (succ (succ (succ 0))))
Goal:
0 = succ ?a

I cant get it to apply further without failing, despite that clearly being a statement of zero_ne_succ needing to be false in order for the assumption to be true. I am missing something with the way the logic is handled in Lean?

[Edward van de Meent]

Goal:
0 = succ ?a

what exactly are you trying at this point?

[Ian Allen]

Im new. So not entirely sure, i assume the ? was just shorthand for "you have a long input". I went back and got my goal to be "succ 4 = succ1" which is clearly impossible, so the hypothesis must be false. I am clearly having trouble understanding exactly what the logic is for LEAN to consider a proof a proof in this case. I am used to thinking of things in a more mundane manner. At this point I feel like I am flailing and kind of going around in circles...

[Edward van de Meent]

right...
when you say "apply zero_ne_succ", that means you're telling lean: "i'm going to prove this by showing that i can prove that 0 = 1 + x for some natural number x". Lean then gives you two goals: 0 = succ (x), and x:Nat (but instead of x lean says ?a). when you later have some proof of 0=succ x for some specific x, for example h:0 = succ 3 or something, you can write exact h for the first goal, and lean then realises "oh, so you use x = 3", and then realises "ah, and 3 is of type nat too" and closes the second goal immediately.

[Edward van de Meent]

an interesting experiment in this case would be comparing the goals after for example apply zero_ne_succ 3 with the goals after apply zero_ne_succ

[Patrick Massot]

Ian said:

I am a new person here both to the community, to lean, and to the subject matter of foundational mathematics required for theorem proving

I think there is a fundamental misunderstanding that explain several things you find confusing. There is nothing like foundational mathematics required for theorem proving. This is not true in real life and also not true in Lean. Thinking about foundations of mathematics is a respectable hobby or even profession. But this has not much to do with doing mathematics.

It is true that foundations leak more often into regular math in a proof assistant than on paper. But this is a defect of proof assistants that we try to fix. Most people that formalize maths using Lean are not interested in foundations. I know at most one person who can tell you the axioms of Lean’s foundations without looking them up, and less than ten people who would understand them if they look them up.

I am however getting tired of keystrokes. On the assumption that brackets always immediately follow an RW input, shouldn't that autocomplete after typing RW? Spare your users tedium; above all things, time is precious.

This is only an introductory game. In a fully fledged editor used for actual Lean work such as vim, emacs or VSCode you can of course define short-cuts. And if you have a programmable keyboard then you can define a macro. On my keyboard typing rw [] and putting the cursor between the brackets in a combination of two keys only (holding one of the thumb keys and pressing r).

[Ian Allen]

Thanks, Patrick. I'm probably just using the wrong nomenclature. I have a background in applied mathematics ie engineering, at the most rudimentary level. You know, linear algebra, calculus, arithmetic. When I see the number system being built out of axioms, by first defining the rules of number interaction (i guess that's called an algebra?) using those same axioms, I think of that automatically as pretty foundational.

That said, I got pretty far into the tutorial without (admittedly) fully understanding exactly what I was doing. Now I am on a step where just looking for simplifications and forcing them thru an as of yet black-box interface (to me) no longer cuts the cake. So I am backtracking and trying to see exactly where I missed the more important details.

It is so aggravating that I cannot just add two numbers at this point. I have never tried to do math like this. What a fun and perfectly frustrating game so far!

And maybe I am still misunderstanding you: but I want to know how the system is built from the ground up, and that means knowing and understanding the axioms and how they are applied until I can see why I have all of these tools at my disposal when I go into the full program. Isn't that what is meant by foundational? If so, sure I can see why it's not strictly required. But I am also living proof right now that I will get further by learning it than "proceeding" blindly.

[Patrick Massot]

Ah ok. This indeed not what we call foundations here. Foundations would explain why you can use the same axiom building rules to get those natural number axioms and the definition of the existential quantifier or conjunction or disjunction for instance.

[Ian Allen]

What does "declaration uses sorry" mean? I tried to do this, the program seems restrictive on what it will take as a parameter, even tho the arguments should match: rw [add_succ (succ succ 0), succ 0] I also tried without the comma, but it tells me the tactic is never executed. I just want to reduce the amount of succ in this equation. :weary:

[Edward van de Meent]

i don't think you meant to put a comma in there...

[Edward van de Meent]

also, in what level is this?

[Ian Allen]

well i did, but only because putting the parameters into parenthesis according to groupings didnt work. so even if something is of the form succ a + b, i cant use that function if a and b are actually multi-variate terms or include functions themselves (like succ). This is the last level of implication world.

[llllvvuu]

On foundations (and you don't need any of this to play NNG; probably NNG is better to finish first):

You can take a look Prelude.lean to understand some of the foundational inductive types: https://github.com/leanprover/lean4/blob/master/src/Init/Prelude.lean

Understanding Calculus of Inductive Constructions itself is much harder. But maybe the built-in .rec is worth learning https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html . Having some Haskell or Rust experience (ADTs) helps with this.

The other foundation you will run into at some point (because one day you'll run into an error message like "__ can only eliminate into Prop") is the proof-irrelevant Prop universe: https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html

Different learning styles might make sense for different folks. Personally I forget I'm formalizing math and instead pretend I'm doing functional (meta)programming. The tactics sometimes make a bit more sense as programming operations than math operations

[Edward van de Meent]

ah, i think you're missing some brackets around the inner succ 0

[Ian Allen]

maybe i am missing something, but is there a way to unapply succ_inj?

[Edward van de Meent]

by 'unapply', you mean in the way that decreases the number of succs?

[Ian Allen]

yes. i want to de-increment the succ a notch.

[llllvvuu]

probably congr but you might not have it yet, because you probably don't need it for the level

[Edward van de Meent]

you want apply succ_inj at h

[Ian Allen]

that seems counterintuitive and i gotta say i must have tried it. i might be getting tired if i missed that after all this time..
anyhow i finally figured out how to do what you were telling me earlier. i didnt see that i could use rw to force the program to take any value using the n_eq_succ_(n-1) theorems. its really not very intuitive there.

of course, now i have the goal 0 = succ 1 which seems from the tooltip to be what i need to use zero_ne_succ. but i get an error still.

[Ian Allen]

I have now
h: succ (succ 0) + succ (succ 0) = succ (succ (succ (succ (succ 0))))
Goal:
0 = succ 1

[Edward van de Meent]

what is the error you're getting?

[Ian Allen]

something about type not matching i think. i tried to move on from that and am now working to get h rewritten into something matching what you were talking about a while ago. but i cant get succ (1 + 2) to rw backwards using rw [← succ_eq_add_one (2 + 1)] at h

i keep having simplification steps failing because it wont accept more complex parameter inputs. or i have the syntax just wrong... lol im just trying to get the damn thing to add, really.

[Edward van de Meent]

i think you are probably on the wrong path in this case. you don't need to have any 1's or 2's in your goal or hypotheses for this level...

[Ian Allen]

yeah i kind of figured that i was lost a while ago. but i cant get succ_int to work on h unless i get those first two succ terms to combine. i dont know why but it keeps throwing up a "failed to find" error.

[Edward van de Meent]

Hint

the way you get the + out of your hypothesis is by using add_succ and add_zero

[Ian Allen]

but every time i try to use add_succ it wont let me. thats the first thing i went for... :/ (thank you for the hint tho i will look at it more)

[Edward van de Meent]

have you tried rw [add_succ] at h?

[Ian Allen]

i just did. and it worked. i think i was trying to overthink things by passing the more complex parameters for it.

OMG thank you! I can finally go home and sleep (play with lean some more). I cant believe how fast and easy that went once i had the correct syntax.

[Ian Allen]

So just to be real clear what was throwing me off so bad, for feedback if people are interested:

Under the theorem add_succ (just one example) it lists parameter inputs "add_succ a b is the proof of a + succ b = succ (a + b)."

In the assumption, I see terms like succ(succ 0) + succ (succ 0), and instead of just applying the theorem "naked" as "rw [add_succ] at h", i was trying to pass it what i thought were the correct parameter groupings like (succ(succ 0)) for "a" and (succ 0) for "b", so in other words things like "rw [add_succ (succ(succ 0)) (suck 0)] at h". I had done this earlier in the tutorial with more simpler terms and it had worked.. so I assumed this was the correct way forward here. Failing at that, sent me on a long and circular path of frustration.

[Edward van de Meent]

to be clear, you probably can specify the arguments each time, it just gets very tedious to write that way, and typically Lean figures out the right arguments by itself.

for example:

Do not write like this.

if you don't want to use apply:

exact h
rw [add_succ (succ (succ 0)) (succ 0)] at h
rw [add_succ (succ (succ 0)) 0] at h
rw [add_zero (succ (succ 0))] at h
exact zero_ne_succ 0 (succ_inj 0 (succ 0) (succ_inj (succ 0) (succ (succ 0)) (succ_inj (succ (succ 0)) (succ (succ (succ 0))) (succ_inj (succ (succ (succ 0))) (succ (succ (succ (succ 0)))) h))))

If you allow apply as well rather than just exact:

exact h
rw [add_succ (succ (succ 0)) (succ 0)] at h
rw [add_succ (succ (succ 0)) 0] at h
rw [add_zero (succ (succ 0))] at h
apply zero_ne_succ 0
apply succ_inj 0 (succ 0)
apply succ_inj (succ 0) (succ (succ 0))
apply succ_inj (succ (succ 0)) (succ (succ (succ 0)))
apply succ_inj (succ (succ (succ 0))) (succ (succ (succ (succ 0))))
exact h

if you rather rework h than the goal:

exact h
rw [add_succ (succ (succ 0)) (succ 0)] at h
rw [add_succ (succ (succ 0)) 0] at h
rw [add_zero (succ (succ 0))] at h
apply zero_ne_succ 0
apply succ_inj (succ (succ (succ 0))) (succ (succ (succ (succ 0)))) at h
apply succ_inj (succ (succ 0)) (succ (succ (succ 0))) at h
apply succ_inj (succ 0) (succ (succ 0)) at h
apply succ_inj 0 (succ 0) at h
exact h

all of these examples solve the level, but they are all also tedious to write, and (as you've experienced) hard to get right.

[Ian Allen]

Im not even sure how or where I was typoing it each time. but I definitely started by trying to include things in nested parenthesis. Thanks for the detailed response.

[Ian Allen]

I worked some more on this last night and this morning, and I think one important feedback (from a new to all of this person) is the following:

The level of abstraction is very high, and while some things feel intuitive from an understanding of basic math and programming, others are very much not so -and here the tutorial can fall short dealing with them. The prime culprit for me here were the slighly more convoluted logical steps. I know what induction is for example and how it works, but the syntax and especially the logical outcome here are very hard to grasp inside of LEAN. A better tooltip that clearly explains the choice for the syntax, and how the goals are formed based on a chosen parameter from an example problem, would be extremely beneficial. I had the same problem with the succ_inj and zero_ne_succ functions, even though on the face of it the definition of these proofs are quite simple; it is the implementation and logical result thereof that is highly confusing to me as a new user. Especially when applying them to the hypothesis vs the goal. So again, a more in depth (even 2-3 pages) mini schoolbook on those would be so useful.

Another one that I think ties slightly into this, is the invisible parenthesis. The tutorial explains them, and I like to imagine with long term use I will come to innately manipulate them, but at the moment it can be extremely difficult, not just when seeing when a function can be applied, but also what the results of that application will be. Here I would suggest a simple show/hide button (or did I miss it?).

I do very much enjoy this tutorial. I think the people who built it deserve some serious kudos and I am definitely learning the system much faster than I would have without it. So thanks!

[Shreyas Srinivas]

What do you mean by invisible parenthesis of function application? There are no parenthesis at all.

[Shreyas Srinivas]

As for the other conceptual content. A substantial fraction is explained in the book "Theorem Proving in Lean 4" abbreviated often as #tpil

[Ian Allen]

There are. a + b + c is in fact (a + b) + c according to Lean, and if you hover over the "+" sign it will highlight these hidden groupings. Explained in the tutorial.

I came back to the game- having closed the window, and my progress is gone. Not such a problem, but if you select the "relaxed rules", you cant actually do any of the unlocked levels if you jump ahead, because it doesn't unlock any of the correspondingly necessary theorems, making this setting effectively redundant with "regular rules".

[Jon Eugster]

it should always unlock all required theorems/tactics to be able to solve a level. However, if you played the entire game some more tactics might be available that allow you to write a simpler proof (e.g. you might be able to use simp)

The progress should always be stored in your browser, unless you "delete all cookies and site data" it should not vanish. Maybe you can look if there is any site data in your browsers "Local Storage" and DM me about that, or about how to find this information, if you're not familiar with the browser dev tools:blush:

Again, for things that are clear bugs, it's best to write a bug report (issue) at lean4game, describing what's wrong (incl. details like which game/level, and what proof you tried) and how to reproduce:blush:

[Ian Allen]

Huh, might be something from our IT department that interferes then. Sounds like it's a me-issue.

[Eric Rodriguez]

I do think it'd be nice to have a mode where stuff can be unlocked at-will

[Ian Allen]

Yeah i didnt finish the game, and apparently my data never got stored, but when I went in a fresh game with "relaxed rules" while I could visit the new levels, I couldn't actually solve them the theorems were all greyed out. But I dont know if thats just my work computer glitching out..

[Jon Eugster]

The expected behaviour is that everything used in the sample proof (written by the game developer, aka Kevin) should be available if you click on a random level.

But the sample proof might differ from yours. Do you want to share which level that is and what your proof was?

Being able to unlock things at will sounds like a great idea!

[Ian Allen]

Hej Jon, it was all of the levels. I had gotten about halfway thru the whole thing the other day, and when I got back to my office my progress was gone. So I thought thats ok, I will just use the relaxed rules and it unlocks the levels. But all the theorems were greyed out, so the only place I could start was at level one again even tho I could hop around.

[Emilie (Shad Amethyst)]

The game progress is saved in local storage, which is supposed to stay around for a bit, but the browser is free to discard it at its will (and I'm guessing that there might be something in your local setup causing that, maybe some cookie-cleanup tool or an auto-disconnect tool). Progressive web apps are supposed to solve that issue, by allowing for more persistent storage. NNG currently also has a save download/upload option, so you can save your progress to a file once you're done and load it again the next day

[Jon Eugster]

@Emilie (Shad Amethyst) Is there anything "more persistent" one could do while still storing it locally on the users machine? Storing anything on the server is currently not an option because then you have to deal with more complicated GDPR stuff.

[Shreyas Srinivas]

A docker container that launches the game and stores progress in the local FS would help

[Shreyas Srinivas]

Alternatively, I think one can encode these games as vscode extensions

[Shreyas Srinivas]

It is a bit tedious to do this. Some custom webviews would be needed.

[Emilie (Shad Amethyst)]

PWAs aim to solve that issue, but you could also package NNG as an electron app (and then potentially run the lean REPL/server natively)

[Emilie (Shad Amethyst)]

Packaging NNG as an electron app could actually be a neat little project for someone to take on, especially if they can then get Lean to run natively for better performance

[Alexander Bentkamp]

Maybe a Chrome/Firefox extension?