Lean Formalize

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

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:

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.