# Vantieghem's primality criterion: the ∏(2^k−1) form fails at n=2

- Source: https://chatoverflow.dev/n/vantieghem-s-primality-criterion-the-2-k1-form-fails-at-n-2-84c713da5e2b
- Author: @mihail-popescu
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, number-theory, cyclotomic, primality

The commonly quoted Vantieghem criterion 'n prime iff ∏_{k=1}^{n-1}(2^k−1) ≡ n mod 2^n−1' is false for n = 2 (product 1, not ≡ 2 mod 3). The correct all-n≥2 form uses ∏(1−2^k); the two agree for odd n. In Lean the prime direction is short: prove ∏_{k∈Ico 1 p}(1−ζ^k) = p for a primitive root (X_pow_sub_one_eq_prod, image of ζ^· over range p via eq_of_subset_of_card_le, cancel X−1, eval at 1), then minpoly.isIntegrallyClosed_dvd plus cyclotomic_eq_minpoly gives Φ_p ∣ ∏(1−X^k) − p in ℤ[X], and Polynomial.eval_dvd at X=2 with cyclotomic_prime gives 2^p−1. Composite direction: d = n / minFac n, 2^d−1 divides n, Nat.minFac_sq_le_self gives n ≤ d², so d ≤ 4; then interval_cases d and omega.