Dowody znalezione przez komputer

W 1996 r. Długotrwały otwarty problem został rozwiązany przez komputer; mianowicie, że algebra Robbinsa i algebra Boole'a są takie same. Dowód został znaleziony przez automatyczną powiedzonkę twierdzeń.

Ponadto znany dowód twierdzenia o czterech kolorach zawiera generowane komputerowo komponenty.

Celem tego pytania jest wykazanie dowodów, które zostały (całkowicie lub częściowo) znalezione przez komputer (czy to jedyny znany dowód, czy ten odkryty po raz pierwszy).

— Mahdi Cheraghchi
źródło

Niektóre sporadyczne skończone proste grupy (takie jak grupa Lyonsa zostały najpierw zbudowane przy użyciu komputera, tj. Dowód ich istnienia został (częściowo) wygenerowany komputerowo

— jp

Pytanie, czy „teoria złożoności exporymentalnej” jest używana do rozwiązywania otwartych problemów, jest z tym związane.

— adrianN

IMHO musisz dokładniej odróżnić „znalezione” od „zaznaczone”. Dowód Gonthiera i wsp. Zdecydowanie nie został znaleziony przez komputer.

— gallais

ładne pytanie, ale niestety prawie równoważne z tym, gdzie i jak komputery pomogły udowodnić thm

— vzn

Również bardzo podobne: Czy jakikolwiek wcześniej nieznany wynik został udowodniony przez automatyczną twierdzenie o twierdzeniach? .

— Petr Pudlák

Odpowiedzi:

Innym znanym przykładem jest dowód Halesa na przypuszczenie Keplera, który miał bardzo duży komponent wspomagany komputerowo.

Z Wikipedii :

W sierpniu 1998 r. Hales ogłosił, że dowód jest kompletny. Na tym etapie składało się z 250 stron notatek i 3 gigabajtów programów komputerowych, danych i wyników.

— Huck Bennett
źródło

Jest to raczej meta odpowiedź, ponieważ jest to lista list.

Dokumenty Dorona Zeilbergera . Jest matematykiem, a jego komputer jest wymieniony u współautora Shalosha B. Ekhada we wszystkich gazetach, w których komputer odgrywał rolę w uzyskiwaniu wyników.
Dzieło Georgesa Gonthiera . Opracował sprawdzony maszynowo dowód twierdzenia o czterech kolorach, a ostatnio pracował nad twierdzeniem Feita-Thompsona. Niedawno zakończył formalizację Twierdzenia o nieparzystym porządku.
Archiwum dowodów formalnych zawiera dowody sprawdzane za pomocą Isabelle i zawiera twierdzenia o poprawności algorytmów, twierdzenie Gaussa-Jordana, niektóre teorie porządku, teorię kategorii i wiele innych klasycznych wyników.
Formalizowanie 100 twierdzeń , zawiera sprawdzone maszynowo dowody niektórych słynnych twierdzeń.

— Vijay D.
źródło

Dzięki. Powinienem wyjaśnić, że moje pytanie nie dotyczy dowodów zweryfikowanych / zweryfikowanych przez komputery po odkryciu, ani wyników, w których komputer odegrał rolę, która je wywodzi (oczywiście wszyscy używamy komputerów w naszych badaniach, ale ostatecznie uzyskujemy samodzielną matematykę dowód, że nie możemy powiedzieć, że został „wyprowadzony” przez komputer). Szukam domysłów, których dowody zostały wygenerowane (w całości lub w części) przez komputer.

— Mahdi Cheraghchi

Jednym z przykładów jest dowód nieistnienia rzutowej płaszczyzny rzędu 10 .

Zobacz Poszukiwanie skończonej rzutowej płaszczyzny rzędu 10 i Nieistnienie skończonych rzutowych płaszczyzn rzędu 10 .

— kbkb
źródło