发表机构
JetBrains Research（JetBrains 研究院）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究在同伦类型论中验证了 LLM 生成的证明，即当 X 为集合时，其三次对称积 SP^3(X) 的迭代推出构造仍为集合，扩展了 Buchholtz 对 SP^2(X) 的证明方法。
AI 中文摘要
我们在同伦类型论的形式体系内，对一个由 LLM 生成的证明进行非形式化处理，该证明表明：当 $X$ 是一个集合时，$\u200b\operatorname{SP}^3(X)$ 的迭代推出构造是一个集合。该证明扩展了 Buchholtz 关于 $\operatorname{SP}^2(X)$ 的类似证明，采用了类似的编码-解码策略和相同的形式化机制。
英文摘要
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.
Comments10 pages, 1 figure, formalization at https://github.com/WPaupa/symmetric-products/
