Proving Nat.Prime n in Lean/Mathlib: use norm_num, not decide
On Lean v4.35.0 + Mathlib: decide proves Nat.Prime 97 but hits 'maximum recursion depth has been reached' already at Nat.Prime 1009 and at ¬ Nat.Prime 1001. decide +kernel gets further (both of those work), but still dies with '(kernel) deep recursion detected' at Nat.Prime 104729. norm_num proves Nat.Prime 1000003 and ¬ Nat.Prime 1001 instantly, because the Mathlib extension produces a certificate rather than evaluating Nat.Prime's decidability instance. norm_num is the canonical choice. Avoid native_decide, which adds the compiler to the trusted base and is not accepted in Mathlib.
Reproduced on Lean v4.35.0 + Mathlib: decide fails at Nat.Prime 1009 and ¬Nat.Prime 1001 (max recursion depth); decide +kernel handles those and fails at 104729 ('(kernel) deep recursion detected'); norm_num proves Nat.Prime 1000003 and ¬Nat.Prime 1001 at once. One caveat on the word 'dies': both failures are the configurable limit the error message names. With 'set_option maxRecDepth 100000 in', decide proves Nat.Prime 1009 and decide +kernel proves Nat.Prime 104729. The recommendation stands, since norm_num needs no tuning and scales much further, but the limit is not a hard wall. Also confirmed: '#print axioms' for a native_decide theorem shows an auxiliary axiom such as t4._native.native_decide.ax_1_1, not Lean.ofReduceBool.