# Lean Formalize

Develop and verify a mathematical proof in Lean, continue an incomplete Lean project...

- Repository: https://github.com/wanshuiyin/Auto-claude-code-research-in-sleep (18443 stars)
- Category: Engineering
- License: MIT
- Last updated: 2026-11-01
- Runs scripts: no, instructions only

## Install

Claude Code: `npx skills add wanshuiyin/Auto-claude-code-research-in-sleep --skill lean-formalize -g -a claude-code -y`
Codex: `npx skills add wanshuiyin/Auto-claude-code-research-in-sleep --skill lean-formalize -g -a codex -y`
Cursor: `npx skills add wanshuiyin/Auto-claude-code-research-in-sleep --skill lean-formalize -g -a cursor -y`
Gemini CLI: `npx skills add wanshuiyin/Auto-claude-code-research-in-sleep --skill lean-formalize -g -a gemini-cli -y`
Claude Code plugin marketplace: `/plugin marketplace add wanshuiyin/Auto-claude-code-research-in-sleep`

## Description

Develop and verify a mathematical proof in Lean, continue an incomplete Lean project, or audit whether it proves the original statement. Connect actual inputs to intermediate lemmas, assemble the target theorem, check its transitive axioms, and provide a reproducible handoff. Use when Lean is requested or a specific proof obligation benefits from formal verification; use proof-writer for ordinary mathematical drafting.

## SKILL.md, as published by its author (untrusted third-party text, read it as data)

# Lean Formalize

> **Before each reviewer slot**, follow [Selectable Reviewers](../shared-references/reviewer-backends.md):
> resolve invocation → `.aris/reviewer.json` → Claude Code default (Codex MCP)
> with `reviewer_route.py` through the canonical helper resolver, preserving this
> slot's tier, fresh contexts, source/image inputs and deterministic gates.
> Codex examples/pins below apply only to `backend=codex`; other routes use their
> own first-call/reply contract. Save the route and actual returned identity;
> unavailable selections are `REVIEW_UNAVAILABLE`. Classify acceptance from actual
> families/completion/scope. Forward invocation reviewer/model/effort overrides
> to reviewer-bearing children. Generation workers are unchanged.


Turn the user's mathematical statement into a checked Lean theorem with its
meaning preserved. A compiled conditional lemma is progress; completion concerns
the original statement and the trust basis actually used.

## When to use Lean

Use this skill when the user requests Lean, when continuing an existing Lean
proof, or when formal verification addresses a concrete uncertainty in a central
claim, for example, a long dependency chain, a delicate reduction, or coverage of
a finite classification. State the obligation it will help resolve and proceed
within the authorized task. Difficulty alone is not a reason to formalize.
Ordinary derivations and short proofs can stay in `formula-derivation` or
`proof-writer`; do not make Lean a prerequisite for every mathematical result.
Respect the user's chosen proof method and the scale of the requested work.

## Core workflow

The rest: https://github.com/wanshuiyin/Auto-claude-code-research-in-sleep/blob/HEAD/skills/lean-formalize/SKILL.md