29.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/29
[ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).
[Er89d] Erdős, P., Some old and new problems on additive and combinatorial number theory. Combinatorial Mathematics: Proceedings of the Third International Conference (New York, 1985) (1989), 181-186.
[Er95] Erdős, Paul, Some of my favourite problems in number theory, combinatorics, and geometry. Resenhas (1995), 165-186.
[Er97c] Erdős, Paul, Some of my favorite problems and results. The mathematics of Paul Erdős, I (1997), 47-67.
[JPSZ24] Jain, V. and Pham, H. T. and Sawhney, M. and Zakharov, D., An explicit economical additive basis. arXiv:2405.08650 (2024).

Imports (1)

theorem Erdos29.erdos_29 sorry line 58 source
depends on sorry what this means
Statement uses: Iff, True, Exists, Set, Nat, And, Eq, HAdd.hAdd, Set.univ, Real, LT.lt, OfNat.ofNat, Asymptotics.IsLittleO, Filter.atTop, AdditiveCombinatorics.sumRep, HPow.hPow
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
25 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.