Formalization of a Proof Calculus for Incremental Linearization for Satisfiability(…)
summary
Formalizes the incremental linearization proof calculus used by cvc5 inside Lean, extends the lean-smt plugin, and proves soundness of 21 proof rules (inequalities, sign/pi handling, Taylor bounds). Implements tactics for computable polynomial/Taylor checks, extends the Taylor remainder lemma to negative offsets, and uses Mathlib plus a 20-digit π approximation. Reconstructs cvc5 proofs via cvc5 proof reconstruction on the authors’ benchmarks, exposes missing side conditions and mismatches with the implementation, and mostly succeeds though mixed integer/real cast holes remain.
AI-written summary · about
chapters (16)
- 0:00Incremental linearization proof calculus
- 1:36Motivation for formalization
- 3:06What incremental linearization does
- 4:27Mathlib foundations
- 5:31Three proof rule categories
- 6:16Inequality rules formalized
- 7:43Sign property rules in Lean
- 8:46Sign shifting theorem
- 10:15Bounding pi with decimals
- 11:20Taylor bounds for transcendental functions
- 13:08Exponential bounds via Taylor
- 14:39Documentation errors found
- 16:03Proof reconstruction with Lean SMT & CVC5
- 17:06Matching rules to CVC5 challenges
- 18:12Future directions
- 19:15Q&A
related talks
21mGenerating Collection Transformations from Proofs
24mWhen Less Is More: Consequence-Finding in a Weak Theory of Arithmetic
19mRamsey Quantifiers in Linear Arithmetics
17mA Systematic Approach to Deriving Incremental Type Checkers
01h 05mAlgebraic Structures in Logic and Query Evaluation 2
01h 24mIntroduction to Constraint Logic Programming
17mFixpoints for the Masses: Programming with First-Class Datalog Constraints
14mVerifying vMVCC, a high-performance transaction library using multi-version concurrency..