Topological Noetherianity of the infinite half-spin representations

We prove that the infinite half-spin representations are topologically Noetherian with respect to the infinite spin group. As a consequence we obtain that half-spin varieties, which we introduce, are defined by the pullback of equations at a finite level. The main example for such varieties is the infinite isotropic Grassmannian in its spinor embedding, for which we explicitly determine its defining equations.