Zespół opisał przypadek, w którym komercyjny model ChatGPT-5.2 (Thinking) pomógł wyprowadzić oryginalny dowód dla geometrycznej hipotezy sformułowanej w 2024 roku przez Ran i Tenga. Autorzy podkreślają przy tym, że końcowa weryfikacja należała do ludzi. W matematyce nie robi wrażenia samo znalezienie odpowiedzi. Prawdziwa stawka leży w dowodzie, czyli w pokazaniu, dlaczego odpowiedź musi być prawdziwa. Właśnie tutaj AI długo wydawała się raczej zręcznym asystentem niż partnerem do odkrycia. Badacze z Brukseli twierdzą, że w ich przypadku model nie ograniczył się do parafrazowania istniejących materiałów, ale pomógł rozwinąć samą strukturę argumentu. Finalny wynik miał powstać po siedmiu sesjach rozmów i czterech kolejnych wersjach dowodu.
AI zaczyna być traktowana nie jak matematyczna wyszukiwarka, ale jak narzędzie do stawiania kroków w obszarze, gdzie nie ma jeszcze gotowej ścieżki. To już nie jest zwykłe odtwarzanie. To raczej wejście w strefę, w której maszyna pomaga układać rusztowanie pod nowy argument, a człowiek sprawdza, czy to rusztowanie naprawdę stoi.
W matematyce nie wystarczy mieć rację. Trzeba jeszcze ją unieść
W szachach, w programowaniu czy w klasycznych benchmarkach można stosunkowo łatwo sprawdzić, czy wynik jest dobry. W matematyce sprawa jest brutalniejsza. Można mieć intuicję, można mieć trafny pomysł, można nawet podejrzewać, że twierdzenie jest prawdziwe i wciąż nic z tego nie wynika, dopóki nie pojawi się szczelny dowód. Dlatego właśnie hipoteza pozostaje hipotezą aż do chwili, gdy ktoś zamknie wszystkie luki.
W opisywanym przypadku badacze nie twierdzą, że AI samodzielnie zastąpiła matematyka przy tablicy. Przeciwnie, zaznaczają, że człowiek był niezbędny do kontroli poprawności, zamykania formalnych szczelin i ostatecznego doprowadzenia argumentu do stanu, który da się traktować poważnie. To uczciwe i bardzo ważne dopowiedzenie, bo bez niego cały temat zamienia się w opowieść o maszynie, która nagle “zaczęła rozumieć matematykę” w ludzkim sensie. Na razie niczego takiego nie pokazano. Pokazano coś innego: model potrafi być zaskakująco dobry w szukaniu architektury dowodu.
Matematyka bywa przedstawiana jak kraina czystej logiki, ale w praktyce często zaczyna się od mglistych przeczuć, niewygodnych analogii, szkiców i przestawiania elementów w głowie. Zanim powstanie formalny tekst, najpierw jest mnóstwo błądzenia. Jeśli model językowy potrafi sensownie uczestniczyć właśnie w tym etapie, to jego rola może okazać się większa, niż wielu matematyków chciałoby przyznać.
Największa zmiana dotyczy stylu pracy
Autorzy tej pracy używają określenia “vibe-proving”, nawiązując do modnego wcześniej “vibe-coding”. Chodzi o sposób pracy, w którym model nie tyle kończy zadanie od A do Z, ile pomaga eksplorować intuicje, układać możliwe linie ataku i porządkować kierunki rozumowania. To brzmi lekko żartobliwie, ale dobrze trafia w sedno. W wielu dziedzinach AI zaczęła od roli pomocnika od rutyny, a potem powoli weszła głębiej do strefy, gdzie wcześniej pracowano niemal wyłącznie ludzką intuicją.
Jeśli ten model pracy się utrzyma, matematyka może wejść w bardzo ciekawy etap. Nie taki, w którym człowiek znika, tylko taki, w którym część najbardziej mozolnej eksploracji zostaje przyspieszona. Szkice, kontrprzykłady, przestawienia definicji, testowanie nieoczywistych tropów, wszystko to może zacząć dziać się szybciej. A skoro w badaniach teoretycznych ogromna część czasu przepada właśnie na szukanie dobrego kierunku, to zysk może być większy, niż sugeruje pojedynczy nagłówek.
Oczywiście jest też druga strona medalu. Im łatwiej model wygeneruje pozornie elegancki argument, tym większe znaczenie będzie miała weryfikacja. Badacze sami wprost piszą, że przyspieszenie formułowania kandydatów na dowody oznacza zarazem, że wąskim gardłem staje się ludzka kontrola poprawności. To bardzo matematyczny paradoks naszych czasów: maszyna może pomóc szybciej dojść do ciekawego pomysłu, ale ktoś wciąż musi z chłodną głową sprawdzić, czy ten pomysł naprawdę nie przecieka.
Źródła: Sci Tech Daily; Phys
