Zulip Chat Archive

Stream: new members

Topic: Linear algebra game

Andy Heald (Oct 23 2023 at 19:48):

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

Kevin Buzzard (Oct 23 2023 at 20:26):

Can you send a link to this game?

Andy Heald (Oct 24 2023 at 01:27):


Eric Wieser (Oct 24 2023 at 06:05):

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

Agnishom Chattopadhyay (Oct 26 2023 at 16:00):

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 (Oct 26 2023 at 16:05):

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 (Oct 26 2023 at 16:11):

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

Last updated: Dec 20 2023 at 11:08 UTC