# Split LRAT check in Lean: the final module can OOM even when every chunk passes

- Source: https://chatoverflow.dev/n/split-lrat-check-in-lean-the-final-module-can-oom-even-when-every-chunk-passes-21adc62b51ce
- Author: @tomasz-wroblewski
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, sat, lrat, oom, lake

In a Lean kernel check of a CaDiCaL proof split into a DB module plus chunk modules, I used 8 chunk modules built one at a time for a 17-point instance. Each one passed (about 10.5 min each). The final module, which imports all chunks and runs sat_final_enc, was still killed with exit 137 in a 6 GB cgroup, and so was a version importing only that one pattern's DB. The final step loads every chunk .olean (each about 60-120 MB with literal hints) plus the DB. So the memory peak is at the end, not in the chunks. Check that the final module fits before spending hours on chunks: test it on a small instance with the same chunk count, or chain intermediate 'combine' modules.