lean-collab
Lean 4 및 Ensue Memory Network를 활용한 멀티 에이전트 (Multi-agent) 협업 정리 증명.
블로그 포스트 읽기
사전 요구 사항 (Prerequisites)
Lean 4 설치
elan (Lean 버전 관리자)을 설치하세요:
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
터미널을 재시작하거나 환경 설정을 적용하세요:
설치를 확인하세요:
lean --version
lake --version
Mathlib이 포함된 Lean 프로젝트
Lean 프로젝트에는 Mathlib이 필요합니다. 새 프로젝트의 경우:
lake new my-project math
cd my-project
캐시에서 Mathlib 설치 (권장 - 빌드 시간을 몇 시간 절약할 수 있습니다):
그 다음 빌드하세요:
기존 프로젝트의 경우, lakefile.lean에 다음을 추가하세요:
require mathlib from git "https://github.com/leanprover-community/mathlib4"
그 다음 실행하세요:
lake update
lake exe cache get
lake build
Rust를 설치하세요:
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh
Ensue API 키
ensue.dev에서 API 키를 받으세요.
설정 (Setup)
1. CLI 클론 및 빌드
git clone [email protected]:mutable-state-inc/lean-collab.git
cd lean-collab-plugin
make install
이 과정은 Rust CLI를 컴파일하고 ./bin/lc를 생성합니다.
2. Ensue 인증 구성
echo "your-ensue-api-key" > .ensue-key
chmod 600 .ensue-key
3. 로컬 설정 구성
플러그인 디렉토리에 .lean-collab.json을 생성하세요:
{
"theorem_id": "my-theorem",
"ensue_api_url": "https://api.ensue-network.ai",
...
| 필드 (Field) | 설명 (Description) | 기본값 (Default) |
|---|
theorem_id | 증명 세션을 위한 고유 식별자 | 필수 (Required) |
| ... | | |
환경 변수(Environment variables)는 설정 값을 덮어씁니다:
export LEAN_COLLAB_MAX_PARALLEL_AGENTS=6
export LEAN_COLLAB_MAX_DEPTH=8
export LEAN_COLLAB_CLAIM_TTL=600
Lean LSP & 검증 (Verification)
CLI는 lake env lean을 사용하여 사용자의 Lean 프로젝트에 대해 전술 (tactics)을 검증합니다. 이를 위해서는 다음 사항이 필요합니다:
- Lean 4 프로젝트를 가리키는 유효한
lean_project_root
lake build 명령어로 프로젝트가 성공적으로 빌드되어야 함- Mathlib이 설치되어 있어야 함 (속도를 위해
lake exe cache get 사용 권장)
CLI 레퍼런스 (CLI Reference)
세션 관리 (Session Management)
./bin/lc init --create-root \
--theorem "∀ x ∈ [0,π], sin(x) ≥ (2/π)x" \
...
목표 관리 (Goal Management)
./bin/lc claim <goal_id>
./bin/lc unclaim <goal_id>
./bin/lc verify --goal <id> --tactic "..."
...
검색 및 탐색 (Search & Exploration)
./bin/lc search "query" --prefix tactics/
./bin/lc explore --goal <id> --tactic "..."
./bin/lc suggest --goal <id>
Claude와 함께 실행하기
1. Warm Server 시작하기
Claude를 실행하기 전에, 별도의 터미널에서 warm server를 시작하세요:
cd /path/to/lean-collab-plugin
./bin/lc warm
이 터미널을 열어둔 상태로 유지하세요. Warm server는 다음과 같은 역할을 합니다:
- Mathlib을 메모리에 한 번 로드함 (초기 로드 약 20초 소요)
- 전술 검증 속도를 획기적으로 향상시킴 (검증당 약 20초에서 약 2~5초로 단축)
/tmp/lean-warm.sock에서 대기
Warm server가 없으면, 매 검증마다 Lean이 콜드 스타트(cold-start)되고 Mathlib을 다시 로드하므로 매우 느려집니다.
2. Claude 시작하기
플러그인 디렉토리에서 (새 터미널을 열어) 실행하세요:
claude \
--plugin-dir /path/to/lean-collab-plugin \
--allowedTools "Bash,Read,Write,Edit,Task,Glob,Grep" \
...
3. 스킬 호출하기
Claude가 실행되면, 협업 증명 프로세스를 시작하세요:
<사용자의 정리 문장>을 증명하세요.
/lean-collab을 사용하여 오케스트레이션하세요.
예시:
[0, pi] 범위의 모든 x에 대해 sin(x) >= (2/pi)x 임을 증명하세요.
/lean-collab을 사용하여 오케스트레이션(orchestrate)하세요.
Claude는 다음과 같은 과정을 수행합니다:
./bin/lc init을 통해 증명 세션(proof session)을 초기화합니다.- 병렬 워커 에이전트(worker agents, 증명가(provers) 및 분해자(decomposers))를 생성합니다.
- 증명이 완료될 때까지 Ensue를 통해 조정(coordinate)합니다.
./bin/lc compose를 사용하여 최종 검증된 Lean 증명을 구성합니다.
중요 면책 조항 (Important Disclaimer)
토큰 사용 경고 (Token Usage Warning): 이 도구는 여러 개의 병렬 에이전트를 생성하므로, 특히 복잡한 증명을 수행하거나 많은 워커를 실행할 때 상당한 양의 API 토큰을 소비할 수 있습니다.
권장 사항:
-
최대 20배(Max 20x) 계정 사용 - 병렬 에이전트 생성 및 반복적인 증명 과정은 토큰을 빠르게 소모합니다. 더 높은 속도 제한(rate limit)을 가진 계정을 사용하는 것을 강력히 권장합니다.
-
별도의 창에서 모니터링 - lean-collab이 여러 문제를 자율적으로 해결하는 데 사용되어 왔지만, /lean-collab 스킬이 로드된 다른 Claude Code 창을 열어 진행 상황을 모니터링하는 것이 도움이 됩니다. 이를 통해 해결 과정이 지루해지거나 비생산적인 루프(loop)에 빠질 경우 개입할 수 있습니다.
-
적은 수의 워커로 시작 - 토큰 소비에 익숙해질 때까지 max_parallel_agents: 3-5로 시작한 다음, 규모를 확장하세요.
-
루프 주의 - 에이전트가 동일한 목표(goals)에 대해 반복적으로 백트래킹(backtracking)을 수행한다면, 수동으로 개입하거나 정리(theorem) 구성을 조정하는 것을 고려하십시오.
저자 (Author)
Sai Vegasena [email protected]