Lean Eval for Alignment on Faithfulness

Open tooling leanscreen A faithfulness screen for Lean 4. pip install leanscreen GitHub → What it catches The compiler has no objection. leanscreen does. leanscreen check Demo.lean exists_perfect_number: REJECTED flags=deterministic-vacuous:reflexive-goal even_add_even: no defect found The first theorem compiles. Its docstring promises a perfect number; its statement says ∃ n : ℕ, n = n. FAST Lints, vacuity checks, elaboration against your mathlib. Free, local, ~0.1s. DEEP Two independent judges and a counterexample probe. Run it before something ships. CALIBRATED Measured against 886 human verdicts. A pass is never a certification. The screen rejects. People certify. When a statement has to be right, we put an expert reviewer behind it. Get in touch