Pseudo-Boolean (PB) solvers perform sophisticated derivations involving cutting-planes proof steps that resolution-based formats cannot efficiently capture. Independent verification of PB solver results is desirable, but existing approaches either lack integration with ITPs or do not scale to large proofs.

PBLean imports VeriPB pseudo-Boolean proof certificates into Lean 4 using reflection: a Boolean checker function whose soundness is fully proved in Lean and executed as compiled native code. The checker supports all VeriPB kernel rules including cutting-plane derivations, proof-by-contradiction subproofs, and redundance-based reasoning for symmetry breaking. The implementation is a standalone Lean 4 project (~900 lines kernel, ~2500 lines checker) with no Mathlib dependency.

PBLean scales to proofs with tens of thousands of steps that would exhaust memory under explicit proof-term construction. It checks Paley graph independence number proofs up to Paley(101) (2329 variables, ~21000 elaboration lines) and combinatorial problems including Langford, Schur, Van der Waerden, and Ramsey instances. The reflect-based approach handles proofs where direct proof-term construction times out.