Komputery rysowały atraktor Lorenza przez dziesięciolecia, zanim matematycy rygorystycznie dowiedli, że naprawdę istnieje
Edward Lorenz opisał w 1963 roku prosty układ trzech równań różniczkowych i zobaczył na komputerze słynny „motylowaty” atraktor. Numeryczne obrazy były niezwykle przekonujące, ale chaos jest właśnie dziedziną, w której błędy zaokrągleń mogą szybko rosnąć, więc sama symulacja nie jest dowodem. Warwick Tucker dopiero pod koniec lat 90. i w pracy z 2002 roku podał rygorystyczny, komputerowo wspomagany dowód, że dla klasycznych parametrów równania Lorenza rzeczywiście mają robustny dziwny atraktor. Między obrazem a twierdzeniem minęły dekady.
Lorenz zaczął od uproszczonego modelu atmosfery
Lorenz badał układ trzech nieliniowych równań różniczkowych opisujących uproszczoną konwekcję. Model jest krótki w porównaniu z prawdziwą atmosferą, ale jego rozwiązania wykazywały bardzo nietypowe zachowanie: trajektorie pozostawały w ograniczonym obszarze, nie osiadały na prostym cyklu i były niezwykle wrażliwe na stan początkowy. Wykres w przestrzeni trzech zmiennych zaczął przypominać dwa skrzydła.
Wykres z komputera nie jest automatycznie dowodem
Symulacja równań wymaga skończonego kroku czasowego i liczb zapisanych z ograniczoną dokładnością. W układzie chaotycznym niewielkie błędy numeryczne rosną, więc pojedyncza policzona trajektoria po długim czasie nie musi być bliska dokładnej trajektorii rozpoczynającej się w tym samym punkcie. Obraz może sugerować strukturę, ale nie gwarantuje, że obserwowany atraktor nie jest artefaktem przybliżenia.
Problem trafił na listę Smale’a
Stephen Smale umieścił rygorystyczne zrozumienie klasycznych równań Lorenza wśród ważnych problemów dla matematyki XXI wieku. Chodziło nie o kolejne ładne wizualizacje, lecz o dowód, że konkretne równania z parametrami używanymi przez Lorenza rzeczywiście mają strukturę odpowiadającą matematycznemu pojęciu dziwnego atraktora.
Tucker połączył teorię z kontrolowaną arytmetyką komputerową
Warwick Tucker użył normal forms oraz arytmetyki przedziałowej, w której komputer śledzi nie jedną przybliżoną liczbę, lecz przedział gwarantujący zawarcie prawdziwej wartości. Dzięki zaokrągleniom prowadzonym w kontrolowany sposób obliczenia stają się częścią dowodu, a nie tylko eksperymentem. W 1999 opublikował krótką wersję wyniku, a w 2002 pełniejsze rozwiązanie związane z problemem Smale’a.
Dowód pokazał więcej niż „obraz wygląda chaotycznie”
Tucker wykazał istnienie robustnego dziwnego atraktora dla klasycznych parametrów oraz trwałość tej struktury przy małych zmianach współczynników. To znacznie mocniejsze stwierdzenie niż obserwacja, że jeden komputerowy wykres wygląda nieregularnie. Rygorystyczny rezultat dotyczy całego przepływu równań i określonego zakresu zachowań, nie jednej wybranej symulacji.
To przykład, gdzie komputer pomógł zamknąć lukę między eksperymentem i dowodem
Historia Lorenza pokazuje dwie role komputera w matematyce. Najpierw maszyna ujawniła zjawisko, którego nikt nie oczekiwał i które zainspirowało teorię chaosu. Później komputer wrócił w zupełnie innej roli: jako kontrolowany element rygorystycznego dowodu. Prosta trójka równań wygenerowała więc zarówno jeden z najsłynniejszych obrazów matematyki, jak i wieloletni problem dotyczący podstaw tego obrazu.
Później zweryfikowano nawet sam rygorystyczny solver użyty w tej historii
Historia nie skończyła się na dowodzie Tuckera. W 2018 roku opublikowano formalnie zweryfikowany w systemie Isabelle/HOL solver równań różniczkowych zdolny certyfikować obliczenia stanowiące rdzeń jego argumentu. To dodatkowa warstwa kontroli: nie tylko matematycy analizują teorię i błędy numeryczne, ale część logiki działania programu zostaje sprawdzona przez formalny system dowodowy. Lorenz stał się więc przykładem całej ewolucji matematyki komputerowej — od nieformalnego eksperymentu numerycznego, przez rygorystyczny dowód wspomagany komputerem, aż po formalną weryfikację narzędzia wykonującego kluczowe obliczenia.