formalizing-qec-claims-in-lean

name	formalizing-qec-claims-in-lean
description	Guides translation of QEC claims into Lean workflows with explicit theorem obligations, build checks, and honest boundaries between formalized results and still-informal reasoning.
version	0.1.0
author	QEC Research Skills
license	MIT
tags	["QEC","Lean","Formalization","Proofs"]
dependencies	["qec-research"]

Formalizing QEC Claims In Lean

What This Skill Is For

Use this skill when a QEC task needs formalization rather than only prose:

• turn a lemma, invariant, or proof sketch into a precise theorem obligation,
• decide whether Lean is the right next step,
• structure a small Lean workflow around a QEC claim,
• record what was actually proved versus what remains informal.

When To Use It Versus Alternatives

Use this skill when the task is about:

• stabilizer or CSS-code lemmas,
• notation cleanup before proof mechanization,
• translating a paper claim into explicit assumptions and definitions,
• building a minimal Lean artifact around a theorem-sized claim.

Do not use this skill when the task is primarily:

• numerical benchmarking,
• circuit sampling or decoder comparison,
• broad literature summarization,
• an under-specified claim that still needs counterexamples, examples, or notation cleanup before formalization.

Required Artifacts And Assumptions

Expected inputs:

• an English statement of the claim,
• the relevant definitions and notation,
• any dependency on prior lemmas, libraries, or external references,
• the current repo/project context if a Lean project already exists.

Expected outputs:

• a theorem obligation record,
• a proposed Lean module or project path,
• a list of unresolved proof gaps,
• a Lean-oriented validation note or future LeanBundle plan.

Assumptions to make explicit:

• whether the claim is algebraic, code-structural, or protocol-specific,
• whether a finite counterexample check should run before formalization,
• whether the proof depends on mathlib, Lean-QuantumInfo, or project-local definitions,
• whether sorry is acceptable for a temporary research stub or forbidden for promotion.

Standard Workflow Checklist

1. Read references/lean-formalization-workflow.md and decide if Lean is the right tool for the current claim.
2. Rewrite the English claim into a precise theorem obligation using templates/theorem-obligation.template.md.
3. Separate definitions, assumptions, and the target conclusion before writing Lean code.
4. Identify the smallest proof slice that is worth checking first instead of formalizing the whole paper at once.
5. If no Lean project exists yet, plan the minimal project bootstrap and dependency imports before proving anything.
6. Record build failures, unresolved goals, and notation mismatches as artifacts of progress instead of hiding them in prose.
7. Keep the repo claim honest: documentation-first support now, executable formalization service later.

Validation Loop

Before closing work:

1. confirm the theorem statement matches the intended English claim,
2. confirm assumptions and imported definitions are explicit,
3. confirm the current proof status is one of proved, partially formalized, or blocked,
4. confirm unresolved goals or sorry placeholders are surfaced as gaps, not buried,
5. confirm any future LeanBundle output would be traceable to a named theorem obligation.

Common Issues And Fixes

Formalizing a vague claim

Problem: the statement sounds plausible in prose but is still too ambiguous for Lean.

Fix: stop and rewrite the claim with precise quantifiers, domains, and assumptions before touching the prover.

Skipping easier falsification

Problem: Lean is started before a quick counterexample search or finite sanity check.

Fix: run the cheaper check first when the claim might simply be false or misstated.

Hidden dependency explosion

Problem: a small claim quietly depends on a large stack of unstated notation and imported theory.

Fix: isolate the minimal dependency frontier and formalize only the slice that can be stated cleanly.

References

• references/api.md
• references/examples.md
• references/lean-formalization-workflow.md
• templates/theorem-obligation.template.md
• ../../docs/ARTIFACT_MODEL.md
• ../../servers/contracts/qec_formalization_mcp.yaml