一个数学新手用一个月的业余时间，消耗了大量的计算资源，并声称找到了一项Conway五十年前提出的复杂猜想的Lean证明。这听上去像个笑话，但作者详细记录了整个过程。几个月前，AI在数学领域的应用引起了广泛关注，"取得突破"成为社交媒体上的热词。出于好奇，作者决定看看自己作为一个数学外行，能否利用前沿AI模型解决一个未解的问题。
他寻求的不仅仅是一个随机结果，而是一个能够"吸引自己"的问题。于是，他向Claude提问：在超实数的领域中，哪些未解的难题最有趣，为什么？超实数这一概念由Conway创造，包含了所有的数字。不仅有所有实数，还有无尽的序数，如无穷大的ω、ω+1、ω*2及更大值等。这一系统是由简单规则生成的：在已有数字之间的空隙中不断"创造"新数，包括数字两端的空隙。如此反复，最终形成超实数。
在这一过程中，第一个空隙诞生了零，第二天有了-1和1，之后逐渐生成更多数字，形成一棵二叉树，不断出现实数和序数，以及一些更加复杂的数字，且其之间具有一致的算术关系。 千亿球友会
作者要求Claude集中在一个特定的问题上，并鼓励它大胆尝试。Claude建议关注Conway的算术，尤其是L'Innocente–Mantova工具中的一个问题——每个具有无限支撑的不可约元是否是素元？这一问题与Conway在1976年提出的猜想等价。这也恰好是Conway关于他自己数系的最后一个未解难题，而2026年则是《On Numbers and Games》出版五十周年。今年的纪念与此猜想的相关性，成为作者选择这道题的情感因素。
Conway的精细化猜想指出，omnific整数具有特定的精细化性质——如果ab = cd，那么总能找到整数e、f、g、h，使得a = ef，b = gh，c = eg，d = fh。omnific整数包含普通整数和更多奇特的数字。它们在超实数树中可以通过特定路径生成。
在对话中，作者最后询问是否有可能用相对简洁的方式将该猜想形式化，Claude表示可以实现。因此，作者决定接下这个项目。值得注意的是，他当时并不知道Claude对"问题已被完美归约"的说法并不准确。真正的证明远不止这个归约。 千亿球友会
作者强调，尽管他的证明尚未经过独立数学家的验证，但他有充分的理由相信其正确性，并欢迎他人进行反驳。该证明已通过Palomar注册表的机械检查，几位在Lean及相关领域有经验的人都认为其陈述合理。因此，只要证明不依赖于Lean内核的错误，其成立的可能性是很大的。
留言框-
