# Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline

arXiv: https://arxiv.org/abs/2604.18882 · HTML: https://mlsanity.com/paper/2604.18882/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 12 of its 29 references that are in the map.
- First posted on arXiv 20 Apr 2026.

## Builds on (most cited first, 12 of 12)

- [Catala: A Programming Language for the Law](https://mlsanity.com/paper/2103.03198/) (2021)
- [On Verifiable Legal Reasoning: A Multi-Agent Framework with Formalized Knowledge Representations](https://mlsanity.com/paper/2509.00710/) (2025)
- [NLP Verification: Towards a General Methodology for Certifying Robustness](https://mlsanity.com/paper/2403.10144/) (2024)
- [PatentMatch: A Dataset for Matching Patent Claims & Prior Art](https://mlsanity.com/paper/2012.13919/) (2020)
- [PatentScore: Multi-dimensional Evaluation of LLM-Generated Patent Claims](https://mlsanity.com/paper/2505.19345/) (2025)
- [Lean4Lean: Verifying a Typechecker for Lean, in Lean](https://mlsanity.com/paper/2403.14064/) (2024)
- [DAPFAM: A Domain-Aware Family-level Dataset to benchmark cross domain patent retrieval](https://mlsanity.com/paper/2506.22141/) (2025)
- [Towards Trustworthy Legal AI through LLM Agents and Formal Reasoning](https://mlsanity.com/paper/2511.21033/) (2025)
- [Beyond Scaling: Predicting Patent Approval with Domain-specific Fine-grained Claim Dependency Graph](https://mlsanity.com/paper/2404.14372/) (2024)
- [A faster algorithm for finding Tarski fixed points](https://mlsanity.com/paper/2010.02618/) (2020)
- [Programming Languages and Law: A Research Agenda](https://mlsanity.com/paper/2206.14879/) (2022)
- [DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs](https://mlsanity.com/paper/2602.18657/) (2026)

## Built on by (most cited first, 1 of 1)

- [Proof-Carrying Certificates for LLM Pipelines: A Trust-Boundary Architecture](https://mlsanity.com/paper/2605.16407/) (2026)

## Abstract (arXiv)

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.