| 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. |
Lean Reasoning Help
Use this skill for hard theorem-local blockers after normal proof workflow steps have produced useful context but no working proof.
Contract
- Preserve the assigned theorem/lemma/example statement exactly.
- Call
lean_reasoning_help with the theorem id, file path, current diagnostics, current attempt, and recent failed attempts.
- Treat the result as advice only; do not accept it until a concrete edit passes
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.
- Do not use auxiliary advice to justify deleting, weakening, renaming, moving, or replacing the declaration with
sorry.
- If the advice suggests a statement change, report that as a blocker instead of applying it. A blocker or accurate open-problem assessment is route-change evidence only: request a distinct route, job, portfolio refresh, or fresh epoch and continue; advisor prose cannot make it terminal.
- If the advice suggests
sorry, admit, axioms, unsafe code, or another placeholder, ignore that part and continue with verified proof repair.
- Helper lemmas or private supporting declarations are acceptable advice when they preserve existing statements and directly support the assigned theorem.
- If the advisor is unavailable, returns no answer, gives irrelevant advice, or recommends stopping, continue the main Lean workflow from the strongest verified local evidence; missing or surrendering advice is not evidence that the theorem statement is wrong or mathematically resolved.
Configuration
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_template
or 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_TEMPLATE
Workflow 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.
