We present a formally verified framework for patent analysis as a hybrid AI + Lean 4 pipeline. The DAG-coverage core (Algorithm 1b) is fully machine-verified once bounded match scores are fixed. Freedom-to-operate, claim-construction sensitivity, cross-claim consistency, and doctrine-of-equivalents analyses are formalized at the specification level with kernel-checked candidate certificates. Existing patent-analysis approaches rely on manual expert analysis (slow, non-scalable) or ML/NLP methods (probabilistic, opaque, non-compositional). To our knowledge, this is the first framework that applies interactive theorem proving based on dependent type theory to intellectual property analysis. Claims are encoded as DAGs in Lean 4, match strengths as elements of a verified complete lattice, and confidence scores propagate through dependencies via proven-correct monotone functions. We formalize five IP use cases (patent-to-product mapping, freedom-to-operate, claim construction sensitivity, cross-claim consistency, doctrine of equivalents) via six algorithms. Structural lemmas, the coverage-core generator, and the closed-path identity coverage = W_cov are machine-verified in Lean 4. Higher-level theorems for the other use cases remain informal proof sketches, and their proof-generation functions are architecturally mitigated (untrusted generators whose outputs are kernel-checked and sorry-free axiom-audited). Guarantees are conditional on the ML layer: they certify mathematical correctness of computations downstream of ML scores, not the accuracy of the scores themselves. A case study on a synthetic memory-module claim demonstrates weighted coverage and construction-sensitivity analysis. Validation against adjudicated cases is future work.

翻译：摘要：我们提出一种形式化验证的专利分析框架，该框架实现为混合AI + Lean 4流水线。在固定界限匹配分数后，其DAG覆盖核心（算法1b）完全由机器验证。实施自由使用权分析、权利要求构建敏感性分析、跨权利要求一致性分析及等同原则分析时，均在规范层面通过内核核验候选证书进行形式化。现有专利分析方法依赖于人工专家分析（速度慢，不可扩展）或机器学习/自然语言处理方法（概率性，不透明，不可组合）。据我们所知，这是首个将基于依赖类型理论的交互式定理证明应用于知识产权分析的框架。权利要求被编码为Lean 4中的有向无环图，匹配强度被编码为已验证完全格中的元素，置信度分数通过经验证正确性的单调函数沿依赖关系传播。我们通过六种算法形式化五种知识产权用例（专利到产品映射、自由使用权、权利要求构建敏感性、跨权利要求一致性、等同原则）。结构性引理、覆盖核心生成器以及闭环路径恒等式 coverage = W_cov 在Lean 4中通过机器验证。其他用例的高层定理仍为非形式化证明草图，其证明生成函数通过架构方式缓解（不可信生成器，其输出经内核核验且经过无公理假定稽核）。保证条件以机器学习层为前提：此类证明确保机器学习评分下游计算的数学正确性，而非评分本身的准确性。针对合成内存模块权利要求的案例研究展示了加权覆盖分析与构建敏感性分析。基于判决案例的验证工作留待未来开展。