Widzę, że w gorących "Politiken hattricken", więc dobry moment, żeby oderwać się od tego przez "matematiken". Ciekawostka, wczoraj opublikowano taki blueprint:

Może pokrótce wyjaśnię, o co chodzi. Ostatnie Twierdzenie Fermata (będę dalej posługiwał się skrótem - LFT), to szczególny przypadek pytania o rozwiązywalność dla konkretnego równania diofantycznego. Równania diofantyczne, to jak powinniśmy pamiętać ze szkoły średniej takie równania zdefiniowane w dziedzinie liczb całkowitych, które ogólnie można wyrazić jako f(x₁, x₂, x₃, ..., xₙ) = 0. Ujmując to prościej, są to takie równana, dla których odpowiedzią są co najmniej dwie zmienne. Na przykład a + 2b = 5 ma takie przykładowe rozwiązania jak (a=1, b=2) czy (a=3, b=1). LFT definiuje takie równanie: aⁿ + bⁿ = cⁿ jako nieposiadające żadnego rozwiązania (a, b, c) dla n ≥ 3. Dla n = 2 sprawa jest prosta, gdyż jak wiemy, takie rozwiązania muszą istnieć, bowiem są odpowiedzią wynikająca wprost z twierdzenia Pitagorasa. Na przykład (a = 3, b = 4, c = 5) i każde wielokrotności będą spełniać to równanie, więc jest ich nieskończenie wiele. Problem jednak komplikuje się, kiedy zwiększamy n. Przez stulecia udało się rozpatrywać różne przypadki, typu n=3, n=4, n=5 itd. Jednak każdy taki przypadek opisywany był innym typem dowodu, przez co nie dało się tego uogólnić na wszystkie liczby naturalne n. Dopiero w roku 1994 Andrew John Wiles opublikował dowód, zbierając całą wiedzę z przeszło 350 lat. Dowód ten jest bardzo mocno skomplikowany i można powiedzieć, że jest jednym z największych osiągnięć teorii liczb XXw. Zahacza on o wiele bardzo nowoczesnych konceptów z zakresu: geometrii algebraicznej, algebry Heckego, deformacji pierścieni, kategorii, schematów, czy krzywych eliptycznych.

Lean jest natomiast projektem, który ma w założeniach pozwolić wyrażać matematykę w sposób maszynowy. Ma to między innymi umożliwić AI rozumienie matematyki. Innymi słowy, nie chodzi o to, żeby AI była w stanie znaleźć dowód jakiegoś twierdzenia matematycznego w internecie i bezmyślnie go przeklepać pytającemu, czy wykonać jakieś algorytmicznie zdefiniowane obliczenie, typu obliczyć pochodną funkcji, tylko żeby faktycznie rozumiała pojęcia i formalizmy matematyczne, którymi operuje oraz zależności między nimi. Dzięki temu możliwym mogłoby być użycie AI do znajdywania odpowiedzi na do tej pory nierozwiązane problemy, co do których nie mamy wyrobionego "algorytmu postępowania".

W oparciu o Lean udało się stworzyć takie sztuczne inteligencje jak Lean AI, czy AlphaGeometry, które są w stanie rozwiązywać zadania matematyczne, które pierwszy raz "widzą na oczy" i nie mają dla nich wyrobionego schematu postępowania. AlphaGeometry udało się nawet uzyskać wydajność na poziomie złotego medalu Międzynarodowej Olimpiady Matematycznej, biorąc pod uwagę tylko zadania z geometrii. Powiedziałbym, że to małe oszustwo, ale byłoby to duże niedopowiedzenie, biorąc pod uwagę, że geometria Euklidesowa jak dowiódł Alfred Tarski, jest teorią spójną, kompletną i rozstrzygalną. Stety-niestety teoria liczb, do której domeny przynależy LFT, takową teorią nie jest, co niesie za sobą pewne implikacje. Możliwe, że jeszcze kiedyś popełnię coś na ten temat, jeżeli kogoś to interesuje.

O zamiarach sformalizowania LFT w Lean było już słychać pod koniec roku 2023, kiedy Kevin Buzzard dostał 5 letnie stypendium właśnie na ten cel, a dziś uzyskujemy końcowy rezultat? Niestety nic bardziej mylnego, tytuł tej pracy to niezły kilkbejt. Cała jest dostępna pod tym linkiem, więc jak kogoś interesuje, to proszę się częstować: https://imperialcollegelondon.github.io/FLT/blueprint.pdf
Natomiast w wielkim skrócie, to można powiedzieć, że nie widać nawet wierzchołka tej lodowej góry. Stwierdzone jest to pośrednio w 12 chapterze (appendix), jeżeli chodzi o twierdzenia zależne, które znane są ludzkości, ale nie istnieje ich formalizacja w Lean. Niektóre z nich to nadal wieloletni reaserch — co też stwierdza dokument.

Zatem czy AI będzie w najbliższym czasie pomocne w rozwiązaniu takich problemów, jak hipoteza Riemanna, czy problem Collatza? Mocno wątpliwe, na ten moment ludzkość jest znacznie bardziej rozwinięta pod kątem formalnej dowodowości matematycznej od jakiegokolwiek AI.