Lean Formalize

Before each reviewer slot, follow Selectable Reviewers: resolve invocation → .aris/reviewer.json → Claude Code default (Codex MCP) with reviewer_route.py through the canonical helper resolver, preserving this slot's tier, fresh contexts, source/image inputs and deterministic gates. Codex examples/pins below apply only to backend=codex; other routes use their own first-call/reply contract. Save the route and actual returned identity; unavailable selections are REVIEW_UNAVAILABLE. Classify acceptance from actual families/completion/scope. Forward invocation reviewer/model/effort overrides to reviewer-bearing children. Generation workers are unchanged.

Turn the user's mathematical statement into a checked Lean theorem with its meaning preserved. A compiled conditional lemma is progress; completion concerns the original statement and the trust basis actually used.

When to use Lean

Use this skill when the user requests Lean, when continuing an existing Lean proof, or when formal verification addresses a concrete uncertainty in a central claim, for example, a long dependency chain, a delicate reduction, or coverage of a finite classification. State the obligation it will help resolve and proceed within the authorized task. Difficulty alone is not a reason to formalize. Ordinary derivations and short proofs can stay in formula-derivation or proof-writer; do not make Lean a prerequisite for every mathematical result. Respect the user's chosen proof method and the scale of the requested work.

Core workflow