{"id":"arxiv/2609.32816","url":"https://arxiv.org/abs/2609.32816","tags":["math.AT","cs.LO"],"score":0,"title":"The third symmetric product of a set is a set in HoTT","domain":"math.AT","source":"arxiv","authors":["Wojciech Paupa"],"reviews":0,"subject":"math.AT","summary":"We deformalize an LLM-generated proof within the formalism of Homotopy Type Theory that an iterated pushout construction for $\\operatorname{SP}^3(X)$ is a set whenever $X$ is a set. The proof expands on a similar proof by Buchholtz for $\\operatorname{SP}^2(X)$, employing a similar encode-decode strategy and the same formal machinery.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-09-26","reactions":{}}