diff --git a/tests/compiler/strictOrSimp.lean.expected.out b/tests/compiler/strictOrSimp.lean.expected.out
deleted file mode 100644
index ce01362503..0000000000
--- a/tests/compiler/strictOrSimp.lean.expected.out
+++ /dev/null
@@ -1 +0,0 @@
-hello
diff --git a/tests/lean/1163.lean.expected.out b/tests/lean/1163.lean.expected.out
deleted file mode 100644
index 3fdbaf7020..0000000000
--- a/tests/lean/1163.lean.expected.out
+++ /dev/null
@@ -1,9 +0,0 @@
-1163.lean:6:8-6:15: warning: declaration uses `sorry`
-1163.lean:11:8-11:15: warning: declaration uses `sorry`
-1163.lean:13:16-13:17: error: failed to synthesize
-  OfNat Bool 0
-use `set_option diagnostics true` to get diagnostic information
-1163.lean:15:8-15:15: warning: declaration uses `sorry`
-1163.lean:18:18-18:19: error: failed to synthesize
-  OfNat Bool 0
-use `set_option diagnostics true` to get diagnostic information
diff --git a/tests/lean/345.lean.expected.out b/tests/lean/345.lean.expected.out
deleted file mode 100644
index bdbcc2fdb1..0000000000
--- a/tests/lean/345.lean.expected.out
+++ /dev/null
@@ -1,9 +0,0 @@
-345.lean:1:12-1:13: error: failed to synthesize
-  OfNat (Sort ?u) 1
-use `set_option diagnostics true` to get diagnostic information
-345.lean:4:8-4:9: error: failed to synthesize
-  OfNat (Sort ?u) 1
-use `set_option diagnostics true` to get diagnostic information
-345.lean:6:19-6:20: error: failed to synthesize
-  OfNat (Sort ?u) 1
-use `set_option diagnostics true` to get diagnostic information
diff --git a/tests/lean/439.lean.expected.out b/tests/lean/439.lean.expected.out
deleted file mode 100644
index fc248a1421..0000000000
--- a/tests/lean/439.lean.expected.out
+++ /dev/null
@@ -1,20 +0,0 @@
-@Fn.imp ((p : P) → Bar.fn p) ({p : P} → Bar.fn p) fn : {p : P} → Bar.fn p
-439.lean:18:7-18:12: error: function expected at
-  fn.imp
-term has type
-  Bar.fn ?m
-439.lean:29:7-29:11: error: function expected at
-  fn.imp
-term has type
-  Bar.fn ?m
-fn.imp : Bar.fn p
-fn'.imp Bp : Bar.fn p
-439.lean:39:11-39:12: error: application type mismatch
-  fn'.imp p
-argument
-  p
-has type
-  P : Sort u
-but is expected to have type
-  Bar.fn ?m : Sort ?u
-fn'.imp (sorryAx (Bar.fn ?m) true) : Bar.fn ?m
diff --git a/tests/lean/603.lean.expected.out b/tests/lean/603.lean.expected.out
deleted file mode 100644
index 8eeb576e85..0000000000
--- a/tests/lean/603.lean.expected.out
+++ /dev/null
@@ -1,30 +0,0 @@
-
-[result]
-def even (x_1 : obj) : obj :=
-  let x_2 : obj := 0;
-  let x_3 : u8 := Nat.beq x_1 x_2;
-  case x_3 : u8 of
-  Bool.false →
-    let x_4 : obj := 1;
-    let x_5 : obj := Nat.sub x_1 x_4;
-    dec x_1;
-    let x_6 : obj := odd x_5;
-    ret x_6
-  Bool.true →
-    dec x_1;
-    let x_7 : obj := 1;
-    ret x_7
-def odd (x_1 : obj) : obj :=
-  let x_2 : obj := 0;
-  let x_3 : u8 := Nat.beq x_1 x_2;
-  case x_3 : u8 of
-  Bool.false →
-    let x_4 : obj := 1;
-    let x_5 : obj := Nat.sub x_1 x_4;
-    dec x_1;
-    let x_6 : obj := even x_5;
-    ret x_6
-  Bool.true →
-    dec x_1;
-    let x_7 : obj := 0;
-    ret x_7
\ No newline at end of file
diff --git a/tests/lean/mangling.lean.expected.out b/tests/lean/mangling.lean.expected.out
deleted file mode 100644
index 0734556612..0000000000
--- a/tests/lean/mangling.lean.expected.out
+++ /dev/null
@@ -1,4 +0,0 @@
-"ab12"
-"_xff"
-"_u03b1_u2081"
-"_U0001d4ab"
diff --git a/tests/lean/scopedunifhint.lean.expected.out b/tests/lean/scopedunifhint.lean.expected.out
deleted file mode 100644
index 5b4accc610..0000000000
--- a/tests/lean/scopedunifhint.lean.expected.out
+++ /dev/null
@@ -1,48 +0,0 @@
-scopedunifhint.lean:28:11-28:12: error: application type mismatch
-  mul x
-argument
-  x
-has type
-  Nat : Type
-but is expected to have type
-  ?m.α : Type ?u
-mul (sorryAx ?m.α true) (sorryAx ?m.α true) : ?m.α
-scopedunifhint.lean:29:11-29:17: error: application type mismatch
-  mul (x, x)
-argument
-  (x, x)
-has type
-  Nat × Nat : Type
-but is expected to have type
-  ?m.α : Type ?u
-mul (sorryAx ?m.α true) (sorryAx ?m.α true) : ?m.α
-scopedunifhint.lean:33:7-33:8: error: application type mismatch
-  mul x
-argument
-  x
-has type
-  Nat : Type
-but is expected to have type
-  ?m.α : Type ?u
-sorryAx ?m.α true*sorryAx ?m.α true : ?m.α
-x*x : Nat.Magma.α
-x*x : Nat.Magma.α
-scopedunifhint.lean:39:11-39:17: error: application type mismatch
-  mul (x, x)
-argument
-  (x, x)
-has type
-  Nat × Nat : Type
-but is expected to have type
-  ?m.α : Type ?u
-sorryAx ?m.α true*sorryAx ?m.α true : ?m.α
-(x, x)*(x, x) : (Prod.Magma Nat.Magma Nat.Magma).α
-scopedunifhint.lean:56:7-56:13: error: application type mismatch
-  mul (x, x)
-argument
-  (x, x)
-has type
-  Nat × Nat : Type
-but is expected to have type
-  ?m.α : Type ?u
-sorryAx ?m.α true*sorryAx ?m.α true : ?m.α