인간이 만든 정리 라이브러리 없이 공리와 추론 규칙만으로 출발해 유용한 정리를 자율 발견하는 에이전트를 제시한 연구다. 증명 탐색과 유용 정리 추출을 번갈아 수행하는 자기지도 정리 발견 알고리즘으로, 발견한 정리를 라이브러리에 쌓아 이후 증명 탐색의 보조정리로 재사용한다. 실험에서 에이전트는 수만 개의 정리를 발견했고 인간이 작성한 벤치마크 문제의 증명도 찾아내, 발견물이 인간 수학 관점에서도 의미 있음을 시사했다. 나아가 발견된 정리를 프롬프트 보조정리로 제공하면 LLM의 증명 성능이 향상돼 LLM 추론의 외부 지식으로도 쓸 수 있음을 확인했다. 인간 사전지식 없이도 유용한 수학이 창발할 수 있고, 그 결과가 형식적으로 검증 가능한 자기진화 수학 AI로 가는 경로를 보여준다. ICML 2026 AI for Math 워크숍 논문이다.

• •인간 정리 라이브러리 없이 공리·추론 규칙만으로 유용한 정리를 자율 발견하는 에이전트 제안
• •증명 탐색과 정리 추출을 교대하며 보조정리로 재사용하는 자기지도 알고리즘
• •수만 개 정리 발견, 인간 작성 벤치마크 문제 증명도 성공
• •발견 정리를 프롬프트에 제공하면 LLM 증명 성능 향상 확인