Koniec ery samotnych geniuszy? Terence Tao wieszczy matematyczną rewolucję przemysłową

Matematyka od wieków uchodziła za sport skrajnie indywidualny, gdzie badacz musiał pełnić rolę stratega, egzekutora i weryfikatora w jednej osobie. Terence Tao, jeden z najwybitniejszych żyjących matematyków, twierdzi jednak, że stoimy u progu historycznej zmiany. Sztuczna inteligencja może wprowadzić do tej hermetycznej dyscypliny to, co w inżynierii jest standardem od dawna: realny podział pracy.

Dlaczego to ważne akurat teraz? Debata o „przemysłowej” matematyce przestała być abstrakcją. W ciągu ostatnich dwóch lat repozytorium mathlib, służące do formalnej weryfikacji twierdzeń, spuchło niemal dwukrotnie, przekraczając w kwietniu 2026 roku barierę 200 tysięcy rekordów. To już nie tylko teoretyczne dywagacje, ale konkretna infrastruktura, na której wyrastają projekty łączące systemy takie jak Lean czy Isabelle z modelami językowymi.

Od rzemiosła do produkcji wielkoseryjnej

Dotychczasowy model pracy matematycznej opierał się na rzemieślniczym podejściu – od postawienia problemu po żmudny dowód. Tao zauważa, że AI wypełni luki kompetencyjne w zespołach, pozwalając na głęboką specjalizację. Pojawia się koncepcja „matematyki przemysłowej”, w której zamiast pojedynczych jednostek pracujących latami, zobaczymy szeroko zakrojone projekty realizowane przez duże, wspierane technologią grupy. Tao wskazuje bezpośrednio: „Metody wspomagane maszynowo mogą uczynić matematykę masowym przedsięwzięciem wspólnotowym, zbliżonym do sposobu, w jaki działają kolaboracje w fizyce cząstek”.

W takim układzie AI przetwarza miliardy punktów danych, a człowiek odpowiada za natchnione hipotezy. Pierwsze dowody skuteczności tego modelu już są: system AlphaProof w 2025 roku aktywnie współtworzył dowody, które przeszły rygorystyczną weryfikację. To otwiera drzwi dla „citizen science” – osób spoza akademii, które dzięki automatyzacji będą mogły dołożyć swoją cegiełkę do globalnej nauki.

Pułapka informacyjnego szlamu

Tao ostrzega przed entuzjazmem bez filtrów. Jeśli modele językowe zaczną generować strategie bez rygorystycznej kontroli, zaleją naukę falą niesprawdzalnego „slopu”. Kluczem do sukcesu nie jest sama moc obliczeniowa, lecz symetryczny rozwój automatyzacji weryfikacji. Zdaniem naukowca, poziom zaawansowania AI, który można bezpiecznie zaadaptować, jest ściśle ograniczony przez surowość procesów sprawdzających.

W nowym paradygmacie rola człowieka pozostaje kluczowa. Modele bywają zawodne, dlatego to matematyk musi być ostatecznym arbitrem jakości. Bez tego matematyka utonie w masowej produkcji atrakcyjnie brzmiących, lecz pustych teorii. Jednak dla tych, którzy opanują nowe narzędzia, przyszłość wygląda fascynująco. Jak zauważają komentatorzy w serwisach branżowych, dzisiejsze zbiory maszynowo zweryfikowanych twierdzeń staną się fundamentem dla przyszłych „AI-matematyków”, którzy mogą ostatecznie przekroczyć ludzkie ograniczenia poznawcze.