Проблема четырёх красок, или компьютер в математике. Занятие 1

Теорема о четырёх красках утверждает, что всякую расположенную на сфере карту можно раскрасить четырьмя красками так, чтобы любые две области, имеющие общий участок границы, были раскрашены в разные цвета. В виде проблемы она была сформулирована в 1852 году – и доказана в 1976-м лишь с помощью компьютера.
Такое решение не всем понравилось, и некоторые до сих пор ждут доказательства, которое можно проверить без компьютера. Другие (как великий математик Владимир Воеводский) – наоборот, стали развивать автоматическую проверку правильности доказательств на компьютере…
В курсе мы разберем доказательство теоремы о четырёх красках (это простая комбинаторика, доступная любому школьнику), а также обсудим сегодняшнее использование компьютера в математике (надо примерно знать, что такое компьютер).