Lean Formalize

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

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. A reviewer who saw only the intended prose has not checked the encoding.

2. Design the connections, then build useful pieces

Map the path from an arbitrary original input to the conclusion. For every substantial interface, record:

Declaration / obligation	What it assumes	Where actual inputs come from	Evidence / remaining gap
A conditional result	Its extra hypotheses	A named construction or theorem from the original input	Actual state

Prioritize the highest unclosed connection. In particular, distinguish:

1. A formula or certificate computes the desired number.
2. The actual mathematical object realizes that formula or certificate.
3. The computed fact implies the original conclusion.

All three may require separate proofs. A structure that stores its desired properties as fields, a supplied probability bound, or an assumption equivalent to the conclusion does not remove the obligation to construct that input.

Use conditional lemmas as development interfaces, explicitly marked as such. Keep incomplete experiments outside the certified target's dependency chain; any temporary sorry remains visible as unfinished work and cannot survive the final target audit. Prefer enough intermediate compilation to localize errors, without interpreting file counts or proved arithmetic statements as completion.

Split parallel work along stable lemma signatures and module ownership. Give each worker its assumptions, conclusion, dependencies, and concrete compile target. Integrate its result against the actual caller before closing the ledger. Do not let parallel workers silently redefine shared objects to suit their proofs.

Implementation loop

Read references/lean-working-loop.md when implementing or repairing an obligation. It develops the search → actual-caller experiment → diagnostic → repair cycle, including representation choices and performance problems, with a compiled library-application example.

1. Select a missing connection or mathematical lemma that changes what the main theorem can prove. State its exact Lean interface and its caller's obligations.
2. Look for the required results in the pinned library and project. Test unfamiliar declarations locally with #check; use existing equivalent representations when they simplify a real bottleneck.
3. Implement the lemma and an actual use site. Compile the affected module; after integration, compile the downstream target whose status depends on it.
4. Diagnose the first relevant error. An elaboration/API mismatch calls for a local implementation fix. An unavailable assumption calls for its derivation, a different argument, or an explicit remaining mathematical obligation.
5. When finite reduction becomes expensive, consider a general counting lemma, recurrence or smaller checked certificate. Do not silently enlarge the trust basis merely to make a tactic finish.
6. At a new load-bearing argument or interface, run checkpoint B. Implement valid fixes, compile them, and request follow-up on the changed obligation.
7. Update the existing ledger with the declaration, actual caller, verification evidence and remaining premise; then advance to the next connection.

For example, a theorem of type Certificate x → Desired x is useful only after the project constructs Certificate x for every original input it needs. Closing that construction and connecting the caller is a distinct result from proving the conditional theorem. Kernel checking does not discharge a parameter merely because its type has a reassuring name.

Do not use a timer, repeated unchanged builds, or repeated model calls as a proxy for progress. After a concrete failure, try another justified representation or proof path; preserve the exact blocker if the requested work cannot yet finish. Distinguish an implementation failure from a failed intermediate claim and an obstruction to the whole method. Retire an unsuccessful route with its reason; rejecting that route does not refute the original theorem. Parallel exploration is most useful when the proposed approaches can fail for different reasons.

3. Use computation with a proved interpretation

Distinguish finite examples, exhaustive computation over a proved domain, checked certificates, and symbolic/general proof. A bounded search is evidence about its searched inputs. Exhaustive finite verification can be a proof when coverage, encoding correspondence, and the verification procedure are established and the user's constraints permit it. For an end-to-end Lean result, the coverage and interpretation must themselves lie in the proved dependency chain under the declared foundations. A comment claiming that a finite list is exhaustive does not turn checked list entries into a universal Lean theorem.

For numeric arguments, use exact arithmetic where the claim needs exactness. Prove the connection between actual objects/events and the finite data before using the numeric conclusion. Document conventions that matter: ordered versus unordered pairs, multiplicities, indices, zero cases, and rounding.

Agree on the intended trust basis from the specification and project conventions. Do not silently introduce axioms or compiler-backed computation to make an otherwise incomplete kernel-level proof appear complete. Conversely, do not turn one project's prohibition on enumeration or native_decide into a universal ban. Explain any extra trust assumption and whether it satisfies this task.

4. Review the mathematical obligations that remain uncertain

Run A, B and C as described in the core workflow. Read references/adversarial-review.md for stage triggers, source packets, adversarial prompts, objection handling, resumption and stopping rules. These are mathematical checks, not votes on whether to trust the executor's summary.

Use proof-checker for the existing ARIS proof-audit/submission role. This skill does not replace its artifact or reviewer contract. When invoked by a parent proof audit, return the checked scope and evidence to that run; do not recursively invoke proof-checker. A standalone Lean task does not automatically require a separate paper-audit workflow. Where installed, use research-review / auto-review-loop for targeted discussion and repair, with the current host's reviewer routing.

For direct model consultations, use available authorized tools and their actual contracts. A Grok or Antigravity MCP consultation is not automatically an ARIS reviewer overlay. Do not hard-code vendor availability, quotas, retry counts, proxy settings, or a particular model into the portable workflow.

Ask concrete questions: translate this declaration; discharge these caller hypotheses; find a counterexample to this new lemma; check this reduction's coverage. Preserve raw responses, actual reading/execution scope, and the executor's disposition of each issue. Model agreement is not a proof. Same-family opinions remain provisional; cross-family opinions are additional review evidence, not mathematical truth certificates.

An unread artifact, an unanswered question, a failed call or an empty response provides no substantive review verdict. A plan review is not a final-code review; reading existing logs is not executing a build. Preserve which claim/version was actually examined. Retry only within current authorization and provider rules; do not rewrite failures as passes after a later success.

Close objections with a specific derivation, verified witness, correction or justified rejection. Preserve unresolved disputes. Apply an invoked ARIS loop's own round/continuation contract; do not create an outer polling loop around it. For direct consultations, re-review changed obligations and stop when settled or when a real availability/budget limit is reached. Unresolved mathematics remains open; an unavailable requested review remains pending. Neither a reviewer score nor exhaustion of rounds is a proof-completion rule.

Host execution and review

Read the local host's reviewer routing for its current model/effort policy and tool contracts. Use the A/B/C mathematical packets in this skill; they do not require a paper, publication score, or a new review service. For delegated proof work, follow the applicable fan-out convention, assign stable lemma interfaces, and integrate each result at its real caller.

On Claude Code, use the host's file/shell tools for Lean and Agent for useful parallel proof work. The default reviewer is Codex MCP: start with mcp__codex__codex, an explicit project cwd, read-only sandbox, and the model/effort pair resolved from the routing reference. Continue that review with mcp__codex__codex-reply using its saved session identity and prompt. Start fresh contexts for A and C; B repair checks may continue the reviewer that found the issue. Verify the executor/reviewer families rather than assuming that every host running this mainline skill is Claude.

Honor an explicitly selected authorized reviewer. Direct Claude, Grok and Gemini transports have different file-access and continuation contracts; read review transport notes when using them. These Lean consultations do not change another skill's reviewer backend or its acceptance rules.

5. Verify the actual final target

Use references/verification-and-handoff.md when preparing the final build, trust audit, or portable package.

For completed delivery, establish the applicable evidence below. Keep a proved theorem distinct from any still-pending reproduction or review requirement:

• The proposition has a proof: inspect the exported declaration's actual type, not its keyword. theorem, lemma, or def may supply a proof term of the target proposition. Merely defining that proposition, proving P → P, or proving an unrelated proposition does not discharge the original target.
• Statement alignment: its expanded type and definitions express the original claim; no internal profile, certificate-validity, coverage, or success premise is left for the user to supply unless the original claim included it.
• Actual assembly: reductions, cases, witnesses, and return to the original conclusion are connected, with all caller hypotheses discharged.
• Executed verification: explicitly build the module that proves the target and print its type and transitive axioms. For a multi-module project, also independently import the actual entry point to check its exported result. Direct compilation plus type/axiom output suffices for a small self-contained file; do not build a new project just to create another import. Save commands, exit status, and output. A successful build of a different root module does not count.
• Trust accounting: no sorryAx or unapproved extra axiom lies on the target's dependency chain. Explain the actual dependencies against the intended basis; the required list need not be exactly any fixed set of axiom names.
• Reproducibility: retain the relevant source and pinned environment, and provide commands that another reader can run.
• Requested review: C concerns the final exported type, definition bodies, axiom output and original claim, not an earlier plan. Record each required reviewer's substantive findings or unavailability separately.

These checks establish the formal result under its stated foundations. A prose proof or HTML edition requires its own correspondence check; Lean does not certify every sentence in a separate exposition. An explicitly required import audit, external reproduction, or review may remain pending even after the formal theorem is checked. Report that missing evidence as such, not as a newly discovered mathematical gap.

An illustrative audit can distinguish available_interface : Target → Target from original_proof : Target, even if both compile without extra axioms. The first leaves the original claim open; the second supplies its proof when Target matches the user's statement. A failed reviewer call changes neither type.

6. Persist and hand off the evidence actually obtained

Reuse the existing specification, proof ledger, and continuation file. A short progress report plus Lean sources, lockfiles, an audit entry point, and logs is usually enough. Add new files only for a concrete reader or execution need.

Report distinct facts rather than a single ambiguous PASS:

• Original theorem: checked, partial, changed claim only, or disproved by a verified counterexample; name the declaration and any remaining obligation.
• Statement alignment and the actual logical trust basis.
• Reproduction: existing/incremental build, clean project rebuild, or another person's independent reproduction—whichever actually happened.
• Reviews: who read what, who ran code, and any requested review still pending.

For unfinished work, save the smallest remaining mathematical/Lean obligation, its known dependencies, the last useful error, and the next action. For completed work, record completion so the next session does not revive obsolete gaps.

Use a compact continuation note rather than a second state system:

Original target and source:
Current exported declaration / main module:
Closed connections and actual build evidence:
Next unclosed obligation or completion:
A/B/C reviews: source scope, reviewer, raw record, remaining issue:
Next action:

Resolve current state from actual artifacts, not an old narrative saying either “finished” or “not finished.” On resume, check what changed before repeating work. Do not merge historical and current reviewer scopes into a larger claimed audit.

If a research wiki is active, update the affected claim through the existing research-wiki / proof-checker workflow with precise evidence and scope; do not overwrite its generated graph or invent a second acceptance format. Literature search should resolve a mathematical gap, API question, or relevant prior result, not become an unrelated requirement to exhaust the literature.

For handoff, provide a reader-oriented proof, source, pinned dependencies, independent audit command, and known trust boundary. Use render-html when a single-file reading edition would help. Mathematical source changes require appropriate rebuild and statement/axiom checks. A theorem or hypothesis changed in Markdown or HTML is also a claim change: redo alignment and affected requested review. Layout or wording that preserves the claim needs presentation checks. Keep change histories in the research record and present the finished proof directly. Do not restart completed proof work solely to satisfy a workflow ritual.