Насколько мне известно, а известно мне это от
профессора Идо Эфрата, не все математики принимают "компьютерные доказательства". При чём, он имел в виду не "автоматические доказательства теорем", а именно перебор вариантов, когда, к примеру, доказательство теоремы разбивают на разные случаи, большинство доказывается в общем виде, а часть доказывается с помощью простого перебора вариантов. Если мне не изменяет память, одна из так называемых теорем "
о раскраске" доказана таким образом, а также часть теорем в
теории Галуа.
При этом он объяснял причину такого скепсиса. Нет, это не проблема округления. Дело в том, что и процессор и память на
физическом уровне могут привести к сбою к вычисление. Грубо говоря, иногда у компьютера 2+2 может быть 5. Бывает это крайне редко, вероятность этого содержит очень много нулей. Однако, когда производят очень много математический вычислений,
такой сбой может произойти. В частности, при распределённых вычислениях, это обстоятельство учитывается. Google, обрабатывает столько информации, что у него есть специальные алгоритмы, которые позволяют находить эти ошибки. Обычно, однако, просто повторяют вычисления ещё раз, иногда, на компьютерах другой архитектуры. Если получают разный результат - был сбой, если один и тот же, то вероятность ошибки очень сильно сокращается и её обычно пренебрегают.
Именно поэтому, никогда нельзя быть до конца уверенным, что в компьютерном доказательстве нет ошибки. Единственный способ, по Идо Эфрату, это проверить, это повторить все вычисления, шаг за шагом в ручную.
UPDATE: Реальный пример сбоя работы памяти, любезно предоставленный
Ильёй Весенним.
UPDATE: Как мне указали в комментариях, "одна из так называемых теорем "о раскраске"" является
проблемой четырёх красок.
UPDATE 17-08-2014:
Компьютер проверил доказательство гипотезы Кеплера