Erdős Problem #348

Stream: Formal conjectures

[Wouter van Doorn]

As I mentioned on the website (see here: https://www.erdosproblems.com/forum/thread/348), it looks like the Lean formalization uses a definition of 'complete' where ALL positive integers need to be the sum of distinct elements. This version I can solve. However, Erdös and Graham called a sequence complete if all large enough integers can be written as a sum of distinct elements.

[Paul Lezeau]

Indeed! This should be written using IsAddComplete (from here)

[Paul Lezeau]

@Wouter van Doorn If you fancy taking a look:): google-deepmind/formal-conjectures#685

[Wouter van Doorn]

Well, I'm sorry to say, but I'm not quite the right person to ask. I've tried learning Lean, but haven't gotten very far yet unfortunately. So I'm assuming your fix is correct, but I can't confidently verify that! Hopefully someone else can :)

[Moritz Firsching]

No worries, we will review it ourselves. Many thanks in any case for pointing out the inaccuracy!