Park, Geon (re-st)
ByteDance 개발
Seed-Prover
Lean
기반 정리 증명 모델,
IMO (올림피아드)
수준 문제 해결 시도
lemma-style proving
: 본 증명 전 레마 생성, 레마의 시드풀 관리, 단계적 접근
Lean 컴파일러 피드백으로 증명 수정·보완, 필요 시 새로운 레마 도출
Seed-Geometry
: 기하학 문제 전용 추론 엔진 추가, 복잡한 도형 문제 대응
(논문) Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
hanbit.co.kr 논문요약
IMO 2025의 P1 증명 (P1.lean)
#Paper-Summary