A Lean 4 system models patent claims as DAGs with match scores in a verified complete lattice and supplies kernel-checked certificates for coverage calculations and five IP use cases, conditional on unverified ML inputs.
Daggitt, Omri Isac, Guy Katz, Verena Rieser, and Oliver Lemon
2 Pith papers cite this work. Polarity classification is still indexing.
2
Pith papers citing it
years
2026 2verdicts
UNVERDICTED 2representative citing papers
Introduces a trust-boundary architecture in Lean 4 with three certificate families and two operators that deliver sorry-free, axiom-audited assurances for LLM pipeline components.
citing papers explorer
-
Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline
A Lean 4 system models patent claims as DAGs with match scores in a verified complete lattice and supplies kernel-checked certificates for coverage calculations and five IP use cases, conditional on unverified ML inputs.
-
Proof-Carrying Certificates for LLM Pipelines: A Trust-Boundary Architecture
Introduces a trust-boundary architecture in Lean 4 with three certificate families and two operators that deliver sorry-free, axiom-audited assurances for LLM pipeline components.