Как машина впервые обыграла математиков: доказательство теоремы о четырёх красках
The Four Colour Theorem: The first time machines mogged mathematicians
В 1976 году Kenneth Appel и Wolfgang Haken доказали теорему о четырёх красках с помощью компьютера, потратив 1200 часов машинного времени и 10 миллиардов решений. Математики разделились: одни приняли результат, другие объявили его не математикой, а оракулом. Споры о том, можно ли доверять доказательству, которое невозможно проверить вручную, продолжаются до сих пор.
«Бог не позволил бы доказать теорему таким ужасным методом!» — Herbert Wilf, University of Pennsylvania
- fhdkweig
Проблема с этим доказательством была в том, что мы знали, что FCT верна, но понятия не имели, почему. Хорошее/элегантное доказательство учит нас чему-то новому о том, как эта проблема связана с другими проблемами. Дело не только в том, чтобы получить ответ «истина/ложь» на эту гипотезу.
- layer8
Я не знал, что мы уже изобрели машины времени. ;)
- jjtheblunt
Название заставило меня вспомнить о гораздо более старом механизме, который использовался для вычислений