diff --git a/tests/lean/run/ack.lean b/tests/lean/run/ack.lean
new file mode 100644
index 0000000000..6ec3751f40
--- /dev/null
+++ b/tests/lean/run/ack.lean
@@ -0,0 +1,5 @@
+def ack : Nat → Nat → Nat
+  | 0,   y   => y+1
+  | x+1, 0   => ack x 1
+  | x+1, y+1 => ack x (ack (x+1) y)
+termination_by' PSigma.lex sizeOfWFRel (fun _ => sizeOfWFRel)