The (very nice) final problem of [IMO 2017](http://imo-official.org/year_info.aspx?year=2017) asked contestants to show:

> If $S$ is a finite set of lattice points $(x,y)$ with $\gcd(x,y)=1$, then there is a nonconstant homogeneous polyonmial $f \in \mathbb Z[x,y]$ such that $f(x,y) = 1$ for all $(x,y) \in S$.

It's claimed [in this forum post](https://artofproblemsolving.com/community/c6h1480686p8648257) that the above IMO problem is a special case of [Lemma 7.3 of arXiv:16040.01704](https://arxiv.org/pdf/1604.01704.pdf). The former post phrases the lemma as follows:

> If $X$ is a finite scheme over $\operatorname{Spec} \mathbb Z$ then $\operatorname{Pic}(X)$ is finite.

Being unknowledgable as I am, I do not see how to deduce the IMO problem from the lemma. Can someone make the connection explicit?