Ostatnie postępy w AI dla matematyki (AI4Math) doprowadziły do znaczących sukcesów w generowaniu formalnych dowodów dla dobrze zdefiniowanych problemów matematycznych za pomocą interaktywnych języków theorem provingów. Jednak obecne systemy oparte na dużych modelach językowych pozostają fundamentalnie ograniczone wobec matematyki na froncie badań - takie jak odkrywanie nowych twierdzeń czy rozwiązywanie otwartych hipotez matematycznych, które są z natury niedookreślone i wymagają wielowarstwowej abstrakcji.
Artykuł zawiera systematyczny przegląd dziedziny, obejmujący zbiory danych, automatyczną formalizację i syntezę dowodów. Autorzy identyfikują kluczowe ograniczenia istniejących systemów: problemy ze zbiorami treningowymi, brakiem zrozumienia struktur relacyjnych, niewystarczającą zdolnością do matematycznej eksploracji, niedostatecznym ekosystemem narzędzi i słabą kolaboracją człowiek-AI. Te czynniki uniemożliwiają obecnym modelom działanie jako autentyczne agenty badawcze zdolne do niezawisłego odkrywania nowych rezultatów matematycznych.
Proponowany kierunek dla przyszłych badań to zmiana paradygmatu - od systemów rozwiązujących predefiniowane problemy do inteligentnych agentów zdolnych do otwartej eksploracji matematycznej z użyciem ścisłego formalnego rozumowania. Taka transformacja wymagałaby nowych podejść do trenowania, rozbudowy narzędziowych możliwości systemów oraz nowych sposobów interakcji między ludzkimi matematykami a agentami AI.