Задача о четырёх красках: первое доказательство компьютером
Возьмите любую карту: страны, области, районы. Нужно раскрасить её так, чтобы граничащие области были разного цвета. Сколько цветов хватит всегда? Ответ, четыре, угадали ещё в XIX веке. Доказательство стало первым крупным математическим результатом, без компьютера невозможным.
Для 6–11 классов. Пригодятся цветные карандаши.
Задача
В 1852 году англичанин Фрэнсис Гатри раскрашивал карту графств Англии и заметил, что ему хватает четырёх цветов. Он спросил: хватит ли четырёх цветов для любой карты? Правила такие: области, у которых общая граница длиной больше точки, должны быть разного цвета; области, касающиеся в одной точке, могут совпадать.
Трёх цветов хватает не всегда. Пример: одна область в центре и три вокруг, каждая из которых граничит с центром и с двумя другими. Здесь нужно четыре цвета.
Сто лет попыток
| Год | Что случилось |
|---|---|
| 1852 | Гатри задаёт вопрос, его брат передаёт его математику Огастесу де Моргану |
| 1879 | Альфред Кемпе публикует доказательство, его признают |
| 1890 | Перси Хивуд находит в доказательстве Кемпе ошибку, но доказывает, что пяти цветов хватает всегда |
| 1976 | Кеннет Аппель и Вольфганг Хакен доказывают гипотезу с помощью компьютера |
| 1996 | Робертсон, Сандерс, Сеймур и Томас упрощают доказательство |
| 2005 | Жорж Гонтье проверяет доказательство в программе для формальной проверки доказательств Coq |
Как помог компьютер
Аппель и Хакен свели задачу к перебору. Они показали: в любой карте обязательно встречается одна из конечного набора особых конфигураций, и каждую из них можно «убрать», не мешая раскраске остальной карты. Конфигураций оказалось почти две тысячи, и проверку каждой выполнил компьютер. На это ушло больше тысячи часов машинного времени.
Многие математики были недовольны: доказательство нельзя проверить вручную, приходится верить программе. Сейчас компьютерные доказательства стали обычными, а формальная проверка в Coq сняла большую часть сомнений.
Попробуйте сами
- Нарисуйте карту из 10–15 областей причудливой формы.
- Раскрасьте её четырьмя цветами.
- Попросите друга нарисовать карту, которая потребует пяти цветов. У него не получится.
- Подумайте, почему на карте, где каждая точка касается ровно трёх областей, легче рассуждать.
Задача о красках относится к теории графов: каждую область можно заменить точкой, а соседство линией. С похожей задачи, о мостах Кёнигсберга, теория графов и началась.
Разберём на занятии
Разберём эту тему и всё, что с ней связано, на живом занятии: преподаватель видит, как ребёнок решает, и поправляет на первом неверном шаге.
Первое занятие бесплатное: можно посмотреть формат вместе с ребёнком и решить, подходит ли он.
Частые вопросы
А для карты на бублике?
На поверхности тора может понадобиться семь цветов. Для таких поверхностей ответ нашли раньше, чем для плоскости.
Где это применяется?
В распределении частот для радиостанций и мобильных вышек, в составлении расписаний и в компиляторах программ: соседние задачи не должны получить один ресурс.