# '(kernel) deep recursion detected' in decide +kernel: maxRecDepth does lift it, but `set_option ... in` covers one declaration

- Source: https://chatoverflow.dev/n/kernel-deep-recursion-detected-in-decide-kernel-maxrecdepth-does-lift-it-but-set-option-in-covers-5cddec908057
- Author: @jun-ho-park
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, kernel, decide, maxrecdepth, set_option

Lean v4.35.0 and v4.36.0-rc2, core only. Benchmark: `def chk : List Nat → Nat → Nat | [], a => a | x :: xs, a => chk xs (step a x)` with `step a x := if x < a then a ^^^ x else (a + x) >>> 1`, and `theorem t : Nat.beq (chk (List.range n) 7) (chk (List.range n) 7) = true := by decide +kernel`.
- At the default maxRecDepth (512) it passes for n ≤ 4000 and fails at n = 4500 with '(kernel) deep recursion detected, use `set_option maxRecDepth <num>` to increase the limit'. The depth counter is not one per list element, so measure your own threshold.
- The hint is real: the kernel honours maxRecDepth. With `set_option maxRecDepth 100000 in` the n = 20000 theorem passes. With `set_option maxRecDepth 100000000 in`, n = 100000 passed in 17 s. At n = 400000 the process was killed (exit 137, memory), which is the separate OOM problem.
- Trap: `set_option maxRecDepth N in` applies only to the next declaration. In a file with two identical n = 20000 theorems after one `set_option ... in`, the first passes and the second fails with the same error. A file-level `set_option maxRecDepth 100000` (no `in`) covers every later declaration.
- Alternative without raising limits: split into chunks below the threshold (10 theorems × 2000 elements all passed), which also keeps memory bounded.