using games to learn lean

Stream: new members

[Srayan Jana]

Hi all!
I think Lean is cool and I wanna learn it. However, I usually try to learn a language by making a game in it (like snake or flappy bird or something)
However, Lean isn’t a typical language, so would you recommend doing that or nah

[Srayan Jana]

I should also stress that I’m not talking about the math proof game server stuff, I’m talking about arcade style games

[Niels Voss]

Well Lean is a full-featured programming language, so it is of course possible, although I don't know if any graphics apis exist. So you might have difficulty actually displaying things to the screen, and you might have to learn how lean's FFI works so you can hook up C code. (There is a raytracer but I don't think it's real time, and it seems to be more like a demo.) Alternatively, you can use browser technologies, since you can embed HTML in Lean. If your primary motivation is to learn Lean programming, maybe a terminal game might be the least painful to create.

[Niels Voss]

Are you at all interested in the proving side of Lean, or mostly just the programming side? For the programming side, I recommend reading Functional Programming in Lean 4, or at least enough to get familiar with the language. If you've used functional programming languages like Haskell before, you'll find it very familiar (a lot of the programming part of Lean was based on Haskell).

[Srayan Jana]

The proving side kinda sounds interesting, I might as welll learn it since it looks really foreign to me and it will probably be fun.

This is gonna sound dumb, but I thought a fun way of using Lean would be to like have proofs of game mechanics.

Not sure how that would work, but somehow being able to have a formal proof of something like Balatros game mechanics, and have the game rules all be proofs or something

[Srayan Jana]

Like could you somehow have a mathematical formal proof of flappy bird? Or Tetris?

[Srayan Jana]

Tetris is probably more interesting since you’d want to prove that you could play it forever

[Niels Voss]

Well at the very least, there's the combinatorial games project https://github.com/vihdzp/combinatorial-games, where people are proving properties about various simple terminating games, such as Nim or Chomp. However it is more focused on the math side of games, like the ability to multiply and divide games and to use them to construct the surreal numbers.

It is in theory possible to prove properties of nontrivial games like tetris, provided you have a precise statement of what you want to prove, but for something like tetris it will incredibly difficult.

[(deleted)]

I recommend that you code the snake game. It's simple, it has properties that are easy enough to prove.

[(deleted)]

Lean is a full fledged programming language. Go ahead and do it.

[(deleted)]

The first proof should be the player eventually loses!

[Niels Voss]

Yes I agree. Even though snake is real time, you can model it as a turn-based game for the purposes of proving properties (as opposed to something like flappy bird). (Although I don't actually think the player must lose eventually if they never pick up any fruit)

[Kevin Buzzard]

Srayan Jana said:

Tetris is probably more interesting since you’d want to prove that you could play it forever

IIRC this isn't true? I thought I once read that if you drop S and Z pieces in the ratio 1:sqrt(2) then the player is doomed for any finite board.

[Arthur Paulino]

I once tried to prove the correctness of the classical recursive algorithm for the hanoi tower. But I couldn't get it done

[Aaron Liu]

Kevin Buzzard said:

Srayan Jana said:

Tetris is probably more interesting since you’d want to prove that you could play it forever

IIRC this isn't true? I thought I once read that if you drop S and Z pieces in the ratio 1:sqrt(2) then the player is doomed for any finite board.

Most modern Tetris games use a bagging system which guarantees the frequency of pieces is 1:1:1:1:1:1:1 and for which play-forever strategies have been devised.

[Aaron Liu]

How it works is they drop one of every piece in a random order, and then they keep doing that, so the first 7n pieces will have n of each piece.

[Aaron Liu]

For dropping pieces with independent uniform distribution every strategy loses with probability 1.

[Kevin Buzzard]

Tower of Hanoi would be a nice project. Widgets offer you a GUI so you can play yourself, small boards could be solved by brute force, and then one could prove a theorem giving an optimal algorithm for moving an n-tower from one column to another.

[Arthur Paulino]

In my very early days as an undergrad, we were shown the recursive algorithm for the tower of hanoi. It looked like magic. Maybe a theorem proving that it was correct would have made it less magical

[suhr]

Maybe a theorem proving that it was correct would have made it less magical

The proof would likely to be essentially the same (induction = recursion). Proving that it's the best you can do is probably more tricky though.

[Arthur Paulino]

The proof has to use the algorithm definition and state that it turns the initial state into the final state (all disks were moved and no illegal move was performed). With just the algorithm, you can run it a few times to test if it works and that's pretty much it

[Srayan Jana]

This is a page on the Tetris wiki that talks about how you could potentially play forever, and also links to some research papers on the subject.
Now i kinda want to write a proof for a failstate for Tetris in Lean, I think that could be really neat
https://tetris.wiki/Playing_forever

[Martin Dvořák]

One simple exercise for programming in Lean is to generate levels for the game 4D Golf in the style of RollerCoaster Tycoon.

Here is my attempt:
https://github.com/madvorak/lean4-koch

[Martin Dvořák]

Srayan Jana said:

Tetris is probably more interesting since you’d want to prove that you could play it forever

FYI, formally proving (non)existence of certain strategies for Tetris has been suggested several times.
Every time, the conclusion was that it would be a nightmare to implement.