lean4 Natural Number Game

Stream: lean4

[Jürgen Uhl]

I'm doing the lean4 Natural Number Game. In the Implication World, level 9 in the final step, it says "You have not unlocked the lemma/definition 'MyNat.zero_ne_succ' yet!", but I suppose the lemma should be given as Peano as I see no level where it could be proved beforehand. Is this a known bug?

[Kevin Buzzard]

No it's not, it's a new bug. I will not have time to look at this before the weekend but this weekend I will be adding new worlds to the game so I will also try and fix this. Thanks for reporting.

[Jürgen Uhl]

Thanks for letting me know!

[Jon Eugster]

I fixed this today, and the new version is already live. Looks like I've been sloppy with another fix I made yesterday, sorry. (thx for the PR!)

[Jürgen Uhl]

Great, thanks! I have a question of which I'm not sure whether it's related to the NumberGame or lean4 in general: in the ImplicationWorld one uses, for example, "apply h2 at h1", applying something to a hypothesis. I don't get this to work in my own example in VSCode, where it shows a syntax error at the "at" (and tries to resolve the rhs of my implication axiom with the goal rather than the lhs with the hypothesis). After DuckDuckGoing for several hours now, I could not find a general method for applying rules to hypotheses in tactics mode. Any suggestion where I could look or what I'm doing wrong?

[Yaël Dillies]

apply at is a tactic that was added to NNG but hasn't made it to mathlib yet. cc @Kevin Buzzard :wink:

[Yaël Dillies]

apply h₂ at h₁ is (roughly) the same as replace h₁ := h₂ h₁ though.

[Jürgen Uhl]

OK, thanks for the quick help! I'll try that. First steps are pretty hard...

[Kevin Buzzard]

I have no idea why our community did not implement apply at in lean years ago. I've been using it time and time again in NNG and I love it. If you have a GitHub account then please give the mathlib issue a thumbs up :-) I am well aware that having a difference between NNG lean and real lean is confusing and I am very clear about the best way to fix this :-) It's #7527

[Jürgen Uhl]

I have an account and will do that. Last Q for today: Since my "h2" is an axiom, how do I get that into my hypotheses before doing the replace?

[Mario Carneiro]

you don't need to

[Mario Carneiro]

you just refer to it by name

[Utensil Song]

It's also brought up here. It would be great to have more forward-reasoning tactics.

[Mario Carneiro]

only h1 needs to be a hypothesis in that example, h2 can also be something like And.left or some other implication theorem

[Jürgen Uhl]

Ah, I see. Thx

[Kevin Buzzard]

You are one of the first people to be playing NNG4 and I'm very happy to hear any other feedback you have. When it's at feature parity with NNG3 the plan is to deprecate NNG3 and start promoting NNG4 on eg social media (I already have ideas for a "how to make a lean game" video) but until then I'm very grateful for any beta testing.

[Jürgen Uhl]

Well, after doing the the current version of NNG4 (up to the implication world), what helped me with my own little exercise, was the Cheatsheet and learning about convert_to, so it would of course be great to have these items in an interactive learning tool like NNG4 ( I just started at looking at lean, so I didn't do NNG3 and don't know what's in there...). Besides that, NNG4 so far was really of great help for me, even after reading the docs pretty extensively!

[Kevin Buzzard]

In NNG4 there is tension between "learn as many tactics as possible so you become better at lean" and "learn as few tactics as possible so the game doesn't become confusing". In particular I encourage people towards power world and claim the "final boss" is there precisely because I discovered (to my shock!) that you could prove $(x+y)^2=x^2+2xy+y^2$ knowing only three tactics (induction, rw, rfl).

[Mario Carneiro]

maybe you need "tactic world" :)

[Kevin Buzzard]

Oh that's an interesting idea! There are some worlds in the pipeline introducing simp, have etc but I could just have an optional world which is a showcase of many tactics (one per level).

[Jon Eugster]

Mario Carneiro said:

maybe you need "tactic world" :)

Or make it a second game which assumes you know the content of the NNG. That way NNG keeps a very slick inventory with less than 10 tactics all in all.

[Patrick Massot]

I think it's better not too change the scope of NNG too much since people liked the previous version so much.

[Kevin Buzzard]

In fact I've noticed this in other games -- they have the problem that they might need to assume the user knows 0 tactics, so the problem of the game writer is to (a) teach some tactics and (b) also teach the maths thing which they want to teach. One could really imagine making "the tactic game"! It just assumes you know some basic maths, imports all of mathlib, and then each world takes some group of tactics and showcases their usage via some simple levels.

[Kevin Buzzard]

And here of course you really don't start changing the rules to make it easier for the user, you teach exactly the Lean/mathlib tactics as they are so that people can transfer their skills directly to lean/mathlib after playing.

[Evgenia Karunus]

I have no idea why our community did not implement apply at in lean years ago.

Oh didn't know about this tactic in NNG3/4, I think it's the absence of precisely this tactic that was confusing to me re:forward-proofs VS backwards-proofs when I was starting to write proofs. Being able to apply the "theorem puzzle piece" to the goal & not being able to apply the exact same "theorem puzzle piece" to hypotheses felt asymmetric/confusing.

[Jeff Wu]

this was so fun! but i want to play more.. "Congratulations! You've finished Algorithm World. These algorithms will be helpful for you in Even-Odd World." :cry: i guess it's not actually implemented?

[Kevin Buzzard]

Not on your computer, no :-) I have a big NNG backlog because I've been distracted by a Diophantine equation. Will try to get to it!

[Jeff Wu]

i'd be interested in help dev for fun in my spare time (though i don't have much spare time and i'm completely new to proof assistants.. so probably a terrible candidate). at any rate, i'm interested in getting it set up locally maybe just so i can play it :)

[Ruben Van de Velde]

Code is here: https://github.com/leanprover-community/NNG4

[Jon Eugster]

And the docs on how to use it locally are here: https://github.com/leanprover-community/lean4game#creating-a-game

You'll probably have more fun creating your own game building on things in the NNG.

And dont hesitate to ask me if you get stuck on any bugs, its all not completely stable yet :)

[Kevin Buzzard]

The experimental even/odd levels are here https://github.com/leanprover-community/NNG4/blob/cdbce04722a5e9af1e139c7faa2be50e9177a39a/Game/Levels/EvenOdd/even.lean but they need some work to make them less painful.

[Terence Tao]

I wonder if it is worth implementing "certificates of achievement" for completing (or partially completing) the game (possibly with some statistics). Ideally displaying an optional user name that one can select before playing the game. This could open up the possibility of using levels in this game (or similar game) as some sort of extra credit homework or something.

[Jon Eugster]

One comment on using the games as credit homeworks, etc.: All the user data is stored in the user's browser and nothing on the server. This means besides modifying it directly in your browser dev-tools, you can also download your progress as JSON, modify it arbitrarily and upload it again (which uploads it to your browser's local storage, not the server). For example, you could just set "completed" as true for each level and after uploading it will show you that you've completed everything, even though you didn't do any proofs.

And there is no intend to move any of this to the server, as then you need to think about GDPR. Nevertheless, it would totally be possible to implement nicer achievements/statistics on the client's side!

[Patrick Massot]

The big thing that will need to be done at some point will be integration with learning platforms such as moodle and canvas. This is totally doable but a non-trivial amount of not fun engineering work.