メニュー
Build, test, and debug Lean 4 projects using Lake. Use when building the ComputationalPaths project, checking for errors, running tests, cleaning artifacts, or debugging Lean 4 compilation issues.
Codex または Claude でインストール この Prompt をコピーして Codex、Claude、または他のアシスタントに貼り付けると、Skill ページを確認してインストールできます。
SOC 職業分類に基づく
Review armada/fleet-generated Lean files for ComputationalPaths invariants, duplicate modules, shallow Path usage, and scaffold-heavy theorem stubs.
Design domain-specific Step types and rewrite certificates in ComputationalPaths modules without confusing them with core Path.Step rewrite rules.
Audit and harden scaffold-heavy ComputationalPaths Lean modules by replacing selected True/trivial/rfl placeholders with typed Path/RwEq certificate records while preserving public APIs.
Keep ComputationalPaths modules suitable as book/paper companion material with clear mathematical narrative, named constructions, and meaningful computational-path evidence.
Recover a broken Lean module with minimal safe edits by weakening non-derivable equalities while preserving declaration shape.
Run Aristotle automated theorem prover on Lean files to fill sorry placeholders. Use when you have a file with sorries that needs automated proof search. Handles API setup, axiom import checks, and result verification.
| name | lean-build |
| description | Build, test, and debug Lean 4 projects using Lake. Use when building the ComputationalPaths project, checking for errors, running tests, cleaning artifacts, or debugging Lean 4 compilation issues. |
Build the ComputationalPaths Lean 4 project using Lake.
# Build entire project
lake build
# Build specific module
lake build ComputationalPaths.Path.CompPath.CircleCompPath
# Clean and rebuild
lake clean && lake build
# Run executable
lake exe computational_paths
| Error | Solution |
|---|---|
unknown identifier | Check imports, use fully qualified name |
type mismatch | Add type annotations or use @ for explicit args |
must be marked as 'noncomputable' | Add noncomputable keyword |
universe level mismatch | Ensure consistent universe variables (typically Type u) |
#check myTerm -- show type
#print axioms myTheorem -- show axioms used
#reduce myTerm -- fully normalize
leanprover/lean4:v4.24.0 (see lean-toolchain)lean-toolchain, then lake clean && lake build