lean4
Редактирует .lean файлы, отлаживает сборки Lean 4 (ошибки типов, lake build), ищет леммы в mathlib. Формализует математику, находит контрпримеры. Помогает с Lean 4, mathlib и lakefile. Не подходит для Coq, Agda, Isabelle.
AIcameronfreer
official
Разработка
★ 459
Что делает навык
Редактирует .lean файлы, отлаживает сборки Lean 4 (ошибки типов, lake build), ищет леммы в mathlib. Формализует математику, находит контрпримеры. Помогает с Lean 4, mathlib и lakefile. Не подходит для Coq, Agda, Isabelle.
Как подключить
1Скачать навык
# возьмите папку навыка «lean4» из репозитория:
# https://github.com/cameronfreer/lean4-skills
2Положить папку с
SKILL.md к навыкам ассистента# положите папку навыка туда, где ассистент ищет skills:
cp -r lean4/ ~/.claude/skills/lean4/
Навык — папка с файлом SKILL.md (описание + инструкции) и опциональными скриптами. Ассистент (Claude, Claude Code и совместимые) подхватывает его по описанию и следует шагам.