Была ли когда-либо ошибка проверки корректности недействительной?

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

Три вопроса в порядке силы:

Разве такое исправление ошибки достоверности когда-либо приводило к тому, что основное доказательство проваливалось без изменения доказательства?
Если (1) верно, требовались ли когда-либо серьезные модификации для исправления доказательства?
Если (2) верно, кто-нибудь доказал неверную основную теорему из-за ошибки в здравом смысле?

Я оставлю определение "майора" другим.

proof-assistants soundness Джеффри Ирвинг
источник

Это, вероятно, показывает мое невежество, но была ли когда-либо установлена основная теорема с помощником по доказательству? Конечно, я знаю о теореме о 4 цветах и гипотезе Кеплера, но я не думаю, что в первых доказательствах использовались помощники по доказательствам. Мне интересно.

Сашо Николов

Я полагаю, что ни один человек не доказал правильность компилятора и не ошибся до CompCert. Но вы правы, что это сделает (3), в частности, менее интересным вопросом.

Джеффри Ирвинг

@SashoNikolov: это не совсем актуально, так как большинство доказательств, выполняемых на практике помощниками по доказательствам, не касаются математики. Обычно речь идет о программных системах, или о свойствах формальных систем и т. Д. (Это только вопрос времени, когда подавляющее большинство доказательств, сделанных на этой планете, не о чистой математике. Роботы идут.) Это было бы довольно раздражающим если, например, кто-то доказал с помощью помощника по проверке, что какая-то критическая система безопасна, а затем выяснилось, что они случайно использовали несоответствие.

Андрей Бауэр

Спасибо @AndrejBauer. Таким образом, «главное доказательство» и «основная теорема» здесь означают не главное для исследовательских математиков, а доказательства правильности важных критических систем?

Сашо Николов

Я думаю, что любые доказательства, которые считают важными достаточно многие люди (математики, эксперты по безопасности, разработчики программного обеспечения), будут рассчитывать. Боюсь, мы не узнаем, потому что, если кто- то наткнулся на эту проблему, скорее всего, они спокойно ее исправят.

Андрей Бауэр

Ответы:

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

Как Андрей отмечает, однако, это иногда случается , что нормативы безопасных непосильных ошибки делать подрезать в этих системах (хотя , как правило , не тихо , как говорит Андрей), а также исправление для этой ошибки предполагает некоторые изменения в существующие доказательства, или, скорее, из стандартная библиотека системы доказательств.

Некоторые примеры таких доказательств взлома библиотеки в Coq:

https://coq.inria.fr/bugs/show_bug.cgi?id=4294

https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.html

Трудно сказать, зависели ли установленные доказательства от несоответствия, так как после исправления требовались незначительные изменения, которые должны были быть приняты проверяющим доказательства. Но это происходит при каждом нетривиальном обновлении!

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

Несоответствия в структурах доказательства обычно требуют интенсивного использования странных комбинаций эзотерических признаков, и поэтому очень редко возникают "случайно".

Коди
источник

Я имел в виду, что люди молча или даже неосознанно решали проблемы в своих сценариях проверки , как реакцию на ошибки в помощниках по проверке. Конечно, несоответствия в помощниках по проверке всегда принимаются с удивительным уровнем волнения. У математиков должно быть несоответствие в математике, которое могло бы составить интересную пару месяцев.

Андрей Бауэр

Что это за люди, которые бросают на меня ссылки из Википедии? @RickyDemer, пожалуйста, объясните, пожалуйста, свою точку зрения. Вы знаете, я слышал о парадоксе Рассела. Это было более 100 лет назад, и это привело к отличной математике. Я предлагаю, чтобы мы созрели для другого.

Андрей Бауэр

Я сейчас приму этот ответ, но, конечно, я не приму его, если кто-то ответит в другом направлении! (Полное раскрытие: это был ответ, на который я надеялся.)

Джеффри Ирвинг

@ GeoffreyIrving Ответ несколько неудовлетворительный, так как мне трудно доказать отсутствие опровержений! Поэтому ответ в некоторой степени обязательно основан на моем недостатке знаний, хотя было очень мало очень крупномасштабных формализаций машин, и я, по крайней мере, немного уверен в своем ответе. Я также слышал, что некоторые важные формализации в методе B , как было показано, имеют противоречивые допущения (вам нужно добавить много аксиом для нетривиальных утверждений, и совокупности аксиом, взятых вместе, впоследствии были показаны ...

cody

... несовместимо). К сожалению, я не могу найти ссылку на это, поэтому я не включил ее в свой ответ. Также формализация была о большой программе, а не о чистой математике.

Коди