一个提出于1928年的数学问题，在人与AI的协作中迎来了解答。
浙江大学计算机科学与技术学院博士生、无界AI联合创始人马千里，与多个AI系统共同探索，完成了Colombo行列式问题的证明。
Bonaparte Colombo与他在1928年提出的问题｜据历史肖像AI创作
这项研究中，AI深入参与了证明策略的发现和初稿生成。马千里则持续拆分问题、比较路线、调配计算资源，推动核查、修改与证明落地。
先后约八条候选路线，一次关键的方向调整，串起了这场协作的核心故事。
8月18日，首版论文在Zenodo公开，完整的Lean证明代码同步开源到GitHub。
8月31日，修订后的《Colombo’s Determinant Problem》提交arXiv，现已公开，作者署名为Qianli Ma（马千里）。从论文到可由计算机逐步检验的证明代码，这项成果向全球研究者开放。
《Colombo’s Determinant Problem》已在arXiv公开
一道看似简单却跨越近百年的问题
选几个互不相同的数，两两相减，再把差值取相同的整数次方，排成一张正方形数表。Colombo的问题是：当数字个数为偶数、幂次至少为个数减一时，这张数表的行列式是否一定不为零？
不熟悉行列式也没关系。可以把它理解为衡量这张数表是否“退化”的一个关键数值：它不为零，意味着用这张数表作为系数的一组线性方程，对任意给定的右端数值都有唯一解。
难点在“一定”二字。算对十组、一万组，都不能代替对所有情形的证明。
1986年，Dyn、Goodman和Micchelli在研究另一类距离矩阵时，顺手解决了这个问题的偶数次幂情况。即，当D≥N-1且D为偶数时，矩阵A行列式总是不为0。
但偶数阶矩阵对应的奇指数部分，因为一直处于一个“没有趁手工具来解答的状态”，而被遗留了下来。
2026年，浙江大学人工智能方向博士生、无界AI联合创始人马千里，在于飞老师的建议下，考察了一批历史数学问题。
而在这其中，Colombo问题吸引他的地方，在于它足够具体：能先用小规模计算寻找规律，也能把最终的推理交给计算机检查。
于是，马千里与AI协作，补上了剩下的奇数次幂情形，给出了完整答案。
这次证明还揭示了更细致的结构：它确定了一个名为Pfaffian的关键数学量的正负规律，由此证明行列式不会为零。这个中间量，也成为人机协作寻找突破口的重要线索。
八条路线背后的人的判断
研究并没有从一个问题直接跳到一份答案。
按照马千里的回顾，团队先后探索了约八条路线：有的容易入手，却随着规模扩大迅速增加计算量；有的概念漂亮，但关键一步缺少可靠的数学依据；还有一些路线留下了有用的中间结果，最终没有成为完整证明的主线。
无界AI团队搭建的WUJIE AIAGENT平台参与了这项工作。
多个AI系统被组织起来，承担文献检索、候选证明生成、反例搜索和形式化辅助等任务。
马千里负责拆分问题、比较路线、分配计算资源，并对结果进行核查和修改。
人与AI共同探索数学证明｜AI生成插画
“AI给出的可能性越多，选择反而越重要。”马千里说。
这种选择贯穿研究过程。每条路线都需要持续回答：已经验证了什么，还缺哪一步，扩大规模后是否依然成立，继续尝试需要付出多少计算成本。
智能体给出分析和建议，人据此决定哪些方向继续投入，哪些暂时停下。
整个过程像一个不断反馈的研究循环：人提出下一轮任务，AI展开探索，再把结果与障碍带回来。
马千里关注的是，这些新结果有没有让研究真正往前走，而不只是又增加了多少代码和报告。
人提出任务，AI探索，人根据结果调整方向
在最接近成功的地方调整方向
最难放下的，往往是已经投入最多的路线。
最初，研究把原问题转化成一个更容易下手的辅助问题。
AI沿着几类经典数学方法深入，在多个小规模情形上取得进展，距离完整答案似乎越来越近。
“就像拼多多一样，永远觉得砍一刀就能出成果了，但是砍一刀之后还要砍一刀，99%之后还有99.9%，而且越到最后越难。”马千里这样描述当时的感受。
然而，局部结果越积越多，能够覆盖任意规模的统一证明仍没有出现。马千里判断，研究需要换一个切入点。
最终，这条路线留下了141项核心研究产物，累计约4.7万行文本与代码。
而在调整方向后，AI提出了关键思路：把辅助问题的次数降低一阶。
可以把它理解为，先解一道与原题紧密相连、结构更清楚的“低一阶问题”，再寻找回到原题的路径。
这一变化带来了突破。
研究先在较低次数上证明关键性质，再通过积分关系逐步推回更高次数，最终解决原来的问题。
一条统一的证明路线由此打通。
此前的探索也并非白费。反例排除了错误捷径，有限情形的结果帮助识别了真正的障碍。
人的调度与AI的数学探索在这里相互作用：调整投入方向，为新的证明结构留出了空间。
把数学证明写成两万行可检查的代码
证明形成后，协作继续进入Lean 4形式化阶段。
Lean是一种数学证明助手，研究者将定义、假设和每一步推理写成精确代码，由计算机逐步检查逻辑是否成立。
这同样是一项细致的协作工作：拆分证明、组织代码、调试报错，再把各部分连接起来。
最终，在AI的加持下，新证明及其完整推理链形成了约两万行Lean代码。
从探索到证明，人与AI共同搭起逻辑之桥｜AI生成插画
8月27日，这项Lean证明通过Palomar平台核验，成为平台第85项登记成果。
Palomar专门收录经过计算机核验的数学证明，由Lean FRO与ICARM共同孵化，数学家陶哲轩参与平台技术维护，并担任科学顾问委员会成员。
约两万行证明代码，把推理过程变成了计算机可以逐步检查的逻辑链。
这次核验中，证明通过了Lean和另一套独立检查工具的双重检查。
从AI提出思路，到形成数学证明，再到代码开源与机器核验，人机协作的成果有了完整、公开的呈现。
2026年8月27日，该成果通过Palomar核验
研究过程中，马千里还与相关领域学者通信，核对已有结果、补充参考文献。论文和代码的公开，让这场探索留下了可以继续研究和复用的成果。
让更多研究者用好AI协作
对无界AI而言，这次实践也带来了一个具体的产品命题：怎样让多个智能体像研究团队一样持续协作？
模型需要查文献、调用计算工具，也需要保存已经验证的结果，让下一轮探索能够接着往下走。
一次失败的尝试，应当留下可供下一条路线使用的经验；一个找到的反例，应当能及时共享，避免其他智能体重复走弯路。让研究者看清进展、及时调整任务和计算投入，是科研智能体平台要解决的实际问题。
Colombo问题的解答，展现了这种协作可以达到的深度。AI带来新的数学思路，人把多条探索组织成持续推进的研究。
无界AI将从这次实践中积累的经验，转化为对科研智能体工具与协作方式的进一步探索。
往期推荐
实拍废片、文案返工、视频白做？仓储制造全自动内容链路，彻底终结无效产出
电商卷到飞起，详情页越换越勤？百年孔凤春的“内容焦虑”，被AI治好了
一天20条视频！AI自动化视频生产，正在降低传统行业的营销门槛
