前端技术圈最具知名度的开发者之一、React核心协作者Dan Abramov，近期以完全的数学外行身份，在GitHub公开了一份针对数学大师约翰·康威（John Conway）50年前猜想的形式化证明。他没有受过专业代数训练，却利用Claude与ChatGPT构建了一套多角色提示流水线，经过整整一个月的试错，最终生成并通过了Lean 4定理证明器的微内核检查。
这篇名为gaearon/conway-refinement的开源代码库，迅速被形式化验证注册表Palomar收录。然而，若将此事简单理解为“程序员靠AI顿悟解决50年数学悬案”，便完全脱离了这场实验的工程本质与学术现实。该成果的核心价值并非AI单挑纯数学，而是人类工程师作为外骨骼调度者，依靠暴力算力与严密反馈闭环完成的工程破拆；更关键的限制在于，形式化代码的逻辑自洽，至今尚未跨越数学界关于语义等价的审判门槛。
400亿token堆叠出的外骨骼工程
这项实验最直观的震撼来自底层算力账本。Abramov估计，整个证明推进过程总共消耗了约400亿（40B）token，其中模型生成的输出token达2.1亿。在此期间，他数次耗尽了对应模型20倍Pro套餐的周度调用额度。
这并非大模型在单次长思考中的灵光一现。高达95%以上的Token调用属于上下文缓存读取。Abramov没有指望LLM写出无懈可击的长篇数学论文，相反，他在最初几周遭遇了严重的模型幻觉与戏剧化伪证。转折点发生在他退回自己最熟悉的领域：软件架构。
他将攻坚流程拆解为多Agent协作系统。由一个PM角色固守康威猜想的主目标，数个Math角色分头探寻突破点，Red角色专门负责证伪与挑错，最后由Lean角色将幸存下来的逻辑拼图转化为形式化代码。在整个闭环中，Lean 4充当了绝对客观的编译器：模型可以胡言乱语，但代码若无法通过内核检查，流水线就会立刻回溯重来。
外行并不能教AI做数学，但优秀的工程师懂得如何把不讲理的死胡同变成自动化测试用例。
- 结论.大模型用于前沿科学研究的破局点，不在于模型自身的纯数学直觉，而在于人类能否搭建一套能即时证伪、阻断幻觉扩散的高频反馈管线。
踩在现代数学肩膀上的形式化转译
这项工作之所以没有彻底滑向民科式胡思乱想，在于模型所依赖的知识底色并非空中楼阁。康威于1976年在《On Numbers and Games》中提出了超现实数体系，并留下全能整数细化猜想：若两对全能整数满足ab=cd，能否将其进一步拆分为公共积木因子。这在本质上断言全能整数构成一个pre-Schreier整环。
在半个世纪里，数学界并未停滞。从Berarducci、Pitteloud到近年来L’Innocente与Mantova的系列论文，数学家已将全能整数不可约元的讨论，大幅收敛至广义幂级数环的代数结构中。
Abramov与大模型找到的路线，正是这套现代数学工具的延续：先把细化猜想转化为原初性命题，将其映射到广义幂级数环中证明pre-Schreier性质，再借助康威范式将结论传导回超现实数。换言之，AI并未另起炉灶发明一套全新数学体系，而是扮演了不知疲倦的高级翻译官，将学者们铺垫好的离散论文定理串联成了完整的机器可读证明。
通过内核检查不等于解决数学猜想
目前，代码库中的Challenge.lean与Solution.lean已通过Palomar注册表的自动化流水线核验。但数学界至今保持着极其审慎的态度，焦点集中在形式化证明中最隐蔽的陷阱：定义漂移（semantic gap）。
康威最初提出的超现实数体系是庞大的真类，超越了普通集合论的边界。但在Lean 4这样的类型论系统中处理真类，往往需要引入宇宙多态或人为设定某种截断与尺度限制。机器能够确保推演过程毫无破绽，但它无法替人类判定：屏幕上这段通过校验的代码命题，在数学本质上是否100%忠实还原了康威1976年的原意？
Abramov在项目文档中坦承，截至2026年9月中旬，尚无超现实数领域的资深数学家对这套形式化编码给出最终审查意见。如果形式化定义在降维处理时悄悄阉割了某些病态情况，那么整个庞大的证明就只是在一个人工修剪过的“安全玩具模型”里自洽运转。
- 风险.形式化工具虽然杜绝了步骤推导中的逻辑疏漏，却将科研欺骗性的源头全部转移到了问题定义本身，未经验证的定义对齐可能使宏大证明化为乌有。
这场耗费400亿token的实验，宣告了科学研究某种新分工的到来。前沿数学的门槛正在从苦行僧式的推演计算，转变为对形式化系统与自动化管线的编排能力。但终局的裁判权仍握在人类手中：在同行评议确认代码定义无误之前，这个被AI与外行撞开的数学缝隙，依然只能算作一段精彩的工程奇袭，而非定论。