본 논문은 대규모 언어 모델(LLM)을 증명 보조기 Lean과 결합하여 정리 증명을 돕는 새로운 프레임워크인 "Lean Copilot"을 제시합니다. 기존 신경 정리 증명 시스템의 한계를 극복하기 위해, LLM을 인간의 정리 증명 과정을 돕는 조력자(copilot)로 활용하는 방식을 채택했습니다. Lean Copilot은 사용자들이 사전 훈련된 모델이나 자신이 보유한 모델을 로컬 또는 클라우드 환경에서 활용하여 증명 단계 제안, 목표 증명 완성, 관련 전제 선택 등의 기능을 제공합니다. Mathematics in Lean 교재를 사용한 실험 결과, Lean Copilot은 기존의 규칙 기반 자동 증명 시스템인 aesop에 비해 인간의 개입을 줄이고 자동 증명률을 크게 향상시키는 것으로 나타났습니다. 모든 코드와 결과물은 MIT 라이선스 하에 공개되었습니다.
