본 논문은 대규모 언어 모델(LLM)을 이용한 수학적 증명 생성의 어려움과 증명 검증 도구인 Lean을 활용한 해결 방안을 제시합니다. 기존 Lean 증명 데이터셋의 부족 문제를 해결하기 위해, LeanNavigator라는 새로운 방법론을 개발하여 기존 Lean 정리에 대한 새로운 증명을 생성하는 방식으로 대규모 데이터셋을 구축했습니다. Mathlib4를 활용하여 470만 개의 정리와 10억 개의 토큰으로 구성된 대규모 데이터셋을 생성하였으며, 이를 이용하여 훈련된 AI 모델은 기존 최고 성능 모델인 ReProver를 능가하는 성능을 보였습니다. 이는 대규모 데이터셋이 자동 정리 증명기 성능 향상에 중요한 역할을 한다는 것을 보여줍니다.
