Что значит "доказано при проведении вычислительного эксперимента в 1979-м году"? Это следствие теоремы Куратовского о невложимости графа
в плоскость, или, если угодно, теоремы ван-Кампена о невложимости (обобщающая первую). Обе никакого отношения к "компьютерным экспериментам" не имеют и доказаны были ранее.
Из подразумеваемой, по-видимому, теоремы о 4 красках действительно следует невложимость графа
в плоскость, но писать, что эта невложимость была доказана как следствие теоремы о 4 красках в 1979 году (в 1976 так-то) это полный бред и непонимание сути вопроса.
(А у племен области могли быть несвязными.)
Простите, я опирался на
Википедию:
Цитата:
Теорема о четырёх красках была доказана в 1976 году Кеннетом Аппелем[en] и Вольфгангом Хакеном из Иллинойского университета. Это была первая крупная математическая теорема, доказанная с помощью компьютера. Первым шагом доказательства была демонстрация существования определённого набора из 1936 карт, ни одна из которых не может содержать карту меньшего размера, которая опровергала бы теорему. Авторы использовали специальную компьютерную программу, чтобы доказать это свойство для каждой из 1936 карт. Доказательство этого факта заняло сотни страниц. После этого Аппель и Хакен пришли к выводу, что не существует наименьшего контрпримера к теореме, потому что иначе он должен был бы содержать какую-нибудь из этих 1936 карт, чего нет. Это противоречие говорит о том, что контрпримера нет вообще.
Изначально доказательство было принято не всеми математиками, поскольку его невозможно проверить вручную. В дальнейшем оно получило более широкое признание, хотя у некоторых долгое время оставались сомнения. Чтобы развеять оставшиеся сомнения, в 1997 году Робертсон, Сандерс, Сеймур и Томас опубликовали более простое доказательство, использующее аналогичные идеи, но по-прежнему проделанное с помощью компьютера. Кроме того, в 2005 году доказательство было проделано Джорджсом Гонтиром с использованием специализированного программного обеспечения (Coq v7.3.1)[4].
Содержание