연구진이 리만 가설급 주요 수학 난제를 AI가 스스로 발굴하도록 돕는 3단계 파이프라인을 제안했다. 구체적 국소 증거 모듈에서 후보 영역을 탐색하고, 기초성·참신성·잠재적 중요성을 반성적으로 검증한 뒤, Lean 4와 Mathlib로 형식적 검증을 거치는 구조다. 목표는 증명될 경우 해당 연구 분야의 언어 자체를 재편하고 인류의 수학 연구에 지속적인 도움을 줄 수 있는 '문제 취향(problem taste)'이 높은 문제를 찾아내는 것이다. 20개 후보를 대상으로 한 실험에서 20개 전부가 Lean 파싱·타입 체크를 통과했고, 20개 모두 exact?로 즉시 해결되지 않았으며 aesop으로도 자동 증명되지 않아 자명하지 않은 난제임이 확인됐고 명시적 중복도 발견되지 않았다.

• •리만 가설급 주요 수학 난제 발굴을 위한 3단계 파이프라인(국소 증거 탐색→반성적 검증→Lean 4 형식 검증) 제안
• •목표는 증명 시 연구 분야의 언어를 재편할 만큼 '문제 취향'이 높은 난제 발굴
• •실험한 후보 20개 전부가 Lean 파싱·타입 체크 통과
• •20개 모두 exact?로 즉시 풀리지 않고 aesop 자동증명도 통과하지 않아 자명하지 않음을 확인, 중복 없음