Gdzie i jak komputery pomogły udowodnić twierdzenie?

Celem tego pytania jest zebranie przykładów z teoretycznej informatyki, w której pomocne było systematyczne korzystanie z komputerów

1. budując przypuszczenie, które prowadzi do twierdzenia,
2. fałszowanie przypuszczeń lub podejścia dowodowego,
3. konstruowanie / weryfikacja (części) dowodu.

Jeśli masz konkretny przykład, opisz, jak to zrobiono. Być może pomoże to innym w bardziej efektywnym korzystaniu z komputerów w ich codziennych badaniach (co wciąż wydaje się dość rzadką praktyką w TCS).

(Oznaczone jako wiki społeczności, ponieważ nie ma jednej „poprawnej” odpowiedzi).

Bardzo dobrze znanym przykładem jest Twierdzenie Czterech Kolorów , pierwotnie udowodnione przez wyczerpujące sprawdzenie.

Napraw punktów na płaszczyźnie. Niech T będzie triangulacją (tj. Płaski wykres liniowy z punktami jako wierzchołkami, który jest w pełni triangulowany), i niech ciężar triangulacji będzie sumą długości krawędzi.$n$

Wykazanie, że minimalny ciężar triangulacji (MWT) był trudny do NP, było długotrwałym problemem otwartym, utrudnianym przez fakt, że długości krawędzi obejmują pierwiastki kwadratowe, a wymaganą precyzję potrzebną do ich dokładnego obliczenia trudno było związać.

Mulzer i Rote wykazali, że MWT jest trudny do NP , a w tym procesie wykorzystali komputerową pomoc do sprawdzenia poprawności swoich gadżetów. O ile mi wiadomo, nie ma alternatywnego dowodu.

Dowód Thomasa Halesa (jego strona, MathSciNet ) przypuszczenia Keplera wymagał tak dużej analizy przypadków - a przypadki zostały z kolei zweryfikowane komputerowo - że postanowił spróbować formalnego dowodu. Jego projektem jest FlysPecK i szacuje, że zajmie to 20 lat pracy.

Badacze języków programowania regularnie używają komputerowych dowodów w swojej pracy, choć nie wiem, jak istotne jest to w procesie badawczym (choć z pewnością nie pozwala im to na pisanie ton żmudnych manipulacji).

Doron Zeilberger wykonał pewne prace w dziedzinie wydruków komputerowych. W szczególności przygotował program Maple w celu udowodnienia tożsamości geometrycznych oraz inny program w celu udowodnienia klasy tożsamości kombinatorycznych . Niektóre z tych metod są wymienione w książce A = B .

Komputery zostały również wykorzystane do ustalenia górnych granic czasów działania programów cofania rozwiązujących problemy trudne dla NP, a także do konstruowania gadżetów w celu udowodnienia niedopuszczalności wyników. Ten i inne wypełnione zabawą tematy czekają na ciebie w krótkim eseju (ostrzeżenie, ekstremalna autopromocja) zatytułowanym „Stosowanie praktyki w teorii”. Zobacz http://arxiv.org/abs/0811.1305

Biorąc pod uwagę tę ładną listę, wygląda na to, że powinienem zaktualizować artykuł!

Kontrprzykład hipotezy Hirscha , ważny dla programowania liniowego i wielościennej kombinatoryki, został niedawno zaproponowany przez Francisco Santosa. W celu ustalenia niektórych właściwości wymaganych w tym przykładzie zastosowano weryfikację komputerową, chociaż później odkryto argumenty bez pomocy mocy obliczeniowej, por. Wpis na blogu Gil Kalai lub artykuł na temat ARXIV .

Nie widziałem tego wspomnianego tutaj, ale automatyczna przysłowia twierdzeń rozwiązała długo istniejący otwarty problem, czy algebry Robbinsa są boolowskie:

http://www.cs.unm.edu/~mccune/papers/robbins/

Jest to szczególnie godne uwagi, ponieważ komputer opracował cały dowód, a problem był otwarty przez kilka dziesięcioleci.

Nie do końca pewny, czy kwalifikuje się jako TCS, ale prawdopodobnie jest blisko spokrewniony.

Algorytm Karloff-Zwicka do MAX 3SAT osiąga oczekiwaną wydajność 7/8. Analiza opiera się jednak na niesprawdzonych nierównościach sferycznych. Nierówności te zostały ostatecznie potwierdzone za pomocą komputerowych dowodów w innym artykule Zwicka .

Oprócz dowodu Halesa na hipotezę Keplera, jak wspomniano powyżej, dowód na hipotezę o strukturze plastra miodu i na hipotezę dodekaedryczną jest również wspomagany komputerowo.

Możesz sprawdzić Shalosh B. Ekhad na stronę główną . Ten komputer od jakiegoś czasu publikuje artykuły (zwykle ze współautorami).

Christian Urban wykorzystał asystenta dowodu Isabelle, aby sprawdzić, czy jedno z głównych twierdzeń w swojej pracy doktorskiej było w rzeczywistości twierdzeniem [1]. Za pomocą asystenta trzeba było wprowadzić kilka zmian, ale wynik prawie się wyrównał.

Podobnie Urban i Narboux również odkryli błędy w pisaku i dowodzie papierowym dowodu kompletności Crary'ego w celu sprawdzenia równoważności.

Meikle i Fleuriot sformalizowali Grundlagena Hilberta w Isabelle i wykazali, że wbrew twierdzeniom Hilberta, nadal polegał na swoim założeniu, że formalizował geometrię w sposób aksjomatyczny (w IIRC były dziury w jego dowodzie pochodzące od Hilberta zakładającego, że chodzi o diagramy) [3] .

[1]: Powrót do eliminacji cięć: jeden trudny dowód jest naprawdę dowodem

[2]: Formalizowanie w dowodzie kompletności Nominalnej Isabelle Crary dla kontroli równoważności

[3]: Formalizacja Hilberta Grundlagena w Isabelle / Isar

Wyniki w „ Geometrii drzew wyszukiwania binarnego ” autorstwa Demaine, Harmon, Iacono, Kane i Patraşcu opracowano za pomocą oprogramowania do testowania różnych schematów ładowania i konstruowania optymalnych ocen dla małych sekwencji dostępu. (I tak, „osły” to poprawny termin.)

N. Shankar zweryfikował (w pełni i mechanicznie) dowód Godela na temat twierdzenia o niekompletności oraz twierdzenia Kościół - Rosser przy użyciu twierdzenia Boyera - Moore'a. Jest książka opisująca, jak to zostało zrobione.

Formuła algorytmu Bailey-Borwein-Plouffe do obliczania n-tego bitu Pi bez obliczania któregokolwiek z bardziej znaczących bitów została odkryta, według Simona Plouffe , przy użyciu komputerowych systemów dowodowych.

Istnieje wiele przykładów analizy algorytmów średniej wielkości przypadków. Być może jednymi z najwcześniejszych są eksperymenty komputerowe, które doprowadziły do ​​opracowania „Niektóre nieoczekiwane oczekiwane wyniki zachowania podczas pakowania pojemników” autorstwa Bentleya, Johnsona, Leightona, McGeocha i McGeocha w STOC 1984.