Tic-tac-toe in Lean

Stream: Program verification

[Adolfo Ochagavía]

Not sure if this is the right place, but I just finished writing a blog post on formalizing tic-tac-toe. It's my first stab at proving something nontrivial (if you may call tic-tac-toe nontrivial), and my first Lean proof at all, so I'm open to suggestions!

[(deleted)]

Where's your code

[Adolfo Ochagavía]

It's linked in the article, but here's a direct link too: https://github.com/aochagavia/tic-tac-toe-lean

[Aaron Liu]

I'd love to see a proof that tic tac toe has no forced win

[Adolfo Ochagavía]

That's the next step :D