Zulip Chat Archive

Stream: new members

Topic: Natural number game


view this post on Zulip Rei (Apr 02 2021 at 04:11):

Hi :) I just finished the natural number game, it was really fun! The levels are well designed and explanations are sufficient to understand the material but not spoil the solutions.

A few questions

  • I noticed in Proposition World, many of the levels are very similar to Function world. I assume this is to instill the "moral" that propositions and functions can be thought of as similar? Level 7 proposition world still says "Function world" though, and there are few more typos. Should I submit a PR for these, or is this intended?
  • I'm not much of a mathematician but I can probably help out on the more programming aspects, are the issues in https://github.com/ImperialCollegeLondon/natural_number_game/issues good to start with if I wanted to help out?
  • I'm a little fuzzy on the concept of "fixed" variables (as introduced in Adv Mult 4/4). If there's a declaration a: mynat, does that mean a is fixed in this context? If I'm doing an induction (for example) on b in a+b>a and my inductive hypothesis ends up being a+k>a, are both a and k the same "kinds" of variables in this context? Fixed? It seems a bit weird because I should be able to substitute anything I want for a in the inductive hypothesis and still have the proof be correct, but of course I cannot substitute succ k for k. Are there other kinds of variables? For example, in \exists z.z \geq 0, is z thought of as "fixed"?

view this post on Zulip Johan Commelin (Apr 02 2021 at 04:39):

cc @Kevin Buzzard

view this post on Zulip Kevin Buzzard (Apr 02 2021 at 09:31):

Oh yeah proposition world and function world are a kind of joke way of teaching mathematicians about the Curry Howard correspondence. I did it like that because at the time I was convinced that mathematicians would better understand intro and apply in the context of functions and I thought that this was quite an amusing way to teach it. Since then I've discovered that mathematicians are just fine with the whole intro apply thing applied directly to propositions and proofs (see for example workshop 1 of my recent course where I just dive straight in) so if I were to write the game again then probably function world would not be in there. I would happily look at PRs, maybe it's about time I added less than world

view this post on Zulip Kalle Kytölä (Apr 02 2021 at 10:28):

As a mathematician with no logic background, I can confirm that Kevin's joke landed, and "amusing" is an understatement.

I was wondering, however, if it is worth avoiding explicit spoilers about that. At least I personally really appreciated sitting back and enjoying the NNG show.

view this post on Zulip n Simplex Pachinko (Apr 02 2021 at 15:23):

In Power World, I noticed that the first two (at least) can be solved using only "refl,". I don't think that should be a valid strategy for either, as they are not literally equal.

view this post on Zulip Kevin Buzzard (Apr 02 2021 at 18:07):

They are definitionally equal though, and that's what refl tests for, and I can't change the behaviour of lean there. I guess I could make a bunch of stuff irreducible, but in practice the one big change to lean I did make (disabling refl after rw) has caused some confusion when people come from NNG to proper lean so I'm reluctant to make any more changes such as breaking refl


Last updated: May 14 2021 at 22:15 UTC