Lean 4

Deterministic timeout: maximum heartbeats (Lean 4)

A command used more than its work budget (maxHeartbeats, 200000 by default) and Lean stopped it — the elaboration is too expensive or stuck, not your computer being slow.

What it looks like

Main.lean:12:2: error: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

What does "Deterministic timeout: maximum heartbeats (Lean 4)" mean?

Heartbeats count memory allocations (in thousands), not seconds, so the same file times out at the same place on every machine — that is what deterministic means. The default maxHeartbeats is 200000 per command; the word after at names the part of Lean that ran out (whnf, isDefEq, simp, typeclass…). Lean 4.22 and later add the Note: and Hint: lines; earlier releases give the same advice on the following line, or in brackets in the oldest versions.

What causes "Deterministic timeout: maximum heartbeats (Lean 4)"?

simp or another tactic with a large lemma set doing too much work on a big goal.
Type class search exploring too many instances (reported as timeout at `typeclass`, which has its own smaller limit, synthInstance.maxHeartbeats = 20000).
Unification (whnf / isDefEq) unfolding large definitions.
A heavy tactic such as nlinarith, ring or norm_num on a big expression.

How do I confirm the cause?

The at `…` part tells you where: typeclass means instance search, simp means the simplifier, whnf or isDefEq mean unfolding definitions.
Comment out the second half of the proof; if it still times out, the expensive step is earlier.
Add set_option diagnostics true in to see the most-unfolded definitions and most-used instances.

How do I fix "Deterministic timeout: maximum heartbeats (Lean 4)"?

Find the slow step and make it cheaper: replace simp with simp only [...] (simp? prints one for you).
Break the proof into smaller have steps or separate lemmas.
Raise the budget for one declaration: set_option maxHeartbeats 400000 in before the theorem (0 means no limit).
For a typeclass timeout raise synthInstance.maxHeartbeats instead, or supply the instance explicitly.

How do I stop it happening again?

Use simp only with explicit lemmas in finished proofs.
Keep each declaration small; a proof close to the limit tends to break when Mathlib changes.

Got a different error? Paste it into the Explain This Error tool → Identifies the family and the fix — runs locally, nothing uploaded.