frenzymath/Archon

✨✨✨

Archon v0.3.0. 더 많은 하네스(harnesses)를 추가했습니다(현재 Codex 및 Claude Code). 또한 claude -p에 적용된 Anthropic의 새로운 속도 제한(rate limits)에 대한 해결책(workarounds)을 추가했습니다.

(Codex, 헤드리스 Claude TUI 및 기타 포함). Archon은 Lean 블루프린트 그래프를 쿼리하기 위한 커스텀 API인 LeanDag를 통해 DAG(Directed Acyclic Graph)를 기반으로 작업을 수행합니다. 대시보드가 더욱 풍부해졌습니다 — 블루프린트가 렌더링되며, DAG를 탐색할 수 있습니다. 증명기(Provers)는 다양한 모드(fine-grained, mathlib-build, …)로 실행될 수 있으며, archon extract를 사용하여 DAG에서 서브프로젝트를 추출하여 별도로 작업한 후, archon merge를 통해 다시 병합할 수 있습니다. 또한 peers.yaml을 추가하여 Archon이 다른 프로젝트의 DAG를 읽고 그들의 증명(proofs)을 재사용할 수 있도록 했습니다.

✨

Archon v0.2.0. 다중 레인 병렬 증명(multi-lane parallel proving; Anthropic + Moonshot + DeepSeek 병행), 에이전트 작업의 내부 Git 버전 관리(inner-git versioning), 고정된 시그니처 인터페이스(archon-protected.yaml), 선택적 서브 에이전트 시스템(blueprint review, strategy critique, Mathlib design advice 등)을 추가했습니다.

🔄

v0.1.0 또는 v0.2.0에서 업그레이드하시나요? 기존 프로젝트에서 archon update를 한 번 실행한 다음 archon init을 실행하세요. 주의: 먼저 작업 내용을 백업해 주세요! ⌛️

그 이전 버전에서 업그레이드하시나요? MIGRATION.md를 참조하세요. 📝 전체 릴리스 노트: CHANGELOG.md.

Archon은 Lean 4에서 연구 수준의 수학을 자율적으로 형식화(formalizes)하는 에이전트 시스템(agentic system)입니다. **플랜 에이전트(plan agent)**는 전략적 가이드를 제공하고, **증명 에이전트(prover agents)**는 증명을 작성하고 검증합니다 — 이는 컨텍스트 폭발(context explosion)을 방지하기 위해 분석과 실행을 분리합니다. 이 시스템은 스캐폴딩(scaffolding), 증명(proving), 다듬기(polish)의 세 단계를 통해 저장소 규모의 형식화(repository-scale formalization)를 처리합니다. 기본적으로 Claude Code 및 Claude Opus 4.8을 기반으로 구축되었으며, lean-lsp-mcp와 lean4-skills의 수정된 포크(fork)를 사용합니다. Archon은 OpenClaw를 통해 Claude Code를 오케스트레이션하는 것에서 시작되었습니다. 저희 블로그와 공지사항도 참조해 주세요.

Archon은 프로젝트 수준의 형식화 (project-level formalization) — 즉, 고립된 경시대회 문제가 아닌 상호 의존적인 정리(theorems)가 포함된 다중 파일 저장소(multi-file repositories) — 를 위해 설계되고 최적화되었습니다. 따라서 단일 문제 벤치마크는 특정 최적화 대상이 아닙니다. 모델 선택의 경우, Opus 4.8을 강력히 권장합니다. 저희의 실험 결과 Fable 5가 매우 유망해 보이며, Sonnet 또한 잘 작동하지만 성능은 그보다 낮습니다. 다른 모델들은 테스트되지 않았습니다. 성능이 낮은 모델은 Archon의 복잡한 기술과 프롬프트 구조(prompt structures)를 다루는 데 어려움을 겪을 수 있으며, 이 경우 시스템 설계가 성능을 돕기보다 오히려 저해할 수 있습니다. v0.3.0부터는 Codex도 사용 가능하며, gpt-5.5는 Opus 4.8의 좋은 대안이 될 수 있습니다. 추가적인 모델들은 Claude Code 하네스(harness)를 통해 실행할 수 있습니다. 예를 들어, Anthropic 호환 API를 통한 DeepSeek 및 Kimi, 또는 모든 OpenRouter 모델(OpenRouter이 API 변환을 처리함)이 이에 해당합니다.

• 📦 설치 (Install)
• 🚀 사용법 (Usage)
• 📚 비형식적 자료 제공 (Supplying informal material)

보안 주의사항: archon loop는 --dangerously-skip-permissions 옵션과 함께 Claude Code를 실행합니다. 이는 모델이 임의의 셸 명령(shell commands)을 실행하고, 프로세스가 접근할 수 있는 모든 파일을 읽거나 쓸 수 있으며, 네트워크 요청을 보낼 수 있음을 의미합니다. 이는 Claude Code가 Linux에서 root 권한으로 실행될 때 거부하는 동작입니다. 저희의 실험에서 Opus나 Sonnet은 결코 해를 끼치지 않았으나, 여전히 위험이 존재하므로 다음과 같은 우회 방법을 권장합니다:

1. 전용 비-root(non-root) 사용자 사용(권장) — 예: adduser로 사용자 생성 — 과도한 root 권한으로 실행되지 않도록 합니다.
2. Claude Code가 이 고위험 옵션으로 시작할 수 있도록 설정합니다: export IS_SANDBOX=1
3. 민감한 데이터나 자격 증명(credentials)에 접근할 수 없는 Docker 컨테이너 또는 VM 내부에서 실행합니다.

참고: Python 가상 환경(예: python3.11 -m venv ~/archon-env) 내에서 실행하는 것을 권장합니다.

CLI 도구와 시스템 의존성을 설치하려면 터미널에서 다음 명령어를 실행하세요:

curl -sSL https://raw.githubusercontent.com/frenzymath/Archon/refs/heads/main/install.sh | bash

원하신다면 수동으로 설치할 수도 있습니다. install.sh

저장소를 가져오고, pip install .을 실행하며, 시스템 레벨의 의존성(uv, Claude Code, ...)을 설치하고 Lean 툴체인 (toolchain)을 검증하기 위해 archon setup을 실행합니다. 설치 프로세스는 처음 실행 시 느릴 수 있습니다.

이제 다음 명령어를 통해 설치를 확인하고 사용법에 대한 안내를 받을 수 있습니다:

archon -h

나중에 기존 설치를 업데이트하려면:

archon update

archon setup은 또한 비공식 에이전트 (informal agent)가 사용하는 API 키(OPENAI_API_KEY 또는 GEMINI_API_KEY)를 확인합니다. 최소 하나를 사용하는 것이 권장되지만 필수는 아닙. Kimi, DeepSeek, 그리고 OpenRouter를 위한 제공자 키는 Claude 호환 레인 (lanes) 및 모델 별칭 (aliases)을 위해 .archon/.env에 저장됩니다.

번들로 포함된 비공식 에이전트는 단순화된 데모입니다: 증명 스케치 (proof sketches)를 위해 외부 모델에 단일 API 호출을 수행합니다. 우리의 내부 구현은 더 복잡하지만 아직 오픈 소스로 공개할 준비가 되지 않았습니다. 실제로 원샷 (one-shot) 방식은 눈에 띄는 성능 저하를 보이지 않는데, 이는 아마도 Claude Code가 반환된 스케치에 대해 자체적인 검증 및 개선 (refinement)을 수행하기 때문일 것입니다.

명령 (Command)	설명 (Description)
archon init	새로운 Archon 프로젝트를 초기화합니다.
archon dag	프로젝트를 위한 전체 비형식적 청사진 (dependency graph, 의존성 그래프)을 상세히 작성합니다.
archon blueprint-doctor	청사진 구조, 참조 (references), 매크로 (macros), 공리 (axioms) 및 커버리지 주석 (coverage annotations)을 린트 (Lint) 합니다.
archon extract	Archon 프로젝트에서 의존성 콘 (dependency-cone) 하위 프로젝트를 추출합니다.
archon merge	DAG를 통해 두 Archon 프로젝트를 병합하며, 최선의 공유 증명 (proofs)을 유지합니다.
archon loop	자동화된 계획 (plan) → 증명 (prove) → 검토 (review) 루프를 실행합니다.
archon doctor	전체 Archon 설정을 검증합니다.
archon dashboard	웹 모니터링 인터페이스를 시작합니다.
archon prove	주어진 명제에 대한 증명 루프를 시작합니다.
archon setup	시스템 수준의 의존성 (dependencies)을 설치합니다.
archon update	Archon을 최신 버전으로 업데이트합니다.
archon discuss	프로젝트에 대한 대화형 토론을 시작합니다.
archon branch	기존의 inner-git 브랜치로 전환하거나, 새로운 브랜치를 포크 (fork) 합니다.
archon log	inner-git 커밋 그래프를 보여줍니다.
archon version	Archon CLI 버전과, 프로젝트 내부인 경우 프로젝트 버전을 보여줍니다.
archon refactor	리팩터링 (refactor) 지침을 초안 작성하거나 실행합니다.
archon migrate	레거시 (legacy) Archon 프로젝트를 위한 일회성 마이그레이션 (migrations)을 실행합니다.

자세한 내용은 archon -h 또는 archon <command> -h를 실행하세요.

초기화하려면:

archon init /path/to/your-lean-project

여기서 /path/to/your-lean-project는 다음 중 하나일 수 있습니다:

• 비어 있을 수 있으며, 이 경우 Archon은 새로운 프로젝트 디렉토리를 생성하고 무엇을 형식화 (formalize)하고 싶은지 묻습니다.
• 기존의 Lean 프로젝트를 포함할 수 있으며, 이 경우 Archon은 이를 형식화의 기반으로 사용합니다.
• 비형식적 자료 (예: 문제 설명, 논문, 청사진 등)를 포함할 수 있으며, 이 경우 Archon은 그 안에 Lean 프로젝트 구조를 생성하고 해당 비형식적 자료를 사용하여 첫 번째 목표 (objectives)를 작성합니다.

archon init은 프로젝트 내부에서 다음을 수행합니다:

• .archon/ 생성

런타임 상태 파일 (runtime state files) 및 Archon 프롬프트의 복사본 (copy)과 함께, 에이전트가 사용할 수 있는 Python 스크립트를 복사합니다. - Archon의 Lean4 기술 (skills)을 프로젝트 범위 (project scope) 내의 lean4@archon-local 플러그인으로 설치합니다. - Archon의 lean-lsp MCP 서버를 프로젝트 범위 내의 archon-lean-lsp로 설치합니다. - 충돌하는 전역 lean4-skills / lean-lsp MCP를 감지하고 비활성화합니다. - leanblueprint, git, lake를 구성하고, 아직 설치되어 있지 않다면 최신 mathlib을 설치합니다. - 프로젝트 상태를 감지하고 초기 목표 (objectives)를 작성하기 위해 Claude Code를 대화형 (interactively)으로 실행합니다.

최신 번들 프롬프트와 기술 (skills)을 가져오려면 Archon을 업데이트한 후 init을 다시 실행하세요. 이는 사용자의 로컬 수정 사항과 설정을 보존하며, 프롬프트를 새 버전으로 유지, 병합 또는 덮어쓰기할 수 있게 해줍니다.

v0.2.0부터는 .archon/config.json을 통해 프로젝트 선호도를 저장할 수 있어 매번 동일한 CLI 옵션을 반복할 필요가 없습니다 🤗. 이곳은 하네스 (harnesses) 및 모델, Claude 실행 백엔드 (launch backends), 활성화된 서브에이전트 (subagents), 멀티 레인 증명 (multi-lane proving), 그리고 루프 기본값 (loop defaults)을 구성하기 위한 권장 장소입니다.

전체 참조를 보려면 CONFIGURATION.md를 확인하세요. 간단한 개요로서, 전형적인 .archon/config.json은 다음과 같습니다:

{
"loop": {
"max_iterations": 2,
...

Anthropic은 이제 구독 플랜에서 헤드리스 (headless) claude -p에 대해 속도 제한 (rate-limits)을 적용합니다 — 이는 Archon이 기본적으로 사용하던 엔진입니다. v0.3.0부터는 이를 우회하는 두 가지 방법이 있습니다.

이 솔루션들은 실험적이라는 점에 유의하십시오. 기본 백엔드인 claude -p를 사용하는 것이 강력히 권장되지만, 비용이 많이 듭니다. claude-p 래퍼 (wrapper) (Claude Agent SDK를 통해 claude -p를 시뮬레이션함)는 현재 설정에서 잘 작동하지만, 불안정할 수 있으며 서브에이전트의 로그가 표시되지 않을 수 있습니다. interactive 백엔드는 수동 상호작용이 필요하여 덜 편리하지만, claude-p 래퍼가 작동하지 않고 크레딧이 소진되었을 때 좋은 대체 수단이 됩니다. vscode / desktop은 역공학 (reverse engineering)을 기반으로 하므로 작동하지 않을 수 있지만, 작동한다면 과금 방식만 제외하고 claude -p와 정확히 동일하게 작동할 것입니다. Codex를 사용하는 경우...

Claude Code 대신 Codex를 사용하는 것도 실행 가능한 옵션이며, 아마도 가장 안정적일 것입니다. OpenAI는 이와 유사한 제한을 API에 적용하지 않았기 때문입니다. 물론, 본인의 API 키를 사용하여 claude -p를 사용한다면 백엔드를 변경할 이유가 없습니다.

실행 백엔드 전환. loop.claude_backend (또는 --claude-backend)는 모델을 변경하지 않고 Claude Code가 시작되는 방식을 변경합니다:

백엔드	역할
default	일반적인 claude -p 헤드리스 (headless) 서브프로세스 — 새로운 제한 사항의 적용을 받습니다.
claude-p	claude-p 래퍼 (wrapper)를 통해 대화형 Claude Code TUI를 헤드리스로 구동합니다. 속도 제한(rate-limited)이 있는 구독 환경에서 권장되는 해결책입니다.
vscode / desktop	역공학 (reverse engineering)에 기반하며, 작동할 경우 세션을 VS Code / Desktop 엔트리포인트(entrypoint)로 귀속시킵니다.
interactive	사용자가 직접 제어할 수 있도록 claude를 포그라운드 (foreground)에서 실행합니다 (직렬 방식, 멀티레인 불가).

하네스(harness)를 Codex로 전환. loop.harness: "codex"를 설정하면 모든 역할(role)과 서브에이전트(subagent)를 Claude 대신 Codex를 통해 라우팅하거나, loop.roles를 사용하여 역할별로 두 가지를 혼합할 수 있습니다. 내장된 Codex 하네스는 하네스 기술자(descriptor)에 model 필드를 추가하지 않는 한, Codex CLI가 설정된/기본 모델을 선택하도록 합니다.

우선순위 규칙과 claude-p 로그인 디렉토리(claude_p_config_dir)에 대해서는 CONFIGURATION.md를 참조하세요.

프로젝트에 따라 Archon이 사용자의 기여분 중 일부를 덮어쓰는 것을 피하고 싶을 수 있습니다. 따라서 archon-protected.yaml을 사용하면 블루프린트(blueprints)나 Lean 파일 내에서 Archon이 수정해서는 안 되는 파일이나 선언(예: 본문 수정 금지, 시그니처 수정 금지 등)을 선언할 수 있습니다.

v0.3.0부터 이 파일은 세 가지 종류의 규칙을 지원하며, 모두 선택 사항입니다. 프로젝트에 필요한 것을 조합하여 사용할 수 있습니다. 패턴은 fnmatch 글로브 (glob) (*, ?, [...]) 형식이므로, 단일 규칙으로 여러 파일이나 선언을 한 번에 다룰 수 있습니다:

# 1. 파일별 Lean 선언 보호.
lean:
MyProject/Core.lean:
...

Archon의 다음 버전에서는 이 기능이 더욱 확장되거나 다른 접근 방식이 선택될 수 있음을 유의하십시오. 현재 구현은 매우 기초적인 수준이며, 만약 예상대로 작동하지 않는다면 이 파일을 비워둠으로써 해당 기능을 비활성화할 수 있습니다.

peers.yaml

은 Archon이 DAG (Directed Acyclic Graph, 유향 비순환 그래프)를 읽고 증명(proofs)을 재사용할 수 있는 다른 Archon 프로젝트들을 나열할 수 있는 파일입니다. 예를 들어, 동일한 인프라 구축이 필요한 프로젝트들을 작업 중이거나, 프로젝트를 더 작은 하위 프로젝트로 나눈 경우, 이 기능을 통해 중복 작업을 방지할 수 있습니다. 또한, 여러 개의 로컬 대시보드(local dashboard)를 실행하는 대신, 대시보드를 통해 각 프로젝트의 대시보드 간 전환, 병합된 DAG 표시 등을 수행할 수 있습니다.

v0.3.0 이후부터

, archon dag는 블루프린트(blueprint) 작성 루프를 실행하며, 이는 메인 루프 이전이나 중간 과정에서 실행할 수 있습니다. 이는 LeanDag를 사용하므로 Archon이 오로지 LLM (Large Language Model, 거대 언어 모델)의 내부 의존성 파악에만 의존하지 않도록 합니다.

archon dag /path/to/your-lean-project

이 단계는 선택 사항이지만 권장됩니다. 에이전트(agents)가 Lean 코드를 작성하기 시작하기 전에 블루프린트가 준비될 수 있도록, 메인 루프를 실행하기 전 최소 한 번은 실행하십시오.

이 단계는 Archon이 주요 작업을 수행하는 곳입니다. archon loop는 프로젝트를 Lean으로 정식화(formalize)하기 위해 계획(plan), 증명(prover), 검토(review) 에이전트를 여러 반복(iterations)에 걸쳐 교대로 실행하며 — 선택적인 하위 에이전트(Subagents)를 사용할 수 있습니다 (Subagents 참조) — 수행합니다.

archon loop /path/to/your-lean-project

상위 수준의 흐름은 autoformalize → prover → polish → COMPLETE 입니다. 이 중 prover가 가장 긴 단계입니다:

단계	수행 내용
autoformalize	스캐폴딩 (Scaffolding) — 비형식적 수학을 sorry가 포함된 Lean 선언으로 번역
prover	증명 (Proving) — sorry 플레이스홀더(placeholder)를 검증된 증명으로 채움
polish	검증 및 다듬기 (Verification and polish) — 코드 골프(golf), 리팩터링(refactor), 재사용 가능한 보조 정리(lemmas) 추출

모든 단계는 그 출력을 .archon/git-dir/에 있는 내부 git에 archon[NNN/phase]: … 형식으로 커밋합니다.