/formalize

name: formalize
description: Interactive formalization — drafting plus guided proving
user_invocable: true
argument-hint: '[topic] [--rigor=checked|sketch|axiomatic] [--source=PATH] [--output=chat|scratch|file]'

Lean4 Formalize

Interactive formalization: draft Lean skeletons from informal claims, then prove them with guided cycles. Combines `/lean4:draft` and `/lean4:prove` in a single human-in-the-loop workflow.

**Compatibility:** Accepts all flags from old formalize (v4.3.x). Semantics are broader — new formalize runs a full prove cycle after drafting. Users wanting the old lighter-weight "draft + shallow proof attempt" behavior should use `/lean4:draft --mode=attempt`. Users wanting skeletons only should use `/lean4:draft`.

Usage

/lean4:formalize "Every continuous function on a compact set is bounded"
/lean4:formalize --rigor=axiomatic "Zorn's lemma implies AC"
/lean4:formalize --source ./paper.pdf          # Ingest, pick claims, formalize
/lean4:formalize --source ./paper.pdf "Theorem 3.2"  # Source as context, topic as claim
/lean4:formalize --output=file --out=MyTheorem.lean "..."

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. Emit the final **Resolved Inputs** summary from the block values. 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 drafting or proving.

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 | — | Informal claim to formalize. Optional when `--source` provides it (source-led flow). At least one of `topic` or `--source` must be given; omitting both is a startup validation error. | | --rigor | no | `checked` | `checked` \| `sketch` \| `axiomatic` | | --verify | no | `best-effort` | `best-effort` \| `strict`. Verification strictness for key claims. See [learn-pathways.md](../skills/lean4/references/learn-pathways.md#verification-status). | | --level | no | `intermediate` | `beginner` \| `intermediate` \| `expert` | | --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. | | --mathlib-template | no | `false` | Emit the mathlib module-system file header on `--output=file` writes regardless of detected project context. Requires `--output=file`; mutually exclusive with `--no-mathlib-template`. | | --no-mathlib-template | no | `false` | Never emit the mathlib module-system file header on `--output=file` writes, regardless of detected project context. Requires `--output=file`; mutually exclusive with `--mathlib-template`. | | --source | no | — | File path, URL, or PDF to seed formalization. See [learn-pathways.md](../skills/lean4/references/learn-pathways.md#source-handling). | | --intent | no | `math` | `auto` \| `usage` \| `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). | | --claim-select | no | — | `first` \| `named:"..."` \| `regex:"..."`. Noninteractive claim selection from `--source`. | | --draft-mode | no | `attempt` | `skeleton` \| `attempt`. Mode for the draft phase (default is `attempt` in formalize context). | | --draft-elab-check | no | `best-effort` | `best-effort` \| `strict`. Elaboration check for the draft phase. | | --deep | no | never | `never` \| `ask` \| `stuck` \| `always`. Deep mode for prove phase. | | --deep-sorry-budget | no | 1 | Max sorries per deep invocation | | --deep-time-budget | no | 10m | Advisory: scopes deep-mode subagent work. Not tracked or enforced. | | --commit | no | ask | `ask` \| `auto` \| `never` | | --golf | no | prompt | `prompt` \| `auto` \| `never` |

Output validation

• `--output=file` without `--out` → startup validation error
• `--output=scratch` → `.scratch/lean4/formalize-<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
• `--mathlib-template` with `--no-mathlib-template` → startup validation error (mutually exclusive)
• `--mathlib-template` or `--no-mathlib-template` without `--output=file` → startup validation error (either flag only affects whole-file writes)

Flag validation

• `--intent`, `--presentation`, or `--verify` with invalid value → startup validation error.
• `--intent=auto` inference: apply the shared [inference rules](../skills/lean4/references/learn-pathways.md#inference-rules-when---intentauto), then coerce `internals` → `usage` and `authoring` → `usage` (formalize does not define behavior for those intents).
• `--source` + unreadable format → warn + ask for text excerpt.
• `--claim-select` without `--source` → startup validation error (nothing to select