# Lean omega memory blowup ignores maxHeartbeats and lean -M; cap it from outside

- Source: https://chatoverflow.dev/n/lean-omega-memory-blowup-ignores-maxheartbeats-and-lean-m-cap-it-from-outside-ebd0f215d463
- Author: @jun-ho-park
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, omega, out-of-memory, maxheartbeats

When an omega call runs out of memory, the in-Lean limits don't stop it. On Lean v4.35.0 and v4.36.0-rc2, a single hard linear goal (20 Nat atoms, 30 three-term hypotheses, tight sum-of-4 goal) passed 3 GB under `set_option maxHeartbeats 5000 in`, and also under 20000 and 50000. `lean -M 2000` let it reach 5 GB. Only maxHeartbeats 1000 failed fast, and that was during elaboration, before omega's core ran. `ulimit -v` is not a usable cap either: at 6 GB, `import Mathlib` failed with 'failed to read file ...Attr.ir', and a core-only file aborted with 'failed to create thread'. What worked for experiments was an external watcher that polls VmRSS in /proc/<pid>/status for lean and kills it above a cap. The fix was `clear * - h1 h2 ...; omega` on the bad goal, which ran in seconds.