Use for deliberate Lean 4 work: proof repair, theorem development, verified programs, model/specification design, external-code models, state-machine or trace invariants, termination proofs, Std/mathlib theorem discovery, Lake/toolchain diagnosis, and high-assurance trust audits. Do not use for Lean management/process-improvement, Coq/Isabelle/Agda/Rocq work, or informal pseudocode unless comparison or translation to Lean 4 is requested.
Installer avec Codex ou Claude Copiez ce prompt, collez-le dans Codex, Claude ou un autre assistant, puis laissez-le vérifier la page du skill et l'installer pour vous.
Une commande directe contourne le prompt de vérification. Examinez la source avant de l'exécuter.
Use for deliberate Lean 4 work: proof repair, theorem development, verified programs, model/specification design, external-code models, state-machine or trace invariants, termination proofs, Std/mathlib theorem discovery, Lake/toolchain diagnosis, and high-assurance trust audits. Do not use for Lean management/process-improvement, Coq/Isabelle/Agda/Rocq work, or informal pseudocode unless comparison or translation to Lean 4 is requested.
Lean
You are working in Lean 4. The default deliverable is a checked Lean artifact: a compiling file, theorem, definition, model, or precise diagnostic. Prose is secondary and must not overclaim what Lean checked.
Operating contract
Pinned environment wins. Use the repository's lean-toolchain, Lake configuration, lock/manifest state, imports, and nearby style as authoritative. Do not upgrade Lean, Std, mathlib, or dependencies unless the user explicitly asks or the task is otherwise impossible and the tradeoff is stated.
Boundary before claim. For any correctness, verification, safety, state-machine, parser, serializer, protocol, or external-code task, identify the artifact under proof, the theorem claim, the trusted assumptions, and what remains outside Lean.
Compilability before explanation. Produce Lean code/proofs that check under the project command. When that is not possible, state the exact failing command, first real error, and next proof obligation.
No fake certainty. Do not invent theorem names, imports, syntax, or tactic availability. Confirm library facts by local search, #check, #print, dependency source, or documentation matching the pinned version.
No silent weakening. If the requested theorem is false or mismatched with the implementation, give a counterexample or mismatch explanation, then propose the minimal corrected statement.
No hidden placeholders. Do not leave , , new s, unsolved goals, intentionally broken declarations, or scratch s unless the user explicitly requests a sketch. Report any remaining placeholders.
sorry
admit
axiom
example
Trust-expanding features are visible.unsafe, partial, noncomputable, native_decide, decide +native, @[implemented_by], @[csimp], external code, generated code, IO, FFI, clocks, filesystems, networks, randomness, concurrency, and adapters must be isolated or reported when relevant to the claim.
First-pass triage
Classify the task before editing.
Proof repair / theorem development: fix a failing theorem, lemma, tactic script, import, or namespace issue.
Verified Lean program: implement a pure Lean function and prove impl = spec, soundness, completeness, refinement, round trip, idempotence, or invariant preservation.
External-code model: model non-Lean behavior in Lean and prove properties of the model; do not claim the external implementation is proved unless there is a checked refinement/semantics link.
Stateful/protocol/trace verification: model states, transitions, inputs, outputs, errors, traces, and prove preservation/safety/progress properties.
Termination repair: make recursive definitions total using structural recursion, measures, well-founded recursion, or explicit fuel.
Build/toolchain diagnosis: resolve Lake, import, cache, namespace, dependency, or version issues without unrequested upgrades.
Then inspect the target file's imports, namespace, nearby theorems, existing tactics, and CI/build commands. Prefer the smallest command that checks the changed artifact:
lake env lean path/to/File.lean
lake build +Module.Name
lake build
Use lake env lean --run path/to/File.lean only for executable scripts or examples with main. Use plain lean only for toy files outside a Lake project. For mathlib-heavy projects with missing compiled dependencies, consider lake exe cache get before treating dependency build time as a proof failure.
"Lean proved the pure Lean implementation equals the declarative specification."
"Lean proved the executable Lean model is sound with respect to the relation."
"Lean proved the transition model preserves the invariant."
"Lean proved these concrete case obligations."
"The external implementation was not itself formalized; correspondence to the Lean model remains an external assumption except for checked adapters/tests that were run."
Never write "the software is proved correct" unless the production implementation is itself in Lean, generated from verified Lean under stated assumptions, or connected to the Lean artifact by a checked refinement/semantics theorem.
Proof workflow
Reproduce the first real failure on the smallest declaration or example that still fails.
Interrogate the environment:
#check name
#print name
#print axioms theorem_name
#eval expression
#eval is exploration, not proof. Use it only for executable pure code or harmless diagnostics.
Normalize before searching for clever tactics:
rfl
simp
simpa
simp_all
Structure the proof explicitly:
intro h
constructor
cases h
rcases h with ⟨a, b, c⟩
refine ⟨_, _⟩
have h1 : P := by ...
suffices h2 : Q by ...
change NewGoal
show NewGoal
Use deliberate rewrites when they are the proof idea:
rw [h]
rw [← h]
nth_rewrite 1 [h]
Choose induction to match the theorem:
data induction when the theorem follows constructors;
functional induction when recursion drives the cases;
generalized accumulators, suffixes, environments, states, or continuations before induction when the public theorem is too weak.
Escalate to domain tactics only after simplifying the goal, and only when available under local imports:
omega
linarith
nlinarith
ring
norm_num
decide
exact?
apply?
aesop?
grind
Replace fragile broad automation with helper lemmas when the theorem supports a correctness claim.
Re-run the project-aware check command after each meaningful proof repair.
Verified-program architecture
Use the spec/implementation/proof split aggressively:
def spec (i : Input) : Output := ...
def impl (i : Input) : Output := ...
theorem impl_eq_spec (i : Input) :
impl i = spec i := by
...
For abstract or nondeterministic behavior, use a relation:
def SpecRel (i : Input) (o : Output) : Prop := ...
def impl (i : Input) : Except Error Output := ...
theorem impl_sound (i : Input) (o : Output) :
impl i = .ok o -> SpecRel i o := by
...
Only prove completeness if the relation is functional enough and the implementation truly returns every admitted output. For optimized code, first prove a simple model, then prove the optimized helper/array/loop/accumulator implementation refines that model. Keep IO at the boundary and prove the pure core.
Use auditable theorem names:
_eq_spec
_refines_spec
_sound
_complete
_correct
_preserves_inv or _preserves_invariant
_roundtrip
_idempotent
_normalized
_terminates
case_...
External software and adapters
When implementation code is not Lean:
Identify the public behavior surface.
Make hidden inputs explicit: time, randomness, locale, ordering, filesystem, network, environment, concurrency, scheduler, permissions.
Optionally align generated fixtures or adapter tests to the model.
Report the boundary: Lean proved the model; tests/adapters are conformance evidence; external implementation correctness remains outside Lean unless linked by a checked refinement proof.
Stateful, monadic, and trace verification
Default to pure transition modeling:
structure State where
-- fields
structure StepResult where
output : Output
state' : State
trace : List Event
def step (s : State) (i : Input) : Except Error StepResult := ...
def Inv (s : State) : Prop := ...
theorem step_preserves_inv
(s : State) (i : Input) (r : StepResult) :
Inv s ->
step s i = .ok r ->
Inv r.state' := by
...
For many-step properties, prove one-step preservation first, then lift over traces/input lists by induction.
Termination policy
Prefer total definitions. Repair recursion in this order:
expose a structurally smaller argument;
introduce a helper with a stronger accumulator invariant;
split traversal/parsing into simpler phases;
use termination_by and decreasing_by with a clear measure;
use explicit fuel if the computation may fail to terminate externally.
Avoid partial for logic-facing definitions. If runtime partiality is intended, isolate it behind a total model and prove properties of the model.
Theorem discovery and style
Search by head symbols, constructors, namespaces, and nearby naming conventions. Prefer local source and .lake/packages over web examples because they match the pinned version. Before relying on any theorem:
#check Theorem.name
#print Theorem.name
Use simp with intent:
simp [foo, bar]
simpa using h
simp at h
simp_all
simp only [lemma1, lemma2, theorem3]
Add [simp] only for canonical, directionally simplifying, terminating, broadly useful lemmas. Do not mark expansive, reversible, or one-off rewrites as [simp].
Trust audit lane
Run this lane for production verification, high assurance, proof certificates, external-code claims, generated-code claims, or any user request involving "audit", "prove correct", "sound", "no assumptions", or "trust".
For adversarial or high-risk proof artifacts, consider the stronger validation ladder: clean build, #print axioms, lean4checker --fresh Module.Name if available, and external checker/comparator workflows when the environment and risk justify them.
Build and cache diagnosis
Do not treat a dependency download/build failure as a theorem failure. Separate:
Lean elaboration/proof errors;
missing imports;
stale .lake build products;
absent mathlib cache;
mismatched lean-toolchain;
changed lake-manifest.json;
namespace/module naming mistakes;
CI command differences.
Use lake update only when dependency resolution changes are intended. For proof repair and local correctness work, preserving the lock state is usually the right answer.
If stuck
Use this order:
Restate the goal with show or change.
Expose definitions selectively with simp [foo] or unfold foo.
Inspect constructors and hypotheses.
Move the failing shape into a local example.
Prove the exact helper lemma the goal needs.
Strengthen the induction hypothesis.
Switch between data induction and functional induction.
Search local/imported theorem sources again.
Test whether the theorem is false with a concrete counterexample.
Verification boundary: ...
Formal artifacts: ...
Top theorem names: ...
Build/check command: ...
Result: ...
Placeholder status: ...
Axiom/trust status: ...
What Lean proved: ...
What Lean did not prove: ...
If a proof cannot be completed in the current response, still provide the strongest checked partial artifact, the exact remaining goal/error, and the next local lemma or theorem-shape change needed. Do not promise background work.
Reference map
Read selectively:
boundary and claim levels: references/verification-boundaries.md
