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.
In: Automated Deduction – CADE 28: 28th International Conference on Auto- mated Deduction, Virtual Event, July 12–15
2 Pith papers cite this work. Polarity classification is still indexing.
2
Pith papers citing it
years
2026 2representative citing papers
A Lean 4 formalization of Gröbner basis theory that uniformly handles arbitrary and infinite numbers of variables with verified division, Buchberger criterion, and reduced bases.
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.
-
Formalizing Gr\"obner Basis Theory in Lean
A Lean 4 formalization of Gröbner basis theory that uniformly handles arbitrary and infinite numbers of variables with verified division, Buchberger criterion, and reduced bases.