The Game of Life is a cellular automaton designed by John Conway in 1969. It consists of an infinite two-dimensional grid of cells, each of which can be either "alive" or "dead". The grid evolves in discrete time steps. If exactly 3 of the 8 neighbors of a dead cell are alive, the cell becomes alive; and a live cell stays alive if it has 2 or 3 live neighbors. Despite the simplicity of the rule, Game of Life has very complex dynamics and is notoriously difficult to analyze.
We present new proof techniques for studying the long- and short-term dynamics of Game of Life (and other cellular automata). Using them, we show that: Game of Life does not reach its limit set in a finite number of steps; its dynamics on the limit set is not transitive; it is decidable whether a finite-population configuration has a predecessor; it is undecidable whether a totally periodic configuration has a predecessor; there exists a finite-population configuration that has a predecessor, but no finite-population predecessor; and various other results.