Color Zen

Stream: general

[Kevin Buzzard]

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]

That's what the levels look like
Screenshot_20221104-235757.png

[Kevin Buzzard]

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

[Gabriel Ebner]

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

[Patrick Johnson]

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]

I'm happy to take it there!

[Scott Morrison]

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.