Cover Image

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

Fuente: arXiv

Saved in:

Bibliographic Details
Main Author:	Koomullil, George
Format:	Preprint
Published:	2026
Subjects:	Artificial Intelligence Logic in Computer Science Programming Languages 68V15 F.4.1; I.2.3; K.5.1
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Proof-Carrying Certificates for LLM Pipelines: A Trust-Boundary Architecture
by: Koomullil, George
Published: (2026)

Deep Vision: A Formal Proof of Wolstenholmes Theorem in Lean 4
by: Linhares, Alexandre
Published: (2026)

An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic
by: Martina, Antoine, et al.
Published: (2023)

Monoid Theory in Alonzo: A Little Theories Formalization in Simple Type Theory
by: Farmer, William M., et al.
Published: (2023)

An Alternative Approach to Formal Mathematics that Focuses on Communication and Accessibility
by: Farmer, William M.
Published: (2026)

A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report
by: Klaus, Natalia, et al.
Published: (2026)

Universal Algebra in UniMath
by: Amato, Gianluca, et al.
Published: (2021)

Implementing Dependent Type Theory Inhabitation and Unification
by: Norman, Chase, et al.
Published: (2026)

Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium
by: Ilin, Vasily
Published: (2026)

Bounded First-Class Universe Levels in Dependent Type Theory
by: Chan, Jonathan, et al.
Published: (2025)

Formally Verifying a Transformation from MLTL Formulas to Regular Expressions
by: Wang, Zili, et al.
Published: (2025)

A formalization of Borel determinacy in Lean
by: Manthe, Sven
Published: (2025)

Higher-Order Pattern Unification Modulo Similarity Relations
by: Dundua, Besik, et al.
Published: (2025)

Canonical for Automated Theorem Proving in Lean
by: Norman, Chase, et al.
Published: (2025)

Internalizing Extensions in Lattices of Type Theories
by: Chan, Jonathan
Published: (2025)

Tractable and Intractable Entailment Problems in Separation Logic with Inductively Defined Predicates
by: Echenim, Mnacho, et al.
Published: (2023)

A SHACL-based Data Consistency Solution for Contract Compliance Verification (Extended Paper)
by: David, Robert, et al.
Published: (2025)

Classification of Covering Spaces and Canonical Change of Basepoint
by: Wemmenhove, Jelle, et al.
Published: (2024)

Formalizing MLTL Formula Progression in Isabelle/HOL
by: Kosaian, Katherine, et al.
Published: (2024)

Mechanised uniform interpolation for modal logics K, GL, and iSL
by: Férée, Hugo, et al.
Published: (2024)

Formalizing Computational Paths and Fundamental Groups in Lean
by: Ramos, Arthur F., et al.
Published: (2025)

Experiments with Choice in Dependently-Typed Higher-Order Logic
by: Ranalter, Daniel, et al.
Published: (2024)

Metric Equational Theories
by: Mardare, Radu, et al.
Published: (2025)

Chain Bounding, the leanest proof of Zorn's lemma, and an illustration of computerized proof formalization
by: Incatasciato, Guillermo L., et al.
Published: (2024)

Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4
by: Aniva, Leni, et al.
Published: (2024)

Mechanized HOL Reasoning in Set Theory
by: Guilloud, Simon, et al.
Published: (2024)

Machine Unlearning for Class Removal through SISA-based Deep Neural Network Architectures
by: Mahi, Ishrak Hamim, et al.
Published: (2026)

A Survey on Group Fairness in Federated Learning: Challenges, Taxonomy of Solutions and Directions for Future Research
by: Salazar, Teresa, et al.
Published: (2024)

TPTP World Infrastructure for Non-classical Logics
by: Steen, Alexander, et al.
Published: (2025)

Logic.py: Bridging the Gap between LLMs and Constraint Solvers
by: Kesseli, Pascal, et al.
Published: (2025)

Formalizing Pick's Theorem in Isabelle/HOL
by: Binder, Sage, et al.
Published: (2024)

A Formalization of the Generalized Quantum Stein's Lemma in Lean
by: Meiburg, Alex, et al.
Published: (2025)

Discernment is all you need
by: Fuenmayor, David
Published: (2026)

Verified Program Extraction in Number Theory: The Fundamental Theorem of Arithmetic and Relatives
by: Wiesnet, Franziskus
Published: (2025)

Incomplete Descriptions and Qualified Definiteness
by: Więckowski, Bartosz
Published: (2024)

Term Orders for Optimistic Lambda-Superposition
by: Bentkamp, Alexander, et al.
Published: (2025)

Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics
by: Firsching, Moritz, et al.
Published: (2026)

Complete Robust Hybrid Systems Reachability
by: Wafa, Noah Abou El, et al.
Published: (2026)

Artifical intelligence and inherent mathematical difficulty
by: Dean, Walter, et al.
Published: (2024)

OnlineProver: Experience with a Visualisation Tool for Teaching Formal Proofs
by: Perháč, Ján, et al.
Published: (2025)