/learn

name: learn
description: Interactive teaching and mathlib exploration
user_invocable: true
argument-hint: '[topic] [--mode=auto|repo|mathlib] [--style=tour|socratic|exercise|game] [--source=PATH]'

Lean4 Learn

Interactive teaching and mathlib exploration. Adapts to beginner, intermediate, and expert audiences.

Usage

/lean4:learn                                 # Start conversational discovery
/lean4:learn Finset.sum                      # Auto-detect mode from topic
/lean4:learn --mode=repo                     # Explore current project
/lean4:learn --mode=mathlib topology         # Navigate mathlib for a topic
/lean4:learn --style=socratic --interactive  # True Socratic method
/lean4:learn --style=game --track=nng-like   # Game-style natural numbers track
/lean4:learn --source ./paper.pdf            # Learn from a paper/PDF
/lean4:learn --presentation=informal "Bolzano-Weierstrass"  # Prose, Lean-backed
/lean4:learn --output=scratch                # Write results to scratch file
/lean4:learn --style=socratic --adaptive=off  # Socratic, no style/level drift

Invocation Contract

Interpret this command's inputs per the [Command Invocation Contract](../skills/lean4/references/command-invocation.md).

**Primary path (hook-validated):** If a `validated-invocation` block for this command appears in context, treat it as the authoritative interpretation of parser-decidable inputs and do **not** re-parse the raw invocation text for those inputs. Start by reading all parser-decided fields from the block. Then, if this command has repo-dependent startup rules (the `--mode=mathlib` scope coercion depends on local-declaration resolution), apply them using runtime context (LSP, grep). Emit the final **Resolved Inputs** summary from the combined result. See [Validated Invocation Block](../skills/lean4/references/command-invocation.md#validated-invocation-block-host-provided).

**Fallback path (other hosts):** If no `validated-invocation` block is present, parse the raw invocation text against this command's input table before discovery.

Startup requirements:

1. Emit a **Resolved Inputs** block with explicit values, defaults, coercions, ignored flags, and startup validation errors. 2. Refuse to start on startup validation errors. 3. Validate output paths and overwrite policy before writing anything.

Inputs

| Arg | Required | Default | Description | |-----|----------|---------|-------------| | topic | no | — | Free-text topic, theorem name, file path, or natural-language claim. If omitted, start conversational discovery; set `--mode` after first user reply. | | --mode | no | `auto` | `auto` \| `repo` \| `mathlib` | | --level | no | `intermediate` | `beginner` \| `intermediate` \| `expert` | | --scope | no | `auto` | `auto` \| `file` \| `changed` \| `project` \| `topic` | | --style | no | `tour` | `tour` \| `socratic` \| `exercise` \| `game` | | --output | no | `chat` | `chat` \| `scratch` \| `file` | | --out | no | — | Output path. Required when `--output=file`; startup validation error if missing. | | --overwrite | no | `false` | Allow overwriting existing files with `--output=file`. Without flag, existing target → startup validation error. | | --interactive | no | `false` | True Socratic method (withhold answers, ask questions). Valid only with `--style=socratic`; ignored with warning otherwise. | | --intent | no | `auto` | `auto` \| `usage` \| `internals` \| `authoring` \| `math`. See [learn-pathways.md](../skills/lean4/references/learn-pathways.md#intent-taxonomy). | | --presentation | no | `auto` | `informal` \| `supporting` \| `formal` \| `auto`. Controls user-facing display, not Lean backing. See [learn-pathways.md](../skills/lean4/references/learn-pathways.md#two-layer-architecture). | | --verify | no | `best-effort` | `best-effort` \| `strict`. Verification strictness for key claims. See [learn-pathways.md](../skills/lean4/references/learn-pathways.md#verification-status). | | --track | no | — | Exercise ladder: `nng-like` \| `set-theory-like` \| `analysis-like` \| `proofs-reintro`. Valid only with `--style=game`. See [learn-pathways.md](../skills/lean4/references/learn-pathways.md#track-ladders). | | --source | no | — | File path, URL, or PDF to seed learning. See [learn-pathways.md](../skills/lean4/references/learn-pathways.md#source-handling). | | --adaptive | no | `on` | `on` \| `off`. Controls whether the debate can change style/level. See [learn-pathways.md](../skills/lean4/references/learn-pathways.md#adaptive-control). |

Scope defaults by mode (when `--scope=auto`)

| Mode | Default scope | |------|--------------| | `repo` | `file` | | `mathlib` | `topic` |

Scope coercions

• `--mode=mathlib` + `--scope=file|changed|project` → warn + coerce to `topic`, unless topic resolves to a local declaration

Output validation

• `--output=file` without `--out` → startup validation error
• `--output=scratch` → `.scratch/lean4/learn-<timestamp>.lean` (workspace-local). Auto-create `.scratch/lean4/` if missing; warn if `.scratch/` is not in `.gitignore`.
• `--output=file` with existing target and no `--overwrite` → startup validation error

Flag validation

• `--intent`, `--presentation`, or `--verify` with invalid value → startup validation error.
• `--track` without `--style=game` → warn + ignore. `--style=game` without `--track` → prompt track picker.
• `--source` + `--scope=file|changed|project` → warn "source overrides scope for initial discovery". Unsupported source type → warn + ask for text excerpt.
• `--adaptive` with invalid value → startup validation error. `--adaptive=off` freezes the Learning Profile: the debate cannot change `style` or `level`. Within-style remediation (hint escalation, trying a counterexample instead of repeating an explanation) is unaffected — those don't modify the profile.

Actions

0. Intent Intake

**Two-layer contract:** All modes are Lean-backed by default. Lean verification is attempted for all key cla