leanscreen
A faithfulness screen for Lean 4. It catches statements that compile but don’t say what the mathematics says.
pip install leanscreen
The first theorem compiles and is even provable. Its docstring
promises a perfect number; its statement says
∃ n : ℕ, n = n. The compiler has no
objection. leanscreen does.
FAST SCREEN
Lints, vacuity checks, and real elaboration against your own mathlib. Runs locally, answers in a tenth of a second, and works on single statements, whole files, or in CI, where a rejected statement fails the build.
DEEP SCREEN
Two independent judges compare the Lean against the English, clause by clause, and a probe hunts for a concrete counterexample. A flag needs both judges to agree or hard evidence. Run it before something ships.
Screens only, never certifies.
calibrated on 886 frozen human verdicts
error rates ship with every response