lean-formalize

Files (4)

• SKILL.md
• adversarial-review.md · references/
• lean-working-loop.md · references/
• verification-and-handoff.md · references/

SKILL.md (first lines)

# 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

```text
Original statement and Lean definitions
  → A: cross-family adversarial statement alignment
  → Proof obligations, representations, and lemma interfaces
  → Lean implementation ↔ B: adversarial review of key arguments and connections
  → Actual inputs connected; original theorem assembled
  → Executed type, definition, and transitive-axiom audit
  → C: cross-family adversarial review of the final exported result
  → Reproducible delivery and research-state update
```

For substantial new proof projects, A/B/C are part of the workflow. For a
continuation, reuse completed checks on unchanged claims and revisit affected
ones. Small routine formalizations need checks proportional to the actual claim;
an explicit user request for cross-family review still applies to them.

Use the authorized reviewer families available in the current host. If the user
specifies both Grok and Gemini, obtain and record both; a same-family agent or
another provider does not silently satisfy either request. Unavailability leaves
that checkpoint pending while independent proof work continues. A checked theorem
and a fully completed requested review workflow are separate deliverables.

## Scope and entry

Follow the requested scope: implement, continue, audit, or package. For an audit,
inspect and report rather than silently repairing or weakening the theorem.
For implementation, develop the mathematical argument as well as its Lean
proof: search relevant literature or library results, explore alternative routes,
and discharge the missing lemmas. Continue through the remaining interfaces and
top-level assembly; do not stop at a target declaration or the first successful
compilation.

Read the authoritative statement, existing Lean entry point, toolchain and
lockfile, and latest progress record. Reuse the project and its document names.
Do not reinstall tools, change dependencies, or start a new proof framework when
the existing environment is suitable. Resolve APIs against the pinned library.

Use the existing proof route when it works. If the mathematical argument itself
is missing, isolate that obligation and use `proof-writer` or ordinary proof work.
A delegated `proof-writer` task develops that argument and returns its proof or
remaining gap to this run; it must not invoke `lean-formalize` again. Syntax
automation cannot discharge an unproved premise. Do not promise that an arbitrary
open problem can be formalized or solved.

### Start or resume the right work

| Current input | First useful action |
|---|---|
|Only a mathematical statement|Fix definitions and quantifiers, then develop a proof route and its first difficult obligation|
|A prose proof|Identify nontrivial dependencies and choose Lean representations; expose any missing argument before coding it|
|A partial Lean project|Inspect the target and its actual callers, read the last useful build/error record, and continue at the highest unclosed connection|
|An audit request|Read definitions and exported types, run applicable checks, and report; do not silently repair the target|
|A completed proof to hand off|Check the current entry point and evidence, then prepare portable sources and commands without restarting the mathematical search|

Name the intended main module, exported declaration, and current next obligation
early. If no complete mathematical route is known, say which statement is being
attempted; do not mark it provable merely because the implementation has started.
Tool/API problems and missing mathematical arguments require different next steps.

## 1. Fix meaning before implementation

Record a short mathematical specification, or reference the existing one:

- Objects, domains, quantifiers, original hypotheses, and conclusion.
- Equivalence of convenient representations to the original objects.
- User constraints on computation, external certificates, and logical foundations.
- The Lean declarations intended to express and prove the result.

Separate original hypotheses from properties introduced by a reduction. Identify
where finiteness, nonemptiness, decidability, normalization, and index conventions
change the statement or require a bridge. Check plausible vacuity and quantifier
failures in the actual theorem, rather than inventing unrelated edge cases.

Keep the user's original statement as the comparison baseline until the user
changes the goal. A working specification rewritten to match the implementation
does not change that baseline. Record authorized scope changes explicitly; do not
request confirmation again for a change already authorized in the session.
If a repair yields only a stronger assumption or weaker conclusion, identify the
proved variant and the original obligation still open. A stronger proved result
can establish the original claim when its implication is supplied.

Run checkpoint A on the actual definition bodies and proposed target. Ask for
independent back-translation before comparison with the original mathematics.
The input packet and prompt are in
[references/adversarial-review.md](references/adversarial-review.md). A reviewer
who saw only the intended prose has not checked the encoding.

## 2. Design the connections, then build useful pieces

From wanshuiyin/Auto-claude-code-research-in-sleep, MIT.

More from wanshuiyin/Auto-claude-code-research-in-sleep