我们发布了第一个专门针对范畴论和形式化证明的Benchmark!

This page has a English version.

大家新年好~新年伊始，我想向大家介绍我们最近发布的LeanCat-1（arXiv: 2512.24796）：据我们所知，这是首个专门面向范畴论（category theory）的 Lean 4 形式化证明 benchmark（基准测试集）。LeanCat 包含100 道statement-level 任务，覆盖 adjunctions / limits–colimits / abelian categories / monads 等 8 个主题簇，专门压力测试“抽象接口层推理 + mathlib 库导航（library-mediated reasoning）”。基线结果非常硬核：最强模型仅8.25% pass@1 / 12% pass@4 ，Medium/High 基本清零，直接暴露 natural-to-formal bottleneck。我们还评估了LeanBridge：结合LeanExplore 检索 + Lean 编译/验证反馈的 retrieve–generate–verify loop，在部分任务上带来稳定提升。

LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)

https://www.alphaxiv.org/abs/2512.24796

以及 Github 仓库

https://github.com/sciencraft/LeanCat

因为我几乎不认识 AI for math 的老师和同学，AI for Science 也认识得极少，因此大家的任何转发和评论都是极富帮助和受欢迎的

。我相信这项工作在Ai for Math和formal proof社区有若干承前启后的意义，所以我想要讲述的主要是个人视角：

在今年暑假一次量子物质会议的会后间隙，罗迪老师向我们感慨说，现在做前沿的量子物理科研不一定需要在科研单位，在企业和公司也可以具有很好的科研环境；很多工作在量子计算或者人工智能前沿的杰出老师其实都持有类似的观点。另一方面，企业拥有的资金流远远大于高校，

这句话一直在我心头萦绕不去。那么在AI4S等主题上，科学家为什么还要做科学问题，而不是完全交给企业去做？在我看来，这是因为有一些事情终究是只有科学家会去做的，因为学术机构当中的科学工作者和大厂中的商业决策者具有不同的价值判断取向：例如，现实里大厂非常关心建立IMO IPhO等竞赛的benchmark并且训练AI”打榜“，并且宣称这体现了自家AI的科学素养和智力水平；但是竞赛内容总是非常成熟的科学知识并且重在考察技巧，而对于前沿科学问题帮助不大；为什么大厂要选择竞赛作为智力能力的评判呢？这有诸多原因，例如竞赛成绩具有直接的评比价值并且易于让资方和公众接受，而且 AI 行业从业的年轻人里有很多IMOer / IOIer 之类的，大家对竞赛题天然熟悉。

相比之下，对科学问题的研究首先需要长期的学术积累；一个很典型的场景是：在讨论AI for Science的产学研合作的时候，字节华为等企业代表和物理学家互相听不懂对方的内部讨论。学术成果往往难以直观理解，而且构建数据集困难。基于这些种种原因，企业在基础数理科学的投入上较少。企业更关心能够带来可观测收益的主题：在生物制药方面，将原先的大分子DFT等步骤每优化一步就有可能带来上亿的利润，清华大学今天刚刚发表一篇「AI助力药物虚拟筛选提速百万倍」的新年首篇Science论文；再比如材料、能源、化工…… 而不是看似少有直接经济回报的基础科学。

然而邱先生说过「科技的基础是科学」，科技最前沿的突破更是要靠基础科学。也正因此，教会AI「什么是科学研究」就显得尤为重要；这也就是我说的「只有科学家会做的事情」——训练和教育AI为科学事业服务。

在这条路线上，我看到很多我景仰的前辈和同学都投身其中，这些工作未免让我于我心有戚戚：

Humanity’s Last Exam (2501.14249)

PHYBench: Holistic Evaluation of Physical Perception and Reasoning in Large Language Models (2504.16074)

Probing the Critical Point (CritPt) of AI Reasoning: a Frontier Physics Research Benchmark (2509.26574)

CMT-Benchmark: A Benchmark for Condensed Matter Theory Built by Expert Researchers (2510.05228)

QMBench: A Research Level Benchmark for Quantum Materials Research (2512.19753)

等等。另一个相近的领域是 scientific agent 的开发：在这些方向里，不仅有前辈，也有同龄人，甚至更出色的后辈：

physmaster: Building an Autonomous AI Physicist for Theoretical and Computational Physics Research (2512.19799)

我一向倡导和推崇「青年学者应该做’时代性的事情’」，这构成了我对于学弟学妹生涯建议的底色；那么作为青年学生的其中一员，一个自然的问题就是，我能为AI4S做些什么呢？这通向了这篇文章的诞生。看到文章顺利挂出来，就会觉得之前的辛勤准备和昼夜努力都是值得的。

##为什么是范畴？

相比于线性代数、微积分等相当成熟的、具有大量数据而且易于复核和检验的数学学科，范畴论，尤其是高阶范畴论，不仅站在形式数理科学的前沿，而且甚至超越了人类智力所及。初级范畴论以一种简洁优雅之美吸引了很多年轻人，这是因为刻画的信息不多，如果只关心函子性那么无异于有限多元素的集合和相互映射；然而范畴论的价值和意义远不止于此。按照孔良大师的提法，范畴论的本质是「带着结构进行运算」，因此天然和诸多数学分支都有对接。然而更细致的研究要求更海量的计算、更细致的引理。

对于物理学家，十年以来拓扑物态的飞快进展引入了诸多新数学——其中最具代表性的就是范畴论。然而理解四维时空当中的拓扑序的话，势必需要用到2-范畴。我们在初等量子力学中学习过角动量，高等量子力学可能时有提及它和classical 3j symbol有关，而三维拓扑序需要用到quantum 6j symbol，四维拓扑序甚至要用到quantum 20j symbol和15j symbol。对应的计算是海量的，甚至人脑难以盛下。

面对前沿数学物理对人类智力极限的这种挑战，一个自然的想法就是——能不能让AI去算？这就是我们做这项工作的一个重要动机。

值得一提的，过去十年当中拓扑物理学当中新数学的引入和应用是令人惊讶的：过去的50年中弦论的进展对形式理论物理引进了大量新数学的用武之地，再往前是微扰量子场论；现在bootstrap、拓扑物态、对称性、CFT、相变和临界点等物理场合则会是我们这个时代的新数学的桥头堡吗？

（一种有趣的观点是，引力物理其实和拓扑物理具有千丝万缕的联系；这种观点最早来自于圈量子社区，但是在最近的拓扑物理研究当中得到了方方面面的implication，尤其是在低维，几乎建立了相当严格的关系）

##为什么是Lean和形式化证明？

因此，我们借助lean语言——这是最成熟的形式化证明平台，基本的思路是「代码跑的通，说明证明没错」，因此可以完全在机器的水平上完成证明检验；这对于数学证明研究的意义是不言而喻的：有史以来人们在验证数学研究当中若干大定理大猜想都花了 佩雷尔曼对三维庞加莱猜想的证明、怀尔斯对费马大定理的证明、望月新一用IUT理论对ABC猜想的证明、四色定理的证明、….. 最近王虹老师对三维挂谷猜想、邓煜对狭义Hilbert第六问题、以及张益唐老师对朗道-西格尔猜想的证明尚在组织同行评议当中 (例如北大国际数学中心BICMR组织了对三维挂谷猜想的验证），而时至今日有限单群的分类的证明的验证仍然需要打一个问号。

这是客观上Lean平台本身的重要性和对于数学证明的意义。在主观上，这也取决于我们之前在Lean和形式化证明这一主题上的积淀：研究团队当中不乏范畴论和数学物理的专家，而容阁师姐的团队又在今年暑假由晓亮老师、东灵老师、罗迪老师等在清华叉院和清华高研院举办的AI4S黑客松上拿了唯一的一等奖，项目名是「LeanBridge灵桥」，搭建起LLM和Lean的的形式化证明桥梁；一些介绍见 https://mp.weixin.qq.com/s/A6EVpCtuCps0BVNzie24dg https://mp.weixin.qq.com/s/Tea0Ow0wlZcZxTw9ilRuag

##下一步….?

在过去的3年间，大语言模型的革命洗刷了整个社会的面貌：从街头巷尾到象牙塔内，人人谈论AI能不能为自己的事业添砖加瓦。我很认同吴恩达的一段话：深度学习是一个圈，而一个人的事业是另一个圈，两个圈的交集（维恩图）是人工智能真正能帮到的。那么对于科学事业，人工智能能起到帮助的边界在哪里？还是说交集在不断扩大？

我想，探索人工智能和科学事业的交集的边界会是这个时代很重要的主题；一年之前我还会觉得人工智能对于科学事业的帮助主要在于大语言模型、Agent系统、符号推理，但是一年以来的进展已经远远超越于此。许多AI近乎独立完成的文章被作出：昨天哈佛大学久负盛名的粒子物理学家Matthew Schwartz在预印本网站arxiv上传了一篇由AI推演计算撰写的文章而人类物理学家只负责监督；也有越来越多的理论学家会在文章致谢部分提到AI助手的帮助。

那么下一个AI热点会是什么？我的判断是具身智能、世界模型、MCP；这三个主题都无一例外是关于「如何教会人工智能认识物理世界」。如此人工智能可以从电子屏中走出来，真正参与物理世界的学术和生产实践，以及进一步体现其「工具作为人类能动性的延伸」的一面。晓亮老师也持有类似的观点，因为人工智能的训练业已非常成熟，下一步就是通过MCP将其投入生活生产。

##感谢和总结

我们感谢西湖大学理学院李牮老师团队的招待：这项工作的最后攻关阶段在那里被做出。我很喜欢杭州这座城市，这也是我第一次造访西湖大学，作为一所小而精的新兴民办高校，西湖大学在方方面面给我留下了非常深刻的印象，无论是出色的教授团队、负责的行政队伍，还是优秀的同学师长，抑或丰富的科研资源、浓厚的学术氛围。

我自己是个很喜欢和煦阳光的人，在江南过冬每每给我留下很美好的印象。初次来到西湖，和李牮老师、朱伟老师、洪光老师、王翀老师、建豪学长的讨论令我受益匪浅，一些学到的宝贵知识是令我裨益终生的。我也感谢西湖大学理学院各位可爱同学们的招待，和他们的相处是一段很愉快的记忆。

最后我们深深感谢容阁师姐的殷切付出：这一工作的绝大部分功劳要归功于她。容阁师姐是李牮老师和孔良老师的高足，在孔良大师那里受到了严格的拓扑物态和范畴论教育，现在是邱中心出类拔萃的博后，功底扎实、富有想法；没有她的辛勤努力和不懈推进，这篇文章就不会见世。

最后我愿以久负盛名的《普林斯顿数学指南》卷尾的一段话作结，这段话在Aityah对青年数学家的建议之前——我推荐所有从事数学物理行业的学生都应该阅读这本书：

「当计算机开始出现在数学家的环境中的时候，几乎一致的反应是它对于证明定理永远也不会有用……彩虹的另一端可能是计算机的更为深远的作用。

在数学的少数几个领域中，我们已经可以做到这一点……通向这个壮丽的新世界的道路还是漫长的而没有人去探险过。」

2025.1.9