我靠“感觉”证出了 Conway 猜想

超现实数与“无”和“零”

• 许多读者卡在了“在无和零之间 / 在零和无之间”这一步。
• 几位评论者用集合论术语重新解释了超现实数：数写作 {L | R}，其中 L、R 是更早出现的超现实数集合；∅|∅ 表示 0，∅|{0} 表示 –1，{0}|∅ 表示 1，等等。
• 解释中特别强调：“无”= 空集，不是 0；这些空隙包括“比一切都左”以及“比一切都右”。
• 有人推荐图示和外部入门材料（例如 Hackenbush、其他博客），认为它们比原始定义更清楚。
• 关于无理数和无穷如何出现的问题，则通过无限阶段来回答：类似 Dedekind 分割的构造，以及无限左/右集合，会产生实数、无限序数和无穷小量。

---

AI 辅导与教学法

• 有人希望出现自适应的、类似 RL 的交互式导师，能建模个人理解并填补知识缺口。
• 建议包括：在你已经熟悉的领域里，提示你去寻找类比；以及利用现有的“教学技能”类设置。

---

AI 在数学中的角色：能力与局限

• 讨论集中在：LLM 驱动的证明究竟是“智能”，还是只是大规模穷举。
• 有人认为，能高效探索巨大的搜索空间，本身就是智能的标志；也有人把它比作 1980 年代那种跑得快但“很笨”的 CPU。
• 理论讨论提到了 Busy Beaver、停机问题和哥德尔：任何固定的计算系统（包括 LLM）都无法判定所有真数学命题。
• 反方观点是：大多数不可判定/独立命题都“丑陋而无关紧要”；实际数学很少会碰到这些极限。

---

验证、Lean 与信任

• Lean 形式化被看作核心：如果那份小的桥接文件和内核都是正确的，那么证明就成立。
• 有人担心 Lean/内核中的 bug 以及最近的“LLM hack”；另一些人则指出可以通过独立内核交叉检查，并且受信代码范围有限。
• 也有人对把可复用的超现实数基础设施提取进主流 Lean 库很感兴趣。

---

署名、作者身份与数学文化

• 围绕把这称作“我的证明”存在强烈分歧：
  • 一方认为：使用 LLM 就像使用强力工具（比如电钻）；人类选择了问题、组织了多次运行、筛选了输出，并对错误负责。
  • 另一方认为：人类几乎没有提供数学洞见，因此把功劳归给自己是误导性的，也会侵蚀文化。
• 更广泛的担忧：
  • 只为结果“剥矿”而不去理解，可能会打击人类研究者的积极性，并损害职业结构。
  • 许多人担心，中层数学家会失去本就稀缺的机会，而收益只会流向少数资深人物或著名难题。
  • 也有人反驳说：把晦涩的 AI 证明系统化、简化，并转化为简短优雅的人类证明，本身就是相当重要的工作。

---

对这个项目及其风格的反应

• 许多读者把这篇文章当作“认识论表演艺术”，并认为它以一种异常易懂、自觉的方式叙述了与不可靠模型合作的过程。
• 有些人喜欢看到一个“业余者”磕磕绊绊地处理高等数学，觉得这比专家讲座更有共鸣。
• 持怀疑态度的人认为这个项目“有悖道德”、缺乏创造性，或对理解没有帮助，尽管他们承认其底层结果（如果正确）在数学上并不平凡。
• 该领域的一位关键人类专家表示，AI 生成的方法看起来是可靠的，而且核心思想可以提炼成一个非常短而优雅的证明，这进一步增强了对建设性 AI–人类合作的希望。