diff --git a/tests/lean/sorryWarning.lean b/tests/lean/sorryWarning.lean
new file mode 100644
index 0000000000..64eca7b8a1
--- /dev/null
+++ b/tests/lean/sorryWarning.lean
@@ -0,0 +1,4 @@
+def f (x : Nat) : Nat :=
+  sorry
+def g (x : Nat) : Nat :=
+  f x
diff --git a/tests/lean/sorryWarning.lean.expected.out b/tests/lean/sorryWarning.lean.expected.out
new file mode 100644
index 0000000000..736756888b
--- /dev/null
+++ b/tests/lean/sorryWarning.lean.expected.out
@@ -0,0 +1 @@
+sorryWarning.lean:2:2: warning: declaration uses 'sorry'