---

name: skill-lean-research description: Research Lean 4 and Mathlib for theorem proving tasks. Invoke for Lean-language research using LeanSearch, Loogle, and lean-lsp tools. allowed-tools: Task, Bash, Edit, Read, Write

Original tools (now used by subagent):

- mcp__lean-lsp__lean_leansearch, mcp__lean-lsp__lean_loogle, mcp__lean-lsp__lean_leanfinder

- mcp__lean-lsp__lean_local_search, mcp__lean-lsp__lean_hover_info, mcp__lean-lsp__lean_goal

---

Lean Research Skill

Thin wrapper that delegates Lean research to lean-research-agent subagent.

IMPORTANT: This skill implements the skill-internal postflight pattern. After the subagent returns, this skill handles all postflight operations (status update, artifact linking, git commit) before returning. This eliminates the "continue" prompt issue between skill return and orchestrator.

Context References

Reference (do not load eagerly):

• Path: .claude/context/core/formats/return-metadata-file.md - Metadata file schema
• Path: .claude/context/core/patterns/postflight-control.md - Marker file protocol
• Path: .claude/context/core/patterns/jq-escaping-workarounds.md - jq escaping patterns (Issue #1132)

Note: This skill is a thin wrapper with internal postflight. Context is loaded by the delegated agent.

Trigger Conditions

This skill activates when:

• Task language is "lean"
• Research involves Mathlib, theorems, or proofs
• Lean-specific MCP tools are needed

---

Execution Flow

Stage 1: Input Validation

Validate required inputs:

• task_number - Must be provided and exist in state.json
• focus_prompt - Optional focus for research direction

# Lookup task
task_data=$(jq -r --argjson num "$task_number" \
  '.active_projects[] | select(.project_number == $num)' \
  specs/state.json)

# Validate exists
if [ -z "$task_data" ]; then
  return error "Task $task_number not found"
fi

# Extract fields
language=$(echo "$task_data" | jq -r '.language // "general"')
status=$(echo "$task_data" | jq -r '.status')
project_name=$(echo "$task_data" | jq -r '.project_name')
description=$(echo "$task_data" | jq -r '.description // ""')

---

Stage 2: Preflight Status Update

Update task status to "researching" BEFORE invoking subagent.

Update state.json:

jq --arg ts "$(date -u +%Y-%m-%dT%H:%M:%SZ)" \
   --arg status "researching" \
   --arg sid "$session_id" \
  '(.active_projects[] | select(.project_number == '$task_number')) |= . + {
    status: $status,
    last_updated: $ts,
    session_id: $sid
  }' specs/state.json > /tmp/state.json && mv /tmp/state.json specs/state.json

Update TODO.md: Use Edit tool to change status marker from [NOT STARTED] or [RESEARCHED] to [RESEARCHING].

---

Stage 3: Create Postflight Marker

Create the marker file to prevent premature termination:

# Ensure task directory exists
mkdir -p "specs/${task_number}_${project_name}"

cat > "specs/${task_number}_${project_name}/.postflight-pending" << EOF
{
  "session_id": "${session_id}",
  "skill": "skill-lean-research",
  "task_number": ${task_number},
  "operation": "research",
  "reason": "Postflight pending: status update, artifact linking, git commit",
  "created": "$(date -u +%Y-%m-%dT%H:%M:%SZ)",
  "stop_hook_active": false
}
EOF

---

Stage 4: Prepare Delegation Context

Prepare delegation context for the subagent:

{
  "session_id": "sess_{timestamp}_{random}",
  "delegation_depth": 1,
  "delegation_path": ["orchestrator", "research", "skill-lean-research"],
  "timeout": 3600,
  "task_context": {
    "task_number": N,
    "task_name": "{project_name}",
    "description": "{description}",
    "language": "lean"
  },
  "focus_prompt": "{optional focus}",
  "metadata_file_path": "specs/{NNN}_{SLUG}/.return-meta.json"
}

---

Stage 5: Invoke Subagent

CRITICAL: You MUST use the Task tool to spawn the subagent.

Required Tool Invocation:

Tool: Task (NOT Skill)
Parameters:
  - subagent_type: "lean-research-agent"
  - prompt: [Include task_context, delegation_context, focus_prompt, metadata_file_path]
  - description: "Execute Lean research for task {N}"

DO NOT use Skill(lean-research-agent) - this will FAIL.

The subagent will:

• Search Mathlib using lean_leansearch, lean_loogle, lean_leanfinder
• Verify theorems with lean_local_search and lean_hover_info
• Analyze findings and synthesize recommendations
• Create research report in specs/{NNN}_{SLUG}/reports/
• Write metadata to specs/{NNN}_{SLUG}/.return-meta.json
• Return a brief text summary (NOT JSON)

---

Stage 6: Parse Subagent Return (Read Metadata File)

After subagent returns, read the metadata file:

metadata_file="specs/${task_number}_${project_name}/.return-meta.json"

if [ -f "$metadata_file" ] && jq empty "$metadata_file" 2>/dev/null; then
    status=$(jq -r '.status' "$metadata_file")
    artifact_path=$(jq -r '.artifacts[0].path // ""' "$metadata_file")
    artifact_type=$(jq -r '.artifacts[0].type // ""' "$metadata_file")
    artifact_summary=$(jq -r '.artifacts[0].summary // ""' "$metadata_file")
else
    echo "Error: Invalid or missing metadata file"
    status="failed"
fi

---

Stage 7: Update Task Status (Postflight)

If status is "researched", update state.json and TODO.md:

Update state.json:

jq --arg ts "$(date -u +%Y-%m-%dT%H:%M:%SZ)" \
   --arg status "researched" \
  '(.active_projects[] | select(.project_number == '$task_number')) |= . + {
    status: $status,
    last_updated: $ts,
    researched: $ts
  }' specs/state.json > /tmp/state.json && mv /tmp/state.json specs/state.json

Update TODO.md: Use Edit tool to change status marker from [RESEARCHING] to [RESEARCHED].

On partial/failed: Keep status as "researching" for resume.

---

Stage 8: Link Artifacts

Add artifact to state.json with summary.

IMPORTANT: Use two-step jq pattern to avoid Issue #1132 escaping bug. See jq-escaping-workarounds.md.

if [ -n "$artifact_path" ]; then
    # Step 1: Filter out existing research artifacts (use "| not" pattern to avoid != escaping - Issue #1132)
    jq '(.active_projects[] | select(.project_number == '$task_number')).artifacts =
        [(.active_projects[] | select(.project_number == '$task_number')).artifacts // [] | .[] | select(.type == "research" | not)]' \
      specs/state.json > /tmp/state.json && mv /tmp/state.json specs/state.json

    # Step 2: Add new research artifact
    jq --arg path "$artifact_path" \
       --arg type "$artifact_type" \
       --arg summary "$artifact_summary" \
      '(.active_projects[] | select(.project_number == '$task_number')).artifacts += [{"path": $path, "type": $type, "summary": $summary}]' \
      specs/state.json > /tmp/state.json && mv /tmp/state.json specs/state.json
fi

Update TODO.md: Add research artifact link:

- **Research**: [research-{NNN}.md]({artifact_path})

---

Stage 9: Git Commit

Commit changes with session ID using targeted staging (prevents race conditions with concurrent agents):

git add \
  "specs/${task_number}_${project_name}/reports/" \
  "specs/${task_number}_${project_name}/.return-meta.json" \
  "specs/TODO.md" \
  "specs/state.json"
git commit -m "task ${task_number}: complete research

Session: ${session_id}

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>"

Note: Use targeted staging, NOT git add -A. See .claude/context/core/standards/git-staging-scope.md.

---

Stage 10: Cleanup

Remove marker and metadata files:

rm -f "specs/${task_number}_${project_name}/.postflight-pending"
rm -f "specs/${task_number}_${project_name}/.postflight-loop-guard"
rm -f "specs/${task_number}_${project_name}/.return-meta.json"

---

Stage 11: Return Brief Summary

Return a brief text summary (NOT JSON). Example:

Research completed for task {N}:
- Found {count} relevant Mathlib theorems
- Identified proof strategy: {strategy}
- Created report at specs/{NNN}_{SLUG}/reports/research-{NNN}.md
- Status updated to [RESEARCHED]
- Changes committed

---

Error Handling

Input Validation Errors

Return immediately with error message if task not found.

Metadata File Missing

If subagent didn't write metadata file:

1. Keep status as "researching"
2. Do not cleanup postflight marker
3. Report error to user

Git Commit Failure

Non-blocking: Log failure but continue with success response.

Subagent Timeout

Return partial status if subagent times out (default 3600s). Keep status as "researching" for resume.

---

Return Format

This skill returns a brief text summary (NOT JSON). The JSON metadata is written to the file and processed internally.

Example successful return:

Research completed for task 259:
- Found 5 relevant Mathlib theorems for completeness proof
- Identified proof strategy using structural induction
- Created report at specs/259_prove_completeness/reports/research-001.md
- Status updated to [RESEARCHED]
- Changes committed with session sess_1736700000_abc123

Example partial return:

Research partially completed for task 259:
- Found 2 theorems before MCP tool timeout
- Partial report created at specs/259_prove_completeness/reports/research-001.md
- Status remains [RESEARCHING] - run /research 259 to continue