The Coq mailing list

[Laurent Théry <Laurent.Thery AT inria.fr>]

Hi,

if you are addicted to the new "productivity killer" app 2048 :

http://gabrielecirulli.github.io/2048/

you can now turn it into a proving activity with Coq :

http://www-sop.inria.fr/marelle/Laurent.Thery/T2048.v

Have fun!

--
Laurent

Ps: if you manage to prove thm1 or thm2 please send me an email ;-)