用 Codex 或 Claude 帮你安装 复制这段 Prompt，粘贴到 Codex、Claude 或其他助手里，让它检查 Skill 页面并帮你完成安装。
直接命令不会经过审查 Prompt；运行前请先检查来源。
npx skills add https://github.com/leanprover/skills --skill mathlib-build命令会保持在同一行。复制前请横向滚动并检查完整内容。
想先保存到本地？可下载 SkillsMP 当前能够提供的文件。
Use when asked to prove something in Lean. Covers one-step-at-a-time proving, error priority, working on the hardest case first, proof cleanup, and handling dependent type rewriting issues.
Bisect Lean toolchain versions to find where behavior changes. Use when trying to identify which Lean 4 commit caused a regression or behavior change.
Create minimal working examples (MWEs) from Lean errors for bug reports. Use when minimizing a Lean error, creating an MWE, or preparing a bug report for lean4 or mathlib4.
基于 SOC 职业分类
正在显示 SKILL.md
| name | mathlib-build |
| description | Building Mathlib |
Fetch the Mathlib olean cache before build:
lake exe cache get
Use lake exe cache get! (with !) to force re-download if the cache appears corrupt.
When building Mathlib reduce verbosity to save on tokens:
lake build -q --log-level=info
For merge conflict resolution or small fixes build only the affected files: lake build Mathlib.Foo.Bar -q --log-level=info.
Often it is fine to leave a complete build to CI. If you need a thorough local build, use lake build Mathlib MathlibTest Archive Counterexamples && lake exe runLinter.