주요 기능

• /prove 및 /autoprove 명령어로 Lean 4 코드의 논리적 증명을 자율적으로 생성
• /formalize 기능을 통해 자연어 수학 명제를 검증 가능한 Lean 4 코드로 자동 변환
• /swarm 시스템을 활용하여 백엔드에서 실행 중인 여러 에이전트의 상태를 실시간 추적 및 제어
• vLLM 서버 연동으로 OpenAI 호환 API를 로컬 GPU에서 실행하여 운영 비용 절감
• 프로젝트 단위의 컨텍스트 관리로 Lean 툴체인과 MCP/LSP 연결을 자동 최적화

어떻게 동작하는가

사용자의 슬래시 명령어를 lean4-skills 워크플로우로 변환한 뒤, 프로젝트 루트에서 관리형 백엔드 자식 에이전트를 생성하여 MCP 및 LSP 통신으로 증명 상태를 동기화합니다.

사용 사례

• 수학 연구자가 복잡한 논문을 Lean 4로 정형화할 때 Claude Code 에이전트와 협업하여 작성
• 로컬 vLLM 서버에 배포된 오픈소스 모델을 활용하여 보안이 중요한 수학적 증명 프로젝트 수행
• 기존 Lean 4 프로젝트를 Gauss 모델로 변환하여 멀티 에이전트 기반의 자동 증명 워크플로우 구축