leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
197 stars 35 forks source link

Competition #242

Open swisstackle opened 5 months ago

swisstackle commented 5 months ago

I havent looked at the codebase yet, but how much effort would it be to build a 1v1 capable gameroom with matchmaking a la Counter Strike (with some sort of ranking). Whoever completes the proof first wins the game.

To have something like that in math would be fun to learning math. Lean is perfect for this I suppose.

An extension based on that would be someting like 2v2 where 2 guys work on one proof.

Ofcourse, creating all the games themselves would be the bottleneck, because always solving the same problems would be boring.

joneugster commented 5 months ago

With the current design that's not easily realisable, mostly because the design choice is to store all user data in the user's browser and have no personal data stored on the server at all.

We mainly decided to do it this way in order to avoid any GDPR related questions.

joneugster commented 5 months ago

but, I hope that after some cleanup there would be some reusablility of the react code in order to create a different project implementing such a server easier if desired. I'd hope things would be documented enough to do so by October.

Creating good games is indeed a bottle-neck. Since you're Swiss too, you might be interested looking at the German game Robo which tries to go into a bit higher maths. There you also see a bit the difficulties of managing that cleanly and designing playable levels, some things are really WIP there...

swisstackle commented 5 months ago

I have a simpler idea then that doesn't involve server side data.

A user can create a game room by generating a link that he can send to a friend to play against him. No ranking is involved. Whoever just submits the proof first wins and then the game is over.

Creating games will still be the bottleneck though, not sure what to do about that one.

But yea, looking forward to where this whole thing goes with Lean.