The four color theorem states that any map can be colored with just 4 colors such that no two regions which touch are given the same color. If you don't believe it, give me a map, any map, and I'll 4-color it for you! This is an example of how proofs correspond to winning strategies for a game: you won't be able to find a map that I can't color. This *interactive* interpretation of proof gives a concrete, testable understanding of truth. We'll explore the connection between proofs and games, and construct some proofs in the programming language Coq, which converts proofs to winning players in those corresponding games. Finally, we'll look at the game of Chomp, where it's clear the first player can always win, but it's actually quite difficult to figure out how!