Zulip Chat Archive

Stream: Lean for teaching

Topic: natural number game


Patrick Massot (Oct 12 2019 at 08:38):

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

Patrick Massot (Oct 12 2019 at 08:38):

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

Patrick Massot (Oct 12 2019 at 08:39):

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

Patrick Massot (Oct 12 2019 at 08:39):

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

Patrick Massot (Oct 12 2019 at 08:42):

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 (Oct 12 2019 at 08:42):

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

Patrick Massot (Oct 12 2019 at 08:44):

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

Patrick Massot (Oct 12 2019 at 08:44):

@Mohammad Pedramfar

Kevin Buzzard (Oct 12 2019 at 09:41):

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 (Oct 12 2019 at 09:42):

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 (Oct 12 2019 at 14:52):

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 (Oct 12 2019 at 15:42):

yeah it's live

Kevin Buzzard (Oct 12 2019 at 15:43):

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

Kevin Buzzard (Oct 12 2019 at 15:43):

I'm getting the undergraduates to debug it.

Mohammad Pedramfar (Oct 14 2019 at 01:51):

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 (Oct 14 2019 at 01:57):

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 (Oct 14 2019 at 02:05):

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 (Oct 14 2019 at 02:10):

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 (Oct 14 2019 at 02:10):

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 (Oct 14 2019 at 02:18):

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 (Oct 14 2019 at 02:23):

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 (Feb 12 2020 at 02:09):

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 (Feb 12 2020 at 02:09):

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 (Feb 12 2020 at 02:28):

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 (Feb 12 2020 at 02:37):

Perfect, thanks.

Mohammad Pedramfar (Feb 13 2020 at 00:08):

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

Alexandre Rademaker (Nov 17 2020 at 15:22):

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 (Nov 17 2020 at 15:48):

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 (Nov 17 2020 at 22:50):

Oh , this is strange! Ok, my mistake

Alex J. Best (Jan 08 2021 at 11:16):

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 (Jan 08 2021 at 11:18):

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 (Jan 08 2021 at 11:37):

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 (Jan 08 2021 at 11:54):

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 (2xy)5xy6=32x580x4y+80x3y240x2y3xy6+10xy4y5(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 (Jan 08 2021 at 13:19):

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 (Jan 08 2021 at 14:17):

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 (Jan 08 2021 at 14:18):

where is NNG4?

Frédéric Dupuis (Jan 08 2021 at 14:19):

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

Frédéric Dupuis (Jan 08 2021 at 14:21):

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

Kenny Lau (Jan 08 2021 at 14:24):

Is it online?

Frédéric Dupuis (Jan 08 2021 at 14:25):

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

Kenny Lau (Jan 08 2021 at 14:26):

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 (Jan 08 2021 at 14:28):

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 (Jan 08 2021 at 14:28):

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

Kenny Lau (Jan 08 2021 at 14:33):

oh never mind then

Kenny Lau (Jan 08 2021 at 14:33):

I mean, maybe other people might still be interested.

Kenny Lau (Jan 08 2021 at 14:33):

@Kevin Buzzard e.g.

Frédéric Dupuis (Jan 08 2021 at 14:35):

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

Kevin Buzzard (Jan 08 2021 at 15:37):

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 (Jan 08 2021 at 16:52):

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 (Jan 08 2021 at 16:59):

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

Frédéric Dupuis (Jan 08 2021 at 17:25):

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

Alex Myltsev (Jan 01 2023 at 13:26):

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 (Jan 01 2023 at 14:33):

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 (Jan 02 2023 at 13:19):

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


Last updated: Dec 20 2023 at 11:08 UTC