Lean 4 programming and proof development

Resolve bundled resources from the skill root; run Lake commands from the consumer's package root. Use official Lean documentation and the reference matching the actual compiler, not a different /latest/ release.

Step 1: Fix the contract and trust level

1. Identify the task: installation, existing package change, executable behavior, mathematical formalization, or validation of an untrusted proof. Read project instructions, lean-toolchain, Lake configuration, manifest, affected imports and declarations before changing them.
2. Record exact theorem statements, binders, hypotheses, type classes, definitions and intended informal meaning. Preserve the requested statement; proving a weaker, shadowed or vacuous proposition is not completion.
3. Separate Lean's formal model from an external program/system. A kernel-checked theorem proves its elaborated proposition relative to its definitions and axioms, not that an unmodeled implementation matches it.
4. Treat Lake configurations, imports, macros, tactics and #eval as executable code. Review ordinary project code before building. For untrusted/AI-generated proof submissions, read references/proofs-mathlib-trust.md before loading them; use the sandboxed validation route and a trusted challenge when statement identity matters.

Gate: the target statement/runtime contract, toolchain selection and executable trust boundary are explicit.

Step 2: Establish the package environment