Mathlib维护者:数学理解的具象载体--形式化

最近大模型猛出数学结论，圈里都在吵“理解到底算不算科研产出”。我倒觉得，人工形式化能把它变成看得见的东西。说白了，就是用 Lean 这类工具把定义、命题和证明一步步写成机器能核实的代码。这活儿不是照搬论文，得反复提炼思路。Mathlib 已经攒到 250 万行代码，靠几百人协作。它存下的不只是定理，更是我们共同吃透一份论证的过程。可现在大家都在推“自动形式化”——让 AI 批量生成代码去核验结果。这事有价值，但我更看重人工打磨。因为自动产出再快，几乎也都依赖 Mathlib。装订成册挺漂亮，可没有印刷术，装订本身也长不大。真正扎心的是学术评价。我们嘴上喊着反对出版商，可升职、拿教职还是看顶刊论文数。博士生沉下心做形式化，收益远不如多发几篇短平快的文章。有评论说得挺狠：AI 几天就能干完人类几十年的活，院系绝不会为慢节奏的人工提炼改评价标准。青年学者干嘛花几年写冷门引理？这话戳到了。可越是自动化泛滥，越需要有人读懂最终的形式化内容。与其等别人把数学交给机器，不如我们自己先把理解做成凭证。

原标题：《Mathlib维护者:数学理解的具象载体--形式化》

阅读原文