On the Erdős Distinct Subset Sums Conjecture

On the Erdős Distinct Subset Sums Conjecture: A Detailed Treatise on Hypercube Embeddings, Information-Theoretic Bounds, Normal Approximations, and Certified Proofs This preprint provides an exhaustive mathematical treatise on the Erdős Distinct Subset Sums Conjecture (Problem #14 in Paul Erdős' collection). A finite set of positive integers $S = \{x_1 < x_2 < \dots < x_n\} \subset \mathbb{N}_{>0}$ is said to have distinct subset sums if the subset sum map $\Sigma : \mathcal{P}(S) \to \mathbb{N}$, defined by: $$\Sigma(A) \coloneqq \sum_{x \in A} x, \quad \text{for every } A \subseteq S$$ is strictly injective ($\forall A, B \subseteq S, \; A \ne B \implies \Sigma(A) \ne \Sigma(B)$). Paul Erdős conjectured that the maximum element must grow exponentially: $\max(S) \ge c \cdot 2^n$ for some universal constant $c > 0$. Key Mathematical Results & Contributions Boolean Hypercube Injection: Formal proof that the linear evaluation map $\Phi : \{0, 1\}^n \to \mathbb{N}$ given by $\Phi(\epsilon) = \sum_{i=1}^n \epsilon_i x_i$ is strictly injective, forcing the subset sum image to contain exactly $2^n$ distinct non-negative integers inside the discrete interval $[0, \sum_{x \in S} x]$. Exact Total Sum Lower Bound: Rigorous demonstration via the Pigeonhole Principle on discrete intervals that: $$\sum_{x \in S} x \ge 2^n - 1$$ Exact Maximum Element Bound: Derivation from the arithmetic mean inequality establishing that: $$\max(S) \ge \frac{2^n - 1}{n}$$ Derivation of the Erdős-Moser (1955) Bound: Detailed pedagogical proof of the second-order asymptotic bound $\max(S) \ge \sqrt{\frac{2}{\pi}} \frac{2^n}{\sqrt{n}} (1 + o(1))$ via variance analysis $\sigma^2 = \frac{1}{4} \sum x_i^2$ on the boolean hypercube and the local central limit theorem / point mass upper bounds ($\mathbb{P}(X = k) \le 2^{-n}$). Comparative Survey of Upper Bound Constructions: Detailed analysis of the Conway-Guy (1969) sequence ($\max(S) < 0.235 \cdot 2^n$) and Tom Bohman's (1996) optimal construction ($\max(S) < 0.22096 \cdot 2^n$). 100% Machine-Checked Verification in Lean 4 Repository and Verification Artifacts The companion machine-checked code and formal verification artifacts are publicly hosted on GitHub: https://github. com/flouzzy/erdos-problems Primary MSC (2020): 11B13, 05B10, 68V20, 11B75, 60C05.Keywords: Erdős Distinct Subset Sums Conjecture, Additive Combinatorics, Boolean Hypercube, Central Limit Theorem, Conway-Guy Sequences, Formal Verification, Lean 4, Mathlib.