Badacze z arXiv przedstawili framework oparty na modelach językowych do automatycznego odkrywania hipotez matematycznych mogących zmienić całe dziedziny nauki. Zamiast polegać na intuicji ekspertów, system wykorzystuje trzy etapy - wyszukiwanie kandydatów z lokalnych dowodów, refleksyjną walidację pod kątem fundamentalności i nowości, oraz formalną weryfikację w Lean 4 i bibliotece Mathlib.
To podejście jest istotne, bo wielkie hipotezy matematyczne - takie jak hipoteza Riemanna czy ostatnie twierdzenie Fermata - tradycyjnie czekają lata na odkrycie, zależne od geniuszu indywidualnych naukowców. Framework zmienia to w systematyczny proces, który może zidentyfikować problemy mogące reorganizować język całych gałęzi matematyki. Naukowcy testowali system na dwudziestu kandydatach i wszystkie przeszły ścisłe sprawdzenie typów w Lean - żadna nie została automatycznie rozwiązana przez istniejące narzędzia, co wskazuje, że system rzeczywiście odkrywał nowe, nietrywialne problemy.
Jeśli framework okaże się skuteczny w większej skali, może to fundamentalnie zmienić sposób, w jaki matematycy odkrywają nowe zagadnienia. Zamiast czekać na epifanię, mogą użyć AI do systematycznego przeszukiwania przestrzeni potencjalnych hipotez, z gwarancją, że znalezione problemy przeszły ścisłą weryfikację formalną.