| 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
- Read
references/lean-formalization-workflow.md and decide if Lean is the right tool for the current claim.
- Rewrite the English claim into a precise theorem obligation using
templates/theorem-obligation.template.md.
- Separate definitions, assumptions, and the target conclusion before writing Lean code.
- Identify the smallest proof slice that is worth checking first instead of formalizing the whole paper at once.
- If no Lean project exists yet, plan the minimal project bootstrap and dependency imports before proving anything.
- Record build failures, unresolved goals, and notation mismatches as artifacts of progress instead of hiding them in prose.
- Keep the repo claim honest: documentation-first support now, executable formalization service later.
Validation Loop
Before closing work:
- confirm the theorem statement matches the intended English claim,
- confirm assumptions and imported definitions are explicit,
- confirm the current proof status is one of proved, partially formalized, or blocked,
- confirm unresolved goals or
sorry placeholders are surfaced as gaps, not buried,
- 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
