writing-lean-proofs — скилл для Claude Code: Lean 4
Помогает писать и проверять доказательства Lean 4 по соглашениям Mathlib. Нужен при формализации теорем, рефакторинге тактик и настройке проверок проекта.
npx skills add trailofbits/skills --skill writing-lean-proofs -a claude-codeЧто делает writing-lean-proofs
Скилл ведёт работу от интерфейса к доказательству: предлагает сначала определить типы, функции и утверждения, затем собрать компилируемый каркас с sorry и закрывать цели по одной. Для цепочек равенств он ориентирует на блоки calc, а для промежуточных шагов различает have и suffices.
Он затрагивает API новых определений, леммы ext, @[simp], приведения и инъективность, а также разбор медленных доказательств и таймаутов maxHeartbeats. Для диагностики состояния целей используются trace_state, done и запуск lake env lean Path/To/File.lean.
Скилл опирается на стиль Mathlib, поэтому в проекте с собственными правилами сначала сверяйте CONTRIBUTING: это повод не переносить рекомендации автоматически. Он не рассчитан на Lean 3, Coq, Isabelle или Agda.
Какие задачи решает
- разбить доказательство Lean 4 на независимые леммы
- заполнить места с
sorryв разработке - переписать длинный тактический код через
calc - найти причину таймаута
maxHeartbeats - настроить проверку непроверенных обязательств в CI
Примеры запросов агенту
- «Составь каркас доказательства для этой теоремы Lean 4 и оставь независимые шаги с
sorry.» - «Проверь этот файл Lean на соглашения Mathlib и предложи, какие леммы вынести.»
- «Разбери таймаут
maxHeartbeatsвPath/To/File.leanс помощьюtrace_state.»
Как установить writing-lean-proofs
1Через Skills CLI (Vercel)
npx skills add trailofbits/skills --skill writing-lean-proofs -a claude-code2Вручную: положить файлы
~/.claude/skills/writing-lean-proofs/SKILL.mdПапка скилла целиком; для одного проекта — .claude/skills/writing-lean-proofs/
1Через Skills CLI (Vercel)
npx skills add trailofbits/skills --skill writing-lean-proofs -a codex2Вручную: положить файлы
.agents/skills/writing-lean-proofs/SKILL.mdДля всех проектов — ~/.agents/skills/
1Через Skills CLI (Vercel)
npx skills add trailofbits/skills --skill writing-lean-proofs -a cursor2Вручную: положить файлы
.cursor/skills/writing-lean-proofs/SKILL.mdCursor читает и .agents/skills/, и .claude/skills/
1GitHub CLI
gh skill install trailofbits/skills writing-lean-proofs2Вручную: положить файлы
.github/skills/writing-lean-proofs/SKILL.md1Через Skills CLI (Vercel)
npx skills add trailofbits/skills --skill writing-lean-proofs -a gemini-cli2Командой платформы
gemini skills install https://github.com/trailofbits/skills --path plugins/writing-lean-proofs/skills/writing-lean-proofsВручную: положить файлы
.devin/skills/writing-lean-proofs/SKILL.mdСтарый путь .windsurf/skills/ тоже читается
Через Skills CLI (Vercel)
npx skills add trailofbits/skills --skill writing-lean-proofs -a opencodeClaude.ai
Упакуйте папку в zip и загрузите в Settings → Capabilities → Skills
По шагам, с командами для каждой платформы: Как установить скилл в Claude Code: пять способов
Вопросы о writing-lean-proofs
Как установить writing-lean-proofs в Claude Code?
Выполните npx skills add trailofbits/skills --skill writing-lean-proofs -a claude-code, затем ещё раз npx skills add trailofbits/skills --skill writing-lean-proofs -a claude-code. Файл скилла расположен в ~/.claude/skills/writing-lean-proofs/SKILL.md.
Что делает writing-lean-proofs?
Скилл помогает строить, проверять и перерабатывать доказательства Lean 4 по практикам Mathlib. Он охватывает структуру библиотек, тактики, линтеры и проверки в CI.
Подходит ли writing-lean-proofs для Lean 3?
Нет. Рекомендации рассчитаны на Lean 4; приёмы и названия тактик Lean 3 отличаются.
