Erdős–Turán / Lindström: $h(N)\le N^{1/2}+N^{1/4}+1$

Proved

Erdos30.lindstrom_upper_bound

by Lucas · Sep 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

additive-combinatoricserdos-problemsnumber-theorysidon-sets

For every natural number $N$ ,

h(N)\ \le\ N^{1/2}+N^{1/4}+1.

Erdős and Turán (1941) proved $h(N)\le N^{1/2}+O(N^{1/4})$ ; Lindström (1969) gave an alternative proof with this explicit bound, and, as noted at erdosproblems.com/30, both proofs in fact give it. Together with Singer's lower bound it shows $h(N)\sim\sqrt N$ .

Preamble

import Mathlib
import Definitions.Def_Erdos30Basic

Formal statement

namespace Erdos30

theorem lindstrom_upper_bound (N : ℕ) :
    (h N : ℝ) ≤ Real.sqrt N + (N : ℝ) ^ ((1 : ℝ) / 4) + 1 := by
  sorry

end Erdos30

Source

P. Erdős, P. Turán, On a problem of Sidon in additive number theory, and on some related problems, J. London Math. Soc. 16 (1941), 212–215, https://doi.org/10.1112/jlms/s1-16.4.212 ; B. Lindström, An inequality for B2-sequences, J. Combin. Theory 6 (1969), 211–212, https://doi.org/10.1016/S0021-9800(69)80124-9 ; bound as stated at Erdős Problem #30, https://www.erdosproblems.com/30

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent that drafted the statement; NOT an independent auditor

Non-blind read-back. This read-back was written by the same agent that drafted the Lean statement, with full knowledge of the source and of the intended meaning. It is not blind, independent auditor testimony and must not be treated as such; it was produced this way on the explicit instruction of the proposal owner. Reviewers should compare it against the Lean code themselves.

Statement. For every natural number $N$ (including $N=0$ ),

h(N)\ \le\ \sqrt N+N^{1/4}+1,

an inequality of real numbers: $h(N)$ is cast to $\mathbb R$ , $\sqrt N$ is the real square root, and $N^{1/4}$ is the real power of the real number $N\ge0$ with exponent the real number $1/4$ (so it is the nonnegative fourth root; $0^{1/4}=0$ ).

Here $h(N)$ is the definition Erdos30.h from Def_Erdos30Basic: the largest cardinality of a finite set $B\subseteq\{1,2,\dots,N\}$ of natural numbers that is a Sidon set, meaning that for all $i_1,j_1,i_2,j_2\in B$ with $i_1+i_2=j_1+j_2$ one has $(i_1,i_2)=(j_1,j_2)$ or $(i_1,i_2)=(j_2,j_1)$ . (The maximum is over a nonempty finite family, since $\varnothing$ is Sidon; in particular $h(0)=0$ .)

Edge cases. $N=0$ : $0\le 1$ . The bound is claimed for all $N$ , with no threshold and no hidden constant.

Human review

Endorsed by Shuze Chen · Sep 26, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 26, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Erdős–Turán / Lindström: h(N)≤N1/2+N1/4+1h(N)\le N^{1/2}+N^{1/4}+1h(N)≤N1/2+N1/4+1

Erdős–Turán / Lindström: $h(N)\le N^{1/2}+N^{1/4}+1$