Erdős Problem 963

### What is the conjecture

https://www.erdosproblems.com/963

Let $f(n)$ be the maximal $k$ such that in any set $A\subset \mathbb{R}$ of size $n$ there is a subset $B\subseteq A$ of size $\lvert B\rvert\geq k$ which is dissociated that is, the sums $\sum_{b\in S}b$ are distinct for all $S\subseteq B$. Estimate $f(n)$ - in particular, is it true that
$$f(n)\geq \lfloor \log_2 n\rfloor?$$

Status: open

### Choose either option
- [ ] I plan on working on this conjecture
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

Start by reading Erdős Problem 963 at https://www.erdosproblems.com/963 and comparing existing formalized conjectures in the repository. Determine the expected Lean representation and supporting proof obligations. Done means Problem 963 has been added to the formal-conjectures collection in a form accepted by the project.

Written by the indexing model from the issue text.