数月之前，AI 数学结果开始登上新闻版面。自然地，我开始好奇——我作为一个数学新手，能否找到一个开放问题并让前沿模型解决它？虽然我花费了一个月的空闲时间和大量的 token，但我相信自己获得了 Conway 在 50 年前提出的 refining conjecture 的 Lean 证明。该猜想声称如果 ab = cd，那么存在整数 e、f、g、h，使得 a = ef、b = gh、c = eg、d = fh。我的证明尚未被数学学家独立验证。然而，我有充分的理由相信它是正确的，并且真诚地邀请反驳。该证明已通过 Palomar registry 的机械检查，熟悉 Lean 和该领域的人士表示该陈述似乎是正确的。因此，假设它不依赖于内核错误，那么它很可能是合法的。在本文中，我将描述我的方法和所学到的东西。选择研究领域我请 Claude 选择一个 surreal 数中的开放问题。surreal 数是 John Conway 的发明，是一种包含各种大小数字的数值系统：所有实数、像 omega 这样的序数数字，以及像 75 + omega*3 + 1/omega 这样的组合。惊人的是，这一丰富的系统从单个规则中孕育而出：在已有数字之间的每个空隙中生成一个新数字。选择问题最初，我请 Claude 提供 surreal 数研究计划中未解决的问题。