Dowody znalezione przez komputer

11

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).

soft-question big-list proofs automated-theorem-proving Mahdi Cheraghchi
źródło
2
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
1
ł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:

12

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
10

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

  1. 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.

  2. 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.

  3. 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.

  4. Formalizowanie 100 twierdzeń , zawiera sprawdzone maszynowo dowody niektórych słynnych twierdzeń.

Vijay D.
źródło
1
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