메뉴
Keep ComputationalPaths modules suitable as book/paper companion material with clear mathematical narrative, named constructions, and meaningful computational-path evidence.
Codex 또는 Claude로 설치 이 Prompt를 복사해 Codex, Claude 또는 다른 어시스턴트에 붙여 넣으면 Skill 페이지를 검토하고 설치를 진행할 수 있습니다.
SOC 직업 분류 기준
| name | paper-companion-style |
| description | Keep ComputationalPaths modules suitable as book/paper companion material with clear mathematical narrative, named constructions, and meaningful computational-path evidence. |
Use this skill when adding or deepening modules intended to accompany the ComputationalPaths paper or book-style exposition.
Each substantial module should have:
Prefer statements that expose computational content:
structure PresentationCertificate where
generators : Nat
relations : Nat
generator_count : Path generators expectedGenerators
relation_count : Path relations expectedRelations
coherence : RwEq (Path.trans generator_count (Path.refl expectedGenerators)) generator_count
Avoid book-companion anti-patterns:
True fields with no surrounding mathematical datafoo_theorem_1PascalCasecamelCase or established local conventionsnake_case if the file already uses
theorem-style namingFooCertificate, FooCoherence, or
FooRewriteCertificateFor code changes, run the smallest meaningful build:
lake build ComputationalPaths.Path.Area.ModuleName
For documentation-only companion edits, run:
git diff --check
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.
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.
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.