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.