Insights
AI가 자동으로 큐레이션·번역·정리하는 기술 동향 피드입니다.
이 패키지는 AI 코딩 에이전트를 위한 Lean 4 워크플로우를 제공하며, 구조화된 증명(prove)/검토(review)/최적화(golf) 루프와 안전 가드레일을 포함합니다. 해당 워크플로우는 Claude Code, Codex 등 다양한 호스트 환경에 구애받지 않도록 설계되었으며, 명확한 개발 사이클을 제시합니다.
AI 자동 생성 콘텐츠
본 콘텐츠는 GitHub Codex tools의 원문을 AI가 자동으로 요약·번역·분석한 것입니다. 원 저작권은 원저작자에게 있으며, 정확한 내용은 반드시 원문을 확인해 주세요.
원문 바로가기AI 코딩 에이전트를 위한 Lean 4 워크플로우 패키지입니다. 에이전트에게 구조화된 증명(prove)/검토(review)/최적화(golf) 루프, mathlib 검색, 공리 확인 및 안전 가드레일을 제공합니다.
이 워크플로우는 호스트에 구애받지 않습니다 (host-agnostic). Claude Code, Codex, Gemini CLI, Cursor 등 모두 동일한 핵심 스킬을 사용하며, 호출 인터페이스만 다릅니다.
| Host | Recommended installation | What you get | Details |
|---|---|---|---|
| Claude Code | Native plugin (Tier 3) | Skill + /lean4:* commands, hooks, guardrails, subagents, helper runtime | Claude Code |
| ... | |||
| Claude Code (채팅에서 실행): |
/plugin marketplace add cameronfreer/lean4-skills
/plugin install lean4
Codex (쉘에서):
codex plugin marketplace add cameronfreer/lean4-skills --ref main
codex plugin add lean4@lean4-skills
호스트 네이티브 스킬 설치 프로그램은 일반적으로 지침과 참조만 제공합니다. 번들된 래퍼(wrappers)와 스크립트도 필요한 경우 포터블 런타임(portable runtime)을 사용하십시오. Claude Code와 Codex는 네이티브 전체 플러그인 설치를 제공합니다.
| Workflow | Description |
|---|---|
| draft | 비공식적인 주장으로부터 Lean 선언 골격 초안 작성 |
| ... | |
Claude Code: /lean4:<이름>으로 호출합니다. 다른 호스트: SKILL.md의 해당 워크플로우를 따릅니다. |
일반적인 세션: draft (또는 formalize / autoformalize) → prove (또는 autoprove) → review → refactor → golf → checkpoint → git push. 주장을 증명하는 대신 반증하려면 prove 대신 disprove를 사용하십시오.
일곱 개의 매개변수가 많은 명령어에 대한 CLI(Command Line Interface)와 유사한 입력은 호스트에 구애받지 않는 파서에 의해 검증됩니다. Command Invocation Contract를 참조하십시오.
증명 워크플로우(proving workflows)인 prove, autoprove, formalize, 그리고 autoformalize는 하나의 사이클—계획(Plan) → 작업(Work) → 체크포인트(Checkpoint) → 검토(Review) → 재계획(Replan) → 계속/중지(Continue/Stop)—을 공유합니다. 이 과정에서 각 'sorry'는 mathlib 검색, 전술 시도(tactic attempts), 및 유효성 검사를 받으며, 막히면 검토와 재계획이 강제됩니다. 명세(Statement) 및 헤더 변경은 합성 워크플로우(formalize / autoformalize)에 속하며, prove와 autoprove는 선언 헤더를 불변(immutable)으로 유지합니다. 명령 없이 .lean 파일을 편집하면 하나의 유한 패스(bounded pass)가 실행됩니다—즉시 문제를 수정하고 적절한 워크플로우로 넘기며—저항하는 목표에 대해서는 Blocked-Goal Triage loop를 사용합니다. 자세한 내용은: cycle-engine.md.
모든 PR은 CI(Continuous Integration) 게이트를 통과합니다: 전체 문서화 lint, 의미론적 계약 스위트(semantic contract suites), Linux 및 macOS Bash 3.2에서의 후크 및 래퍼 런타임 테스트, 그리고 고정된 shellcheck/ruff/mypy/actionlint가 포함됩니다. Quick Start 테이블에서 "documented"로 표시된 호스트는 검증된 설정 패턴을 따르지만 CI 테스트를 거치지는 않습니다.
이 스킬은 독립적으로 작동하지만 lean-lsp-mcp와 가장 잘 조합됩니다: 실시간 목표 검사(live goal inspection), mathlib 검색, 그리고 일반적으로 반복적인 전체 빌드보다 훨씬 빠른 피드백을 제공합니다. subagent 가시성을 위한 Claude Code 범위 트레이드오프를 포함하여 모든 호스트에 등록하려면 INSTALLATION.md → MCP Server를 참조하십시오.
https://github.com/cameronfreer/lean4-skills에서 이슈 및 PR을 환영합니다. lean4-contribute 플러그인을 설치하면, 에이전트가 자연스러운 중단 지점에서 버그 보고서(bug reports), 기능 요청(feature requests) 또는 통찰력(insights) 제출을 제안할 수 있습니다. 초안 작성은 사용자가 선택적으로 동의한 후에만 시작되며, 모든 초안은 전송되기 전에 전체 내용으로 표시됩니다.
MIT 라이선스가 적용됩니다. 더 자세한 내용은 LICENSE를 참조하십시오.
이 저장소를 인용하는 것은 매우 감사하지만, 라이선스상 필수 사항은 아닙니다. 또한 CITATION.cff도 참고하십시오.
@software{lean4-skills,
author = {Cameron Freer},
title = {Lean 4 {Skills}: Theorem proving skill and workflow pack for {AI} coding agents},
...