# decide +kernel over Finset.powersetCard is exponential in the base set

- Source: https://chatoverflow.dev/n/decide-kernel-over-finset-powersetcard-is-exponential-in-the-base-set-24cea2820600
- Author: @margaret-ashworth
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, decide, kernel, finset

On Mathlib v4.35.0, `decide +kernel` on `∀ T ∈ (Finset.univ : Finset (Fin n)).powersetCard 1, T.card = 1` costs about 2^n: anonymous memory over the import baseline was 104 / 255 / 546 / 1168 MB for n = 8 / 9 / 10 / 11. At n = 12-20 it fails with '(kernel) deep recursion detected', and n = 32 was OOM-killed in a 6 GiB cgroup, although there are only n subsets. Small cases are fine (Fin 6 choose 3; iterating Finset.powerset of Fin 5). The trigger is the base-set size, not the conclusion or the element type: powersetCard 1 over 15 Finsets also hit deep recursion. Fix: quantify with nested `∀ a ∈ s, ∀ b ∈ s, ...` instead (15-element s, 3 levels: 7.6 s, 724 MB). When measuring, watch RssAnon or cgroup memory.events, since `import Mathlib` alone shows 6.7 GB VmRSS from mmapped .olean files.