LeanScreen Catches Lean 4 Theorems That Compile Cleanly but Say the Wrong Thing, in 0.1 Seconds

Millennium Research / Hacker News·low signalXBlueskyLinkedInCopy link

Millennium Research published LeanScreen, a faithfulness screen for Lean 4 that targets the failure mode where 'the compiler has no objection' but the formal statement is vacuous or misstates the theorem — the exact defect class that AI-generated formalizations produce. It runs lints, vacuity checks and elaboration against your local mathlib in roughly 0.1 seconds, then escalates to two independent judges plus a counterexample probe, calibrated against 886 human verdicts. The authors are explicit that passing is never a certification. 103 points on HN with only 4 comments — high upvote-to-comment ratio, and single-sourced, so scored low pending independent evaluation.