■ 马千里

　　Colombo问题的证明路线打通时，我的智能手表发出了心率过快的提醒。

　　这是意大利数学家Bonaparte Colombo（博纳帕尔特·科隆博）在近百年前留下的一道猜想。问题本身并不复杂，研究的只是数字经过减法、乘方后形成的一类特殊矩阵，但要证明其中的规律对所有情况都成立，却远非易事。近一个世纪以来，数学家逐步解决了部分情形，仍留下最后的证明缺口。

　　今年8月，我与AI合作，为这道1928年提出的数学问题补上了缺失的证明。到10月中旬，在之江实验室的论坛上分享这段经历时，论文和代码已经公开，成果也被北京大学北京国际数学研究中心长聘教授董彬等发起的开放数学问题库ICMConjectures收录。

　　我学的是计算机，并非数学科班出身。有人会好奇，一个研究代码的人，怎么就解决了百年数学问题呢？

　　时间回到7月，在浙大数学科学学院副教授于飞的建议下，我从开放问题库中选中了Colombo问题。选择数学，有一个很实际的考虑：结论能够接受严格检验。我可以先用计算寻找线索，但最终必须拿出完整的证明。算对一万个例子，依然不能代替对所有情形的证明。

　　几个AI工具分头查文献、提思路、找反例，每天都有新的材料需要处理。刚觉得一种办法可行，往下推才发现，还得补读另一领域的论文。文献原来并没有“查完”这回事。眼前这一步该怎么走，成了更具体也更费心的事。

　　我们陆续试过8条路线。其中一条不断传来好消息，文本与代码积累了超过4.7万行，小规模的结果越来越多，适用于所有情形的证明却迟迟没有出现。材料越来越厚，我需要停下来问自己：这是在接近答案，还是只是在同一个地方做得更细？

　　继续安排计算总是容易的，判断是否值得却不容易。自己的电脑、租用的千核级算力、需要接入的专业软件，都有真实的成本。预计一周的事，可能一个月仍未结束。这些数学探索，很难指望即时回报。方向要有希望，投入也要负担得起。

　　我最终换了一个方向。此前的反例和中间结果留了下来，AI提出了新的想法：先处理一个更简单的相关问题，再回到原题。2个多小时后，证明路线打通了。后来写进论文的关键数学思路，确实来自AI；而在它出现之前，我们先得从那条投入最多的路上退出来。

　　心跳平复之后，工作还要接着做。我让其他AI寻找漏洞，把重要计算换一种方式重做，再把推理写成计算机能逐步检查的代码。前面盼着好消息，这时却希望尽早发现问题。一个条件漏了，就往前查；某一步说不清楚，就重新推演。屏幕上还是那些专业、繁复的反馈，一份接着一份。

　　我后来和于飞等人谈起一个比喻，大家都觉得贴切：科研有时像移动互联网流行的“砍一刀”，自以为到了99%，后面却还有99.9%、99.99%。即便选对了路，最后那个缺口也可能最难，补上它花的时间，甚至不亚于此前全部工作的时间。AI让许多尝试快了起来，却没有让剩下的难处也按同样的速度消失。

　　相关证明通过了机器核验，论文也已公开，但机器核验不能代替期刊同行评审。我与专业数学家通信，核对文献，寻求批评。请人看一份证明，远不只是请他认可一个结论。他得真正读懂，判断哪一步成立、哪里值得怀疑，还要看前人已经走到了哪里。模型生成材料很快，读懂这些材料的人却要付出实实在在的时间。

　　这些反馈让我越来越珍惜人类的专业判断。关键处的一句提醒，可能省掉很长一段弯路。AI给了我走进这个领域的机会，走进去以后，我才更清楚自己缺少什么，需要向谁请教。

　　解开Colombo问题后，我自然想做第二道、第三道。第二道是与矩阵计算稳定性有关的五阶难题，比Colombo花费了更多时间和算力，像个“大号Colombo”，暂且按下不表。真正让我心绪复杂的是第三道——一项关于四阶矩阵的不等式猜想。国庆假期，它也到了最后关口，以色列数学家伊尔·拉维（Yair Lavi）公开了预印本，先一步给出了证明。核对结果后，我起初难免懊恼。仔细读他的论文，才知道他早在2018年便开始研究相关的矩阵问题。一个月与多年放在一起，我的不甘渐渐淡了：若我抢在他前面，他该有多失落？我写信向他祝贺，此后我们仍保持邮件往来，也一起交流、探索新的问题。

　　写完那封信，我想把更多精力放到一些无论谁先取得进展大家都能高兴的研究上。我发起公益项目“骋原AI实验室”，在网站上公开探索过程。生物医药方向关注渐冻症等罕见疾病，寻找运动神经元受损背后值得实验检验的线索；天文方向尝试寻找“三体星”——双星像钟表一样规律地相互遮挡，如果时间出现细微偏差，会不会有第三颗星在暗中施加引力？材料方向，我也正与浙江大学信息与电子工程学院教授林时胜合作，探索高温超导材料等课题。病人盼望新药，产业需要更好的材料，未知的天体牵动人类的好奇心。这些研究离真正的发现还很远，却让我愿意投入。

　　至于数学，我并不担心AI接连解开人类提出的猜想，就会把数学问题做完。我们已经写下的猜想，不过是已知世界的一部分。数学如宇宙般浩瀚，越往深处走，未知越多。今天的答案，也许正是明天新问题的起点。除了用AI解题，我还想和它一起，发现此前没有想过的问题。

　　（作者系无界AI联合创始人，浙江大学人工智能方向工程博士）