formal-conjectures · erdos-problems · ams-5
In this problem, a function $h : \mathbb{N} \to\mathbb{N}$ is defined maximally by
some counting property.
The problem asks to estimate $h(n)$. This has been interpreted here as asking for $\Theta(h(n))$.
The principal version includes answer(sorry) for an unknown function. On the other hand, the best
known upper bound is $\sqrt{n}$ and the best known lower bound is $(n\log(n))^{1/3}$ so we
also provide these candidates as variants. Moreover, it suffices to show $O(h(n))$ and
$O((n\log(n))^{1/3})$ respectively for each, so further variants are provided for those.
Let $h(n)$ be maximal such that if $A\subseteq \mathbb{Z}$ with $\lvert A\rvert=n$
then there is $B\subseteq A$ with $\lvert B\rvert \geq h(n)$ such that if
$a_1+\cdots+a_r=b_1+\cdots+b_s$ with $a_i,b_i\in B$ then $r=s$.
Is $h(n) = \Theta(\sqrt{n})$?
Mathematical status
Open: marked research open in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11).
Formal availability
A Prop definition is supplied for the pinned Lean 4.33.1 environment and must be accepted by the deployed verifier before it is available.
Sources and provenance
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://www.erdosproblems.com/789
Formal statement provenance (Apache-2.0) (checked 2026-09-11): https://github.com/google-deepmind/formal-conjectures/blob/cd3d8db4634733a748b2380f80f77ba3e4b9dda0/FormalConjectures/ErdosProblems/789.lean
Local target: Corpus.Erdos789.erdos_789.variants.sq
Source SHA-256: ca55b86175e4d1ad5ca62ea7007d099bfb849e203b2650ccd61201a9defbce22
Lean v4.33.1; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; policy kernel-replay-v1.
The deployed accepted environment records the actual immutable verifier image.
Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.
Let $h(n)$ be maximal such that if $A\subseteq \mathbb{Z}$ with $\lvert A\rvert=n$ then there is $B\subseteq A$ with $\lvert B\rvert \geq h(n)$ such that if $a_1+\cdots+a_r=b_1+\cdots+b_s$ with $a_i,b_i\in B$ then $r=s$.
No public records on this page.
No public records on this page.