[proofplan]
We reduce the asserted finiteness to the general Siegel finiteness theorem for integral points on affine curves. The given Weierstrass equation defines a smooth projective genus-one curve over $\mathbb Q$ with a rational point at infinity, and the affine model is obtained by deleting that point. Because the defining equation has integer coefficients, every integer solution gives a $\mathbb Z$-integral point on this affine curve. The general Siegel theorem then gives finiteness, and hence the original set of integral affine points is finite.
[/proofplan]
[step:Place the affine Weierstrass equation inside its smooth projective elliptic curve]
Let the given Weierstrass equation with integer coefficients be written in affine coordinates as
\begin{align*}
F(x,y)=0,
\end{align*}
where $F \in \mathbb Z[x,y]$ is the Weierstrass polynomial defining the affine model. Since $E$ is an elliptic curve over $\mathbb Q$, this Weierstrass equation has nonzero discriminant, so its projective closure is a nonsingular projective curve $\overline E$ over $\mathbb Q$ of genus $1$ with distinguished rational point $O \in \overline E(\mathbb Q)$ at infinity. The affine curve appearing in the theorem is
\begin{align*}
U := \overline E \setminus \{O\}.
\end{align*}
Thus an integral point in the stated affine Weierstrass model is a pair $(a,b) \in \mathbb Z^2$ satisfying $F(a,b)=0$, equivalently a rational point of $U(\mathbb Q)$ whose affine coordinates are integers.
[guided]
We first make precise which curve is being used. The affine equation has the form
\begin{align*}
F(x,y)=0,
\end{align*}
with $F \in \mathbb Z[x,y]$. The phrase "elliptic curve over $\mathbb Q$" is not merely saying that the equation has rational coefficients: it includes nonsingularity. For a Weierstrass equation this is the condition that the discriminant is nonzero. Under that condition, the projective closure of the affine Weierstrass equation is a nonsingular projective curve $\overline E$ over $\mathbb Q$ of genus $1$, and it has the distinguished rational point at infinity, denoted $O \in \overline E(\mathbb Q)$.
Define the affine curve
\begin{align*}
U := \overline E \setminus \{O\}.
\end{align*}
This is exactly the affine Weierstrass model in the statement: deleting the point at infinity leaves the affine chart with coordinates $x$ and $y$ satisfying $F(x,y)=0$. Therefore a point counted by the theorem is a pair $(a,b) \in \mathbb Z^2$ such that $F(a,b)=0$. Equivalently, it is a rational point of $U(\mathbb Q)$ whose two affine coordinate functions take values in $\mathbb Z$.
[/guided]
[/step]
[step:Apply Siegel finiteness to the affine curve obtained by deleting the point at infinity]
We use the general Siegel finiteness theorem for integral points on affine curves: if $C$ is a nonsingular projective curve over $\mathbb Q$ of genus at least $1$ and $D \subset C$ is a nonempty finite divisor, then the set of $\mathbb Z$-integral points on $C \setminus D$ is finite. Apply this theorem with
\begin{align*}
C := \overline E, \qquad D := \{O\}.
\end{align*}
The hypotheses are satisfied: $\overline E$ is nonsingular and projective over $\mathbb Q$, its genus is $1$, and $D$ is nonempty because it contains the rational point at infinity $O$. Hence the set of $\mathbb Z$-integral points on
\begin{align*}
\overline E \setminus \{O\} = U
\end{align*}
is finite.
[guided]
Now we invoke the external finiteness input. The general Siegel finiteness theorem for integral points on affine curves says: if $C$ is a nonsingular projective curve over $\mathbb Q$ of genus at least $1$ and $D \subset C$ is a nonempty finite divisor, then $C \setminus D$ has finitely many $\mathbb Z$-integral points.
We apply this theorem with
\begin{align*}
C := \overline E, \qquad D := \{O\}.
\end{align*}
Each hypothesis is accounted for. The curve $\overline E$ is nonsingular and projective because the Weierstrass equation defines an elliptic curve, hence has nonzero discriminant. Its genus is $1$, so the genus condition "at least $1$" is satisfied. The divisor $D$ is nonempty because it contains the point at infinity $O$. Therefore Siegel's theorem gives that the set of $\mathbb Z$-integral points on
\begin{align*}
\overline E \setminus \{O\}
\end{align*}
is finite. By the definition of $U$ from the previous step, this curve is precisely the affine Weierstrass model $U$.
[/guided]
[/step]
[step:Identify Siegel integral points with the integral affine points in the theorem]
Let
\begin{align*}
E(\mathbb Z)_{\mathrm{aff}} := \{(a,b) \in \mathbb Z^2 : F(a,b)=0\}
\end{align*}
denote the set of integral points in the given affine Weierstrass model. Because $F$ has coefficients in $\mathbb Z$, every pair $(a,b) \in E(\mathbb Z)_{\mathrm{aff}}$ defines a $\mathbb Z$-integral point of $U = \overline E \setminus \{O\}$. Thus there is an inclusion
\begin{align*}
E(\mathbb Z)_{\mathrm{aff}} \subseteq U(\mathbb Z).
\end{align*}
The preceding step proves that $U(\mathbb Z)$ is finite, and every subset of a finite set is finite. Therefore $E(\mathbb Z)_{\mathrm{aff}}$ is finite, which is exactly the asserted finiteness of integral points in the affine Weierstrass model.
[/step]
