百年历史回响与数学范式的价值重塑
大家好,这里是最佳拍档,我是大飞。如果你觉得数学家是这个世界上最不需要担心被AI抢饭碗的一群人,那今天这期节目可能会彻底改变你的看法。在2026年7月24日,也就是在备受瞩目的国际数学家大会(International Congress of Mathematicians: 简称ICM)2026的公开演讲现场,当世最顶尖的数学家之一陶哲轩做了一场题为《数学在AI时代》的重磅报告。在这场学术盛会的开头,他便抛出了一个相当沉重且富有洞察力的判断:当前的数学界正在经历一场前所未有的新危机。
需要强调的是,陶哲轩所指的这场危机关乎的并不是某条定理的对错,也不是AI在计算或者推理中算错题那么简单的事。他所指出的深层危机,是当AI真的能够从事研究级数学工作时,我们过去几百年里默认并遵循的那套价值体系、学术评价机制以及共同体的工作方式,可能都要面临从头改写的命运。
为了能够彻底理解陶哲轩口中的这场“新危机”,我们有必要先将历史的指针往回拨一百多年。在20世纪初,数学界也曾经历过一次动荡的范式转变。在那之前的几百年里,数学一直运行在一种近乎朴素的基础上。诸如“什么是集合”、“什么是数”、“什么是无穷”、甚至“数学的公理系统究竟是什么”这类根本性、本体论的底层问题,数学家们基本是扔给哲学家去操心的。数学家们自己则是该算题算题,该证明证明,彼此相安无事。然而,这种朴素的安宁在1901年被彻底打破了。
当时,英国哲学家、数学家罗素(Bertrand Russell)提出了著名的罗素悖论(Russell's Paradox: 关于自指集合的逻辑悖论)。用通俗的话来说,这就好比一个理发师声称自己“只给城里所有不给自己理发的人理发”,那么他究竟该不该给自己理发?如果他给自己理发,他就违反了自己的声明;如果他不给自己理发,按照声明他又应该给自己理发。这个简单却致命的逻辑困境,一下戳穿了当时朴素集合论的逻辑漏洞。
随后在1931年,奥地利数学家哥德尔(Kurt Gödel)抛出了更为震撼的不完备定理(Incompleteness Theorems: 证明在包含基本算术的相容形式系统中存在无法被证明亦无法被证伪的命题)。这两大发现交织在一起,给数学大厦的根基带来了毁灭性的打击,逼着数学家们不得不停下手中的研究,重新审视和重构自己脚下的逻辑地基。
从1900年到1930年前后,数学界经历了一段异常混乱、各种学术流派激烈争鸣的时期。但也正是在这一过程中,数学界因祸得福,最终产出了一套明确、严谨、标准化的现代数学基础框架。这套框架经受住了此后近百年的严苛检验,至今仍是全世界数学研究最可信的运行环境。
陶哲轩据此敏锐地指出,我们现在正处于一个极其相似的动荡转折期。只不过这一次,我们需要重新梳理和检视的,不再是数学的逻辑根基,而是数学研究的价值基础与共同体实践方式。他坚信,只要我们能够像前人那样,把这些底层的价值逻辑彻底厘清并建立新共识,数学共同体最终会变得比以前更加强大、更有韧性。然而在这个重塑的过程中,阵痛与动荡是注定无法避免的。
元数学追问与AI能力猜想的思想实验
在这场备受瞩目的报告中,整场演讲都围绕着一个最为核心的元命题展开。陶哲轩将这个命题称为共同体应对问题(Community Response Problem: 科学共同体面临技术冲击时在机制与伦理上的调适过程)。也就是说,数学共同体应该如何理性、规范且有建设性地去回应现代AI技术,尤其是去面对AI在解决数学任务时那些真实的或者被宣称具备的能力。
陶哲轩特别强调,这个问题本身绝非一个简单的数学问题。它实际上是一个元数学(Metamathematics: 以数学系统本身为研究对象的哲学与逻辑学科)问题,甚至带有强烈的政治、伦理、社会和文化色彩,已经远远超出了公式、公理和定理能够直接解决的范畴。他虽然会借用数学中精确且令大家感到熟悉的符号与概念来阐述观点,但讨论的核心指向早已越过了数学边界。对此他非常坦诚地表示,这是整个数学共同体都需要共同参与回答的问题,他自己并没有标准答案,但有些关键的共识需要立刻开始凝聚。
要想探讨是否需要认真对待这个问题,关键在于去评估一个由他设计的核心概念——AI能力猜想(AI Capability Conjecture: 对AI系统在研究级任务中达成特定表现的系统性假说)。为了让这一评估具备逻辑严密性,陶哲轩将这个猜想设计成了一个包含诸多占位符的参数化模板:
“在未来的某个时间点,某些AI工具将会以某种花费、在某种人类监督水平下,完成某个具体数学领域里某种比例的研究级数学任务,并达到某种成功率、正确性以及质量水平。”
在这个模板中,你可以将每一个“某个”都填入不同的具体变量。如果你填入的数值和时间非常激进,那它就是一个“强版本能力猜想”;如果填入得非常保守,那它就是一个“弱版本能力猜想”。陶哲轩指出,我们如何填这些占位符在细节上的区分并不是他最关心的,但这里存在一个非常现实且关键的分叉点:
如果连最弱版本的AI能力猜想在未来都是伪命题,即AI永远只能帮数学家做一些查文献、排版或者跑跑简单程序的边角料工作,那么数学界完全可以继续高枕无忧,直接把AI当作一种更加好用一点的“高级计算器”,继续用以前那种沿用了上百年的老办法、老范式去做研究。
但反过来,如果最强版本的AI能力猜想在未来不幸被证明是真的,尤其是当我们的数学共同体依然盲目地把“尽可能多地解决未解问题”作为最优先、甚至唯一的学术优化指标时,那么数学界现有的价值取向和工作文化就将面临系统性的崩溃,很难再维持下去了。
在过去几年里,关于AI到底能不能做数学研究的争论在互联网和学术界一直非常激烈。陶哲轩在很多讲座、文章和社交平台上也曾深度参与过讨论。但他非常冷静且理性地指出,目前虽然有大量的证据支持或者反对这一猜想,但其中绝大多数数据都缺乏科学的对照和控制。目前公开的大多数关于AI证明数学题的优异成果,往往受到严重的报道偏差(Reporting Bias: 倾向于只宣传成功案例而隐藏失败过程的选择性倾向)和非学术商业动机的影响。比如在宣传中,哪些成功的惊艳结果被无限放大,而背后的算力成本、人工提示词微调、参数过滤等变量却被刻意隐去。这其中存在太多的公关和技术操作空间。
为了摆脱这种公关泡沫,陶哲轩在演讲中特意引用了一项最新的独立且客观的评估数据——First Proof挑战赛(First Proof Challenge: 一项针对前沿人工智能在数学研究级任务上表现的科学评测项目)。这是一个旨在对前沿AI模型与工具链的真实能力进行科学、受控、独立评估的项目。每一期测试都会包含十道由专家组全新设计、涵盖不同前沿数学领域的、从未在互联网上公开过的研究级数学难题。
在2026年5月28日,第二批测试题目在高度受控的科学实验条件下,针对四套不同的AI工具链进行了集中盲测。结果由多位数学界的同行专家分别从“解答的正确性”和“论文的写作质量”两个维度进行独立评审。
测试的结果令人震惊:在十道前沿难题中,有七道被至少一支AI团队及其工具链做到了可以直接发表的学术水准。而令人更加瞩目的是,每道题所消耗的实际算力花费在10美元到1000美元之间。目前,更多批次的评测计划正在紧锣密鼓地推进中。这一具有说服力的数据点究竟意味着什么,陶哲轩并没有直接下结论,而是选择将思考的权力留给在座的所有听众。
在交代完这一客观背景之后,陶哲轩做出了一个极具智慧的方法论抉择。他宣布,在接下来的报告中,他将不再纠结于AI技术的演进速度,而是直接将整场演讲建立在一个强有力的工作假设(Working Hypothesis: 假定某种强AI能力猜想成立的条件框架)之上:
假定在不久的将来,某种强版本的AI能力猜想是成立的。也就是说,AI工具将能够以极低的成本、极高且合理的成功率、较少的人类监督,高效地批量完成相当一部分研究级数学任务。
陶哲轩对此进行了解释,他并不是在强迫听众接受这个工作假设,而是在进行一种条件分析。这好比是一个思想实验。因为无论这个工作假设在未来的某一天是否会成真,只要我们接受这个假设,一个被数学界长期忽视、掩盖在繁荣学术产出之下的根本性问题就会不可避免地浮出水面:
数学共同体和数学研究这项人类共同的事业,其真正的价值终点和底层目标到底是什么?
古德哈特定律的扭曲与解题流程的异化风险
在过去,关于数学研究价值的讨论,往往被视作无关痛痒的虚务,通常被扔给搞历史或哲学的人文学家去关心。数学家们则默认只要埋头攻克一个个技术难关、证明一条条定理,就是在为人类做贡献。陶哲轩警告道,如果上述工作假设一旦成立,这种逃避根本反思的奢侈特权就不复存在了。
在追问“数学研究到底图什么”时,陶哲轩在幻灯片上列举了一系列我们习以为常的理由:解决未解决的难题、建立和发展新的理论体系与计算技巧、理解我们所处的自然世界、建设健康活跃的数学共同体、培养和输送下一代数学研究人才、为整个人类共享的知识网络添砖加瓦、以及创造具备永恒审美价值的精神财富。
在传统的数学范式下,这些林林总总的多元目标之间呈现出强烈的正相关关系。这是一种健康的良性循环。如果一个数学家在一个方向上取得了突破,证明了一道极为困难的世纪难题,他往往在证明的过程中发展出了全新的理论体系,并在带研究生的过程中培养了后辈人才,同时为人类知识库做出了贡献,其证明过程本身还往往充满了数学独特的简洁美。正因为这些目标高度绑定,数学界在过去的百年里,可以偷懒地选择其中一两个最显性的指标——例如“解决了多少难题”、“发表了多少论文”来作为整个学科发展的代理指标,并默认其他目标也会自然实现。
然而,陶哲轩在这里抛出了社会科学和经济学中著名的古德哈特定律(Goodhart's Law: 指一旦某项指标被选为优化的单一目标,它就不再是一个好的指标)。当大语言模型和生成式AI技术被引入数学研究时,由于AI工具本身具有一种缺乏根基(Ungrounded: 指模型仅通过模式匹配生成看似正确的符号,而缺乏对物理世界或抽象概念逻辑闭环的真正理解)的特性,加之AI开发商在商业利益驱动下对特定跑分指标的疯狂公关,使得AI系统在面对古德哈特效应时表现得极其脆弱。
在强大的AI算法过度优化下,原本在人类数学家身上和谐统一的多个学术目标,将会出现剧烈的撕裂与分化。解决未解难题、做奥数题、做以匈牙利数学家保罗·埃尔德什命名的埃尔德什问题、发展前沿理论、人才培养、共同体建设以及创造审美价值,这些原本指向同一个终点的矢量,在AI的强力干预下会各走各的路,甚至彼此冲突。
为了将这个抽象的逻辑分化说深说透,陶哲轩在接下来的演讲中,特意抽离了解题这一具体的数学研究环节,来做了一次经典的解构分析。他一再强调,数学并不等同于解题,理论体系的建设是另一个同样重要且更需要深度分析的维度。他之所以选择“解题”作为解构切片,仅仅是因为这个环节对指标度量的反馈最为直接,是AI技术最容易攻克和冲击的“桥头堡”。
让我们沿着陶哲轩的逻辑推演:在最原始的数学范式下,数学界设定的核心目标是“尽可能多地解决那些未被解决的数学难题”。这相当于在优化一个从“未解决问题(Unsolved Problem)”到“解答(Answer)”的线性流程,其间的关键驱动力是“证明生成(Proof Generation)”。
但在AI诞生之前,数学界就已经尝到过盲目追求该指标的苦头。例如在黎曼猜想等重大难题周围,从来都不缺所谓的“终极解答”。每天都有成百上千篇声称自己彻底证明了黎曼猜想的论文被上传到网络上。这其中99%以上的论文不仅毫无学术价值,而且存在各种各样的逻辑漏洞与计算错误。因此,为了维持学术共同体的运转,目标必须升级为“在解决问题的同时,必须验证其正确性”。
于是,整个流程被改写为:未解决问题通过“证明生成”变成“未验证的解答”,再通过人类专家的“证明验证(Proof Verification)”最终转化为“已验证的解答”。
近年来,随着AI自动形式化技术与诸如证明助手(Proof Assistant: 基于逻辑系统自动检验定理证明正确性的交互式软件,如Lean、Rocq、HOL等)的迅猛发展,证明生成与形式化验证这两个环节的速度已经被明显拉快。在工作假设成立的前提下,这种机器辅助的验证速度还会呈现指数级的爆发。但随之而来的,是一个让所有数学家感到背脊发凉的逻辑悖论:
如果AI在几毫秒内生成了一份长达上万页、通过了机器形式化验证、但其复杂度和符号量超出人类大脑认知极限的正确证明,人类该如何面对它?
这并不是科幻小说中的狂想。在现实中,这种迹象已经在局部蔓延。在像埃尔德什问题库这样的在线平台中,已经堆积了几十份由各种算法和AI工具生成的解答提交。这些提交根据形式化语法检验,大概率是完全正确的。但是,目前没有任何一位人类专家愿意贡献自己宝贵的时间,去通读这些晦涩的代码与符号,为它们背书。更尴尬的是,连利用AI生成并提交这些证明的研究人员自己都公开承认,他们本人完全没有能力去阅读和验证这些证明。
基于这一尖锐的现实,陶哲轩向全场抛出了一个直击灵魂的问题:
“如果未来数学界出现这样一种景象——一份通过了机器严苛验证的重大数学成果,却没有任何一个活生生的人类能够真正理解并清晰地解释它。如果那一天到来,这个所谓的正确证明,对于人类的知识大厦和文明而言,究竟意味着什么?”
消失的认知摩擦力与瑟斯顿共识的坚守
为了不让数学成为冰冷的机器自嗨,陶哲轩指出,我们的流程目标必须再次升级。我们不仅要确保解答正确、通过验证,更要确保其结果能够被数学共同体清晰地理解与交流。因此,流程中必须强行插入一个环节——证明阐述(Proof Exposition: 将机器或高度专业化的符号证明转化为人类易于理解、掌握并传授的自然语言表述过程)。
那么,目前的生成式人工智能在证明阐述这一环节的表现如何呢?陶哲轩用了一个充满英式幽默的词来评价:参差不齐。
一方面,在排版、拼写、LaTeX排版美观度、甚至语法语气的丝滑度上,AI写出的文稿几乎是完美无瑕的,甚至有些“完美得过头了”。但另一方面,AI在阐述论证时表现得非常机械和呆板。它经常会在一些极其平庸、琐碎的常规计算步骤上花费大量笔墨进行铺陈;而对于整篇证明中真正具有跨时代意义、最闪光、最需要直觉突破的核心逻辑跃迁,AI却往往一笔带过,甚至写得含混不清。它无法站在科学史的全局高度,去向读者指出这篇证明与过去几十年文献的深刻关联,更无法提炼出一个高屋建瓴的“全局概览”,告诉人类学者这个证明的精髓究竟在哪里。
更重要的是,证明阐述是一个极为主观的优化目标,这与是非对错的二元验证截然不同。哪怕未来AI在阐述能力上大踏步前进,陶哲轩依然敏锐地指出,过度光滑的AI阐述本身也是一种隐形陷阱。
在人类学者的阅读习惯中,那些最具挑战性、最难跨越的逻辑断层,往往会在作者的行文中留下天然的“认知摩擦力”。这种摩擦力可能是作者在此处不厌其烦地变换角度解释,可能是文字中流露出的犹豫与挣扎,也可能是特意做出的警示标记。这些不完美的摩擦痕迹,其实是在向读者的脑波发出信号:在此处请放慢阅读速度,注意,这里是关键的逻辑深渊!
然而,一个被AI利用文字算法过度润色和抛光的证明文稿,往往会把这些天然的摩擦痕迹全部磨平。读者在阅读时感觉流畅无比、毫无阻碍,但当他合上书本时,却发现脑子里一片空白,根本没有捕捉到任何实质性的数学思想。在这个意义上,人类在写作中留下的那些逻辑瑕疵与笨拙挣扎的痕迹,反而是认知传递过程中不可或缺的导航标识。
在此,陶哲轩深情地引用了菲尔兹奖得主威廉·瑟斯顿(William Thurston)在1994年发表的学术名篇《论数学中的证明与进展》中的一段话:
“我们并不是在努力完成某种定义、定理和证明的生产指标。真正衡量我们工作是否成功的标准,在于我们所做的事有没有让人们能够更清楚、更有效地理解和思考数学。”
在人工智能浪潮席卷学术界的今天,瑟斯顿的这段话显得震耳欲聋。如果一份证明仅仅是正确的、易读的,这远远不够。它必须能够被人类共同体所消化和吸收(Digestion and Assimilation),能够被其他年轻的数学家拆解为工具,应用到他们各自的子领域中去。
在传统的科研中,人类作者通过在论文或报告中真诚地剖析自己的解题心路历程——自己是如何走进死胡同的、如何经历失败的、又是如何在一瞬间灵光乍现的——来帮助同行消化成果。但目前的AI模型在推理过程上高度不透明。如果你向它追问某一个奇妙证明的灵感来源,它给出的解释往往是根据统计概率“事后合理化”的粉饰,并不是它真实生成这个符号序列时的逻辑轨迹。对于那些商业公司闭源的专有大模型,其推理路径更是一团漆黑的黑盒。
这就逼着我们的流程链条必须再次向右延伸:已验证且阐述清晰的解答,必须经历证明发表(Proof Publication)与同行评审的洗礼,变成被共同体普遍接受的解答,再经过极其漫长的“证明消化”,最终抵达整条价值链的终点——典范化(Canonicalization: 将零散、复杂的学术证明通过长期的教学、重构与筛选,最终沉淀为教科书中的经典标准理论体系的过程)。
证明消化不良与莱顿宣言的防线
如果将这个完整的解题价值链条绘制出来,我们会清晰地看到:每一层链条的递进,都意味着在单纯的“正确性”之上,叠加上了更深层次的人类认知与文化价值属性。然而,陶哲轩极其严厉地警告道,一旦前述的工作假设在未来成真,而数学共同体的政策、文化与价值评价体系又未能及时做出调整,这整条长链条的每一个衔接处都将发生严重的系统性拥堵。他将这种由于上下游处理速率不匹配导致的崩溃状态称为证明消化不良,或者借用电子工程学里的专业术语——阻抗不匹配(Impedance Mismatch: 输入端的高速率与输出端的低承载能力之间的矛盾导致能量耗散与阻塞)。
具体而言,在这种阻抗不匹配的极端学术环境下:
- 证明生成环节在AI加持下超速运转,导致无数“未验证解答”疯狂堆积,远远超出了形式体验证和人类检查的承载力;
- 哪怕通过了机器验证,无数冗长复杂的代码化证明依然在那里排着长队,急切地等待着能翻译成人类看得懂的自然语言文本;
- 即使这些论文既正确又好读,其庞大的数量也会在瞬间挤兑并压垮现有的学术同行评审机制。审稿人将不堪重负;
- 退一万步讲,即便论文成功发表,由于人类的精力、寿命和脑容量是有限的,共同体也根本没有能力去消化和讨论这些成果,更遑论将其重新阐述、提炼并编纂进教科书,使之沉淀为人类的“典范知识”。
陶哲轩一针见血地指出,这种学术消化不良的危机并不是在AI时代才突然降临的。其实在AI大规模介入之前,学术界因“唯论文论(KPI)”导致的论文发表通胀、共同体交流效率下降等问题就已经初露端倪。AI的发展,只是将这层长期被掩盖的系统性矛盾以一种极其戏剧化、甚至带有毁灭性的方式给放大了。
为了在海量证明涌现的时代为数学界的价值坚守防线,陶哲轩在演讲中重点提到了近期在数学界达成的《莱顿人工智能与数学宣言》(Leiden Declaration on AI and Mathematics: 旨在规范人工智能在数学研究中应用边界与伦理的宣言)。这份由多位顶尖学者联合起草的宣言,试图为AI时代的科研伦理锚定一个稳固的基准。在演讲中,陶哲轩详细展示了宣言针对个人数学家提出的五条核心行动纲领,并做出了精辟的个人点评:
-
工具使用的公开披露与FAIR原则的践行 建议所有数学家在论文和日常科研中,坦诚且详尽地披露自己所使用的所有自动化与AI工具(包括大语言模型、定理证明助手、代数计算软件等)。在精神上,应当全面看齐联合国教科文组织关于“开放科学”的倡议以及FAIR原则(FAIR Principles: 可发现 Findable、可访问 Accessible、可互操作 Interoperable、可重用 Reusable)。当作为同行评审人时,若使用了AI辅助审稿,也必须进行公开披露,并为自己提交的最终评审结论负全部学术责任。陶哲轩特别指出,数学界要极力避免一种最坏的行业风气:即学者们为了提升产出暗中大量使用AI,却因为害怕被主流学术圈指责而选择隐瞒。这种偷偷摸摸的非规范化行为一旦成为行业潜规则,将会彻底腐蚀整个学术共同体的信任基石。
-
积极减轻审稿负担与学术指标的价值转移 AI的批量创作会极大地增加审稿负担。因此,作者有义务在投稿时主动提供形式化证明文件、提供精确到行号的文献引用,以此降低同行审稿人的信息校验难度。基于此,陶哲轩给出了一个颠覆性的行业发展建议:数学界应当主动降低对“证明生成速度”以及“谁是第一个冲过终点线解出题目的人”的狂热崇拜,转而将学术声誉和评价资源,大力向“证明的消化、阐述、科普与经典化”环节倾斜。在AI可以低成本批量制造证明的时代,单纯做“解题第一人”的含金量将面临贬值,而能够将复杂真理讲明白、帮助共同体真正吸收知识的“布道者”与“整理者”,其价值将迎来大幅上升。
-
保留关于正确性的终极人类责任 宣言重申,当自动化或人工智能技术被引入学术研究时,无论AI工具在写作中多么天花乱坠,该项研究中所有逻辑推理的正确性、完备性、以及引用前人工作的准确性,其终极学术责任始终且完全由人类作者个人承担。AI出错不能作为人类甩锅的理由。
-
认真对待学术署名与致谢 鉴于目前的AI模型在自动溯源、合理致谢前人灵感方面存在天生的算法缺陷,极易发生“学术剽窃”或“忽略关键文献”的现象,人类作者必须花费极大的精力去追溯那些让新证明成为可能的真正思想源头。陶哲轩在此给出了一个非常质朴却极具杀伤力的判断标准:
“如果一位论文的作者,无法在没有AI辅助的情况下,向同行专家做一场清晰、严谨、具备专业水准的学术报告,去把自己的证明过程和思想脉络讲清楚,那么这项研究成果就不应该被允许发表。”
如果你自己都讲不明白,你怎么证明你真的理解并拥有了这项知识?
-
积极参与关于AI的公共讨论 由于评估前沿数学成果的难度和深度需要极高的专业门槛,外行和科技记者极易被公关软文误导。因此,数学家有义务站出来,积极参与社会公共讨论,向大众客观阐明AI辅助数学的来龙去脉与真实边界,并主动与面临类似冲击的其他学科(如创意设计、法律等)的学者和从业者建立广泛的同盟与互助网络。
在整场精彩演讲的尾声,陶哲轩以一位智者的宽广视野提醒所有听众,AI对数学的解构与重塑绝不仅限于解题这一个侧面。从教学的考核方式、研究生的培养范式、高校的招聘标准、科研基金的评审机制、到科普大众的社会责任,每一个角落都在经历着AI潮水的冲刷。
在教育和人才培养的某些核心地带,我们甚至应该像保护圣地一样突出人类的肉身作用,严格甚至强制限制AI工具的使用。因为在数学学习中,那种面对难题抓耳挠腮、百思不得其解的“挣扎与痛苦过程”,本身就是人类大脑皮层建立神经元链接、培养抽象思维能力的唯一途径。任何试图用AI进行“无痛学习”的走捷径行为,最终换来的只能是人类智力的退化。
数学界不能被动地躺在沙滩上,等待硅谷的商业科技巨头来为自己制定规则。数学共同体必须主动出击,用数学家特有的严谨与团结,去定义AI在学术界使用的最佳实践指南,并积极搭建诸如Mathlib(数学形式化库)、Mathematical Discourse(数学话语项目)、SAIR竞赛平台等一系列属于科学界自己的新型数字基础设施。
正如陶哲轩在演讲最后那句力拔千钧的宣告:
“整个数学共同体现在需要坐下来,坦诚地讨论AI能力的问题,也坦诚地讨论我们数学界自己的目标与价值。在这个变革的时代,回避这场真诚的对话,才是数学界未来最大的风险。”
📌 文中提及的人物和组织
产品/模型: Lean, Rocq, HOL, Mathlib
媒体/书籍: 论数学中的证明与进展, 莱顿人工智能与数学宣言