菜单
Auxiliary proof-strategy help for hard Lean theorem repairs. Use when repeated focused attempts fail and another configured model or command expert should advise without editing files or changing existing statements.
用 Codex 或 Claude 帮你安装 复制这段 Prompt，粘贴到 Codex、Claude 或其他助手里，让它检查 Skill 页面并帮你完成安装。
基于 SOC 职业分类
Native Lean search entry. Use the shared `lean_search` surface first across local-project and Mathlib/semantic modes, with provider-aware fallbacks and result provenance.
Run a user-approved Lean swarm with clear file ownership, verifier roles, and strict zero-sorry verification.
Native diagnostics/review/doctor entry. Use structured capability, inspection, and verification state instead of ad hoc summaries.
Native formalization workflow entry. Follow the formalize/draft specs, typed Lean tools, and queue-driven verification ladder.
Native proving workflow entry. Follow the prove/formalize specs, structured Lean tools, queue state, and router decisions instead of free-form proof guessing.
Native refactor/golf routing entry. Load the linked workflow specs as the contract, preserve theorem meaning, and keep optimization inside the direct Lean tool surface.
| name | lean-reasoning-help |
| description | Auxiliary proof-strategy help for hard Lean theorem repairs. Use when repeated focused attempts fail and another configured model or command expert should advise without editing files or changing existing statements. |
Use this skill for hard theorem-local blockers after normal proof workflow steps have produced useful context but no working proof.
lean_reasoning_help with the theorem id, file path, current diagnostics, current attempt, and recent failed attempts.lean_incremental_check(check_target) for the assigned declaration, or lean_verify(mode=file_exact) when doing a final Lake sweep or explicit canonical check.sorry.sorry, admit, axioms, unsafe code, or another placeholder, ignore that part and continue with verified proof repair.lean_reasoning_help routes through the shared auxiliary client task lean_reasoning by default. When explicitly configured with codex or claude-code, it instead invokes the corresponding command expert in an advisory mode.
Configure it with either:
auxiliary.lean_reasoning.providerauxiliary.lean_reasoning.modelauxiliary.lean_reasoning.base_urlauxiliary.lean_reasoning.api_keyauxiliary.lean_reasoning.command_templateauxiliary.lean_reasoning.codex_command_templateauxiliary.lean_reasoning.claude_code_command_templateor environment overrides:
AUXILIARY_LEAN_REASONING_PROVIDERAUXILIARY_LEAN_REASONING_MODELAUXILIARY_LEAN_REASONING_BASE_URLAUXILIARY_LEAN_REASONING_API_KEYAUXILIARY_LEAN_REASONING_COMMAND_TEMPLATELEANFLOW_EXPERT_CODEX_COMMAND_TEMPLATELEANFLOW_EXPERT_CLAUDE_CODE_COMMAND_TEMPLATEWorkflow launches can also pass --expert-provider codex, --expert-provider claude-code, and --expert-command-template .... Command experts receive the advisor prompt on stdin and must still be treated as unverified advice.