skill-lean-research

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	Agent, Bash, Edit, Read, Write

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.

Trigger Conditions

This skill activates when:

• Task type is "lean4" or "lean" (either accepted)
• 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
task_type=$(echo "$task_data" | jq -r '.task_type // "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:

bash .claude/scripts/state-write.sh \
  '(.active_projects[] | select(.project_number == $num)) |= . + {
    status: $status,
    last_updated: $ts,
    session_id: $sid
  }' \
  --session-id "$session_id" \
  --argjson num "$task_number" \
  --arg ts "$(date -u +%Y-%m-%dT%H:%M:%SZ)" \
  --arg status "researching" \
  --arg sid "$session_id"

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

---

Stage 3: 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}",
    "task_type": "lean"
  },
  "focus_prompt": "{optional focus}",
  "metadata_file_path": "specs/{N}_{SLUG}/.return-meta.json"
}

---

Stage 4: Invoke Subagent

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

Required Tool Invocation:

Tool: Agent (NOT Skill, NOT Plan)
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/{N}_{SLUG}/reports/
• Write metadata to specs/{N}_{SLUG}/.return-meta.json
• Return a brief text summary (NOT JSON)

---

Stage 4b: Self-Execution Fallback

CRITICAL: If you performed the work above WITHOUT using the Agent tool (i.e., you read files, wrote artifacts, or updated metadata directly instead of spawning a subagent), you MUST write a .return-meta.json file now before proceeding to postflight. Use the schema from return-metadata-file.md with the appropriate status value for this operation.

If you DID use the Agent tool, skip this stage -- the subagent already wrote the metadata.

---

Postflight (ALWAYS EXECUTE)

The following stages MUST execute after work is complete, whether the work was done by a subagent or inline (Stage 4b). Do NOT skip these stages for any reason.

Stage 5: Parse Subagent Return

Read the metadata file:

metadata_file="specs/${padded_num}_${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 6: Update Task Status (Postflight)

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

Update state.json:

bash .claude/scripts/state-write.sh \
  '(.active_projects[] | select(.project_number == $num)) |= . + {
    status: $status,
    last_updated: $ts,
    researched: $ts
  }' \
  --session-id "$session_id" \
  --argjson num "$task_number" \
  --arg ts "$(date -u +%Y-%m-%dT%H:%M:%SZ)" \
  --arg status "researched"

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

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

---

Stage 7: Link Artifacts

Add artifact to state.json with summary.

if [ -n "$artifact_path" ]; then
    bash .claude/scripts/state-write.sh \
      '(.active_projects[] | select(.project_number == $num)).artifacts += [{"path": $path, "type": $type, "summary": $summary}]' \
      --session-id "$session_id" \
      --argjson num "$task_number" \
      --arg path "$artifact_path" \
      --arg type "$artifact_type" \
      --arg summary "$artifact_summary"
fi

Update TODO.md: Link artifact using count-aware format. Apply the four-case Edit logic from @.claude/context/patterns/artifact-linking-todo.md with field_name=**Research**, next_field=**Plan**.

---

Stage 8: Git Commit

Commit changes with session ID:

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

Session: ${session_id}

---

Stage 9: 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/{N}_{SLUG}/reports/MM_{short-slug}.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. 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.