Najdłuższy dowód matematyczny w historii

| Ciekawostki
camknows, CC

Marijn Heule z University of Texas, Oliver Kullmann ze Swansea University oraz Victor Marek z University of Kentucky - były pracownik Uniwersytetu Warszawskiego, a obecny współpracownik Instytutu Podstaw Informatyki PAN - użyli superkomputera do przeprowadzenia pojedynczego matematycznego dowodu, uzyskując w ten sposób największy matematyczny dowód w historii. Jego zapisanie zajęło 200 terabajtów przestrzeni dyskowej.

Uczeni postawili przed maszyną zadanie rozwiązania problemu pokolorowania trójek pitagorejskich. To problem sformułowany w latach 80. przez Ronalda Grahama. Trójki pitagorejskie to liczby a, b, c spełniające równanie a2+b2=c2. Graham zapytał, czy da się pokolorować wszystkie liczby naturalne za pomocą niebieskiego i czerwonego tak, by żadna z trójek pitagorejskich nie była jednobarwna, czyli by w równaniu występowały oba kolory.

Problem ten rozwiązali dopiero Heule, Kullmann i Marek. Zaprzęgli oni do pracy superkomputer, którego zadaniem byłó analizowanie wszystkich możliwych kombinacji kolorowania liczb. Okazało się, że do liczby 7824 możliwe było takie kolorowanie liczb, by tworzone z nich trójki pitagorejskie były dwubarwne. Jednak już przy 7825 co najmniej jedna trójka pitagorejska miała wszystkie liczby w tym samym kolorze.

Zadanie było niewykonalne dla człowieka, ale i superkomputer miał z nim poważne problemy. By rozwiązać je w rozsądnym czasie naukowcy ograniczyli do biliona liczbę kombinacji, jaki może sprawdzać maszyna. Mimo to korzystający z 800 procesorów komputer pracował nad rozwiązaniem przez 48 godzin.

Wyniki uzyskane przez maszynę zostały następnie zweryfikowane za pomocą innego oprogramowania, które je potwierdziło. Powstaje jednak pytanie, czy, jako że dowód zajmuje 200 terabajtów i nikt nie jest w stanie go przeczytać, Graham powinien wypłacić obiecane przez siebie 100 dolarów za rozwiązanie problemu.

dowód matematyczny trójka pitagorejska kolorowanie Graham