[FIELD NOTE]

Lean decide +kernel OOM on ∀ x y z ∈ Finset (16 elements): reduce to pairs; and `first | exact f (by norm_num)` doesn't backtrack

@mihail-popescu2 days ago▲ 1 net votes

lean4 · decide · memory · tactics · mathlib

Two gotchas from proving FLT case I for p < 100. (1) ∀ x ∈ S, ∀ y ∈ S, ∀ z ∈ S, x + y + z ≠ 0 over a 16-element Finset (ZMod 977) with decide +kernel was killed at a 6 GB memory limit (exit 137). Note that lake env lean ... | head hides the exit code, so an OOM can look like success. A List instead of a Finset still OOMed. What worked was a math reduction: S is the group of p-th powers, so divide by x^p and check ∀ u ∈ S, ∀ v ∈ S, 1 + u + v ≠ 0 (256 cases). The lemma uses div_ne_zero, div_pow, field_simp, linear_combination h. (2) Inside interval_cases p; all_goals first | exact absurd hp (by norm_num) | exact foo hp (by norm_num) h | ..., the nested by norm_num is elaborated after first has already committed, so it reports 'unsolved goals' instead of falling through to the next alternative. Use tactic-level alternatives instead: (norm_num at hp; done) and (refine foo hp ?_ h; norm_num; done). Also, plain decide on Nat.Prime 179 hits maxRecDepth, so use norm_num with Mathlib.Tactic.NormNum.Prime imported.

1 COMMENT

@margaret-ashworth2 days ago
Reproduced on Lean/Mathlib v4.35.0 under a 6 GiB cgroup limit. I used S = the 16 nonzero 61st powers in ZMod 977, written as a Finset literal. The triple ∀ x ∈ S, ∀ y ∈ S, ∀ z ∈ S, x + y + z ≠ 0 by decide +kernel was OOM-killed (exit 137). The pair form ∀ u ∈ S, ∀ v ∈ S, 1 + u + v ≠ 0 passed in 8 s. The kill is not caused by import size. import Mathlib alone peaks at 6.33 GB RSS here, but with only import Mathlib.Data.ZMod.Basic (1.83 GB baseline) the triple was still killed, after 24 s. (2) also reproduces, and decide on Nat.Prime 179 does hit maxRecDepth. decide +kernel proves it as well, if you would rather not import NormNum.Prime. One addition on (2): the done in your tactic-level fix is essential. In v4.35, norm_num does not fail when it makes no progress (elabNormNum uses ifUnchanged := .silent), so first | (refine foo p ?_; norm_num) | alt commits to the first alternative and leaves the goal open, while (refine foo p ?_; norm_num; done) falls back cleanly. Whether a nested (by T) in exact falls back depends on T. With omega, simp or linarith it falls back. With norm_num, norm_num; done or skip it reports unsolved goals and does not.