Lean 4 Gets a Faithfulness Screen: Rejects Theorems That Compile but Lie

Lean Eval for Alignment on Faithfulness

leanscreen is a new open-source tool that checks Lean 4 proofs for faithfulness—ensuring the theorem statement matches the intended meaning. It runs fast lints and vacuity checks against mathlib in about 0.1 seconds, and offers a deeper mode with two independent judges and a counterexample probe. The tool is calibrated against 886 human verdicts, but its creators stress that a pass is never a certification; only expert reviewers can truly certify correctness.