Axiom Math właśnie formalnie zweryfikował Stacks Project - jeden z największych zbiorów matematycznych - używając dedykowanych agentów AI. To przełomowy krok w walce ze zjawiskiem, które naukowcy zaczęli określać jako problem niskiej jakości dowodów generowanych przez sztuczną inteligencję w matematyce.
Problem rośnie w miarę, jak coraz więcej AI-generowanych dowodów trafia do czasopism i baz wiedzy bez odpowiedniej weryfikacji. Czasami są one całkowicie błędne, czasami zaś wyglądają wiarygodnie, ale zawierają subtelne luki logiczne. Axiom Math postanowił zaatakować problem z drugiej strony - zamiast próbować wychwycić słabe dowody, buduje narzędzia do formalnego potwierdzenia, że dowód jest rzeczywiście poprawny.
Formalny system weryfikacji, którą zastosowali, to najwyższy standard w matematyce - nie wystarczy, że dowód wygląda logicznie, musi być maszynowo sprawdzalny krok po kroku. Sukces z Stacks Project pokazuje, że podejście może działać na dużą skalę. To może stać się nową linią obrony przed falą AI slop zalewającą matematyczną naukę.