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，一种将VeriPB伪布尔（PB）证明证书导入Lean 4的方法。我们方法的核心在于反射：一个布尔检查函数，其正确性在Lean中得到完整证明，并以编译后的原生代码执行。该方法可扩展至包含数万步的证明，此类证明在显式证明项构造下会耗尽内存。我们的检查器支持所有VeriPB核心规则，包括割平面推导和反证法子证明。与仅生成验证结果的外部验证检查器不同，我们的集成方法可生成Lean定理，这些定理可在更大型的形式化开发中作为可组合引理使用。为了推导关于原始组合问题而非仅关于PB约束的定理，我们支持验证编码。由于约束转换及其正确性证明均在Lean中形式化，这消除了求解器输出与问题语义之间的信任鸿沟。我们在多种组合问题上验证了该方法的有效性。