diff --git a/bench/README.md b/bench/README.md
index 3855ec44..9055b632 100644
--- a/bench/README.md
+++ b/bench/README.md
@@ -16,6 +16,12 @@ time agda -i src file.agda
 time idris2 --check file.idr
 ```
 
+### Lean
+
+```
+time lean file.lean
+```
+
 ### Kind2
 
 ```
@@ -45,4 +51,5 @@ Kind2-C  |   0.17 s
 Kind2    |   0.58 s
 Agda     |  15.55 s
 Idris2   |  67.40 s
+Lean     |  timeout
 ```
diff --git a/bench/nat_exp.lean b/bench/nat_exp.lean
new file mode 100644
index 00000000..cf98a958
--- /dev/null
+++ b/bench/nat_exp.lean
@@ -0,0 +1,25 @@
+inductive NAT where
+  | Z : NAT
+  | S : NAT -> NAT
+
+inductive The : NAT -> Type where
+  | val : (x : NAT) -> The x
+
+def add : NAT -> NAT -> NAT
+  | a, NAT.S b => NAT.S (add a b)
+  | a, NAT.Z   => a
+
+def mul : NAT -> NAT -> NAT
+  | a, NAT.S b => add a (mul a b)
+  | _, NAT.Z   => NAT.Z
+
+def exp : NAT -> NAT -> NAT
+  | a, NAT.S b => mul a (exp a b)
+  | _, NAT.Z   => NAT.S NAT.Z
+
+def nul : NAT -> NAT
+  | NAT.S a => nul a
+  | NAT.Z   => NAT.Z
+ 
+def work : The (nul (exp (NAT.S (NAT.S (NAT.S NAT.Z))) (NAT.S (NAT.S (NAT.S (NAT.S (NAT.S (NAT.S (NAT.S (NAT.S NAT.Z))))))))))
+  := @The.val NAT.Z