157.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/157
[ESS94] Erdős, P. and Sárközy, A. and Sós, T., On sum sets of Sidon sets, I. Journal of Number Theory (1994), 329-347.
[Er94b] Erdős, Paul, Some problems in number theory, combinatorics and combinatorial geometry. Math. Pannon. (1994), 261-269.
[Pi23] Pilatte, C., A solution to the Erdős–Sárközy–Sós problem on asymptotic Sidon bases of order 3. Compositio Math. (2024), 1418-1432.

Imports (1)

theorem Erdos157.erdos_157 sorry line 44 source
depends on sorry what this means
Statement uses: Iff, True, Exists, Set, Nat, And, Set.Infinite, IsSidon, Set.IsAsymptoticAddBasisOfOrder, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.