Lista długich dowodów matematycznych

To jest lista niezwykle długich dowodów matematycznych . Takie dowody często wykorzystują obliczeniowe metody dowodowe i można je uznać za niepodlegające przeglądowi .

Od 2011 r. Najdłuższym dowodem matematycznym, mierzonym liczbą opublikowanych stron czasopism, jest klasyfikacja skończonych grup prostych, obejmująca znacznie ponad 10 000 stron. Istnieje kilka dowodów, które byłyby znacznie dłuższe, gdyby szczegóły obliczeń komputerowych, na których polegają, zostały opublikowane w całości.

Długie dowody

Długość niezwykle długich dowodów wzrosła z czasem. Z grubsza przyjmuje się, że 100 stron w 1900, 200 stron w 1950 lub 500 stron w 2000 to niezwykle długi dowód.

1799 Twierdzenie Abela-Ruffiniego zostało prawie udowodnione przez Paolo Ruffiniego , ale jego dowód, obejmujący 500 stron, został w większości zignorowany, a później, w 1824 roku, Niels Henrik Abel opublikował dowód, który wymagał zaledwie sześciu stron.
1890 Klasyfikacja prostych złożonych algebr Liego dokonana przez Killinga, w tym jego odkrycie wyjątkowych algebr Liego , zajęła 180 stron w 4 artykułach.
1894 Konstrukcja linijki i kompasu wielokąta o 65537 bokach autorstwa Johanna Gustava Hermesa zajęła ponad 200 stron.
1905 Oryginalny dowód twierdzenia Laskera-Noethera Emanuela Laskera zajął 98 stron, ale od tego czasu został uproszczony: współczesne dowody mają mniej niż stronę.
1963 Twierdzenie o nieparzystym porządku Feita i Thompsona miało 255 stron, co w tamtym czasie było ponad 10 razy dłuższe niż to, co wcześniej uważano za długi artykuł z teorii grup.
1964 Rozdzielczość osobliwości . Oryginalny dowód Hironaki miał 216 stron; od tego czasu został znacznie uproszczony do około 10 lub 20 stron.
1966 Dowód Abyhankara na rozwiązanie osobliwości dla 3-krotnej charakterystyki większej niż 6 obejmował około 500 stron w kilku artykułach. W 2009 Cutkosky uprościł to do około 40 stron.
1966 Reprezentacje szeregów dyskretnych grup Liego. Ich konstrukcja przez Harisha-Chandrę obejmowała długą serię artykułów obejmujących łącznie około 500 stron. Jego późniejsza praca nad twierdzeniem Plancherela dla grup półprostych dodała do nich kolejne 150 stron.
1968 Novikov - Adian dowód rozwiązujący problem Burnside'a na skończenie generowanych nieskończonych grupach ze skończonymi wykładnikami ujemnie. Trzyczęściowy oryginalny artykuł ma ponad 300 stron. (Britton opublikował później 282-stronicowy artykuł, w którym próbował rozwiązać ten problem, ale jego artykuł zawierał poważną lukę).
1960-1970 Fondements de la Géometrie Algébrique , Éléments de géométrie algébrique i Séminaire de géométrie algébrique . Praca Grothendiecka na temat podstaw geometrii algebraicznej obejmuje wiele tysięcy stron. Chociaż nie jest to dowód jednego twierdzenia, jest w nim kilka twierdzeń, których dowody zależą od setek wcześniejszych stron. ^{[ wątpliwe – dyskutuj ]}
1974 Twierdzenie o grupie N. Klasyfikacja Thompsona grup N obejmowała 6 artykułów o łącznej objętości około 400 stron, ale wykorzystała również jego wcześniejsze wyniki, takie jak twierdzenie o nieparzystym porządku , które dają łączną długość do ponad 700 stron.
1974 Przypuszczenie Ramanujana i przypuszczenia Weila . Chociaż ostatni artykuł Deligne'a dowodzący tych przypuszczeń miał „tylko” około 30 stron, zależał od wyników tła w geometrii algebraicznej i kohomologii etalnej , które Deligne oszacował na około 2000 stron.
1974 Twierdzenie o 4 kolorach . Dowód tego przeprowadzony przez Appela i Hakena zajął 139 stron i opierał się również na długich obliczeniach komputerowych.
1974 Twierdzenie Gorensteina-Harady klasyfikujące skończone grupy przekrojowe o 2-rzędowym co najwyżej 4 miało 464 strony.
Seria Eisensteina z 1976 roku . Dowód Langlandsa na równanie funkcjonalne dla szeregu Eisensteina miał 337 stron.
1983 Twierdzenie o trychotomii . Dowód Gorensteina i Lyonsa dla przypadku rangi co najmniej 4 miał 731 stron, a dowód Aschbachera dla przypadku rangi 3 dodaje kolejne 159 stron, w sumie 890 stron.
1983 Wzór śladu Selberga . Dowód Hejhala ogólnej postaci formuły śladu Selberga składał się z 2 tomów o łącznej długości 1322 stron.
Formuła śladowa Arthura – Selberga . Dowody Arthura dotyczące różnych wersji tego obejmują kilkaset stron rozłożonych na wiele artykułów.
2000 Twierdzenie Almgrena o regularności . Dowód Almgrena miał 955 stron.
2000 Twierdzenie Lafforgue'a o hipotezie Langlandsa dla ogólnej grupy liniowej nad polami funkcyjnymi. Dowód Laurenta Lafforgue'a na to miał około 600 stron, nie licząc wielu stron wyników w tle.
2003 Hipoteza Poincarégo , Twierdzenie o geometryzacji , Hipoteza o geometryzacji . Oryginalne dowody Perelmana hipotezy Poincarégo i hipotezy geometryzacji nie były długie, ale były raczej pobieżne. Kilku innych matematyków opublikowało dowody z wypełnionymi szczegółami, które zajmują kilkaset stron.
2004 Grupy quasihin . Klasyfikacja prostych grup quasitynowych dokonana przez Aschbachera i Smitha miała 1221 stron i była jedną z najdłuższych pojedynczych prac, jakie kiedykolwiek napisano.
2004 Klasyfikacja skończonych grup prostych . Dowód na to jest rozłożony na setki artykułów w czasopismach, co utrudnia oszacowanie całkowitej długości, która prawdopodobnie wynosi od 10 000 do 20 000 stron.
2004 Twierdzenie Robertsona – Seymoura . Dowód zajmuje około 500 stron rozłożonych na około 20 artykułów.
2005 Przypuszczenie Keplera . Dowód Halesa na to obejmuje kilkaset stron opublikowanych argumentów wraz z kilkoma gigabajtami obliczeń komputerowych.
2006 twierdzenie o silnym grafie doskonałym autorstwa Marii Chudnovsky , Neila Robertsona , Paula Seymoura i Robina Thomasa. 180 stron w Annals of Mathematics .

Długie obliczenia komputerowe

Istnieje wiele twierdzeń matematycznych, które zostały sprawdzone przez długie obliczenia komputerowe. Gdyby zostały one zapisane jako dowody, wiele z nich byłoby znacznie dłuższych niż większość powyższych dowodów. Tak naprawdę nie ma wyraźnego rozróżnienia między obliczeniami komputerowymi a dowodami, ponieważ kilka z powyższych dowodów, takich jak twierdzenie o 4 kolorach i hipoteza Keplera, wykorzystuje długie obliczenia komputerowe, a także wiele stron argumentów matematycznych. W przypadku obliczeń komputerowych w tej sekcji argumenty matematyczne mają tylko kilka stron, a długość wynika z długich, ale rutynowych obliczeń. Niektóre typowe przykłady takich twierdzeń obejmują:

Kilka dowodów na istnienie sporadycznych grup prostych , takich jak grupa Lyonsa , pierwotnie wykorzystywało obliczenia komputerowe z dużymi macierzami lub permutacjami miliardów symboli. W większości przypadków, takich jak grupa małych potworów , dowody komputerowe zostały później zastąpione krótszymi dowodami unikającymi obliczeń komputerowych. Podobnie obliczenie maksymalnych podgrup większych grup sporadycznych wykorzystuje wiele obliczeń komputerowych.
2004 Weryfikacja hipotezy Riemanna dla pierwszych 10 ¹³ zer funkcji zeta Riemanna .
2007 Weryfikacja, że warcaby to remis.
2008 Dowody, że różne liczby Mersenne'a z około dziesięcioma milionami cyfr są pierwsze.
Obliczenia dużych liczb cyfr liczby π.
2010 Pokazanie, że Kostkę Rubika można ułożyć w 20 ruchach .
2012 Pokazuje, że Sudoku potrzebuje co najmniej 17 wskazówek .
2013 Trójskładnikowa hipoteza Goldbacha : Każda liczba nieparzysta większa niż 5 może być wyrażona jako suma trzech liczb pierwszych.
2014 Dowód hipotezy rozbieżności Erdősa dla konkretnego przypadku C = 2: każda sekwencja ± 1 o długości 1161 ma rozbieżność co najmniej 3; oryginalny dowód, wygenerowany przez solver SAT, miał rozmiar 13 gigabajtów, a później został zmniejszony do 850 megabajtów.
2016 Rozwiązanie problemu potrójnych boolowskich pitagorejczyków wymagało wygenerowania 200 terabajtów dowodu.
2017 Marijn Heule , który był współautorem rozwiązania problemu potrójnych boolowskich pitagorejczyków, ogłosił dowód o długości 2 petabajtów, że piąta liczba Schura to 161.

Długie dowody w logice matematycznej

Kurt Gödel pokazał, jak znaleźć jednoznaczne przykłady zdań w systemach formalnych, które są w tym systemie dowodliwe, ale których najkrótszy dowód jest absurdalnie długi. Na przykład stwierdzenie:

„Tego stwierdzenia nie można udowodnić w arytmetyce Peano za pomocą mniej niż symboli googolplex”

jest dowodliwy w arytmetyce Peano, ale najkrótszy dowód ma co najmniej symbole googolplex. Ma krótki dowód w potężniejszym systemie: w rzeczywistości można go łatwo udowodnić w arytmetyce Peano wraz ze stwierdzeniem, że arytmetyka Peano jest spójna (czego nie można udowodnić w arytmetyce Peano za pomocą twierdzenia Gödla o niezupełności ) .

W tym argumencie arytmetykę Peano można zastąpić dowolnym bardziej wydajnym spójnym systemem, a googolplex można zastąpić dowolną liczbą, którą można zwięźle opisać w systemie.

Harvey Friedman znalazł kilka wyraźnych naturalnych przykładów tego zjawiska, podając kilka wyraźnych zdań w arytmetyce Peano i innych systemach formalnych, których najkrótsze dowody są absurdalnie długie ( Smoryński 1982 ). Na przykład oświadczenie

„istnieje taka liczba całkowita n , że jeśli istnieje ciąg zakorzenionych drzew T ₁ , T ₂ , ..., T _n taki, że T _k ma co najwyżej k +10 wierzchołków, to pewne drzewo może być homeomorficznie osadzone w późniejszym jeden"

⁰ jest dowodliwy w arytmetyce Peano, ale najkrótszy dowód ma długość co najmniej ¹⁰⁰⁰ 2, gdzie 2 = 1 i ^{n + 1} 2 = 2 ^{( ⁿ 2)} ( wzrost tetracyjny ). Stwierdzenie to jest szczególnym przypadkiem twierdzenia Kruskala i ma krótki dowód w arytmetyce drugiego rzędu .

Zobacz też

Krantz, Steven G. (2011), Dowód jest w puddingu. Zmieniający się charakter dowodu matematycznego (PDF) , Berlin, Nowy Jork: Springer-Verlag , doi : 10.1007/978-0-387-48744-1 , ISBN 978-0-387-48908-7 , MR 2789493
Smoryński, C. (1982), "Odmiany doświadczenia nadrzewnego", Math. Intelligencer , 4 (4): 182–189, doi : 10.1007/bf03023553 , MR 0685558 , S2CID 125748405