← All papers
Automatically Generalizing Proofs and Statements
cs.LO
Jan 1, 2020 · v1
TL;DR
Implements automatic generalization of Lean proofs by weakening hypotheses.
Abstract
This paper presents methods for automatically generalizing proofs and mathematical statements in the Lean proof assistant. The approach identifies hypotheses in a proof that can be weakened or removed while preserving correctness, producing more general versions of theorems that may apply to broader mathematical structures.
Problem
Theorems in proof assistants are often stated with stronger hypotheses than necessary, limiting their applicability to broader mathematical structures.
Approach
The paper presents methods for automatically generalizing proofs and statements in the Lean proof assistant. The approach identifies hypotheses in a proof that can be weakened or removed while preserving correctness, producing more general versions of theorems.
Results
The system produces more general versions of theorems that may apply to broader mathematical structures by automatically identifying and removing unnecessary hypotheses.