Dziesięć osiągnięć w matematyce i informatyce teoretycznej

Chcemy zapewnić naukowcom i matematykom narzędzia, które przyspieszają dokonywanie odkryć. Dlatego niedawno ogłosiliśmy inicjatywę ChatGPT dla badaczy akademickich⁠, która zapewnia 100 000 naukowców i matematyków bezpłatny dostęp do naszych najlepszych modeli ChatGPT. W trakcie prac rozwojowych nadal oceniamy też nasze modele na podstawie otwartych problemów badawczych.

W maju przedstawiliśmy wygenerowane przez AI obalenie⁠ hipotezy Erdősa o odległości jednostkowej, odkryte podczas oceny nieudostępnionego jeszcze modelu. Praca ta zainspirowała już kolejne osiągnięcia w matematyce i informatyce teoretycznej¹. Dziś przedstawiamy dziesięć wyników, z których każdy rozwiązuje od dawna otwarty problem lub stanowi istotny postęp w pracach nad nim. Problemy te obejmują geometrię wysokowymiarową, teorię kodowania, złożoność obwodów arytmetycznych, teorię grup, algebry operatorowe, złożoność kwantową, kryptografię kratową i kombinatorykę ekstremalną. Wszystkie te problemy mają duże znaczenie dla zajmujących się nimi społeczności matematycznych, a kilka z nich jest przedmiotem szerokiego zainteresowania całego środowiska matematycznego.

Przedstawiamy nowe wyniki dotyczące następujących problemów. Wyniki uzyskała wewnętrzna wersja Astry, naszego następnego ważnego modelu. Łączna liczba tokenów potrzebnych do znalezienia rozwiązań tych problemów kosztowałaby około 2000 USD według stawek interfejsu API Sol. Następnie ludzie, korzystając z tego samego modelu, opracowali te argumenty w formie manuskryptów. Później model sformalizował każdy argument w postaci certyfikatu Lean⁠(otwiera nowe okno). Udostępniamy również wygenerowany przez model opis toku rozumowania dla każdego rozwiązania.

1. Pakowanie sfer w wysokich wymiarach. Nowe górne ograniczenia gęstości upakowania sfer, sięgające progu Cohna–Elkiesa.
2. Kody binarne i sferyczne: wykładniczo lepsze ograniczenia maksymalnego rozmiaru kodów binarnych dla dowolnej zadanej odległości minimalnej oraz analogiczne wyniki dla wysokowymiarowych kodów sferycznych.
3. Grupy niesoficzne. Konstrukcja dowodząca istnienia grup niesoficznych, rozstrzygająca jeden z głównych otwartych problemów teorii grup.
4. Hipoteza sztywności Connesa. Obalenie wieloletniej hipotezy, według której pewne grupy są jednoznacznie wyznaczone przez swoje algebry von Neumanna.
5. Złożoność obwodów arytmetycznych. Nowe dolne ograniczenia obliczania permanentu za pomocą obwodów i formuł arytmetycznych, w tym dolne ograniczenie dla formuł arytmetycznych rzędu n⁴/log n.
6. Kwantowe powtórzenie równoległe. Twierdzenie o wykładniczym powtórzeniu równoległym dla ogólnych dwuosobowych gier kwantowych, rozszerzające fundamentalną zasadę klasycznej teorii złożoności.
7. Problem najbliższego wektora. Trudność aproksymacji problemu najbliższego wektora z dokładnością do czynnika wielomianowego — fundamentalnego problemu teorii krat związanego z kryptografią postkwantową.
8. Hipoteza Ehrharta o objętości. Wyznaczenie w każdym wymiarze maksymalnej możliwej objętości ciała wypukłego, którego środek ciężkości jest jedynym wewnętrznym punktem kratowym.
9. Wielobarwne liczby Ramseya. Superwykładnicze dolne ograniczenie wielobarwnych trójkątnych liczb Ramseya, rozwiązujące problem Erdősa nr 183.
10. Hipotezy dotyczące liczb ekstremalnych. Wyniki dotyczące hipotez zwartości i degeneracji w ekstremalnej teorii grafów, rozwiązujące problemy Erdősa nr 146 i 180.

Pojawienie się systemów zdolnych wnosić wkład w badania matematyczne rodzi pytania, na które sama firma technologiczna nie może odpowiedzieć. Istnieje wiele poglądów na rolę AI w matematyce. Głęboko szanujemy i rozumiemy osoby zaniepokojone jej wpływem, w tym sygnatariuszy deklaracji lejdejskiej w sprawie AI i matematyki⁠(otwiera nowe okno). Uważamy, że informacja o autorstwie powinna rzetelnie odzwierciedlać sposób uzyskania wyniku: przypisanie człowiekowi autorstwa dowodu wygenerowanego w całości przez system AI zafałszowałoby zarówno wkład systemu, jak i charakter autentycznej pracy intelektualnej człowieka. Pomogliśmy przygotować manuskrypty i sformalizować dowody w Lean oraz bierzemy odpowiedzialność za ich poprawność, natomiast same argumenty matematyczne wygenerował nasz system. Mamy nadzieję, że społeczność matematyczna wnikliwie przeanalizuje te wyniki, osadzi je w odpowiednim kontekście i rozwinie stojące za nimi idee poprzez nowe badania i odkrycia.

W miarę jak systemy AI stają się coraz bardziej zaawansowanymi partnerami badawczymi, zapewnienie szerokiego dostępu ma fundamentalne znaczenie dla wspierania naukowców i matematyków, którzy w tej przełomowej epoce wytyczają przyszłość swoich dyscyplin.