Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics

Motivation

• Known: 기존의 agentic formal theorem proving 시스템들(Hilbert, AxiomProver, Seed Prover, Aristotle, Ax-Prover 등)은 formal prover와 여러 모델·도구를 조합하는 agentic workflow를 통해 강력한 성능을 달성해 왔다.
• Gap: 그러나 이러한 시스템들은 task-specific하게 설계된 고정 파이프라인과 대규모로 학습된 전용 formal prover에 의존하여 유연성이 떨어지고, 대부분 closed-source로 구현 세부사항이 공개되지 않아 재현과 확장이 어렵다는 한계가 있다.
• Why: 범용 coding agent를 formal math reasoner로 직접 활용하는 패러다임은 proving 외 다양한 reasoning task에 자연스러운 인터페이스를 제공하고, 추가 학습 없이 base model 교체만으로 성능 향상이 가능하며, MCP를 통해 복잡한 수작업 설계 없이 도구를 유연하게 확장할 수 있다는 점에서 formal math AI 연구에 중요한 패러다임 전환을 제시한다.
• Approach: 고정된 Orchestrator-Prover-Verifier 루프를 따르는 기존 방식과 달리, Claude Code라는 범용 coding agent가 Numina-Lean-MCP가 제공하는 다양한 reasoning 도구를 현재 상태에 따라 자율적으로 선택·호출하도록 설계했다.

Achievement

Figure 2. Numina-Lean-Agent dynamically leverages reasoning tools to autonomously navigate and advance formal proofs

1. Putnam 2025 전체 문제 해결: Claude Opus 4.5를 base model로 사용해 William Lowell Putnam 2025 대회의 12문제를 모두(12/12) 해결하며 최신 closed-source 시스템인 AxiomProver와 동등한 성능을 보였고, Harmonic의 Aristotle 및 Seed-Prover 1.5를 능가했다.
2. 효율적인 증명 생성: Problem B1 등 일부 문제에서 AxiomProver, Seed-Prover 1.5보다 더 간결한 증명(proof length)을 산출함을 계산 비용과 함께 보고했다.
3. 실제 수학 연구로의 일반화 검증: 벤치마크 평가를 넘어, 수학자들과 상호작용하는 "vibe proving" 방식으로 Brascamp–Lieb 부등식에 관한 최근 harmonic analysis 논문의 formalization을 성공적으로 수행함으로써 시스템의 범용성을 입증했다.

How

Figure 2. Numina-Lean-Agent dynamically leverages reasoning tools to autonomously navigate and advance formal proofs

• Claude Code(일반 coding agent)를 핵심 reasoning 엔진으로 사용하고, Numina-Lean-MCP를 통해 여러 전문 도구를 노출시킴
• Lean-LSP-MCP: Lean과의 상호작용(goal state 확인, diagnostic message 수신 등)을 담당
• LeanDex: Mathlib 등 Lean 라이브러리에 대한 semantic retrieval로 관련 정리·보조정리 검색
• Informal Prover: 자연어 형태의 informal proof 생성
• Discussion Partner: 외부 언어모델에 질의하여 아이디어나 문법적 문제에 대한 자문 제공
• 에이전트가 고정된 워크플로우 없이 현재 proof state에 따라 자율적으로 도구를 호출하며 thinking-tool calling을 반복하는 방식으로 증명을 구성

Originality

• 학습된 전용 formal prover 대신 범용 coding agent(Claude Code)를 formal mathematics reasoner로 직접 재활용한다는 새로운 패러다임 제시
• 고정된 멀티에이전트 파이프라인(예: Ax-Prover의 Orchestrator-Prover-Verifier 순환) 대신, 자율적 도구 선택 기반의 유연한 워크플로우를 채택
• MCP 기반 plug-and-play 도구 확장 구조로, 파이프라인 재설계 없이 새로운 도구 추가가 가능한 구조적 개방성 확보
• 벤치마크 성능뿐 아니라 실제 수학자와의 협업을 통한 정리 formalization이라는 실용적 활용 사례로 시스템의 범용성을 실증

Limitation & Further Study

• Putnam 2025라는 단일 대회 벤치마크(12문제)만으로 state-of-the-art를 주장하기에는 통계적 표본이 작아 일반화 주장에 한계가 있음
• Claude Opus 4.5라는 특정 상용 closed-source base model에 의존하고 있어, 완전한 "open" 시스템이라 보기 어렵고 비용·재현성 측면의 제약이 존재
• 자율적 도구 호출 방식의 신뢰성(예: 잘못된 도구 선택이나 무한 루프 가능성)에 대한 정량적 실패 분석이 부족해 보임
• 후속 연구로 다양한 base model(오픈소스 포함)에서의 일반화 성능 비교, 더 넓은 범위의 대회·연구 논문 formalization에 대한 체계적 평가가 필요함

Evaluation

총평: 범용 coding agent와 MCP 기반 도구 통합만으로 전용 학습 없이 최신 formal proving 성능을 달성했다는 점에서 실용적이고 개방적인 대안을 제시한 의미 있는 연구이나, 평가 규모와 base model 의존성 측면에서 추가 검증이 필요하다.