Open tooling
A faithfulness screen for Lean 4. It catches statements that compile but don’t say what the mathematics says.
pip install leanscreen
What it catches
leanscreen check Demo.lean exists_perfect_number: REJECTED flags=deterministic-vacuous:reflexive-goal even_add_even: no defect found
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.
How it works
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