The first player wins exactly when n ≥ 5, by a strategy that is formalized in Lean 4.
arXiv preprint, October 2026
arXiv PDF Site Source