최근 대규모 언어 모델(Large Language Models, LLMs)은 엄밀한 수학적 증명 생성에 있어 중요한 진전을 이루었다. 그러나 형식 언어(예: Lean)에서 정리 증명을 수행하는 데 LLM을 활용하는 것은 여전히 도전적이고 계산적으로 비효율적인 문제를 안고 있다. 특히 대학 수준 이상의 문제를 다룰 때 더욱 그렇다. 본 연구에서는 대규모 에이전트 기반 강화학습을 통해 훈련된 형식적 정리 증명 모델인 Seed-Prover 1.5와 함께 효율적인 테스트 시스케일링(Test-time Scaling, TTS) 워크플로우를 제안한다. 이 모델은 Lean 및 기타 도구와의 광범위한 상호작용을 통해 강화학습 과정 동안 지속적으로 경험을 축적함으로써, 형식적 정리 증명의 능력과 효율성을 크게 향상시킨다. 또한 자연어 증명 분야의 최신 기술 발전을 활용하여, TTS 워크플로우는 자연어와 형식 언어 사이의 격차를 효과적으로 메운다. 최첨단 기법들과 비교했을 때, Seed-Prover 1.5는 더 작은 컴퓨팅 예산으로도 우수한 성능을 달성한다. PutnamBench(대학 수준) 문제의 88%, Fate-H(대학원 수준) 문제의 80%, Fate-X(박사 수준) 문제의 33%를 해결하였다. 특히 본 시스템을 활용하여 Putnam 2025의 12개 문제 중 11개를 9시간 내에 해결하였다. 본 연구 결과는 고품질의 형식적 피드백을 기반으로 경험 학습을 확장하는 방식이 형식적 수학적 추론의 미래에 막대한 잠재력을 지닌다는 점을 시사한다.