Sztuczna inteligencja zdobywa medale na olimpiadach matematycznych i weryfikuje dowody, których ludzie nie byli pewni. Polak z UAM na łamach „Nature” wyjaśnia rewolucję.
W skrócie:
- Polski naukowiec, Bartosz Naskręcki z Uniwersytetu Adama Mickiewicza, wraz z Kenem Ono opublikował w prestiżowym „Nature Physics” artykuł o rewolucyjnym wpływie AI na matematykę.
- System AlphaGeometry od Google DeepMind osiągnął poziom srebrnego medalisty na Międzynarodowej Olimpiadzie Matematycznej, samodzielnie rozwiązując złożone zadania z geometrii.
- Narzędzia AI, takie jak asystenci dowodzenia (np. Lean), pozwalają na formalną weryfikację skomplikowanych teorii, co udowodnił przełomowy projekt „liquid tensor experiment”.
Matematyka, królowa nauk, przez stulecia wydawała się ostatnim bastionem ludzkiego intelektu. Miejscem, gdzie intuicja, kreatywność i abstrakcyjne myślenie triumfują nad surową mocą obliczeniową. Cóż, ten bastion właśnie drży w posadach. A o skali tego wstrząsu piszą na łamach prestiżowego „Nature Physics” Polak, dr hab. Bartosz Naskręcki z Uniwersytetu Adama Mickiewicza w Poznaniu, oraz Ken Ono z University of Virginia. Ich komentarz, zatytułowany „Mathematical discovery in the age of artificial intelligence”, to nie jest kolejny futurologiczny esej. To rzeczowa, momentami mrożąca krew w żyłach, analiza rewolucji, która dzieje się na naszych oczach.
Jak AI w ogóle „rozumie” matematykę?
Zapomnijmy na chwilę o obrazie humanoidalnego robota kreślącego wzory na tablicy. Prawdziwa rewolucja zaczyna się gdzie indziej – w procesie zwanym formalizacją. Matematycy od wieków posługują się językiem, który jest mieszanką symboli i języka naturalnego. Jest precyzyjny, ale dla maszyny – wciąż niejednoznaczny. Sztuczna inteligencja potrzebuje czegoś twardszego. Potrzebuje dowodów rozpisanych krok po kroku, w języku, który nie pozostawia cienia wątpliwości. Tutaj na scenę wchodzą tak zwani asystenci dowodzenia (proof assistants), jak choćby Lean, Coq czy Isabelle. To systemy, które pozwalają przekształcić „ludzką” matematykę w kod, który komputer może zweryfikować linijka po linijce.
Przez lata było to zadanie tytaniczne, zarezerwowane dla garstki specjalistów. Jednak, jak wskazują Naskręcki i Ono, dzięki dużym modelom językowym proces ten gwałtownie przyspiesza. AI uczy się tłumaczyć nieformalne notatki matematyka na rygorystyczny, formalny język. To trochę tak, jakby dać maszynie zdolność czytania między wierszami i zamieniania intuicyjnych przeskoków myślowych w logiczny, niepodważalny ciąg argumentów. Efekt? Drzwi do weryfikacji i tworzenia matematyki na niespotykaną dotąd skalę zostały wyważone.
Czy maszyna może być geniuszem geometrii?
Odpowiedź brzmi: tak, i ma już na to dowody w postaci medali. Na początku 2024 roku zespół Google DeepMind ogłosił, że ich system, AlphaGeometry, osiągnął poziom srebrnego medalisty w zadaniach z geometrii na Międzynarodowej Olimpiadzie Matematycznej (IMO). To nie jest proste rozwiązywanie równań. Mówimy o problemach, które wymagają od ludzkich uczestników nie tylko wiedzy, ale też niezwykłej kreatywności i „geometrycznej intuicji”. AlphaGeometry, trenowany na miliardach syntetycznych przykładów, nauczył się tej intuicji. Potrafi „dostrzec” pomocnicze konstrukcje i znaleźć ścieżki dowodowe, które umykają nawet utalentowanym uczniom.
Co to oznacza w praktyce? Oznacza to, że AI przestała być tylko potężnym kalkulatorem. Zaczyna wkraczać na pole zarezerwowane dla twórczego geniuszu. System nie tylko sprawdza, ale i tworzy. „Narzędzia te przekształcają sposób, w jaki prowadzone są badania matematyczne” – podkreślają autorzy w „Nature Physics”. To już nie jest science fiction. To nowa rzeczywistość, w której matematyk może mieć cyfrowego partnera do burzy mózgów – partnera, który potrafi w ciągu kilku sekund przeanalizować miliony potencjalnych rozwiązań.
Kto pilnuje, żeby dowody nie miały błędów?
Historia matematyki pełna jest dowodów, które zawierały subtelne błędy, odkrywane dopiero po latach. Słynny dowód Wielkiego Twierdzenia Fermata liczył ponad 100 stron i był zrozumiały tylko dla garstki ekspertów na świecie. Co, jeśli w tak złożonym rozumowaniu kryje się błąd? Tu właśnie wkracza AI ze swoją nadludzką skrupulatnością. Przełomowym momentem był tak zwany „liquid tensor experiment”. W 2020 roku czołowy matematyk, Peter Scholze, rzucił wyzwanie społeczności, by sformalizować jeden z kluczowych dowodów w jego teorii. Przez kilka miesięcy zespół ekspertów, używając asystenta Lean, przekuł jego idee na w pełni weryfikowalny przez maszynę kod. Udało się. Komputer potwierdził: dowód jest poprawny.
Ten sukces pokazał, że asystenci dowodzenia stają się kluczowym narzędziem gwarantującym poprawność najbardziej skomplikowanych teorii matematycznych. To polisa ubezpieczeniowa dla całej nauki. Bartosz Naskręcki i Ken Ono nie mają wątpliwości, że przyszłość to ścisła współpraca człowieka z maszyną. Matematyk będzie dostarczał wizję i intuicję, a AI zadba o rygor, sprawdzi każdy detal i zaproponuje nowe, nieoczywiste ścieżki. To nie koniec matematyków. To narodziny matematyków-cyborgów, których możliwości poznawcze będą wykraczać poza wszystko, co znaliśmy do tej pory.