Lean formalization of bounded grids and computable cellular automata defined thereover. - Frantisek Silvási; Martin Tomásek (Sci. Comput. Program., 2020)