world 5 is <=. about natural_number_game

[kbuzzard]

They used to be there in the slightly chaotic

http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game_v1.0/

but I removed them because people were saying that they couldn't solve them and it was frustrating. That version makes no mention of intro, apply or cases. In the beta I have documented intro and apply and I will do cases later on this week, and hopefully by the weekend we will have the harder levels back.

[kbuzzard]

Done first 6 levels for v1.0. Can add more for v1.1

[alreadydone]

Currently http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ "version 0.16" only has four worlds. http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game_beta/ "version 1.08beta" has six worlds but none is about inequalities.
Strangely, people on https://xenaproject.wordpress.com/2019/10/24/chalkdust-and-the-natural-number-game/ mentioned World 5 with inequalities.

[alreadydone]

Thanks! I finished them all. 3.12 (mul_left_cancel) was the hardest: combining trichotomy of the order (with isn't available) with distributivity (add_mul) and mul_pos seems the most natural, but I finally solved it by generalizing over b (revert b) and induction on c. Looking forward to more inequality problems.

[kbuzzard]

If you're prepared to install Lean and mathlib locally you can just play them now at https://github.com/ImperialCollegeLondon/natural_number_game/blob/master/levels/world3_le.lean Kevin

…

On Thu, 7 Nov 2019 at 05:39, Junyan Xu ***@***.***> wrote: Thanks! I finished them all. 3.12 (mul_left_cancel) was the hardest: combining trichotomy of the order (with isn't available) with distributivity (add_mul) and mul_pos seems the most natural, but I finally solved it by generalizing over b (revert b) and induction on c. Looking forward to more inequality problems. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#6?email_source=notifications&email_token=AHTEHMYECONSDJJXQG2LYNTQSOSZTA5CNFSM4JCUDEK2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEDKMFWQ#issuecomment-550814426>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AHTEHM4RFOKQB2WM3MRM3VDQSOSZTANCNFSM4JCUDEKQ> .

[alreadydone]

Thanks! I installed Lean with VSCode a while ago and was able to make this repo work after including lean library, mathlib, and src directory in this repo in the environment variable LEAN_PATH. I just pushed my solutions to alreadydone@1a39e69