leanscreen · Millennium Research

Skip to content

Open tooling

leanscreen

A faithfulness screen for Lean 4.

pip install leanscreen<br>Copy

GitHub &rarr;<br>What it catches

The compiler has no objection.<br>leanscreen does.

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. Its docstring promises a perfect number;<br>its statement says &exist; 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.<br>People certify.

When a statement has to be right, we put an expert reviewer behind<br>it.

Get in touch