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

This paper introduces a formally verified framework for patent analysis, employing a hybrid AI and Lean 4 pipeline. It marks the first known application of interactive theorem proving to intellectual property analysis, addressing the shortcomings of manual or probabilistic methods.