How to prove there are exactly $8$ integer points on the elliptic curve $y^2 = x^3 + 17$ Consider the elliptic curve $y^2 = x^3 + 17$. I know that there are exactly $8$ integer points $(x,y)$ with $y>0$. But how do I prove it? Is there any specific approach to it or any proof for it?
 A: Using the mathematical programming language Sage, we can run the E.integral_points() command to get a (proof verified) confirmation that there are only $8$ integral points.
The points are $(-2,3)$,  $(-1,4)$, $(2,5)$, $(4,9)$, $(8,23)$, $(43, 282)$, $(52, 375)$, and $(5234,378661)$. Note that some would call this $16$ points, since all of these points remain solutions to your curve when $(x,y)$ is replaced with $(x,-y)$.
If you wish to learn more about the algorithm implemented by Sage, I do believe that they are transparent about their algorithms on their website.
NOTE: This case is much easier than the general one, since there is a theorem of Stark (see Theorem 7.2 in Silverman's AEC) which states that there is an effectively computable constant $C_{\epsilon}$ for every $\epsilon$ such that all integral solutions of the curve $y^2=x^3+D$ satisfy $\log(\max\{x,y\})\leq C_{\epsilon}|D|^{1+\epsilon}$, so for $D=17$ there are really not too many values to check.
The Hall-Lang conjecture states that this bound can be reduced to one of the form $|x|\leq C_{\epsilon}D^{2+\epsilon}$ but seeing as that is still a conjecture it cannot be used for finding rational points on your curve.
