Natural Number Game: Level 4 / 9 : the simplest approach

Stream: new members

[Steven Clontz]

:wave: I'm playing through the natural number game for Lean 4, and I'm stuck on https://adam.math.hhu.de/#/g/hhu-adam/NNG4/world/Algorithm/level/4 - the first step is to create a new tactic, but when I do what I'm told and copy-paste the macro line to create a new tactic simp_add, I'm getting the error "no goals left This probably means you solved the level with warnings or Lean encountered a parsing error."

[Ruben Van de Velde]

Same here. CC @Kevin Buzzard

[Mauricio Collares]

I don't think you're supposed to "try it" by pasting the macro definition. Typing simp_add works to use the macro.

[Mauricio Collares]

I agree the explanation is ambiguous, though.

[Kevin Buzzard]

Oh thanks for this! Yeah that code is already in Lean, so you can just type simp_add to solve that goal! Thanks a lot for this feedback, I will try and make it much clearer.

[Steven Clontz]

Great, thanks. I'm also having trouble with defining the prec function on the next level, but maybe it's already defined there as well? I'm afk but will try again later.

[Steven Clontz]

Really enjoyed puzzling through this so far. I remember playing the old version and getting hung up at Proposition world (?), but that seems to be omitted from this version

[Steven Clontz]

Steven Clontz said:

Great, thanks. I'm also having trouble with defining the prec function on the next level, but maybe it's already defined there as well? I'm afk but will try again later.

Yep - I read the instructions as "you need to define these things , not, "we defined these things for you".

[Steven Clontz]

Has there been a pedagogical discussion of the voicing of "you/we/me" in the NNG? I don't want to retread old ground, but my hot take having just beat the game (less FLT) is that more use of "you" when the player is directed to do something, and "I" when something has been done for the player (e.g. defining simp_add) might add clarity throughout (albiet it only bit me in this last world for whatever reason).

Also if it's not clear I had a lot of fun doing this and would happily take the learning opportunity to pick up more Lean by playtesting/codesigning future worlds, if there's interest.

[Kevin Buzzard]

There has been no pedagogical discussion of anything in NNG4, I just threw some stuff together over the last two months. We have waiting on my hard drive: advanced multiplication world (almost readty to go), even/odd world, divisibility world, prime number world and a world full of unsolved problems (where I'll move FLT to).

[Jon Eugster]

Thanks @Steven Clontz for the PR NNG4#43 to change the wording of that level! I believe I'm also speaking for @Kevin Buzzard that if you felt inclined to improve any other wording throughout the game, like your suggestion to use "you & I" consistently, that would always be very welcome!

(There might also be lots of places in proofs where you'd like some hint but the hint doesn't exist yet)

[Kevin Buzzard]

NNG3 was extensively tested by undergraduates but that testing never happened for NNG4 so I would be very happy to have feedback from users :-)