Erdős Problem 539

formal-conjectures · erdos-problems · ams-5 · ams-11

In this problem, a function $h : \mathbb{N} \to\mathbb{N}$ is defined maximally by a specified
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 $n^{2/3}$ and the best known lower bound is $\sqrt{n}$ so we
also provide these candidates as variants. Moreover, it suffices to show $O(h(n))$ and
$O(\sqrt{n})$ respectively for each, so further variants are provided for those.

In the source paper [Er73], Erdős also remarks that it should not be too difficult
to determine $\lim_{n\to\infty}\log(h(n))/\log(n)$. This does not appear on the website, and
it is not clear whether this remains open, but we include it here either way.

Let $h(n)$ be maximal such that, for any set $A\subseteq \mathbb{N}$ of size $n$, the
set$$\left\{ \frac{a}{(a,b)}: a,b\in A\right\}$$has size at least $h(n)$.
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/539
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://arxiv.org/abs/2607.09474
Formal statement provenance (Apache-2.0) (checked 2026-09-11): https://github.com/google-deepmind/formal-conjectures/blob/cd3d8db4634733a748b2380f80f77ba3e4b9dda0/FormalConjectures/ErdosProblems/539.lean
Local target: Corpus.Erdos539.erdos_539.variants.sq
Source SHA-256: d6eb176cfec008a763c507a4ce1d162feb625c910c8926c6e36f9b1f4717ca7b
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.

Public JSON record