Menu
Recover a broken Lean module with minimal safe edits by weakening non-derivable equalities while preserving declaration shape.
Install with Codex or Claude Copy this prompt, paste it into Codex, Claude, or another assistant, and let it review the skill page and install it for you.
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.
Based on SOC occupation classification
| 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.