Jak zestrzelić swoje dowody

Jakie są ogólne wytyczne dotyczące sprawdzania twoich dowodów? Uważam, że jest to ważne dla absolwentów takich jak ja. Wiem już, co musimy zrobić, aby coś udowodnić, ale zawsze musisz wszystko sprawdzić przed wysłaniem. Nawet do twojego własnego doradcy.

Opracowałem sobie strategie metodą prób i błędów i otrzymałem wiele porad od mojego doradcy. Ale to zawsze jest bardzo żmudna praca. Zwykle, kiedy coś skończysz, po prostu chcesz przejść do następnego problemu, ale nadal musisz trzymać się bieżącego problemu, dopóki wszystko nie będzie idealne. Oto przykład mojej własnej listy sztuczek:

1. Podaj szczegóły. Wiele błędów jest w miejscach, w których piszesz „jasne jest, że ...”, „bez utraty ogólności ...” itp.
2. Wypróbuj kilka liczb. Spróbuj ekstremalnych przypadków, takich jak „co się stanie, gdy ustawię lub ”.$n=1$$n=1000$
3. Zachowaj czysty notatnik. Pisz o tym na co dzień i porównuj z szorstkimi notatkami. Próbuję pisać także w lateksie, w ten sposób znalazłem wiele błędów.

Jakie są ogólne strategie stosowane do sprawdzania dowodów?

Celem tego pytania jest uczynienie z niego wiki społeczności.

Inżynierowie oprogramowania mają pojęcie, które nazywają „ zapachami kodu ”. Są to objawy w kodzie, które mogą wskazywać na głębszy problem. Inżynierowie oprogramowania zbierają mentalne listy zapachów, o których należy pamiętać (tj. Zbyt długie metody lub zbyt wiele parametrów). Nie musi to oznaczać, że występuje problem, ale po prostu wskazać, że pisarz może chcieć sprawdzić dwukrotnie.

Proponuję, abyśmy również wzięli pod uwagę „nieprzyjemne zapachy” . To nie da ci algorytmu do sprawdzania twoich dowodów, ale daje język i metaforę do rozpoznawania możliwych problemów w dowodach. Kilka przykładów zapachów pachnie:

1. Przysłówki „wyraźnie”, „oczywiście” itp.
2. Odniesienie do dowodu poprzedniego wyniku zamiast odniesienia do samego wyniku.
3. Niekorzystne wykorzystanie wyniku z wieloma warunkami technicznymi.

Są też bardziej subtelne zapachy. Na przykład, jeśli dowód używa twierdzenia dwumianowego do rozwinięcia wyrażenia, a następnie używa twierdzenia dwumianowego, aby powrócić do formy zamkniętej, być może istnieje bezpośrednia manipulacja formą zamkniętą, która daje ten sam wynik.

Moja sugestia to zebranie (mentalnej lub pisemnej) listy takich zapachów i sprawdzanie ich podczas czytania. Przyjemnym efektem ubocznym tego podejścia jest to, że uczyni cię lepszym czytelnikiem.

Uwaga: Moją nadzieją w tej odpowiedzi było udzielenie intuicyjnej strony rygorystycznej odpowiedzi dostarczonej przez Lamporta Jak napisać dowód wymieniony w odpowiedzi M. Alaggana.

Jest bardzo dobra praca Leslie Lamporta ( Jak napisać dowód ). W rzeczywistości jest to jego propozycja dotycząca stylu pisania szczegółowych dowodów w taki sposób, aby:

(1) Umożliwia wykrywanie błędów w prosty sposób

(2) Wyjaśnia, które założenia i twierdzenia zastosowano w poszczególnych częściach, co sprawia, że ​​dość łatwo jest zobaczyć, co się stanie, jeśli chcesz (na przykład) zastosować słabsze założenia

Istnieje również pewne doświadczenie społeczności i inspirujący komentarz do tej techniki na temat MO, który pokazuje ogólnie pozytywne doświadczenia (i niektóre inne zasoby).

Aktualizacja: dostępna jest nowa wersja Jak napisać dowód XXI wieku .

Dick Lipton ma fajny artykuł zatytułowany „ Jak udowodnić, że dowód jest dowodem ”

Wydaje mi się, że pamiętam dawno temu popularne opowiadanie o tym, jak fizycy radzą sobie z analogicznym problemem. Kto wie, jak dokładna jest jego następująca wersja; poprawki są mile widziane. Uważam jednak, że podstawowa strategia jest dość niezwykła.

Wyjaśnili, jak uwierzyli w czarne dziury. Czarne dziury były początkowo konstrukcjami czysto matematycznymi, podobnie jak inne dziwne obiekty w fizyce, takie jak tunele czasoprzestrzenne. Ich strategia była uderzająca: matematycznie rzucali innymi przedmiotami w badany obiekt. Tunele czasoprzestrzenne nie przeszły pomyślnie testów, ponieważ odkryli, że tunel czasoprzestrzenny zapadnie się nawet w obecności normalnego obiektu fizycznego, może asteroidy. Ale czarne dziury przeszły ten test: czarna dziura przetrwałaby po rzuceniu w nią asteroidą. Próbowali więc rzucić w to gwiazdą. Ten sam wynik. W końcu rzucili kolejną czarną dziurę w czarną dziurę i ta przetrwała. W rezultacie nabrali wystarczającej pewności w istnieniu czarnych dziur, aby faktycznie zacząć ich szukać w prawdziwym wszechświecie.

Tak więc stosowność i zastosowanie powyższej strategii polega na tym, aby zacząć rzucać rzeczami na swój dowód. Czy przetrwa kontrolę poczytalności ? Jeśli usuniesz niezbędne założenie, to czy ono się zawali, jak powinno? Czy zwija się tak, jak powinien, gdy jest stosowany do spraw poza jego zakresem? Czy wytrzymuje rozsądne uogólnienia i specjalizacje? Spójrz na listę heurystyk w artykule Polya How to Solve . Spróbuj zmutować swój dowód za pomocą tych heurystyk i sprawdź, czy stoi i spada tak, jak powinien.

Myślę, że jednym z najbezpieczniejszych sposobów jest opracowanie wielu niezależnych dowodów. Dzięki temu możesz mieć pewność, że główny wynik jest prawidłowy, nawet jeśli popełnisz błąd w niektórych szczegółach dowodu.

Jedną z technik, które uważam za przydatne, jest zastanowienie się, jakie inne wyniki byłaby w stanie udowodnić strategia dowodu. Jeśli z łatwością mogę dostosować strategię dowodu, aby udowodnić duży otwarty problem lub nawet problem, który nie jest otwarty, ale który ma zbyt skomplikowane rozwiązanie w porównaniu ze złożonością strategii sprawdzania, to jest to duży powód do wątpliwości dowód.

Zawsze sprawdzam ponownie swoje dowody za pomocą narzędzia sprawdzającego, takiego jak COQ lub ISABELLE . Jeśli możesz udowodnić swój dowód w dowolnym z tych języków programowania, możesz być pewien, że jest on poprawny. Tak prosty jak termin lambda;).