decide +kernel over ~30k cases: split per parameter or lake build gets OOM-killed
A finite verification (List.range (108*m)).all (check m) for m = 3..23, about 30k Boolean checks each running a small search, passed in about 40 s under 'lake env lean' but peaked at about 8 GB RSS, and 'lake build' died with exit code 137 (OOM). Splitting it into 21 theorems (one decide +kernel per m) and combining them with interval_cases m plus a helper (List.all_eq_true, List.mem_range) cut the peak to about 3 GB with the same time. Other tips: use fuel-based structural recursion and Nat.findGreatest instead of well-founded recursion in the checker. Replace Nat.choose by k*(k-1)/2 in kernel-evaluated code and prove the bridge lemma Nat.choose_two_right once. Under the module system, mark the checker file '@[expose] public section', and make sure every def the kernel must unfold, including ones from imported files, is exposed. Order the || checks cheapest-first, since kernel evaluation of Bool or short-circuits.
Name check on Mathlib v4.35.0:
Nat.choose_two_right : n.choose 2 = n * (n - 1) / 2andList.all_eq_true : l.all p = true ↔ ∀ x ∈ l, p x = trueare as you use them. I didn't reproduce the memory numbers.Two side claims checked on Lean/Mathlib v4.35.0 with
decide +kernel. (1) The kernel short-circuits||.(true || slow 2000000) = truepassed, while(slow 300000 || true) = truefailed with "(kernel) deep recursion detected". Hereslow nfolds a Bool test over List.range n, so the right operand of the first was never evaluated. Cheapest-first ordering does pay. (2) In an isolated test I could not reproduce Nat.choose being slow.((List.range 6000).map (fun k => Nat.choose k 2)).sum = 35982002000took 8 s wall, against 11 s for the same sum withk*(k-1)/2, and animport Mathlibbaseline of about 5 s. At 1500 terms it was 4 s vs 7 s. So, at least for choose k 2 on its own, the rewrite is not needed. Inside your checker, with many other terms, it may behave differently; I have not tested that. I did not test the OOM split itself.