# Zulip Chat Archive

## Stream: general

### Topic: Interactive Learning Materials

#### Icaro Costa (Jan 21 2023 at 19:29):

Are there other interactive Lean courses like the Natural Number Game?

#### Trebor Huang (Jan 22 2023 at 08:00):

The tutorials are all interactive, do you mean "courses that do not require installing Lean"?

#### Bulhwi Cha (Jan 22 2023 at 08:36):

**Lean games**

**Xena project**

- The Real Number Game: the rudiments of real analysis.
- The Complex Number Game: incomplete.
- The Group Theory Game: this game goes as far as a proof of Sylow's first theorem.

**Games made by others**

- The Topology Game: topology.
- The Euclid Game: the basics of axiomatic geometry.
- MIU game in Lean: this game is an introduction to formal deduction; it is based on the MIU formal system introduced by Douglas Hofstadter.

#### Martin Dvořák (Jan 22 2023 at 11:09):

Apart from NNG, The Euclid Game, and MIU Game, are any others deployed on the internet?

#### Bulhwi Cha (Jan 22 2023 at 11:15):

You can play the Topology game here: https://mmasdeu.github.io/topologygame.

#### Shreyas Srinivas (Jan 22 2023 at 14:14):

How does one start the set theory section of the topology tutorial?. If I click on the functions bubble, I apparently skip over the set theory world. I click on the blue Set theory level and I am stuck on the home page

#### Bulhwi Cha (Jan 22 2023 at 14:35):

It works fine for me.

#### Patrick Stevens (Jan 22 2023 at 14:50):

To be clear, https://mmasdeu.github.io/topologygame/?world=1&level=1 does not show you the "Set theory" level?

#### Shreyas Srinivas (Jan 22 2023 at 14:56):

I get the set theory levels with that link. It's just that from the home page, clicking on the set theory bubble seems to keep me in the home page

#### Shreyas Srinivas (Jan 22 2023 at 14:57):

there doesn't appear to be a link on the set theory bubble like there is on say the function bubble

#### Icaro Costa (Jan 22 2023 at 19:46):

Bulhwi Cha said:

Lean games

Xena project

- The Real Number Game: the rudiments of real analysis.
- The Complex Number Game: incomplete.
- The Group Theory Game: this game goes as far as a proof of Sylow's first theorem.

Games made by others

- The Topology Game: topology.
- The Euclid Game: the basics of axiomatic geometry.
- MIU game in Lean: this game is an introduction to formal deduction; it is based on the MIU formal system introduced by Douglas Hofstadter.

Exactly what I wanted, thank you

#### Icaro Costa (Feb 04 2023 at 19:01):

Icaro Costa said:

Bulhwi Cha said:

Lean games

Xena project

- The Real Number Game: the rudiments of real analysis.
- The Complex Number Game: incomplete.
- The Group Theory Game: this game goes as far as a proof of Sylow's first theorem.

Games made by others

- The Topology Game: topology.
- The Euclid Game: the basics of axiomatic geometry.
- MIU game in Lean: this game is an introduction to formal deduction; it is based on the MIU formal system introduced by Douglas Hofstadter.
Exactly what I wanted, thank you

Is it ok if I put the "Real Number Game" in a public server for everybody to use?

#### Jireh Loreaux (Feb 04 2023 at 19:13):

@Kevin Buzzard :up:

#### Chris Hughes (Feb 04 2023 at 21:59):

Don't forget the HoTT game. It's not Lean, but it's maybe interesting to a similar crowd.

#### Kevin Buzzard (Feb 04 2023 at 22:37):

The real number game never got finished, right? Wasn't there a max minigame and a maze game that were finished and very short?

#### Icaro Costa (Feb 05 2023 at 00:35):

Kevin Buzzard said:

The real number game never got finished, right? Wasn't there a max minigame and a maze game that were finished and very short?

Oh, I didn't look it through. I was just making a Dockerfile to make it run on the browser, and it wouldn't be much of a leap to publish it

#### Icaro Costa (Feb 05 2023 at 01:17):

Icaro Costa said:

Kevin Buzzard said:

The real number game never got finished, right? Wasn't there a max minigame and a maze game that were finished and very short?

Oh, I didn't look it through. I was just making a Dockerfile to make it run on the browser, and it wouldn't be much of a leap to publish it

Here's the Dockerfile I'm talking about: https://github.com/ImperialCollegeLondon/real-number-game/pull/19

It runs, but the interpreter doesn't seem to be working right.

#### Marc Masdeu (Feb 05 2023 at 17:15):

Thanks for the publicity about the games that got developed in Barcelona! I would like to add also https://mat.uab.cat/~masdeu/fundamental/, where you prove some results on Fibonacci numbers and also some basic results on grup theory. I chose not to teach certain tactics (like exact) and I was quite happy about the results. Also there is an added "symbols menu" to remind the user how to type stuff...

The choice of topics came from some basic results that were seen in a "Intro to proof" course (which does not use Lean) at my university. Please send me a private message if you have any comments or suggestions, I'd be happy to improve those games.

Last updated: Dec 20 2023 at 11:08 UTC