Czy błąd sprawdzania kiedykolwiek unieważnił ważny dowód?

Większość (wszystkich?) Dowódców ma czasami naprawione błędy związane z dźwiękiem. Jednak z tych, które widziałem, błędy te zwykle trudno jest przypadkowo natknąć się, a wyniki udowodnione przed naprawieniem błędu zwykle są wstrzymywane po naprawie.

Trzy pytania, w kolejności według siły:

Czy taka poprawka błędu dźwiękowego spowodowała, że jakiś główny dowód zawiódł, bez modyfikacji dowodu?
Jeśli (1) jest prawdziwe, czy kiedykolwiek konieczne były poważne modyfikacje, aby naprawić dowód?
Jeśli (2) jest prawdziwe, to czy ktoś udowodnił błędne główne twierdzenie z powodu błędu poprawności?

Pozostawię definicję „major” innym.

proof-assistants soundness Geoffrey Irving
źródło

To prawdopodobnie pokazuje moją niewiedzę, ale czy główne twierdzenie zostało kiedykolwiek ustalone z asystentem dowodowym? Oczywiście wiem o twierdzeniu o 4 kolorach i przypuszczeniu Keplera, ale nie sądzę, aby pierwsze dowody były tam asystentami. Jestem ciekaw.

Sasho Nikolov

Uważam, że żaden człowiek nie udowodnił poprawności kompilatora i miał rację, aż do CompCert. Ale masz rację, że sprawiłoby to w szczególności (3) mniej interesujące pytanie.

Geoffrey Irving

@SashoNikolov: to nie jest tak naprawdę istotne, ponieważ większość dowodów wykonanych w praktyce przez asystentów nie dotyczy matematyki. Zazwyczaj dotyczą systemów oprogramowania lub właściwości systemów formalnych itp. (To tylko kwestia czasu, kiedy zdecydowana większość dowodów wykonanych na tej planecie nie dotyczy czystej matematyki. Roboty nadchodzą.) Byłoby to dość denerwujące jeśli na przykład ktoś udowodnił za pomocą asystenta dowodu, że jakiś krytyczny system jest bezpieczny, a później okazało się, że przypadkowo zastosował niespójność.

Andrej Bauer,

Dzięki @AndrejBauer. Czyli „główny dowód” i „główne twierdzenie” oznaczają tutaj nie duże dla matematyków badawczych, ale dowody poprawności ważnych systemów krytycznych?

Sasho Nikolov,

Myślę, że każdy dowód uznany za ważny przez wystarczająco wielu ludzi (matematyków, ekspertów ds. Bezpieczeństwa, inżynierów oprogramowania) byłby ważny. Obawiam się, że nie będziemy się dowiedzieć, bo jeśli ktoś nie natknąć się ten problem, szanse są cicho naprawił.

Andrej Bauer,

Odpowiedzi:

O ile mi wiadomo, żaden dokument sprawdzony przez maszynę złożonego rozwoju matematycznego nigdy nie został wycofany.

Jak zauważa Andrej, czasami zdarza się, że błędy te powodują pojawienie się błędów w tych systemach (choć zwykle nie cicho , jak sugeruje Andrej), a naprawa tego błędu wiąże się z pewnymi zmianami w istniejących dowodach lub, co bardziej prawdopodobne, z standardowa biblioteka zaangażowanego systemu sprawdzania.

Niektóre przykłady takich dowodów łamania bibliotek w Coq:

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

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

Trudno powiedzieć, czy ustalone dowody zależały od niespójności, ponieważ po poprawce wymagały drobnych poprawek, które zostały zaakceptowane przez sprawdzającego dowody. Ale dzieje się tak przy każdej nietrywialnej aktualizacji!

Moim osobistym zdaniem jest mało prawdopodobne, aby takie błędy się zdarzyły, ponieważ papierowy dowód musi być dobrze dopracowany, zanim będzie można spróbować sformalizować maszynę.

Niespójności w ramach dowodowych zwykle wymagają intensywnego użycia dziwnych kombinacji cech ezoterycznych, a więc bardzo rzadko pojawiają się „przypadkowo”.

cody
źródło

Miałem na myśli osoby , które dyskretnie rozwiązują problemy w swoich skryptach próbnych , a nawet nieświadomie, jak zauważył Geoffrey, jako reakcję na błędy w asystentach dowodowych. Oczywiście niespójności w asystentach dowodowych są zawsze odbierane z niesamowitym poziomem podniecenia. Matematycy powinni mieć niespójność w matematyce, co stanowiłoby interesującą parę miesięcy.

Andrej Bauer,

Co się dzieje z ludźmi rzucającymi we mnie linkami z Wikipedii? @RickyDemer, czy mógłbyś wyjaśnić swój punkt widzenia? Słyszałem o paradoksie Russella. To było ponad 100 lat temu i doprowadziło do doskonałej matematyki. Proponuję, abyśmy byli gotowi na kolejny.

Andrej Bauer,

Na razie zaakceptuję tę odpowiedź, ale oczywiście nie zaakceptuję jej, jeśli ktoś odpowie w innym kierunku! (Pełne ujawnienie: to była odpowiedź, na którą liczyłem.)

Geoffrey Irving

@GeoffreyIrving Odpowiedź jest nieco niezadowalająca, ponieważ trudno mi udowodnić brak wycofań! Odpowiedź jest więc w pewnym stopniu oparta na moim braku wiedzy, chociaż było tak niewiele formalizacji maszyn na bardzo dużą skalę, że przynajmniej trochę ufam swojej odpowiedzi. Słyszałem również, że wykazano, że niektóre ważne formalizacje w metodzie B mają niespójne założenia (musisz dodać wiele aksjomatów dla wyrażeń nietrywialnych, a kolekcje aksjomatów razem wykazano następnie ...

cody

... niespójny). Niestety nie mogę znaleźć odniesienia do tego, więc nie uwzględniłem go w mojej odpowiedzi. Również formalizacja dotyczyła dużego programu, a nie czystej matematyki.

cody