ChatGPT 5.6 Sol 实质参与构造更小的不可判定群与 Adian–Rabin families，并由 Lean 4 验证核心代数结果

Marc Kegel、Shana Yunsheng Li 与 Qiuyu Ren 构造出一个具有不可解 word problem 的 3-generator 9-relator group，并据此得到两个 fixed-size Adian–Rabin families：4 generators / 11 relators 与 2 generators / 10 relators；进一步推出 #7(S²×S²) 在拓扑意义下不可识别、#9(S²×S²) 在光滑意义下不可识别，改进此前已知界。arXiv comment 明确写明 main results were developed by ChatGPT 5.6 Sol；论文同时给出代数结果的 Lean 4 machine-checked formalization。