Zulip Chat Archive

Stream: general

Topic: Color Zen

Kevin Buzzard (Nov 04 2022 at 23:21):

Since I discovered lean I have essentially stopped playing all computer video games other than Lean. But occasionally I find myself on mobile with no internet access, and for years the only game on my phone was Simon Tatham's puzzles. For most of those puzzles I think "yeah I could make a type for those levels in lean". But recently I went back to the Android game Color Zen. How would you formalise the type whose terms were levels of that game? Perhaps forget the physics and just make an arbitrary algorithm to break collision ties based on eg position of collision in [0,1]^2. Or is it better to use @Joseph Myers 's beautiful ideas? Something which models some of the levels for which topology is not really playing a role would be a good start.

Kevin Buzzard (Nov 04 2022 at 23:23):

That's what the levels look like

Kevin Buzzard (Nov 04 2022 at 23:34):

Writing a solver would be cool but you'd have to understand the question first

Gabriel Ebner (Nov 05 2022 at 00:55):

The game reminds me a bit of pi-calculus, but with a weird communication rule.

Patrick Johnson (Nov 05 2022 at 11:22):

How would you formalise the type whose terms were levels of that game?

The first step would be to provide public and unrestricted access to the game. Is it open source? Can it be played on PC? Is there an online version? There are a few gameplay videos on youtube, but in order to understand all mechanincs of the game, one would need to play the game. I don't have an iphone, and for the android, google play store is blocked in my country. How am I supposed to think about formalizing it if I can't access it? (not only me, but anyone who can't access the game).

Topics about formalizing closed-source games (or mobile-only games) are more suitable for reddit or discord, rather than zulip, in my opinion.

Kevin Buzzard (Nov 05 2022 at 11:35):

I'm happy to take it there!

Scott Morrison (Nov 05 2022 at 12:09):

For what it's worth, I disagree and think this is a reasonable topic of conversation on zulip. If I had more time, I would love to look at the game to understand Gabriel's intriguing comment. :-) Its irrelevance to some people is a reason for them to mute the conversation or stream, but not much more.

Last updated: Aug 03 2023 at 10:10 UTC