Świat matematyki wkracza w znaczącą zmianę. Sztuczna inteligencja nie pomaga już tylko w obliczeniach, ale jest teraz w stanie sprawdzać złożone dowody matematyczne, co było zadaniem wcześniej zarezerwowanym wyłącznie dla ludzkich ekspertów. Ten przełom może przyspieszyć badania, wyeliminować błędy i zasadniczo zmienić sposób tworzenia i weryfikowania wiedzy matematycznej.
Wyzwanie formalizacji
Przez dziesięciolecia matematycy marzyli o automatycznym sprawdzaniu dowodów. Istniejące narzędzia mogą weryfikować dowody, ale tylko wtedy, gdy zostaną najpierw przetłumaczone na rygorystyczny format czytelny dla komputera, co jest procesem zwanym formalizacją. Jest to niezwykle żmudne i często wymaga miesięcy, a nawet lat żmudnej pracy. Problemem nie jest sama matematyka; ale w braku elastyczności języków programowania, które wymagają absolutnej precyzji tam, gdzie zapis ludzki może być bardziej płynny.
Math, Inc. i Gauss AI
Startup o nazwie Math, Inc. twierdzi, że pokonał tę barierę dzięki swojej sztucznej inteligencji o nazwie Gauss. Firma z sukcesem sformalizowała dwa przełomowe proofy autorstwa Mariny Wiazowskiej, która w 2022 roku otrzymała prestiżowy Medal Fieldsa za pracę nad opakowaniami kulistymi o większych wymiarach. Dowody te uznano za niezwykle złożone, a zdolność sztucznej inteligencji do ich automatycznego tłumaczenia jest ważnym krokiem naprzód.
Puzzle dotyczące pakowania kul: dlaczego jest to ważne
Badania Wiazowskiej rozwiązały klasyczny problem: jak najskuteczniej rozmieścić kule. W trzech wymiarach najciaśniejsze opakowanie przypomina układanie pomarańczy w sklepie spożywczym. Jednak wraz ze wzrostem wymiarów zadanie staje się wykładniczo trudniejsze. Wiazowska rozwiązała to dla ośmiu i 24 wymiarów, udowadniając, że przeniesienie efektywnych układów z niższych wymiarów może pomieścić dodatkową kulę w każdej wyższej przestrzeni.
To nie jest tylko abstrakcyjna teoria. Upakowanie kul ma zastosowanie w takich dziedzinach, jak teoria kodowania, inżynieria materiałowa, a nawet opracowywanie leków. Do postępu tych prac potrzebne są dokładne dowody.
Zerwana współpraca
Historia sukcesu Gaussa jest także przestrogą. Badacze współpracowali przez lata, aby ręcznie sformalizować dowody Vyazovskaya, dzieląc pracę na łatwiejsze do opanowania części dla społeczności zajmującej się formalizacją Lean. Math, Inc. po cichu wykorzystała ich postępy, a następnie opracowała sztuczną inteligencję, aby ukończyć zadanie w ciągu kilku tygodni, nie ujawniając w pełni jego postępów.
Jak ujął to Hariharan, jeden ze współautorów, „sztuczna inteligencja jest destrukcyjna”. Zespół planował wykorzystać ich sformalizowanie jako podstawę do napisania pracy dyplomowej, ale sztuczna inteligencja rozwiązała go pierwsza.
Przyszłość: sztuczna inteligencja jako obserwator matematyczny
Od tego czasu firma Math Inc. sformalizowała drugi dowód Wiazowskiej, generując 120 000 linii kodu Lean. Konsekwencje są dalekosiężne. Sztuczna inteligencja może nie tylko tłumaczyć dowody, ale także wykrywać i poprawiać błędy w oryginalnych artykułach.
Poiroux, założyciel Math, Inc., wyobraża sobie przyszłość, w której sztuczna inteligencja „kontroluje całą matematykę… i może nawet prześcignąć ludzi w badaniach”. Gdy sztuczna inteligencja w pełni zrozumie pojęcia matematyczne, będzie mogła podejść do nich w zupełnie nowy sposób i wygenerować nowe wyniki.
Rodzi to krytyczne pytania dotyczące roli matematyków. Czy sztuczna inteligencja stanie się ostatecznym arbitrem prawdy matematycznej? Rozwój Gaussa sugeruje, że odpowiedź może być bliżej, niż nam się wydaje.
