NOT_RUN: Lean compiler not installed. This is NOT a proof-check success.
Lean check exit code: 2 (2 means unavailable, not passed)
