Не подлежащее проверке доказательство

В философии математики необозримое доказательство — это математическое доказательство , которое считается невозможным для проверки человеком-математиком и, следовательно, имеет спорную обоснованность . Этот термин был придуман Томасом Тимочко в 1979 году в критике компьютерного доказательства теоремы о четырёх красках Кеннета Аппеля и Вольфганга Хакена и с тех пор применяется к другим аргументам, в основном с чрезмерным разделением случаев и/или с частями, отправленными труднопроверяемой компьютерной программой. Обозримость остаётся важным соображением в вычислительной математике .

Тимочко утверждал, что три критерия определяют, является ли аргумент математическим доказательством:

• Убедительность , которая относится к способности доказательства убедить рационального доказывающего в его выводе;
• Возможность проверки , которая относится к доступности доказательства для проверки членами человеческого математического сообщества; и
• Формализуемость , которая относится к способности доказательства апеллировать только к логическим связям между концепциями для обоснования своего аргумента. ^[1]

По мнению Тимочко, доказательство Аппеля–Хакена не соответствует критерию наблюдаемости, поскольку, как он утверждал, в нем дедукция заменяется экспериментом :

…если мы принимаем [теорему о четырех красках] как теорему, мы стремимся изменить смысл «теоремы» или, что более важно, изменить смысл лежащей в ее основе концепции «доказательства».
…[использование] компьютеров в математике, как в [теореме о четырех красках], вводит в математику эмпирические эксперименты. Независимо от того, решим ли мы считать [теорему о четырех красках] доказанной или нет, мы должны признать, что текущее доказательство не является традиционным доказательством, не является априорным выводом утверждения из посылок. Это традиционное доказательство с лакуной или пробелом, который заполняется результатами хорошо продуманного эксперимента.

—  Томас Тимочко, «Проблема четырех красок и ее философское значение» ^[1]

Без возможности обзора доказательство может выполнить свою первую задачу — убедить читателя в своем результате, но при этом не достичь своей второй цели — прояснить читателю, почему этот результат верен, — оно может играть роль наблюдения, а не аргумента. ^{[2] [3]}

Это различие важно, поскольку оно означает, что не поддающиеся исследованию доказательства подвергают математику гораздо более высокому потенциалу ошибки. Особенно в случае, когда не поддающиеся исследованию обусловлены использованием компьютерной программы (которая может иметь ошибки ), особенно когда эта программа не опубликована, убедительность может пострадать в результате. ^[3] Как писал Тимочко:

Предположим, что некий суперкомпьютер был запущен для работы над непротиворечивостью арифметики Пеано и он сообщил доказательство непротиворечивости , доказательство, которое было настолько длинным и сложным, что ни один математик не мог понять его за пределами самых общих терминов. Можем ли мы иметь достаточно веры в компьютеры, чтобы принять этот результат, или мы скажем, что эмпирических доказательств их надежности недостаточно?

—  Томас Тимочко, «Проблема четырех красок и ее философское значение» ^[1]

Однако точка зрения Тимочко оспаривается аргументами о том, что доказательства, которые трудно проверить, не обязательно столь же недействительны, как доказательства, которые невозможно проверить.

Пол Теллер утверждал, что обзорность — это вопрос степени и читательской зависимости, а не то, что есть или не есть у доказательства. Как утверждает Теллер, доказательства не отклоняются, когда у студентов возникают проблемы с их пониманием, так и доказательства не должны отклоняться (хотя их можно критиковать) просто потому, что профессиональные математики считают аргумент сложным для понимания. ^{[4] [3]} (Теллер не согласился с оценкой Тимочко, что «[Теорема о четырех красках] не была проверена математиками шаг за шагом, как проверялись все другие доказательства. Действительно, ее нельзя проверить таким образом».)

Аналогичный аргумент заключается в том, что разделение случаев является общепринятым методом доказательства, а доказательство Аппеля–Хакена — лишь крайний пример разделения случаев. ^[2]

С другой стороны, точка зрения Тимочко о том, что доказательства должны быть по крайней мере поддающимися обзору и что ошибки в доказательствах, которые трудно обозреть, с меньшей вероятностью попадут под проверку, в целом не оспаривается; вместо этого были предложены методы для улучшения обзорности, особенно компьютерных доказательств. Среди ранних предложений было предложение о распараллеливании: задача проверки может быть разделена между многими читателями, каждый из которых может обозреть часть доказательства. ^[5] Но современная практика, как прославил Флайспек , заключается в том, чтобы представить сомнительные части доказательства в ограниченном формализме, а затем проверить их с помощью средства проверки доказательств , которое само по себе доступно для обзора. Действительно, доказательство Аппеля–Хакена было таким образом проверено. ^[6]

Тем не менее, автоматизированная проверка пока не получила широкого распространения. ^[7]