メニュー
Recover a broken Lean module with minimal safe edits by weakening non-derivable equalities while preserving declaration shape.
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.
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.
| name | lean-module-compile-recovery |
| description | Recover a broken Lean module with minimal safe edits by weakening non-derivable equalities while preserving declaration shape. |
| domain | lean-proof-maintenance |
| confidence | high |
| source | earned |
Use this when a single Lean module has many local type-mismatch failures caused by over-strong endpoint equalities that are not derivable from available assumptions, and the goal is to restore compilation safely.
Path/RwEq endpoints on abstract carriers, switch to reflexive witnesses (Path.refl _, RwEq.refl _) when no lawful proof source exists.True in targeted rescue passes.lake build <Module>) to confirm the fix is scoped.Derivation₂/Derivation₃ live in Type (u + 2)), or wrappers/structures will fail with universe and missing-field cascades.MetaStepHigh.diamond_filler (n := n) c₁ c₂), not as unapplied constants.Equivalences.Equiv, prefer ≃ₚ with toFun/isEquiv.inv/sect/retr; avoid unavailable core identifiers like _root_.Equiv and Function.Bijective.theorem declarations must be proposition-valued: when available evidence is Path ..., convert witnesses via .toEq at theorem boundaries.ComputationalPaths/Stable/HomotopyGroups.lean:
Path/RwEq;SpectrumHom.comp_id and SpectrumHom.id_comp to True;& "$env:USERPROFILE\.elan\bin\lake.exe" build ComputationalPaths.Stable.HomotopyGroups.ComputationalPaths/Path/OmegaGroupoid/TruncationProof.lean:
Type u wrappers over Derivation₂/Derivation₃ to Type (u + 2);MetaStepHigh.diamond_filler with explicit n, c₁, c₂;& "$env:USERPROFILE\.elan\bin\lake.exe" build ComputationalPaths.Path.OmegaGroupoid.TruncationProof.ComputationalPaths/Path/HoTT/Descent.lean:
≃ₚ-compatible usage;.toEq;Pushouts.Circle.loop;& "$env:USERPROFILE\.elan\bin\lake.exe" build ComputationalPaths.Path.HoTT.Descent.sorry to silence failures.