Ang's conjecture on products of distinct integers fails for large primes

Let S(n) be the set of products of subsets of {1, …, n}. In 2020 Yan Sheng Ang conjectured (OEIS A060957) that for every prime p ≤ n, if m and pam lie in S(n), then so does pkm for every 0 < k < a. Wentao Li disproved this in October 2026 with a counterexample in which p ≤ √n. We show that the conjecture also fails for large primes: for every ε > 0 there are arbitrarily large n, primes p with p2 > n and p > n1−ε, and integers u prime to p such that {e ≥ 0 : peu ∈ S(n)} = K + {0, 1, 3, 4} for some integer K. For p2 > n the multiples of p up to n are p times integers below √n, and the products of such integers are again admissible factors. We use all of them. A linear form in the prime exponents forces every factorisation of u to contain a fixed large set of factors. The rest of u then has exactly two factorisations into admissible factors: one uses the weighted columns of an array of primes, and the other uses a row of the array, all monomials of degree at most t in three further row products, and these three row products multiplied by p. The array is built with Bertrand's postulate, and p is about nt/(t+1). We give explicit examples for t = 2, where n has 33 digits, and for t = 3, where p = 223 · 2512 + 1 > n0.73. We also keep the results of an earlier version: an independent counterexample with p ≤ √n that is smaller than Li's, the failure of a variant without the powers of p for n = 1125, an analogue for subset sums in simplices, and a verification of the conjecture for n ≤ 56. The existence statement of the main theorem and the earlier counterexample are formalized in Lean 4. MSC2020: 11B75 (primary); 11A51, 11A41, 52B20, 68V15 (secondary) Files: the paper (PDF, 20 pages), its LaTeX source (ZIP), the Lean 4 sources of the formal proofs (ang-subset-products-lean_v2.0.0.zip, an archive of tag v2.0.0 of the GitHub repository below) and the supplementary material with the certificates, checking programs and logs (ZIP). Formal verification: the existence statement of Theorem 1.2 and the disproof of the conjecture by the counterexample of Theorem 7.1 (the negation of the statement oeis_60957_conjecture_0 of the OEIS-Open benchmark) are proved in Lean 4.33.1 with Mathlib v4.33.1 and kernel-checked; the proofs depend only on the axioms propext, Classical.choice and Quot.sound (sources: https://github.com/TEAM-42KR/ang-subset-products-lean, tag v2.0.0, commit 6f512eb8475ae2abe95a1947206c7a9c4c4b6a29).