topPart Wydział Matematyki i Informatyki UJ Katedra Matematyki Obliczeniowej UJ

Komputerowo wspierane dowody

Z gruba rzecz biorąc, komputerowo wspierany dowód polega na:

Problem czterech barw

W 1852 roku Francis Guthrie, student University College w Londynie postawił problem: czy każdą mapę polityczną daje się pokolorować przy użyciu co najwyżej czterech kolorów tak, by żadne dwie przylegające do siebie jednoski administracyjne nie były pokolorowane tym samym kolorem. Problem ten przedstawił swojemu profesorowi, Augustowi de Morganowi, który, nie umiejąc sam znaleźć odpowiedzi, poprosił o pomoc szereg innych matematyków. Tak m.in. problem ten trafił na forum Londyńskiego Towarzystwa Matematycznego, W roku 1879 Alfred Kempe opublikował w Nature dowód hipotezy o czterech barwach, który przez jedenaonie lat uchodził za poprawny. Po odkryciu błędu w dowodzie problem zyskał na atrakcyjnooci i był bez powodzenia atakowany przez licznych matematyków przez blisko 100 lat. Z początkiem drugiej połowy XX wieku niemiecki matematyk Heinrich Heesch doszedł do wniosku, że przeprowadzenie dowodu może wymagać przeanalizowania bardo dużej, jednak skończonej liczby przypadków.

W 1970 roku amerykańscy matematycy Kenneth Appel i Wolfgang Haken zdecydowali się sięgnąć po pomoc komputera, by te przypadki wygenerować i je przeanalizować. Praca ta zakończyła się sukcesem po szeociu latach pracy nad potrzebnymi algorytmami i oprogramowaniem, 1200 godzinach pracy trzech dużych komputerów, które znalazły i przeanalizowały 1936 t.zw. konfiguracji.

Dowód twierdzenia o czterech barwach był pierwszym spektakularnym osiągnięciem matematyki komputerowej w samej matematyce. Na początku wzbudzał kontrowersje, ale po przeprowadzeniu szeregu niezależnych podobnych dowodów ostatecznie problem czterech barw uznany został za rozstrzygnięty.

Hipoteza Feigenbauma

Pod koniec lat 70-tych dwudziestego wieku M. Feigenbaum i inni matematycy zaobserwowali, że w jednoparametrowej rodzinie odwzorowań unimodalnych odcinka w siebie występują kolejne bifurkacje podwojenia okresu, a stosunki odległooci pomiędzy kolejnymi bifurkacjami zmierzają do stałej 4.669... .

W 1982 roku Oscar E. Lanford opublikował w prestiżowym Bulletin American Mathematical Society komputerowo wspierany dowód tego faktu. W tym celu sprowadził on problem do istnienia punktu stałego pewnego operatora w stosownej przestrzeni funkcyjnej i przy wykorzystaniu ocisłych obliczeń komputerowych znalazł stałą Lipschitza tego operatora, która okazała się być mniejsza od jeden, co pozwalało wnioskować o istnieniu punktu stałego.

Praca Lanforda uchodzi za pierwszy w historii przykład komputerowo wspieranego dowodu ważnego nierozwiązanego problemu spoza matematyki dyskretnej.

Chaos w równaniach Lorenza

Z końcem XIX wieku postępy w fizyce i matematyce sprawiły, że problem uzyskiwania pewnych prognoz pogody wydawał się bliski rozwiązania. Od strony teoretycznej wszystko było opracowane. Znane były równania różniczkowe opisujące stan atmosfery. Wystarczyło dokonać dokładnego pomiaru stanu atmosfery, wstawić wyniki pomiarów do równania i rozwiązać je, by uzyskać prognozę. Jedyną przeszkodą była wielka ilooć obliczeń potrzebnych do rozwiązania równania.

Wraz z pojawieniem się w połowie XX wieku komputerów odrodziły się nadzieje na uzyskiwanie pewnych prognoz pogody, bo duża ilooć obliczeń przestała być przeszkodą. Jednak przygotowywane tak prognozy nie sprawdzały się. W 1963 amerykański matematyk i meteorolog Edward Lorenz, usiłując zrozumieć dlaczego prognozy pogody nie udają się, odkrył zjawisko zwane deterministycznym chaosem. W równaniu różniczkowym, pomimo jego deterministycznego charakteru, mogą zachodzić procesy chaotyczne. Wyjaoniało to dlaczego numeryczne prognozy pogody nie są łatwe do uzyskania nawet na bardzo szybkich komputerach.

Lorenzowi nie udało się nadać swemu odkryciu formy matematycznego twierdzenia. Podał jednak przykład prostego układu równań różniczkowych trzech zmiennych, w którym podejrzewał istnienie chaosu.

Odkrycie Lorenza wydawało się sprzeczne z ówczesnym stanem wiedzy na temat zachowania się rozwiązań równań różniczkowych i początkowo matematycy nie chcieli dawać wiary, że jest to możliwe. Wkrótce jednak udało się skonstruować przykłady prostych układów dynamicznych, w których zjawisko chaosu można było udowodnić. Istnienie chaosu w równaniach Lorenza pozostawało jednak nierozstrzygnięte do roku 1995, kiedy to Marian Mrozek z Instytutu Informatyki UJ oraz Konstantin Mischaikow z Georgia Institute of Technology, Atlanta, USA opublikowali w Bulletin of the American Mathematical Society komputerowo wspierany dowód tego faktu. Wynik ten został uznany przez Encyclopedia Britannica za jedno z czterech największych na owiecie osiągnieć w matematyce w 1995 roku. Dowód opierał się na wykorzystaniu pewnego niezmiennika topologicznego równań różniczkowych, który udało się dla równania Lorenza wyliczyć przy pomocy komputera w oparciu o metody ocisłej analizy numerycznej równania różniczkowego. W pierwotnej wersji wymagało to około 80 godzin obliczeń, choć dzio dzięki szybszym komputerom, a przede wszystkim lepszym algorytmom potrzebne rachunki daje się przeprowadzić w kilka minut.

Warto dodać, że w 1999 roku Warwick Tucker w swojej pracy doktorskiej wzmocnił wynik Mrozka i Mischaikowa podając komputerowo wspierany dowód chaotycznooci atraktora w równaniach Lorenza.

Hipoteza Keplera

W 1611 roku Johannes Kepler sformułował hipotezę o optymalnym upakowaniu kul. Hipoteza ta mówi, że jeoli chcemy ulokować w pojemniku możliwie dużo kul o jednakowym promieniu, to optymalne ulokowanie uzyskamy układając warstę kul o orodkach w wierzchołkach szeociokątnej sieci na płaszczyźnie, na niej kolejną taką warstwę przesuniętą tak by znalazła się w najniższym punkcie i tak dalej.

Kepler nie potrafił udowodnić swojej hipotezy. Pierwszy istotny krok w stronę dowodu uczynił Carl Friedrich Gauss, który w 1831 roku pokazał, że jeoli istnieje rozwiązanie lepsze od zaproponowanego przez Keplera, to musi ono być rozlokowane w nieregularnej sieci punktów.

W 1953 roku węgierski matematyk László Fejes Tóth pokazał, że problem znalezienia optymalnej konfiguracji może zostać sprowadzony do przeanalizowania problemu skończonego.

Plan ten został zrealizowany przez amerykańskiego matematyka Thomasa Halesa. Sprowadził on problem do minimalizacji funkcji 150 zmiennych i wykorzystując komputer do rozwiązania około 100 000 problemów optymalizacji liniowej w 1998 ogłosił, że dowód jest kompletny. Dowód tego twierdzenia, po sprawdzeniu pracy przez 12 niezależnych recenzentów, opublikowany został w 2005 roku w Annals of Mathematics.