# Discovering New Theorems via LLMs with In-Context Proof Learning in Lean

### 저자

Kazumi Kasaura, Naoto Onda, Yuta Oriike, Masaya Taniguchi, Akiyoshi Sannai, Sho Sonoda

### 💡 개요

본 연구는 대규모 언어 모델(LLM)을 활용하여 새로운 수학 정리를 발견하고 검증 가능한 증명을 생성하는 방법을 제안합니다. 제안된 '추측-증명 루프'(CPL) 파이프라인은 이전 단계에서 생성된 정리와 증명을 LLM의 맥락 학습(in-context learning)에 활용하여, 파라미터 조정 없이 증명 전략을 개선합니다. 이 접근 방식은 기존의 동시 생성 방식보다 어려운 정리를 발견하는 비율을 높이며, LLM이 스스로 생성한 결과를 재활용하는 것이 증명 성공률 향상에 효과적임을 입증했습니다.

### 🔑 시사점 및 한계

- LLM의 맥락 학습 능력을 활용하여 새로운 수학 정리를 발견하고 검증하는 자동화된 파이프라인 구축 가능성을 제시합니다.

- LLM이 스스로 생성한 결과를 반복적으로 학습에 활용함으로써, 점진적으로 더 어려운 정리를 발견하고 증명하는 능력이 향상됨을 보였습니다.

- 현재 연구는 Lean 4 환경에서의 실험에 국한되어 있으며, 다른 형식 증명기(formal theorem prover)나 더 복잡하고 추상적인 수학 분야로의 확장 가능성에 대한 추가 연구가 필요합니다.

---

[PDF 보기](https://arxiv.org/pdf/2509.14274)

For the site tree, see the [root Markdown](https://slashpage.com/haebom.md).