Linear algebra game

Stream: new members

[Andy Heald]

In Cauchy-Schwartz world does anyone know how ||x|| is defined?

[Kevin Buzzard]

Can you send a link to this game?

[Andy Heald]

https://stavan-jain.github.io/linear_algebra_game

[Eric Wieser]

(Repo at https://github.com/stavan-jain/linear_algebra_game)

[Agnishom Chattopadhyay]

Interesting stuff.

How does this work from the devops perspective? I see in the make file that there is a command make-lean-game. Where is this implemented?

[Patrick Massot]

This is a Lean 3 version so it is completely obsolete. You can learn about the Lean 4 version at https://github.com/leanprover-community/lean4game. Porting this linear algebra game to Lean 4 would be a very nice exercise if you are interested in this technology.

[Agnishom Chattopadhyay]

Thanks for the link! It is quite impressive how the server is almost entirely built using Lean itself. This suggests that Lean already has the things that could make it a usable general-purpose language