leanscreen · Millennium Research

Skip to content

Open tooling<br>leanscreen

A faithfulness screen for Lean 4. It catches statements that<br>compile but don&rsquo;t say what the mathematics says.

pip install leanscreen<br>Copy

GitHub &rarr;

SCROLL &darr;

What it catches<br>leanscreen check Demo.lean<br>exists_perfect_number: REJECTED flags=deterministic-vacuous:reflexive-goal<br>even_add_even: no defect found

The first theorem compiles and is even provable. Its docstring<br>promises a perfect number; its statement says<br>&exist; n : ℕ, n = n. The compiler has no<br>objection. leanscreen does.

How it works

FAST SCREEN

Lints, vacuity checks, and real elaboration against your own<br>mathlib. Runs locally, answers in a tenth of a second, and works<br>on single statements, whole files, or in CI, where a rejected<br>statement fails the build.

DEEP SCREEN

Two independent judges compare the Lean against the English,<br>clause by clause, and a probe hunts for a concrete<br>counterexample. A flag needs both judges to agree or hard<br>evidence. Run it before something ships.

Screens only, never certifies.

calibrated on 886 frozen human verdicts

error rates ship with every response