A counterexample to Vaught's Conjecture for $L_{{\omega }_1,\omega }$

We construct a sentence of $L_{{\omega }_1,\omega }$ having exactly ${\mathrm{\aleph }}_1$ many countable models up to isomorphism, but no perfect set of non-isomorphic models. This disproves Vaught’s conjecture for infinitary logic. The construction follows a framework devised by Robin Knight, and the proof has been formally verified in Lean.