imperialcollegelondon / natural_number_game

Building the natural numbers in Lean 3. The original natural number game, now frozen. See README for Lean 4 information.

IMPORTANT

This is Lean 3 code so it's end-of-life. This repo is now frozen; development of the natural number game continues in Lean 4 (with more levels and a better user interface) ihere.

Natural Number Game

This is a game about the natural numbers, which are the numbers {0, 1, 2, 3, ...}. It is based on this blog post but takes things a lot further.

The idea of the game is to teach you what actually goes into the proofs of all the statements about natural numbers which are presented to us as children and which we are told are "obvious". Examples of such statements are: a + b = b + a, or a * (b + c) = a * b + a * c.

If one uses a "geometric" and informal definition of addition, such as "a + b is the number of marbles you have, if you have a marbles in one hand and b in the other", then statements like a + b = b + a do become obvious. However such a definition of addition is not appropriate for a computer. Our job in this game is to convince a computer that statements such as a + b = b + a are not just "obvious", but actually have proofs.

In this game, we start with the natural numbers and the principle of mathematical induction, and induction is the main tool that we will be using. If you are already happy with the principle of mathematical induction then hopefully you will be able to make some progress playing this game, and it might even teach you more about what the principle is.

Computers are currently being taught mathematics by mathematicians, and this game will give you some idea about how one has to think about mathematics in order to teach it to a computer. Computer scientists would like to teach difficult modern research mathematics to a computer, but this is currently extremely hard to do because computers find it very hard to read mathematics written by humans, even with recent advances in machine learning and AI. This is a big stumbling block in training computers to become brilliant mathematicians. The natural numbers game teaches you a language which computers find it much easier to understand. The language we will be using is called Lean. Lean is a piece of free and open source software developed by Leonardo de Moura at Microsoft Research.

Playing the game

Play here.

Note: in recent months Imperial College have been increasingly sloppy about keeping www.ma.imperial.ac.uk online (as I write the site has been down for three days and all I can do is file an issue, which thus far has been ignored). Thanks to Chris Birkbeck for hosting a mirror of the game here.

Authors

Lean stuff: Kevin Buzzard. Find Kevin on the Zulip Lean chat or on Twitter at @XenaProject

Computery stuff : Mohammad Pedramfar. See in particular Lean game maker.

#naturalnumbergame @XenaProject

natural_number_game's Issues

world 5 is <=.

Need to do <=.

email

Dear Kevin,

I just finished everything on natural number game. It is a fun exercise, the only serious advice (may not be correct or appropriate) I have is that add_left_eq_zero should make arguments explicit. Some other minor points: on level 2, Proposition world Gödel spelled wrong and level 10, advanced proposition, there is a missing right parenthesis.

sandbox

Should there be a sandbox?

Shorter proof of 8-8

There exists a shorter and straightforward proof of Advanced Addition level 8. It uses add_left_cancel instead of induction.

pow_succ typo

Daniela
7 hours
Small fix: the theorem list in Power World displays pow_succ (a b : mynat) :
a ^ succ(b) = a ^ b * b. I think that should be pow_succ (a b : mynat) :
a ^ succ(b) = a ^ b * a. It does behave correcly when used.

contrapositive not proved?

Andrew Helwer on Twitter:

"Also in advanced proposition world level 9 it says "we proved earlier that (P → Q) → (¬ Q → ¬ P)" but that was not in any previous lesson"

add documentation for `have`

A user needs it in 2-12 because they can't turn a+b=a into a+b=a+0.

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/rewriting.20in.20hypotheses/near/179068781

Advanced Addition World, Level 11: add_right_eq_zero

If you enter in.

induction a with d hd,
intro h,
refl,
intro h,
rw succ_add at h,
exfalso,
apply (succ_ne_zero (d+b)) at h,
exact h,

You will get "no goals".

To get "Proof Complete"

Change this line.

apply (succ_ne_zero (d+b)) at h,

To

apply (succ_ne_zero (d+b)),

I don't know if this is a bug in the lean parser, but it doesn't seem like proper behavior.

binomial theorem?

Should we do the binomial theorem?

more proposition world

10 more levels explaining tactics split, cases, left, right, use, and types <->, and, or, exists, forall

decidability

From an anonymous reader:

• I hate being confronted with constructive logic. When
  playing the natural number game, when doing the proof of
  "eq_zero_or_eq_zero_of_mul_eq_zero", I tried

  by_cases h : a = 0,

  And then that stupid system said:

  by_cases tactic failed, type of given expression is not decidable state:
  a b : mynat,
  h : a * b = 0
  ⊢ a = 0 ∨ b = 0

  At that point I wanted to throw Lean screamingly out of
  the window. What the fuck! "decidable state"? Leave
  me alone!

Don't worry reader, we can fix this :-)

Description ahead of `succ_inj'`

IMO, this could be slightly improved so that the players understand they just need to use succ_inj instead of trying to go even deeper to first principles.

basic tactics file

I just deleted tactics.md because it's now in the game. Where should this go?

mention that it works best in Chrome

although I've not had any problems with firefox

LEUNG Donald Sebastian blog comments

https://xenaproject.wordpress.com/2019/11/12/the-natural-number-game-an-update/

not_succ_le_self better solution

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/noob.20question%28s%29/near/193711182

Premature level complete status

It seems that by completing only the first goal in induction tactic the level is already marked as complete (with check mark in its header).

\l and \1

Someone on reddit complained that \1 gave them a smaller 1 and not a <- arrow. Make it clear that it's an L

our non-linear world stuff overlaps

blue dots appear on top of each other. And they can be scrolled off the screen.

playing the game on CoCalc

Needs to be written.

Ambiguous remark about "rw not applicable"

In Advanced Addition level 2 there is a remark in "sample solutions": "And remember that rw is no use to us here". This is ambiguous as it is equality, so:

apply succ_inj,
apply succ_inj,
rw h,
refl,

is a valid proof!

P.S. I think this remark was about succ_inj only but it's unclear from the text.

Check last-level descriptions

I need to signpost the user's next steps at the end of a world, I should check that these are all correct now we have nonlinear worlds.

hacker news UX comments

"
Previously: A real nice similar project using Coq: https://news.ycombinator.com/item?id=4014646

That's very polished, visually or at least typographically, which might not please everyone. But the idea of "proof by pointing" is solid.

OTOH the 'UX' of this Lean system is all over the place: being told to remove the word 'sorry' is a bizarre way to start. With my browser and reasonable font sizes, it's just not possible to make the column wide enough to get all the text on the same page. So the following paragraph refers to something that's not visible (because it's at the end of the text).

"At the bottom of the text in this box, there's a lemma, which says that if x, y and z are natural numbers then xy + z = xy + z. Locate this lemma (if you can't see the lemma and these instructions at the same time, make this box wider by dragging the sides). Let's supply the proof. Click on the word sorry and then delete it. When the system finishes being busy, you'll be able to see your goal -- the objective of this level -- in the box on the top right. [NB if your system never finishes being busy, then your computer is not running the javascript Lean which powers everything behind the scenes. Try Chrome? Try not using private browsing?]"

This paragraph is also bad because it's all jumbled up. There's advice on resizing the UI, there's a casual/vague comment on browser compatibility, and there's the random placeholder word "sorry" which appears to have no pedagogical purpose. All this as well as the fact that the lemma isn't yet visible.

From a UX, accessibility, and teaching aspect, there's a lot of room for improvement. The current state of this app really comes across as idiosyncratic rather than straightforward. The experience has got a complicated, intrusive, handmade personality rather than being a lucid exposition. Logitext has a particular personality as well but it's a slicker one. It hides the incidental complexity better (though the implementation isn't necessarily as simple as it should be).

"

worlds no longer have numbers

I need to remove numbers in descriptions of worlds

nat versus mynat issue with literal zeros

(I am a total newb so there may be wrong assumptions etc. baked into this bug report.)

I'm looking at Advanced Multiplication level 1. For some reason my browser forgot stuff when I last restarted my computer, so I haven't (in this session) actually done any earlier levels, but e.g. all the necessary tactics and theorems are present in the left sidebar.

I do

intro a0,
intro b0,
cases a with n,

so now I have to get a contradiction out of 0 ≠ 0. Obviously I can do that by introducing a new goal 0 = 0 and proving it with refl, right?

have zz : 0=0,
refl,
exfalso,

... so far so good ...

exact a0(zz)

but now I get

type mismatch at application
  a0 zz
term
  zz
has type
  @eq nat 0 0
but is expected to have type
  @eq mynat 0 0

This goes away if I explicitly say have zz : (0:mynat)=(0:mynat) but I don't think players are supposed to have to do that.

May be related to #1?

Night Mode

It'd be nice if we could have night mode for this too. Would make it a lot easier on my eyes.

"end credits"

Mario suggests adding some approximation to the contents of

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/After.20finishing.20Natural.20Number.20Game/near/189919796

to the game somewhere

it's hard to find this repository

I stumbled upon the natural number game recently. It would be great if the homepage had an explicit direct link here. I did eventually find it via the changelog link, but not after searching through https://xenaproject.wordpress.com/.

Suggesting to

• add an explicit link here (mentioning both source code and issue tracker)
• also a link in the "useful links" part of https://xenaproject.wordpress.com/?

missing tactics

exfalso needs doing in the tactic guide.
cases needs a section on natural numbers.
revert there is a intro h that should be an intro h [fixed]

world 3

Need to turn level 9 into levels 9, 10, 11, 12

comments for experts?

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Natural.20Numbers.20Game/near/190606866

Explain somewhere how this is a modded version of Lean (e.g. cover how I'm covering up notation issues etc)

Joseph Myers comments on v1.09b on my blog

deal with them at some point soon

typo

In world 2-6: the last sentence ('This will take you to world 3, multiplication world. You won't need to know any new') seems to have been cut off.

(I thought I spotted some other little typos on my playthrough but can't find any now... will update this list if I find any!)

Save progress

Having restarted my computer I lost all progress. I was hoping there would be some kind of a cookie mechanism at least. Restarting from scratch would be rather daunting.

Am I missing something or would be a good idea to add a mechanism to save progress to play over sessions?

inconsistent letters between the text description and the formal theorem statement in Advanced Addition world level 6

a b c is used in the text description while t a b is used in the formal theorem statement.

advanced addition/multn/inequality world

Once we get the ten extra levels of prop world in, we can finally move to advanced addition world! And multn and inequality world.

function world level 2

it's a definition not a lemma.

Level 5.1 seems to have broken markup

Level 5.1 seems to have broken markup on my browser. The font is monospaced and HTML tags are visible.

(BTW, nice game!)

old notes

Found these comments whilst tidying up. Probably no longer relevant:

---

Note:

• The theorem one_eq_succ_zero : 1 = succ 0
  • The theorem ne_iff_implies_false : a ≠ b ↔ (a = b) → false

those are currently undocumented. As is symmetry, rw \l.

Advanced muit world level 4 revert

This whole "revert" thing needs to be explained much better in world 9 level 4 -- it trips up a lot of people.

25 rewrites not 27 for (a+b)^2

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/function.20with.20random.20definition/near/179723073

"unknown identifier 'not_iff_imp_false'" error in Advanced Proposition Level 9

As per the title. In Advanced Proposition world, Level 9, enter the following:

intro h,  
intro p,  
rw not_iff_imp_false at h,  

Instead of obtaining:

P Q : Prop,
h : (Q → false) → ¬P
p : P
⊢ Q

the console throws this error:

58:0: error:
unknown identifier 'not_iff_imp_false'
state:
P Q : Prop,
h : ¬Q → ¬P,
p : P
⊢ Q

Naturally, using repeat {rw not_iff_imp_false at h}, for the last line, as the example in the text says, simply gives the same state (but no error).

This error does not occur in Advanced Proposition world, Level 10.

Lean server fails to initialize correctly in Safari 13.0.3 on macOS Catalina 10.15.1

When attempting to play the Natural Number Game in Safari 13.0.3 on macOS Catalina 10.15.1, the top-right window keeps displaying "Lean is busy ..." indefinitely (i.e. after a substantial period of time, e.g. 15 seconds):

Performing "Inspect Element" on the webpage reveals that the Lean server is not correctly initialized - even though the console message states that the Lean server is initialized:

... the error messages reveal that a number of Promise-related errors/exceptions are thrown:

possibly missing levels

lemma le_mul (a b c d : mynat) : a ≤ b → c ≤ d → a * c ≤ b * d :=

lemma pow_le (m n a : mynat) : m ≤ n → m ^ a ≤ n ^ a :=

@[elab_as_eliminator]
theorem strong_induction (P : mynat → Prop)
(IH : ∀ m : mynat, (∀ d : mynat, d < m → P d) → P m) :
∀ n, P n :=

Do we have them? Shall we add them? Note that the induction needs < .

Proofs are in file world_experiments/world10/levels.lean.txt, deleted in commit 3cc0f0d

3-11 issue

3-11 needs to be explained better.

Lean can get stuck an infinite loop

I accidentally got the interpreter on the website stuck in an infinite loop by writing repeat { rw add_comm },. It seems like once this happens, the only recourse is refreshing the page, which loses all progress.

world 3 reordering

Level 13 should be much earlier (mul_right_comm)

symmetry' at

symmetry at h should work. So we need the symmetry' command from mathlib and we need to hack it into a symmetry command in the natural number game.

some tactics need modifying

induction leaks. We want to always see 0 and never see zero or mynat.zero, but sometimes they escape into the context after the induction tactic is applied.

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/notational.20leakage/near/169698952

is Chris Hughes' suggested fix. cases will have the same problem.

rw closes goals which become X = X. Is this good?

world 4

power world. Thank Sian.