一位数学新手通过使用Claude和ChatGPT等AI模型，结合Lean形式化验证工具，成功证明了John Conway在1976年提出的细化猜想1。该猜想声称，若两组整数的乘积相等（即ab=cd），则必然存在四个整数e、f、g、h，使得a=ef、b=gh、c=eg、d=fh1。这是康威关于超现实数最后一个未解决的猜想1。
该项目耗时约一个月，历经多个失败的重启周期，最终采用多智能体实验室架构才得以成功1。整个证明过程消耗了约40亿个token的AI计算量（其中超过95%为缓存读取），API成本估计约4万美元1。证明已通过Lean形式化验证并通过Palomar注册表的机械检查1，但目前尚未获得独立数学家的验证1。该项目选择在《ONAG：论数字与游戏》出版50周年之际进行1。
A mathematician has announced the completion of a formal proof of John Conway's refinement conjecture, a problem that remained unsolved for half a century, using artificial intelligence models and machine verification 1. The conjecture posits that for any integers where ab=cd, there must exist integers e, f, g, and h such that a=ef, b=gh, c=eg, and d=fh, a property described as the refinement property of omnific integers 1.
The proof was developed over approximately one month through iterative collaboration with Claude and ChatGPT, leveraging what the researcher describes as a multi-agent laboratory architecture after several failed restart cycles 1. The project consumed roughly 4 billion tokens, with over 95 percent consisting of cached reads, resulting in an estimated API cost of approximately $40,000 1. The work was formalized using Lean and has passed mechanical verification through the Palomar registry 1.
Conway originally posed this conjecture in 1976 as his final unresolved question concerning surreal numbers, and the researcher chose to tackle it in conjunction with the 50th anniversary of Conway's foundational work "On Numbers and Games" 1. While the proof has been formally verified through automated systems, it has not yet undergone independent validation by the mathematical community 1.
评论
还没有评论，欢迎留下第一条。