First episode of the Iowa Type Theory Commute.\xa0 The basic idea of computer-checked proofs.\xa0 The example of the original proof of the Four Color Theorem.