Zespół badaczy proponuje transformacyjny przeskok w sztucznej inteligencji dla matematyki - przejście od spekulacyjnych solwerów rozwiązujących predefiniowane problemy do inteligentnych agentów mogących pracować nad rzeczywistymi wyzwaniami badawczymi. Dotychczasowe systemy oparte na modelach językowych sprawdzają się w generowaniu formalnych dowodów dla jasno sformułowanych zadań za pomocą języków interaktywnego dowodzenia twierdzeń (ITP), ale brakuje im elastyczności do pracy z problemami otwartymi, niedospecyfikowanymi i wymagającymi abstrakcji na wielu poziomach.
Pracę motywuje obserwacja, że matematyka badawcza - odkrywanie nowych twierdzeń, testowanie hipotez, eksploracja nieznanych obszarów - stanowi fundamentalnie inny problem niż poprawne rozwiązanie zadania ze zbioru treningowego. Badacze przeanalizowali aktualny stan field pod kątem dostępnych zbiorów danych, automatycznej formalizacji matemtyki i technik syntezy dowodów, identyfikując siedem kluczowych ograniczeń obecnych systemów.
Mapa drogowa wskazuje na potrzebę lepszych narzędzi ekosystemu matematycznego, głęboką integrację człowiek-AI w procesie badawczym, oraz zdolność agentów do eksploracji matematycznej bez wcześniej zdefiniowanego celu. Publikacja ta stanowi wezwanie do przeorientowania badań AI4Math - z fokusu na benchmarki wydajności ku systemom zdolnym do wspierania frontierowej pracy matematyków.