natural number game

Stream: Lean for teaching

[Patrick Massot]

I think https://github.com/ImperialCollegeLondon/M40001_lean deserves its own thread.

[Patrick Massot]

I just played the first two levels. Some remarks about design:
pasted image

[Patrick Massot]

What is this huge white gap at the bottom of my proof? It's constantly there, and feels weird.

[Patrick Massot]

The tick mark left of "Lemma" feels weird before the lemma is proven.

[Patrick Massot]

You really need some postprocessing of the state window. The most important is that displaying information on refl is very distracting. The line numbers refer to nothing meaningful to the player. Syntax highlighting is missing. The upper right switch is irrelevant.

[Patrick Massot]

When proving, the red squiggle under the last character which simply indicates the proof is not finished is very confusing.

[Patrick Massot]

When navigating from page to page, the browser remembers the proofs, but still displays "Click to prove", hiding the proof.

[Patrick Massot]

@Mohammad Pedramfar

[Kevin Buzzard]

Mohammad -- the undergraduates also have some feedback about this game. I have some notes in my office -- we should maybe meet on Monday. It's just about playable but we should make some minor changes before I start banging on about it on Twitter. In my mind one big question is whether we should make it all very beautiful -- but this is something that I am incapable of doing and which might take forever. Another big question is how this compares to the approach which @Bryan Gin-ge Chen was taking using Observable. I know that Patrick feels like proving things about natural numbers is hellishly boring, but it's actually what we're teaching the undergraduates at Imperial right now so I thought it was worth pushing on with this.

[Kevin Buzzard]

I have a bunch of levels which aren't pushed. By the way, Mohammad's code which made the website from the Lean code is here https://github.com/mpedramfar/Lean-game-maker and the Lean code which we used is here https://github.com/mpedramfar/natural_number_game although I made some local modifications which I didn't push because I got confused about if I could fork his fork of my project :-)

[Bryan Gin-ge Chen]

Is there a link to a "live" version of the site that I'm missing or do we have to install it locally to try it out? I did actually experiment a bit with implementing some of the "natural number game" in Observable back when you first mentioned it but I didn't get much further than parsing some edited version of the comments into markdown (see here, but there's really not much).

[Kevin Buzzard]

yeah it's live

[Kevin Buzzard]

http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/

[Kevin Buzzard]

I'm getting the undergraduates to debug it.

[Mohammad Pedramfar]

I just played the first two levels. Some remarks about design:
pasted image

Thanks, these are good points. Most of them are easy to implement and I'll get to them soon. This is the first version.

[Mohammad Pedramfar]

Mohammad -- the undergraduates also have some feedback about this game. I have some notes in my office -- we should maybe meet on Monday. It's just about playable but we should make some minor changes before I start banging on about it on Twitter. In my mind one big question is whether we should make it all very beautiful -- but this is something that I am incapable of doing and which might take forever. Another big question is how this compares to the approach which Bryan Gin-ge Chen was taking using Observable. I know that Patrick feels like proving things about natural numbers is hellishly boring, but it's actually what we're teaching the undergraduates at Imperial right now so I thought it was worth pushing on with this.

Yeah, sure. Monday's fine. I'm not an expert on Observable so I'm not sure, but it seems to me that it's ideal for when you want people to be able to play around with "everything" in the page, including the javascript. If I understand it correctly, whether it's a website or observable, the codes to make it more beautiful and shiny must be written and are almost the same codes, but Observable might limit how much we will be able to control the design. I'm not sure though.

[Bryan Gin-ge Chen]

There are indeed some style limitations for Observable notebooks hosted on the observablehq site. However, it's possible to host notebooks on your own without those restrictions. There's probably not a big advantage to redoing all your work in a notebook if you've already gotten things to work well with the lean-web-editor project though.

[Mohammad Pedramfar]

I have a bunch of levels which aren't pushed. By the way, Mohammad's code which made the website from the Lean code is here https://github.com/mpedramfar/Lean-game-maker and the Lean code which we used is here https://github.com/mpedramfar/natural_number_game although I made some local modifications which I didn't push because I got confused about if I could fork his fork of my project :-)

I forgot that I had access to the repository. I updated it, which didn't modify any files, just added the "game" folder.

[Mohammad Pedramfar]

There are indeed some style limitations for Observable notebooks hosted on the observablehq site. However, it's possible to host notebooks on your own without those restrictions. There's probably not a big advantage to redoing all your work in a notebook if you've already gotten things to work well with the lean-web-editor project though.

Makes sense.
Is it really easier to work with it ?

[Bryan Gin-ge Chen]

Is it really easier to work with it?

I can't really give an unbiased answer to this. I did try to make it easier to do some things, like embed a bunch of different Lean editors into a document and pass data between Lean and JavaScript...

[Mohammad Pedramfar]

Yeah, that embedding was good. It definitely makes it easy to make some kinds of interactive pages, in a way that you can play with it.

[Chris B]

Hi, I'm interested in doing a foreign language translation of the natural numbers game. Javascript is out of my comfort zone so this might be a stupid question, but if I build a game and it works locally when accessed through the run_locally.sh script, can I just take out the html directory and serve people the index.html or are there other items from the repo that need to be on the server?

[Chris B]

Also I guess this is a question for Prof. Buzzard, but are there any resources being used that require an API key or anything like that?

[Bryan Gin-ge Chen]

I think the answers are "yes, you only need the html directory" and "no, there are no such resources", respectively, but the right person to tag would probably be @Mohammad Pedramfar .

[Chris B]

Perfect, thanks.

[Mohammad Pedramfar]

Yes, everything you would need to run the server is in the html directory.

[Alexandre Rademaker]

Hi @Kevin Buzzard , in Level 6/17 of inequality world, have h0 := eq_zero_of_add_right_eq_self he at some point works, but using ave h0, from eq_zero_of_add_right_eq_self he didn't work! This is strange because the have P, from ... works in some situations but the tactic is documented in the game only with the have P := ... syntax.

Sorry if this is already reported.

[Kevin Buzzard]

have he : a + b = a,
  sorry,
have h0 := eq_zero_of_add_right_eq_self he,
have h1, from eq_zero_of_add_right_eq_self he,
sorry,

works for me, and the local context just before the final sorry is

a b : mynat,
hab : a ≤ b,
hba : b ≤ a,
he : a + b = a,
h0 h1 : b = 0
⊢ a = b

[Alexandre Rademaker]

Oh , this is strange! Ok, my mistake

[Alex J. Best]

I was just thinking some more about what @Patrick Massot said during the panel, about students "spamming" their solutions into lean (trying every possible tactic without really thinking what they expect to work ahead of time).
Lean and the natural number game are very good at providing positive reinforcement of what works ("Goals accomplished :tada: ") but have no real negatives to trying 100 things without thinking (typing is easier than thinking hard after all, I'm definitely guilty of getting lost in a lean proof and just spamming tactics without taking a step back).
I'd be very interested in seeing the impact on student experiences if there was some sort of feedback for doing this, I'm thinking something like at each new world you start with 100 points in the top right, each time you enter a new tactic line and the line fails you get your points reduced by 90% of your total, and a cumulative total is kept summing the totals for all levels completed or something, nothing as harsh as actually losing lives and dying and being reset to a new level in a video game, but some extra stat people will want to keep up.
Of course this might discourage genuine experimentation with different proof strategies (which is of course a good thing), so I really have no idea if its actually a useful addition so it would be very cool to see some actual A/B testing type data on this (as always).

[Alex J. Best]

Maybe this could be a "hard mode" option on the nng people opt into or something? @Kevin Buzzard you don't get any data from the nng do you?

[Kevin Buzzard]

I don't, and I don't know how to, and Mohammad now works for Uber. I've read that penalising people for wrong moves makes your game less popular though ;-)

[Riccardo Brasca]

Can you really go that far in the natural number game just trying random tactics? In my opinion it is not that students realize that for easy stuff they can basically go in "autopilot mode". It is the same for a more experienced mathematician when he has to prove that $(2x-y)^5-xy^6= 32 x^5 - 80 x^4 y + 80 x^3 y^2 - 40 x^2 y^3 - x y^6 + 10 x y^4 - y^5$: we don't think, we just start doing the computation, and we know that this will work. Knowing that sometimes there is no need of thinking is a good skill... of course this is not interesting mathematics, but that will come a little later, with more difficult exercises.

[Patrick Massot]

I lacked time yesterday but indeed one of the first thing I tell students in this course is I want them to be able to stop thinking when no thinking is required. When a goal starts with "forall epsilon : ..." I don't want them to think before writing: "Let epsilon be ...". But somehow this works too well in Lean and they have trouble transferring that skill to paper.

[Frédéric Dupuis]

I actually tried to play the NNG in Lean 4 a few days ago, and I was surprised to find out that it really is possible to solve most of these on "autopilot", i.e. just try induction with rfl in the base case without even thinking about it, or just keep adding the first lemma that come to mind in an rw call, etc.

[Kenny Lau]

where is NNG4?

[Frédéric Dupuis]

Part of that game (the hardest part in fact!) is to translate the definitions of mynat into Lean 4 :-)

[Frédéric Dupuis]

One benefit of playing in Lean 4 is that you can add the line notation "ℕ" => mynat and not mess up anything.

[Kenny Lau]

Is it online?

[Frédéric Dupuis]

I could put what I have online if there is interest.

[Kenny Lau]

So by you trying to play the NNG in Lean 4 what you meant is that you ported NNG to Lean 4 yourself?

[Frédéric Dupuis]

It depends what you mean by "ported the NNG": I ported the basic setup (definition of mynat, instances to make it usable with numeric literals, etc), but I haven't written custom tactics or anything to make it as beginner-friendly as the original.

[Frédéric Dupuis]

I found it pretty playable with the tactics currently in Lean 4.

[Kenny Lau]

oh never mind then

[Kenny Lau]

I mean, maybe other people might still be interested.

[Kenny Lau]

@Kevin Buzzard e.g.

[Frédéric Dupuis]

Yeah, there's really not much to it, I just wanted to try out Lean 4.

[Kevin Buzzard]

It's on my infinitely long job list to have a go at NNG in Lean 4, I'm sure it will teach me a lot. But I wasn't considering a full port to e.g. a browser game seriously -- it is not clear to me that the gain will be worth the pain.

[Frédéric Dupuis]

I encountered far fewer obstacles than I thought, actually. The biggest issue was figuring out what happened to has_zero and has_one.

[Bryan Gin-ge Chen]

@Frédéric Dupuis I'd be curious in seeing your code if you don't mind putting it online!

[Frédéric Dupuis]

https://github.com/dupuisf/lean4-experimentation/blob/master/src/nng.lean

[Alex Myltsev]

at https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=7&level=10

there is the tactic by_cases p : P; by_cases q : Q, with the semicolon. if I omit the semicolon, then I would have 3 goals instead of 4, and I can prove all 3 (i.e. no unreachable goals). that seems for me that, say, if I seeded the bug (using colon instead of semicolon), then the fourth case just slipped from the proving. still, the proof is valid from Lean perspective. does it mean that a proof itself might have a bug in tactics?

[Eric Wieser]

by_cases p : P; by_cases q : Q,
sorry,
sorry,
sorry,
sorry

Is the same as

by_cases p : P,
by_cases q : Q,
sorry,
sorry,
by_cases q : Q,
sorry,
sorry

Does that answer your question?

[Kevin Buzzard]

The answer to your question "does this mean that lean has a bug" is "no"