lean-formalize

wanshuiyin/Auto-claude-code-research-in-sleep/skills/lean-formalize

在 Lean 中开发验证数学证明并检查公理链

Develop and verify a mathematical proof in Lean, continue an incomplete Lean project, or audit whether it proves the original statement. Connect actual inputs to intermediate lemmas, assemble the target theorem, check its transitive axioms, and provide a reproducible handoff. Use when Lean is requested or a specific proof obligation benefits from formal verification; use proof-writer for ordinary mathematical drafting.

把下面的话发给 Claude Code、Codex 或 Cursor。智能体会先检查内容，经你确认再安装。

请帮我安装这个 Agent Skill：https://github.com/wanshuiyin/Auto-claude-code-research-in-sleep/tree/main/skills/lean-formalize

1. 先读取该目录下的 SKILL.md 和其他文件，检查是否有可疑内容（执行未知脚本、读取密钥、向外发送数据等），用中文告诉我它会做什么、需要哪些权限；
2. 等我确认后，再把整个目录安装到 ~/.claude/skills/lean-formalize/（如果你不是 Claude Code，安装到你自己约定的 skills 目录）；
3. 安装后告诉我怎么触发它。

安装到个人 Skill 目录（对所有项目生效）。只想在当前项目用，改为 .claude/skills/。

git clone --depth 1 --filter=blob:none --sparse https://github.com/wanshuiyin/Auto-claude-code-research-in-sleep.git /tmp/lean-formalize-src
cd /tmp/lean-formalize-src && git sparse-checkout set "skills/lean-formalize"
mkdir -p ~/.claude/skills && cp -r "skills/lean-formalize" ~/.claude/skills/lean-formalize

Skill 可以让智能体执行脚本。安装第三方 Skill 前务必看一遍内容，详见「安全」一课。

SKILL.md

在 GitHub 查看

正在从 GitHub 读取……