Чотири фарби: доведення, яке перевіряла машина
У липні 1976 року Кеннет Аппель і Вольфганг Гакен з Іллінойського університету подали доведення того, що будь-яку плоску карту можна розфарбувати чотирма кольорами. Воно зводилося до скінченного набору конфігурацій, кожну з яких треба було перевірити на зводність; перевірку зробили програми авторів на комп'ютерах IBM.
Чому це важливо
Задачу, першу опубліковану спробу розв'язати яку, за статтею, зробив Кемпе 1879 року, закрило доведення, вирішальну частину якого людина не може перевірити вручну, а лише повторити як обчислення. Питання, чи можна довіряти доведенню, яке виконала машина, стало для математики практичним.
Частина I описує процедуру розрядження, яка доводить, що кожна плоска тріангуляція містить хоча б одну конфігурацію з набору; частина II, разом із Джоном Кохом, — зводність цих конфігурацій. За приміткою частини I, під час подання в липні 1976 року набір оголосили як 1 936 конфігурацій; прибравши близько сотні повторів, статті подають 1 834, а мікрофішний додаток показує, що досить 1 482. Кожну конфігурацію з кільцем 11 і більше, крім однієї, перевірили програми авторів — на IBM 360-75 в Урбані, IBM 370-158 у Чикаго й 370-168 адміністративного обчислювального центру університету, мовою асемблера. Одна перевірка кільця з чотирнадцяти вершин тривала близько 25 хвилин на 370-158 або 6 хвилин на 370-168. Чого запис не стверджує: поширених «1 200 годин машинного часу» — в обох частинах статті такого числа немає.