feat(ErdosProblems): add statement for Erdős Problem 882

[ToshiDad]

Adds a formalisation of Erdős Problem 882 (Erdős and Sárközy): the size of the largest A ⊆ {1,...,n} whose nonempty subset sums form a divisibility antichain.

The problem is listed as solved, with answer (1+o(1)) log₂ n:

• lower bound |A| > log₂ n - 1 from the construction A = {2^m - 2^i : 0 ≤ i < m} of Erdős, Lev, Rauzy, Sándor and Sárközy [ELRSS99];
• upper bound |A| ≤ log₂ n + ½ log₂ log n + O(1) from Erdős Problem 1, since the antichain property implies distinct subset sums.

Contents:

• IsSubsetSumAntichain, maxAntichainCard, and the main statement erdos_882;
• A m, the ELRSS99 construction, with card_A;
• erdos_882.variants.lower_bound: the key antichain property of A m. This one is proved: a sorry-free Lean 4 proof is hosted at https://github.com/ToshiDad/erdos-882 and linked via @[formal_proof using lean4 at ...]. The proof is elementary binary arithmetic (popcount subadditivity/submultiplicativity, digit splitting, and monotonicity of n - popcount n); it is ~600 lines, hence hosted externally per CONTRIBUTING. Axiom check: 'Erdos882.no_div' depends on axioms: [propext, Classical.choice, Quot.sound].
• erdos_882.variants.sandor and erdos_882.variants.greedy for the other bounds mentioned on the problem page.

I was unable to build locally (toolchain mismatch on my machine), so I would appreciate CI catching any syntax issues; happy to iterate.

[ToshiDad]

Updated: I have now built the repository locally (Lean 4.27.0 + mathlib cache) and lake env lean FormalConjectures/ErdosProblems/882.lean reports no errors, only the expected sorry warnings on the five open statements. The main statement was rewritten as a Tendsto ... (nhds 1) form and a cast was fixed in the greedy variant.

[ToshiDad]

Disclosure: after opening this PR I found a prior sorry-free Lean formalization of the ELRSS99 lower bound by Boris Alexeev, published 2026-08-17 in https://github.com/plby/lean-proofs (src/latest/ErdosProblems/Erdos882.lean), which covers more than my file does: it proves the full statement log2 n - 1 < maximumSize n, whereas mine formalizes only the core non-divisibility lemma. My proof was written independently and follows a similar route (binary digit sums), which seems to be the natural one. I have updated my README to state this. If you prefer, the formal_proof attribute could point to Alexeev's repository instead of mine, or the statement file could be restructured to match his formulation; happy to do either.