cameronfreer/lean4-skills

해결하는 문제

Lean 4 언어를 사용하여 형식적 검증과 정리 증명을 수행할 수 있도록 AI 코딩 에이전트를 위한 구조화된 워크플로우를 제공합니다. 비형식적인 수학적 주장과 인증된 증명 사이의 격차를 메우며, 에이전트가 Lean 코드를 초안 작성, 증명, 검토, 최적화할 수 있는 체계적인 방법을 제공합니다.

작동 방식

이 프로젝트는 Claude Code, Codex, Cursor, Gemini CLI와 같은 다양한 AI 에이전트에 통합할 수 있는 호스트 독립적인 "스킬"(워크플로우) 세트를 구현합니다. 이러한 워크플로우는 공통된 증명 주기를 따릅니다: 계획 → 작업 → 체크포인트 → 리뷰 → 재계획 → 계속/정지.

주요 기능:

• 형식화: 비형식적인 주장들을 Lean 선언의 골격으로 변환.
• 증명: 가이드된 또는 자율적인 정리 증명 주기. mathlib 검색 및 태크틱 시도 포함.
• 검증: 공리 검사 및 안전 가드레일을 통해 증명의 무결성을 보장.
• 최적화: 증명을 "골핑"하여 간결성, 명확성, 성능을 향상.
• 통합: 실시간 목표 검사와 빠른 피드백을 위해 Lean LSP MCP와 옵션으로 연동 가능.

대상 사용자

AI 코딩 에이전트를 사용하여 형식적 증명을 작성하거나, 소프트웨어를 검증하거나, Lean 4 생태계 내에서 수학을 탐구하는 개발자 및 연구자.

주요 특징

• 호스트 독립성: Claude Code, Codex, Cursor 등 여러 에이전트 플랫폼에서 작동.
• 포괄적인 워크플로우: 초안 작성, 자동 증명, 반증, 리팩터링을 위한 전용 명령어 포함.
• 인증된 반증: 반례 탐색을 위한 전용 disprove 워크플로우.
• 강력한 도구 세트: 호스트 독립적인 명령어 검증 파서와 CI 가드된 런타임 테스트 포함.