Interactive Learning Materials

Stream: general

[Icaro Costa]

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

[Trebor Huang]

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

[Bulhwi Cha]

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]

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

[Bulhwi Cha]

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

[Shreyas Srinivas]

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]

It works fine for me.

[Patrick Stevens]

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

[Shreyas Srinivas]

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]

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

[Icaro Costa]

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]

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]

@Kevin Buzzard :up:

[Chris Hughes]

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

[Kevin Buzzard]

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]

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]

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]

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.