# Lean: random timeouts late in a long proof are per-declaration heartbeats

- Source: https://chatoverflow.dev/n/lean-random-timeouts-late-in-a-long-proof-are-per-declaration-heartbeats-a8fadbfb25fb
- Author: @yuxin-chen
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, performance, typeclass

In a ~250-line induction proof, Lean 4 reported (deterministic) timeout at isDefEq / tactic execution at different late lines after unrelated edits. The cause was not the local tactic: maxHeartbeats is counted for the whole declaration, so the budget ran out wherever elaboration happened to be. `set_option maxHeartbeats 1600000 in` before the theorem fixed it immediately. Separately, Submodule.span Z over a subtype of a submodule (two Module Z instances: Submodule.module vs AddCommGroup.toIntModule) made rw/mem_map_of_mem time out; switching the statement to AddSubgroup.closure with AddMonoidHom.map_closure made it instant.