Zulip Chat Archive

Stream: new members

Topic: Real number game

Christian Kolker (Jun 02 2022 at 18:01):

Is there any way to gain the real number game? Perhaps a video tutorial that someone can link me to gain an instance to the Real number game?

Alex J. Best (Jun 02 2022 at 18:04):

You should be able to install the project https://github.com/ImperialCollegeLondon/real-number-game like any other lean prooject (such as tutorials) using leanproject get https://github.com/ImperialCollegeLondon/real-number-game and then play it locally

Kevin Buzzard (Jun 02 2022 at 21:49):

I'm not sure that game ever got past the "vague plan" stage.

Last updated: Dec 20 2023 at 11:08 UTC