# Lean Formalization Intake

> Use when deciding whether a research claim should enter the optional Lean formalization lane.

- Skill: `hoanganhduc/lean-formalization-intake` (Agent Skill)
- Install (CLI): `npx skillmds@latest add hoanganhduc/lean-formalization-intake`
- Raw SKILL.md: https://api.skillmd.com/api/skills/hoanganhduc/lean-formalization-intake/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Research & Search
- Author: hoanganhduc (https://skillmd.com/u/hoanganhduc)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/hoanganhduc/lean-formalization-intake

---


# Lean Formalization Intake

## Windows Runtime Commands

On native Windows, use the managed Windows runner and the native runtime command target. Set `$runtime` to the installed runtime root. Multi-agent installs usually use `%LOCALAPPDATA%\ai-agents-skills\runtime`. Then run:

```powershell
$runtime = if ($env:AAS_RUNTIME_ROOT) { $env:AAS_RUNTIME_ROOT } else { "$env:LOCALAPPDATA\ai-agents-skills\runtime" }
& "$runtime\run_skill.ps1" "skills/lean-formalization-intake/run_lean_formalization_intake.ps1" doctor
```

PowerShell runner target:

```powershell
& "$runtime\run_skill.ps1" "skills/lean-formalization-intake/run_lean_formalization_intake.ps1" doctor
```

POSIX examples below use `run_skill.sh` and `.sh` command targets; use the Windows command target above on native Windows.

Use this skill before spending effort on Lean formalization. It decides whether a research claim is suitable for the optional formal lane and records a conservative decision:

- `proceed`: definitions and scope look suitable enough to try formalization
- `defer`: formalization is relevant but blocked by definitions, toolchain, library support, semantic alignment, or budget
- `not_applicable`: Lean is not useful for this claim or outside scope
- `blocked`: formal support was required but cannot proceed without clarification or missing tooling

`defer`, `not_applicable`, and missing Lean are not failed theorem evidence. They are only formal-lane status.

## Runtime Helper

Check the local tool status:

```bash
bash "${AAS_RUNTIME_ROOT:-$HOME/.local/share/ai-agents-skills/runtime}/run_skill.sh" \
  skills/lean-formalization-intake/run_lean_formalization_intake.sh doctor
```

Run non-installing version/toolchain probes when you need reproducibility
metadata:

```bash
bash "${AAS_RUNTIME_ROOT:-$HOME/.local/share/ai-agents-skills/runtime}/run_skill.sh" \
  skills/lean-formalization-intake/run_lean_formalization_intake.sh doctor --probe
```

Assess a claim:

```bash
bash "${AAS_RUNTIME_ROOT:-$HOME/.local/share/ai-agents-skills/runtime}/run_skill.sh" \
  skills/lean-formalization-intake/run_lean_formalization_intake.sh assess \
  --claim "Every finite tree has a leaf" \
  --claim-id C1 \
  --output formal/intake-C1.json
```

Set `AAS_LEAN` or `AAS_LAKE` to select a specific already-installed local
executable. Invalid explicit paths are reported as unavailable instead of being
masked by another tool on `PATH`.

The helper never installs Lean, Lake, mathlib, Python packages, Node packages, credentials, services, or MCP servers.

## Output Contract

The runtime emits JSON with:

- `formalization_decision`
- `reason`
- `required_definitions`
- `expected_cost`
- `recommended_next_step`
- `formal_check_requirement`
- `tool_status`
- `limitations`

The result can be copied into a v2 `evidence.jsonl` row or attached as a run artifact, but it does not itself prove the research claim.

## Recommended templates

When this skill is involved, consider these workflow templates (install via
the `workflow-templates` artifact profile, or `--with-deps` to pull backing skills):

- `informal-to-lean-formalization-runbook` -- Local-first intake mapping an informal proof to Lean declarations with a scanner-first verification gate separating typecheck status from claim support.

## Personal library cooperation

When `lean-research-library` is installed, run its `search` verb alongside
intake (before formalizing: mathlib > personal library > formalize new), and
after an accepted result run its `intake` verb — its user-approval gate, not
this skill, decides whether anything enters the personal library.