Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

PBLean: Pseudo-Boolean Proof Certificates for Lean 4

Stefan Szeider

TL;DR

PBLean addresses the trust gap between VeriPB PB solvers and formal verification by embedding a sound, reflection-based checker inside Lean 4 to certify pseudo-Boolean proofs; it formalizes PB constraints in Lean and proves 13 soundness lemmas, enabling end-to-end verification through verified encodings that relate PB certificates to problem semantics. The approach scales to proofs with tens of thousands of steps and yields Lean theorems rather than mere verdicts, demonstrated on combinatorial problems such as Paley graphs where the independence-number bound is certified within Lean. The main contributions are the formal Lean encoding of VeriPB kernels, the two verification strategies (explicit proof terms and reflection), and the end-to-end verified workflow that produces bridge theorems about original problems. Practically, this enables integrating PB certificates into larger formal developments and provides a path toward automated, trusted PB reasoning within Lean 4. The results show notable scalability (e.g., Paley$(101)$) and establish end-to-end verified encodings for multiple combinatorial problems as a foundation for future automation and broader formalization.

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 and proof-by-contradiction subproofs. 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.

PBLean: Pseudo-Boolean Proof Certificates for Lean 4

TL;DR

PBLean addresses the trust gap between VeriPB PB solvers and formal verification by embedding a sound, reflection-based checker inside Lean 4 to certify pseudo-Boolean proofs; it formalizes PB constraints in Lean and proves 13 soundness lemmas, enabling end-to-end verification through verified encodings that relate PB certificates to problem semantics. The approach scales to proofs with tens of thousands of steps and yields Lean theorems rather than mere verdicts, demonstrated on combinatorial problems such as Paley graphs where the independence-number bound is certified within Lean. The main contributions are the formal Lean encoding of VeriPB kernels, the two verification strategies (explicit proof terms and reflection), and the end-to-end verified workflow that produces bridge theorems about original problems. Practically, this enables integrating PB certificates into larger formal developments and provides a path toward automated, trusted PB reasoning within Lean 4. The results show notable scalability (e.g., Paley) and establish end-to-end verified encodings for multiple combinatorial problems as a foundation for future automation and broader formalization.

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 and proof-by-contradiction subproofs. 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.
Paper Structure (14 sections, 1 equation, 1 figure, 3 tables)

This paper contains 14 sections, 1 equation, 1 figure, 3 tables.

Table of Contents

  1. Introduction
  2. Background
  3. Lean Formalization
  4. Explicit proof terms.
  5. Reflection.
  6. Implementation
  7. Evaluation
  8. Langford pairing.
  9. Schur number.
  10. Van der Waerden number.
  11. Ramsey number.
  12. Equitable chromatic number.
  13. Related Work
  14. Conclusion

Figures (1)

  • Figure 1: End-to-end workflow for trusted encodings. OPB (Optimized Pseudo-Boolean) is the standard input format for PB solvers. Solid boxes are verified in Lean; the dashed box is untrusted. The dotted arrow represents the bridge theorem composing encoding correctness with the PB refutation.