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

터미널을 재시작하거나 환경 설정을 적용하세요:

source ~/.elan/env

설치를 확인하세요:

lean --version
lake --version

Mathlib이 포함된 Lean 프로젝트

Lean 프로젝트에는 Mathlib이 필요합니다. 새 프로젝트의 경우:

lake new my-project math
cd my-project

캐시에서 Mathlib 설치 (권장 - 빌드 시간을 몇 시간 절약할 수 있습니다):

lake exe cache get

그 다음 빌드하세요:

lake build

기존 프로젝트의 경우, lakefile.lean에 다음을 추가하세요:

require mathlib from git "https://github.com/leanprover-community/mathlib4"

그 다음 실행하세요:

lake update
lake exe cache get
lake build

Rust 툴체인 (Rust Toolchain)

Rust를 설치하세요:

curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh

Ensue API 키

ensue.dev에서 API 키를 받으세요.

설정 (Setup)

1. CLI 클론 및 빌드

git clone git@github.com: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",
...

환경 변수(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)을 검증합니다. 이를 위해서는 다음 사항이 필요합니다:

1. Lean 4 프로젝트를 가리키는 유효한 lean_project_root
2. lake build 명령어로 프로젝트가 성공적으로 빌드되어야 함
3. Mathlib이 설치되어 있어야 함 (속도를 위해 lake exe cache get 사용 권장)

CLI 레퍼런스 (CLI Reference)

세션 관리 (Session Management)

# 초기화 및 루트 목표 (root goal) 생성
./bin/lc init --create-root \
  --theorem "∀ x ∈ [0,π], sin(x) ≥ (2/π)x" \
...

목표 관리 (Goal Management)

./bin/lc claim <goal_id>                    # 작업을 위해 목표 점유 (Claim)
./bin/lc unclaim <goal_id>                  # 목표 점유 해제
./bin/lc verify --goal <id> --tactic "..."  # 전술 (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는 다음과 같은 과정을 수행합니다:

1. ./bin/lc init을 통해 증명 세션(proof session)을 초기화합니다.
2. 병렬 워커 에이전트(worker agents, 증명가(provers) 및 분해자(decomposers))를 생성합니다.
3. 증명이 완료될 때까지 Ensue를 통해 조정(coordinate)합니다.
4. ./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 sai@ensue.dev