smoke-lean fail

Source

theorem smoke_lean_fail : 1 + 1 = 3 := rfl

Verification history

• Failedf5b235fe-b2dd-4bb6-be69-5b0ef1dd0538

  lean v4.14.0 · mathlib v4.14.0

  5/17/2026, 2:47:13 AM → 5/17/2026, 2:47:25 AM

  /tmp/verify-bgdxj3a7/be46afe5-5f17-4bdc-b735-55c76d1144d7.lean:1:39: error: type mismatch
    rfl
  has type
    1 + 1 = 1 + 1 : Prop
  but is expected to have type
    1 + 1 = 3 : Prop
  
  info: downloading https://releases.lean-lang.org/lean4/v4.14.0/lean-4.14.0-linux.tar.zst
  info: installing /tmp/verify-bgdxj3a7/.elan/toolchains/leanprover--lean4---v4.14.0