PBLean: Pseudo-Boolean Proof Certificates for Lean 4

TL;DR

PBLean introduces a scalable method for importing and verifying VeriPB pseudo-Boolean proof certificates within Lean 4, enhancing trust and composability in formal proofs of combinatorial problems.

Contribution

It presents a reflection-based approach for importing VeriPB proofs into Lean 4, supporting all kernel rules and verified encodings, improving scalability and trustworthiness.

Findings

Supports proofs with tens of thousands of steps

Enables formalized proofs about original combinatorial problems

Provides a fully verified, native execution checker

Abstract

We present PBLean, a method for importing VeriPB pseudo-Boolean (PB) proof certificates into Lean 4. Key to our approach is reflection: a Boolean checker function whose soundness is fully proved in Lean and executed as compiled native code. Our method scales to proofs with tens of thousands of steps that would exhaust memory under explicit proof-term construction. Our checker supports all VeriPB kernel rules, including cutting-plane derivations, proof-by-contradiction subproofs, and redundance-based reasoning for symmetry breaking. In contrast to external verified checkers that produce verdicts, our integration yields Lean theorems that can serve as composable lemmas in larger formal developments. To derive theorems about the original combinatorial problems rather than about PB constraints alone, we support verified encodings. This closes the trust gap between solver output and problem semantics since the constraint translation and its correctness proof are both formalized in Lean. We demonstrate the approach on various combinatorial problems.