Dlaczego komputerowi tak trudno jest coś udowodnić?

To może być uznane za głupie pytanie. Nie jestem informatyką (i jeszcze nie jestem matematyką), więc przepraszam, jeśli uważasz, że poniższe pytania zawierają pewne błędne założenia.

Chociaż istnieją plany sformalizowania ostatniego twierdzenia Fermata (patrz ta prezentacja ), nigdy nie czytałem ani nie słyszałem, że komputer może udowodnić nawet „proste” twierdzenie takie jak Pitagoras ”.

Dlaczego nie? Jaka jest (są) główna trudność (trudności) w ustanowieniu w pełni autonomicznego dowodu przez komputer, wspomagany tylko przez niektóre „wbudowane aksjomaty”?

Drugie pytanie, które chciałbym zadać, brzmi: dlaczego jesteśmy w stanie sformalizować wiele dowodów, podczas gdy komputer nie jest w stanie samodzielnie udowodnić twierdzenia? Dlaczego to „trudniejsze”?

automated-theorem-proving

— Max Muller
źródło

Dwie główne trudności. Niekompletność (patrz Twierdzenia Gödla) i ogromny rozmiar przestrzeni poszukiwań (jest znacznie więcej nieciekawych twierdzeń niż ciekawych). Osiągnięto znaczny postęp dzięki asystentom dowodowym (Coq, Isabelle, Agda itp.). Za ich pomocą matematyk pisze twierdzenia i lematy, a asystent dowodu pomaga znaleźć dowody i zapewnia ich logiczną ważność.

— Dave Clarke

@Dave Clarke: ok, więc faktycznie mówisz, że komputer jest w stanie udowodnić (nowe) twierdzenia, ale ogromna liczba możliwych wyszukiwań utrudnia mu / jej / jej napisanie twierdzenia, które ma jakąkolwiek wartość lub jest interesujące, czy mam rację? Czy mógłbyś wyjaśnić, dlaczego twierdzenia Gödla i „Niepełność” są tutaj istotne? Ponadto, czy masz odniesienie do artykułu badawczego lub artykułu z ankiety, w którym wykazano, że komputer faktycznie dowodzi twierdzenia? Wreszcie, czy jest wiele badań nad próbą przekonania komputerów do twierdzeń? Jak nazywa się ten obszar badań (ciąg dalszy ...)

— Max Muller

i czy znasz dobry materiał wprowadzający? Jakie są warunki wymagane zarówno w matematyce, jak i informatyce, aby zrozumieć ten materiał?

— Max Muller

Być może zainteresują Cię niektóre prace Doriana Zeilbergera, takie jak „ Nauczanie komputera odkrywać (!), A następnie Udowodnij (!!) (wszystko przez siebie (!!!)) Analogi notorycznej przypowieści Collatza 3x + 1 ” ( math.rutgers.edu/~zeilberg/mamarim/mamarimhtml/collatz.html ). Częstym współautorem Zeilbergera, Shalosh B. Ekhad, jest komputer.

— Rob Simmons,

Poniższe pytanie podaje również kilka dobrych przykładów komputerów pomagających udowodnić twierdzenia: cstheory.stackexchange.com/questions/82/...

— Mugizi Rwebangira

Odpowiedzi:

Chociaż istnieją plany sformalizowania ostatniego twierdzenia Fermata (patrz ta prezentacja), nigdy nie czytałem ani nie słyszałem, że komputer może udowodnić nawet „proste” twierdzenie takie jak Pitagoras ”.

W 1949 r. Tarski udowodnił, że prawie wszystko w Elementach mieści się w rozstrzygającym fragmencie logiki, gdy wykazał rozstrzygalność teorii pierwszego rzędu rzeczywistych zamkniętych pól. W szczególności twierdzenie Pitagorasa nie mówi zbyt wiele, ponieważ nie jest szczególnie trudne.

$A$ $A$

$A$ $B$ $A$

— Neel Krishnaswami
źródło

Dwie główne trudności. Niekompletność (patrz Twierdzenia o niekompletności Gödla) i ogromna wielkość przestrzeni poszukiwań (jest znacznie więcej nieciekawych twierdzeń niż ciekawych). Osiągnięto znaczny postęp dzięki asystentom dowodowym ( Coq , Isabelle, Agda itp.). Za ich pomocą matematyk pisze twierdzenia i lematy, a asystent dowodu pomaga znaleźć dowody i zapewnia ich logiczną ważność.

$P$ $Q$ $P\wedge Q$

W tym artykule opisano, w jaki sposób stosuje się asystenta dowodu Coqa do udowodnienia twierdzenia o czterech kolorach. Matematyka zmechanizowana ( przegląd ) jest jednym z obszarów TCS poświęconym (częściowo) automatycznemu dowodzeniu twierdzeń (i na ogół używaniu komputerów do pomocy matematykom).

Jednym z obszarów, w którym automatyczne dowodzenie twierdzeń (swego rodzaju) ma wpływ, jest sprawdzanie i znajdowanie modeli. Sprawdzanie modelu zajmuje się określaniem, czy dany system spełnia daną właściwość, podczas gdy wyszukiwanie modelu znajduje system spełniający daną kolekcję właściwości. Narzędzie Alloy wykorzystuje sprawdzanie modeli i znajdowanie modeli z dobrym skutkiem i jest całkiem użyteczne.

— Dave Clarke
źródło

Nie mogłem wybierać między tymi dwiema odpowiedziami, ponieważ obie są świetne. Rzuciłem monetą, aby zdecydować, którą wybrać. Przepraszam, nie wybrałem twojego! W każdym razie bardzo dziękuję.

— Max Muller,

Niektóre wygrywasz, niektóre tracisz.

— Dave Clarke,

Mniej techniczna, bardziej matematyczny rachunek dowodu czterech kolorów, a jego znaczenie zostało opublikowane w ostatnim numerze Anonse AMS (cała sprawa może być wskazane lekturą dla osób zainteresowanych w pytaniu OP).

— Francois G,