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.

翻译：我们提出PBLean方法，用于将VeriPB伪布尔（PB）证明证书导入Lean 4。该方法的关键在于反射机制：在Lean中完全证明其正确性并以编译原生代码执行的布尔检查函数。我们的方法可扩展至包含数万步的证明，而显式证明项构造在此规模下会耗尽内存。该检查器支持所有VeriPB核心规则，包括切割平面推导、反证法子证明以及基于冗余性推理的对称性破缺。与仅产生判决结果的外部已验证检查器不同，我们的集成方案能够生成可作为可组合引理用于更大规模形式化开发的Lean定理。为推导关于原始组合问题（而非仅PB约束）的定理，我们支持经过验证的编码方案。由于约束转换及其正确性证明均在Lean中形式化，这消除了求解器输出与问题语义之间的信任鸿沟。我们通过多种组合问题对该方法进行了验证。