feat(ErdosProblems/342)

[aditya-ramabadran]

Description

With $a_1=1 $ and $a_2=2$ let $a_{n+1} $ for $n\ge 2 $ be the least integer greater than $a_n $ which can be expressed uniquely as $a_i + a_j $for $i < j <= n$. Do infinitely many pairs $(a,a+2)$ occur in the sequence? Does Ulam's sequence eventually have periodic differences? Is the density of the sequence 0?

• Closes Erdős Problem 342: Ulam's Sequence: Properties and Asymptotic Behavior #2120
• Quantifies over all u with IsUlamSequence u, I think this is cleaner than defining a specific Ulam Sequence

Testing

• Compiles successfully

$ lake build FormalConjectures/ErdosProblems/342.lean
Build completed successfully.

[mo271]

Thanks!
Looks good mathematically, just a few suggestions for improvement

[aditya-ramabadran]

I made the changes @mo271 and added TODOs for the other parts. Part (iii) is also equivalently in Ben Green's problems as Problem 7. There are also some more open ended parts (Ben Green asks "Can one
explain the curious Fourier properties of this sequence?") that can't really be formalized

[aditya-ramabadran]

Actually I was able to formalize the second part as well by looking at how periodic differences were formalized in https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/341.lean

[aditya-ramabadran]

Formalized the third part as well, also removed the comment about Ben Green's open problem 7 from part (iii) since it's not exactly equivalent (Ben Green Problem 7 asks if the sequence has positive asymptotic density, this is only the negation of having 0 asymptotic density if we assume the asymptotic density / limit exists)

[aditya-ramabadran]

Thanks @eric-wieser!

[mo271]

LGTM, just some comments.

A good follow up might be to do problem 7 from Greens open problem list?!

[aditya-ramabadran]

Thanks @mo271, not sure what's better between having the test for a3, having the test but sorrying it out, or not having it at all so for now just committed your changes with the test :)

And yes, can easily do Ben Green problem 7 next!

[aditya-ramabadran]

Thanks! These changes are definitely cleaner

[mo271]

LGTM, thanks!