cameronfreer/lean4-skills

Registry 信息

项目简介

一个 Claude Skill 仓库，提供用于 Lean 4 定理证明的工具和配置，支持 AI 辅助的形式化验证和数学推理。

要点

• 为 Lean 4 集成的 Claude Skill
• AI 辅助定理证明设置
• 形式化验证工作流配置

使用场景

• 使用 AI 自动化 Lean 4 证明步骤
• 在 Claude 辅助下学习形式化验证
• 增强数学推理工作流

README 摘要

# Lean 4 Skills Lean 4 workflow pack for AI coding agents. Gives your agent a structured prove/review/golf loop, mathlib search, axiom checking, and safety guardrails. The workflows are host-agnostic — Claude Code, Codex, Gemini CLI, Cursor, and others all use the same core skill; only the invocation surface differs. ## Workflows | Workflow | Description | |---|---| | draft | Draft Lean declaration skeletons from informal claims | | formalize | Interactive formalization — drafting plus guided proving | | autoformalize | Autonomous end-to-end formalization from informal sources | | prove | Guided cycle-by-cycle theorem proving | | autoprove | Autonomous multi-cycle proving with explicit stop budgets | | checkpoint | Save point (per-file + project build, axiom check, commit) | | review | Read-only quality review | | refactor | Leverage mathlib, extract helpers, simplify proof strategies | | golf | Improve proofs for directness, clarity, performance, and brevity | | learn | Interactive teaching and mathlib exploration | | doctor | Diagnostics and migration help | **Claude Code:** invoke as `/lean4:<name>`. **Other hosts:** follow the corresponding workflow in [SKILL.md](plugins/lean4/skills/lean4/SKILL.md). Typical session: `draft` (or `formalize` / `autoformalize`) → `prove` (or `autoprove`) → `review` → `refactor` → `golf` → `checkpoint` → `git push`. CLI-like inputs are validated by a host-agnostic parser (`plugins/lean4/lib/command_args/`) for the six parameter-heavy commands. The Claude Code adapter pre-validates `/lean4:*` prompts via a `UserPromptSubmit` hook; other hosts fall back to model-parsed startup. Commands must announce resolved inputs, reject invalid startup configs, and treat wall-clock budgets as best-effort rather than host-enforced timeouts. See

话题

暂无话题