The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Omg, how do you know? Maybe you should put it on the proofmarket?

-- Matthieu

Le dimanche 30 mars 2014, Laurent Théry <Laurent.Thery AT inria.fr> a écrit :

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 ;-)

--