北大AI4Math董彬、刘若川等多位学者合作：《数学的一种现代重构——韦伊猜想的形式化证明与阐述》2026-11-11
★置顶zzllrr小乐公众号，追踪《小乐数学科普》系列报道，参与数学 vs AI投票！
坚持不炒作的数学与AI报道，投稿信箱zzllrr@gmail.com
数学的一种现代重构
韦伊猜想的形式化证明与阐述
日期：2026-11-11
作者：（以下按姓氏字母排序）
董彬、关乃粼、姜杰东、刘若川、Christian Merten、潘翔宇、史庭潇、吴彬、解云舟（Edison Xie）、杨威
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
摘要
（本文是发表于Xena项目（凯文·巴扎德Kevin Buzzard主持）博文《数学的一种现代重构》的扩充版本）本文介绍韦伊猜想项目：一个原型系统，它把数学内容组织成多层自然语言讲义，并和可机器核验的形式化证明关联在一起。项目的核心目标，是把高层数学思想与严谨、可核验的证明融为一体，同时展示人类与AI如何在不同粒度的讲解层、形式化层协同工作。项目网站：https://weil-conjectures.merten.dev
1 引言
我们数学家应当投入更多精力去传递数学思想。要做到这一点，不能只传播定义、定理与证明，更要传递我们思考问题的方式。
——威廉·P·瑟斯顿，《论数学中的证明与进步》（1994）
自数学研究诞生之初，人们就一直在梳理、传递数学思想。数学家会精心挑选贴合直觉的名称与符号，以求增进理解。在漫长历史中，数学成果的载体一直是线性文本：一篇由定义、定理、证明构成的论文。但现代数学里，证明以及背后思想的规模、复杂度飞速膨胀，撰写与阅读证明都要耗费越来越大的精力。
人们已经做出诸多尝试，对数学内容重新整理、组织，以此改善理解效果。布尔巴基学派[6]编写了一套教科书，以自洽统一的体系搭建数学理论。传统教科书大多只能采用线性结构，而网页支持更灵活的交互式浏览。《Stacks项目》[21]是一部代数几何线上教科书，书中定理、定义都打上标签、互相链接，按主题层级化组织，它本身并不适合从头到尾线性阅读。Kerodon[15]是高阶范畴论领域的同类网站。Kedlaya的线上讲义[14]则是p进上同调方向的又一例。
还有另外两个值得一提的项目。nLab[20]是协作式维基站点，侧重思想与抽象视角。它并不按照证明的逻辑结构做层级编排，而是围绕概念及其相互关系组织内容。另一方面，Mathlib[19]是一套统一的形式化数学库，按数学领域分类，保存了证明的全部细节。
1.1 数学的两个层面
上面提到的后两个范例，代表了数学当中两种同等不可或缺的组成部分。一方面是类比、口号式概括、实例，甚至是启发式的非严格论述，这些承载着数学理解；另一方面是严谨详尽的证明，把模糊的想法打磨、落实为可靠的论证。我们往往用第一种方式思考，却用第二种方式落笔成文。
举一个概率论的例子：若随机变量 X、Y相互独立，则
Var(X+Y)=Var(X)+Var(Y)
写出完全严谨的证明并不困难。但我们推导、使用这条公式时，指引我们的是勾股定理的直观图像。
我们认为，数学理解二者缺一不可：高层思想与严谨证明。口号、类比可以说明一套证明策略为什么有可能成立；但只要还没有转化为完整的证明，它就仅仅只是策略。只靠口号写成的文本如同踏云而行，或许能支撑你往前走一两步，之后便会坠落。反过来，仅有一份细节完备的证明，也无法让人把握整体图景。这也正是阅读AI生成的证明会如此煎熬的原因：每一步推导都正确，但你完全体会不到背后的思考动机。
阐释高层图景有点像讲故事。但把叙事性内容融入专业数学文本，现实中困难重重。筛选、构造有代表性的例子需要耗费精力。更麻烦的是，口号与类比很容易出错；不少人宁可干脆不写，也不愿写下有可能出错的内容。还有很多证明，概念层面思路很清晰，难点全部来自技术性细节。研究者攻克技术难关、得到严谨证明之后，这部分成果就得以发表。但没有人会另外发表这样一份文字：“这是我最初想到的论证，这是它哪里行不通，这里是我做的修正。”这也是为什么和数学家交流，收获往往比读论文更大。
不过最近情况有所好转。大语言模型与智能体已经非常擅长推导证明、补全繁琐的细节。形式化技术依靠证明助手校验每一步，保证所有细节准确无误。同时大语言模型的自动形式化能力也在快速进步，减少人工形式化的工作量。我们如今有机会让AI减轻整理数学内容的负担（而不是像现在这样反而加重负担），把数学的两个层面融合到一处，彼此关联对照。
1.2 我们搭建的成果
上文所说的高层构想与严谨证明，是数学表述的两端。二者之间可以搭建一层层不断细化的中间层。我们希望把这套逐步细化的过程直接呈现给读者，让你既能看清证明的整体脉络，也可以一路下钻，看到完整细节。
以韦伊猜想这类大型证明为例：最顶层就是前面所说的类比、概念对照字典、整体策略。如果能构造一套韦伊上同调理论，猜想就可以直接得证，ℓ进上同调就是其中一例。接下来再把论证展开，细化每一步，得到粒度更细的证明。韦伊上同调的核心性质，可以由f^!函子的计算，以及(pro-)étale site（(准)艾达尔景，site：景、广拓扑）上六函子的一般形式体系推导而来。就这样，口号式的顶层论述，一步步细化为可以逐点校验的内容。原本模糊的叙事，由此变成完全严谨的证明；过程之中会遇到各类技术障碍，也一并得到解决。
我们的站点 https://weil-conjectures.merten.dev 是一个原型，尝试用这套范式整理、完整呈现韦伊猜想的证明。这套成果分为两部分：第一部分是多层级网页文本，一份具备多种粒度的证明，由顶层论述不断向下细化得到，读者可以任选自己想要的细节深度切入阅读。第二部分是配套的形式化产物：最底层的每一步都经过证明助手校验，整套证明可以由机器核验。
这套分层结构，也定义了人类与AI的分工边界。由人类来讨论、确定整体证明路线[1]，敲定底层关键定义与数学框架。论证向下细化时，大语言模型补全人类已经定好的关键定理的细节，人类负责审阅、调整。到最底层，AI接收人类可读、但尚未完全严谨的文本，自行展开全部细碎步骤，再通过形式化完成校验。也就是说：由人类的数学判断力定下路线，AI负责把细节一路推进到机器可核验的完整证明。
我们投入人力完成导出范畴、(pro-)étale site六函子这套主体框架的形式化，参考了Riou关于导出范畴与导出函子形式化的工作[17]，同时分享了处理内核性能问题的实践经验[2]。详尽证明的形式化工作，则全部交给自动形式化工具。最底层人类完全可以不去阅读。读者阅读适配自己的层级即可，文本经过凝练、容易理解，足以展示策略如何落地；读者同时知道下层已经经过校验，证明本身可靠。
网站同时展示讲义与形式化内容，附带一张关系图，同时呈现细化关系与证明依赖。高层节点可以点开，展开对应的下层细化节点，证明依赖用箭头绘制。每一个节点对应一篇页面：高层节点承载叙事，底层节点是严谨证明，并且链接对应的形式化代码。读者可以任选细节深度切入，自由切换通俗讲解和机器核验证明；网页内容也可以导出为传统线性排版讲义。
能实现这套方案，完全得益于近年大语言模型与智能体的进步：模型的数学证明能力用来生成分层讲义，自动形式化能力完成形式核验，代码能力搭建网页展示界面。这三块工作里，人类只确定高层策略与目标，AI负责实现具体细节。依靠这种人机协作，我们得以实现数学的现代重构。
项目现状：
讲义网站已经上线，我们已经完成韦伊猜想的全套形式化。该形式化成果已经提交至https://lean-lang.org/eval/problems/weil_conjectures/ 并通过验收。但项目仍在持续推进。我们选择优先追求速度，在自动形式化快速迭代的背景下，对所有细节做自动形式化，没有施加高强度质量管控。我们计划持续优化网站、检查并改善代码质量，并且把核心的六函子框架贡献到Mathlib库。
我们的形式化工作基于Mathlib的代数几何库[19]，该库最早由Buzzard、Hughes、Lau、Livingston[8]发起，后续由众多贡献者拓展，包括Angdinata、Buzzard、Commelin、Merten、Morrison、Riou、Xu、Yang、Zhang。本工作还依赖Riou的导出范畴库[17]，以及Jiang、Merten实现的(pro-)étale site与ℓ进上同调[12]；后者建立在Merten实现、已经并入Mathlib的étale site形式化基础之上[16]。代数与算术几何领域其他相关形式化项目包括椭圆曲线相关工作[1,18]，以及费马大定理[2,7]、Stacks项目及其在Axiom Math韦伊猜想上的应用[3,4]这类大型项目，它们的数学内容和我们的工作有部分重叠。
韦伊猜想这套成果的构建分为三个阶段：首先选定证明路线，写成多层讲义；接着把讲义中的对象和论证落实为形式化代码；最后通过网站把各个层级以及它们之间的对应关系呈现给读者。下文依次介绍这三个阶段。
2 自然语言讲义
整个流程从自然语言讲义开始。韦伊猜想有若干主流证明路线，比如韦伊第一证明[9]、韦伊第二证明[10]、Kedlaya的p进证明[13]；我们的讲义选用韦伊第二证明。路线确定之后，我们再决定如何行文，兼顾整体思路与必要细节。路线选择决定了讲义需要引入哪些工具、突出哪些核心思想，也为后续形式化定下基本方向。
2.1 证明路线的选择
第一条指导原则：
只要具备形式化可行性，我们优先选择表述成熟、且能尽可能复用已有形式化成果的路线。
例如韦伊猜想，我们选择ℓ进路线而非p进路线：(pro-)étale site已经在Mathlib中可用[19]，并且它和艾达尔上同调的比较定理已经在(pro-)étale 仓库完成形式化[12]；而p进路线需要刚性上同调，要单独搭建一套底层基础。对于可构造层的导出范畴，我们选用Bhatt–Scholze的(pro-)étale 拓扑[5]，以及Hemo–Richarz–Scholbach的凝聚数学框架[11]，而不是SGA里经典的adic系统。迹公式我们选用Lefschetz–Verdier配对的证法，光滑纯净性选用形变到正规锥的证法，原因是它们更适配抽象六函子体系。
第二条原则：
避开形式化难度过高、技术过于繁琐的路线。
例如本项目全程不使用高阶范畴；光滑基变换定理、Künneth公式直接采用Stacks项目的证明，以此规避局部无环性、近邻/消失循环的复杂工具；我们尽量少用代数群，在研究光滑韦伊层的几何单值群时不使用类域论。
2.2 讲义的撰写
证明路线确定之后，我们使用GPT-6.1-sol，以最终主定理和关键中间定理为骨架组织讲义，向读者展示论证主线，同时给后续形式化给出清晰的中间目标。我们先让大模型生成粗略大纲，厘清核心组成部分。我们曾经尝试递归式扩充大纲，直到每一个叶子节点都对应Mathlib里已有的内容，写出和形式化证明同等详尽的自然语言文本。当时我们还不信任大模型直接生成Lean代码，以为所有细节都必须预先写死。但实践证明这个方案速度极慢，而且没有明确的终止条件，就像一个不断生成sorry（占位证明）、看不到终点的形式化项目。文本长度膨胀到原来十倍，细节多到人类无法阅读，因此这个方案基本不可用。
当然，“向下对接Mathlib”这个思路并非完全不可行。关键在于：对于Stacks项目这类已有成熟详细论述的内容，可以跳过一大块细节。固定主证明策略，下层证明只做精简表述，就形成讲义骨架。
骨架搭建完成后，我们把证明路线写成传递数学理解的文本。数学写作能力本身离不开数学理解。正式写作前，我们让大模型先理解整体结构和每一条论证，保证后续润色只改动表达形式，不改变数学实质。因此主体写作阶段我们从GPT切换到Claude Opus 5.5。只需要给出记号、排版的基础指引，模型就能产出质量尚可的文本；它可以研读大量优秀论文，学习数学家的行文风格——这种风格本身很难用抽象规则描述。
人类精力有限，因此我们让大模型模拟对应背景的读者，主动识别论证薄弱点。对于还不够完善的部分，用正反示例引导写作，效果远好于抽象原则。必要时由人类作者直接修改文本、补充实例。此外，人类想要传递的独特思想，必须有意识地嵌入这套工作流。人类决定哪里展开、哪里省略细节，本身就是数学判断与取舍的体现。
3 形式化
讲义给读者提供清晰可懂的证明路线，而形式化工作的目标是产出和讲义对齐的形式化代码，反过来验证讲义本身的正确性。最终生成的形式化代码约550万行，提交Lean评测时精简至280万行。整套自动形式化的订阅成本大约7万至8万美元。
基础设施方面，我们使用https://github.com/chrisflav/orchestra和https://github.com/frenzymath/SHEAF。两套调度框架的智能体可以通过共享平台互通，人类和机器人协同工作。本项目也是在大规模场景下测试Mathlib部分模块的一次探索，重点是导出范畴相关内容，我们也为此向Mathlib提交了改进PR[注]。
3.1 人工形式化
想要做到讲义和形式化对齐、互相校验，在搭建证明骨架、更关键的是设计命题所需定义时，人工介入尤为重要。相比其他环节，这部分需要我们投入最多精力。比如项目早期，六函子的整体设计、六函子作用的导出范畴还没有敲定。如果不在底层做人工决策，智能体很容易生成一套和讲义完全错位的定义。
我们还要把数学文献里常常默认省略的大量细节显式写出来，例如宇宙层级约束、歧义记号。这些省略不仅会误导智能体，留到后期处理还会严重拖慢效率。
除了会造成形式化错误的问题，选取合适的一般性程度也会影响效率。项目早期我们花了大量时间，确定构造的一般性范围。从中总结出两条实用原则：
如果一个构造有多个具体应用场景，可以先实现具体情形，等到打磨整套体系时再统一抽象；
在设计统一抽象构造时，尽早用它预期的具体应用做测试，保证抽象框架确实能容纳这些场景。
我们在过程中确实人工形式化了所有里程碑结论，但经验表明：人工主导的形式化最核心的产出，其实是陈述证明骨架所需的整套定义。骨架本身原则上可以交给智能体完成。
3.2 自动形式化
基础定义、目标命题就位之后，工作重心变为调度智能体，沿着既定路线补全证明。我们使用两套互补框架：Orchestra与SHEAF。Orchestra是一个常驻调度程序，用来管理和运行智能体。项目初期，智能体通过issue看板协同。这种中转方式虽然方便人类查看进度，但拖慢了智能体，于是我们改为设置一个主智能体，直接调用Orchestra API派发任务。我们在Zulip实例上和主智能体沟通，接收进度、下达调整指令。
SHEAF在项目中途加入，此时目标命题已经写完、人工蓝图已经定稿，并且已经有大量Lean代码。SHEAF选取若干上游目标作为终点，分批推进任务，每一批任务都经历SHEAF的三阶段流程：
自顶向下拆解目标，拆成自然语言命题节点，每个节点绑定蓝图或者文献出处；
自底向上，基于Mathlib和已有代码，为这些节点写出Lean命题；
再次自顶向下证明sorry占位节点，这个过程中经常找到更短的证明路径，绕过下层节点，被绕过的节点直接删除。
调度器按阶段顺序派发任务，但允许跨阶段并行：后序阶段的就绪任务可以在前序阶段完全结束前启动。整个过程一共生成约54000个节点，其中超过一半（约28600个）最终被删除。
这个过程中我们必须警惕路线跑偏。有一次智能体完全自主运行，脱离了人工审定的蓝图，改用∞-范畴搭建六函子，引入整套证明完全不需要的复杂体系。在人类引导下，我们回到蓝图原定路线，删除了近2000个多余节点。这说明至少在本项目中，持续的数学指导，是自动化形式化流水线必不可少的补充。
因为SHEAF和Orchestra操作同一批代码模块，很容易出现重复劳动。两套系统的管理机器人直接在Zulip上协商分工。分工没有固定规则，随任务类型变化：Orchestra更适合在主分支上零散补sorry；SHEAF更适合一次性完成一整块sorry，这类模块通常需要先新增大量定义和引理，刚好匹配SHEAF的工作流程。项目全程，人类专家也参与机器人之间的大量讨论，解答诸多问题，极大支撑了AI驱动的形式化部分。
3.3 性能问题
编译效率是一大难点，在本项目大量使用导出范畴的场景下尤为突出。表现为内核类型检查开销极高，编译耗时极长、内存占用巨大，甚至超时。我们从基变换态射超时这一案例出发，排查了大量情形，最终形成一套诊断、修复这类问题的系统性方案（相关文档：https://weil-conjectures.merten.dev/#/blog/lessons-from-formalization，以及给智能体使用的诊断手册：https://weil-conjectures.merten.dev/blog/files/lean4_performance_diagnostic_and_remediation_guide.md）。
但目前我们的理解大多还停留在个案层面。我们已经对遇到的特定问题有有效的修复手段，却还没有搞清楚：为什么包含导出范畴的开发，在Mathlib里总是“坑很多”。背后底层原因仍是开放问题。
4 网站呈现
分层讲义与对齐的形式化代码共同构成成果，但这套数学结构本身还需要清晰的展示。这就是蓝图网站的意义：把整套结构铺开，让读者可以在不同细节粒度下沿着同一条证明路线阅读。
4.1 网站结构
https://weil-conjectures.merten.dev/ 主要包含三块：关系图、文档、进度。
关系图页面：
展示项目节点图，包含自然语言讲义里所有声明，以及形式化中用到的重要命题。图里每个声明都绑定对应的Lean名称，方便核验形式化是否遵循讲义路线、证明的命题是否一致。节点之间的箭头代表章节、声明之间的依赖引用关系。
文档页面：
存放自然语言讲义，目录清晰，借鉴了Stacks项目网站的设计思路。文档保留讲义全部上下文，按原有顺序分层排版；在更细的层级里，记录细化后的定义与定理，展示这些内容送入Lean形式化时的具体形态。
进度页面：
记录形式化推进节奏。后台持续监控形式化项目里和讲义声明对应的Lean名称，按状态分类；保存形式化历史，也可以查看项目统计数据。
除此之外还有博客板块，记录项目过程中积累的经验与技巧。
4.2 网站特性
关系图、文档、进度页从不同侧面展示成果。网站设计有两个核心目标：一是保证讲义和形式化的一致性，让读者可以通过形式化结果核验讲义的正确性与完备性；二是保证可复用，方便其他数学项目采用这套展示范式。
一致性方面：
我们投入大量精力核对Lean声明和讲义表述。这件事并不简单，很多自然语言陈述在形式化时会被打散、重组。但这项工作是值得的：网站忠实记录讲义里最重要定义、定理的精确陈述，反过来指导形式化证明，并且可以同步讲义和形式化两边的改动。
可复用性方面：
网站代码拆成两个GitHub仓库：蓝图基础框架https://github.com/chrisflav/blueprint，以及韦伊猜想项目专属蓝图仓库https://github.com/formal-arithmetic-geometry/weil-conjectures-blueprint。关系图、文档页的大部分设计不绑定韦伊猜想，支持无损导入新的自然语言讲义。同时可以自定义开场页面、图标等装饰元素，页面布局、新增统计项、附加文件都有很高自由度。
5 展望
目前，讲义、形式化、网站展示已经整合为一个自洽的整体。想要把这套范式推广到更多数学课题，还有两件事需要推进：一是让这套方案更容易泛化；二是降低对人工经验的依赖。以当前围绕主定理的成果为基础，同时改进这两点，我们可以逐步拓展，对接更大的数学文库。
5.1 形式化代码质量
形式化社区已经有多种提升代码质量的手段，从静态检查工具到人工代码评审。但对于大规模AI生成的形式化代码，我们仍然缺少一套清晰、可规模化的质量提升方案。
前文讨论的内核性能优化，就是提升形式化质量的一次具体尝试，也为故障诊断积累了系统化经验。代码质量直接决定这些成果能不能被后续项目复用。一个优秀的形式化项目，应当产出可复用的数学基础设施，让后续工作可以在它之上继续搭建；否则项目就会止步于“证明完第一条主定理”。
如果忽视代码质量，形式化项目就仅仅只是对最终定理做一次机器核验。好的形式化项目还应当产出基础设施，造福同领域后续研究。但另一方面，即便使用智能体，想要把代码打磨到Mathlib库的标准，成本依然很高。我们面临的挑战是：找到一套可规模化的质量优化方案，让大规模形式化成果真正可复用，同时不至于成本过高。
5.2 走向更自动化的形式化
本项目积累了大量经验，能够大幅加速同领域后续的形式化工作。例如，借助本次项目沉淀的知识，同类性能问题可以在较少人工干预下诊断和修复。我们也相信，后续开发可以避开很多我们走过的弯路。举个例子：构造的一般性程度选择，有了本次经验，加上对蓝图全局的把握，智能体早期就可以做出更合理的判断，减少试错。
更有野心的目标：让智能体承担更多底层实现工作。前面提到，自然语言蓝图常常隐去一部分数学设定，只看蓝图局部的智能体很难识别出正确形式化所需的前提与选择。我们设想一种交互式自动形式化范式：智能体可以通读整张蓝图，理解全局数学语境，主动识别需要澄清的细节。
理想情况下，它还可以和撰写蓝图的智能体沟通，在细节层提出澄清需求。如果这一点可行，人类的工作最终可以收敛到最高层级的数学决策，就像本项目中六函子整体构造方案的选择。
5.3 彼此交织的数学之网
这是构建融合自然语言与形式化语言文库的一次早期尝试。当前原型围绕韦伊猜想这一巨型证明搭建，但这套范式可以像《Stacks项目》一样向外拓展。当开发一套新的相关理论，比如反常层、近邻循环与消失循环，同样可以用这套逐层细化的流程：新证明会拆分为全新编写的部分，以及文库中已经存在、可以复用的部分。同样的底层细节，可以重新组织，服务于新的高层叙事。反映在依赖关系图上，就是新增、删除部分模块，原有底层模块重新组合，形成新的高层单元。无数数学思想，依靠共享的底层细节彼此勾连。就这样，我们编织出一张彼此交织的数学之网。
我们希望未来有更多数学内容，都可以用这种多层级的方式重新组织。想象这样一套完备文库：无数核心高层思想被撰写、展示、展开，向下落实到细节，底层全部由形式化保证正确。我们可以这样做数学：在高层思考、写作，人机协作完成中间层，底层完全交由AI自动处理。这会是一种迷人的全新方式，用来理解、研究，甚至拓展这张彼此交织的数学之网。
原文参考文献
David Kurniadi Angdinata and Junyan Xu. "An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any Characteristic". In: 14th International Conference on Interactive Theorem Proving (ITP 2023). Vol. 268. LIPIcs. Schloss Dagstuhl, Leibniz-Zentrum für Informatik, 2023.
Anthropic. Formalizing Fermat's Last Theorem. Lean 4 formalization. 2026. github.com/anthropics/fermats-last-theorem
Axiom Math. The Stacks Project in Lean. 2026. github.com/AxiomMath/Stacks
Axiom Math. The Weil Conjectures in Lean. A Lean 4 formalization of the proof of the Weil conjectures. 2026. github.com/AxiomMath/Weil
Bhargav Bhatt and Peter Scholze. "The pro-étale topology for schemes". Astérisque 369 (2015), pp. 99–201. doi:10.24033/ast.960
Nicolas Bourbaki. Éléments de mathématique. Paris: Hermann, 1939–.
Kevin Buzzard and The FLT Project. Fermat's Last Theorem. Ongoing Lean 4 formalization. 2026. github.com/ImperialCollegeLondon/FLT
Kevin Buzzard, Chris Hughes, Kenny Lau, Amelia Livingston, Ramon Fernández Mir, and Scott Morrison. "Schemes in Lean". Experimental Mathematics 31.2 (2022), pp. 355–363.
Pierre Deligne. "La conjecture de Weil: I". Publications Mathématiques de l'IHÉS 43 (1974), pp. 273–307.
Pierre Deligne. "La conjecture de Weil. II". Publications Mathématiques de l'IHÉS 52 (1980), pp. 137–252.
Tamir Hemo, Timo Richarz, and Jakob Scholbach. "Constructible sheaves on schemes". Advances in Mathematics 429 (2023), p. 109179. doi:10.1016/j.aim.2023.109179
J. Jiang and C. Merten. Proétale Cohomology in Lean. GitHub repository. github.com/chrisflav/proetale
Kiran S. Kedlaya. "Fourier transforms and p-adic 'Weil II'". Compositio Mathematica 142.6 (2006), pp. 1426–1450.
Kiran S. Kedlaya. Notes on Prismatic Cohomology. kskedlaya.org/prismatic
Jacob Lurie. Kerodon. kerodon.net
Christian Merten. The Étale Fundamental Group of a Scheme. Lean 4 formalization. 2025. github.com/chrisflav/pi1
Joël Riou. "Formalization of derived categories in Lean/mathlib". Annals of Formalized Mathematics 1 (July 2025), pp. 1–42. doi:10.46298/afm.13609
Michael Stoll. Elliptic Curves. Formalization in Lean of basic results from the theory of elliptic curves. 2026. github.com/MichaelStollBayreuth/EllipticCurves
The mathlib Community. "The Lean Mathematical Library". In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. CPP '20. ACM, 2020, pp. 367–381. doi:10.1145/3372885.3373824
The nLab Authors. The nLab. ncatlab.org
The Stacks Project Authors. The Stacks Project. stacks.math.columbia.edu
求点赞
求分享
求喜欢
参考资料
https://xilbert.com/en/blog/weil-conjectures
https://weil-conjectures.merten.dev
https://leanprover-community.github.io/teams/reviewers.html
https://frenzymath.com/blog/weil/
https://xenaproject.wordpress.com/2026/11/11/a-modern-reorganization-of-mathematics/
董彬教授2026.4.21《AI人工智能与科研诚信》——SIAM青年学者研讨会发言稿全文
小乐数学科普：2022国际数学家大会一小时报告《数学形式主义的兴起》Kevin Buzzard 演讲全文
小乐数学科普：专访ICM 2022国际数学家大会一小时报告者Kevin Buzzard：计算机可以成为数学家吗？——译自量子杂志
小乐数学科普：2024年ICTP &IMU发展中国家青年数学家拉马努金奖Ramanujan Prize授予我国刘若川教授
小乐数学科普历年合集
《小乐数学科普》2026年Q3精选文章目录
zzllrr小乐微信公众号栏目《小乐数学科普》2026年6月文章精选
zzllrr小乐微信公众号《小乐数学科普》2026年5月文章精选
《小乐数学科普》2026年4月文章精选
2026Q1《小乐数学科普》精选文章合集目录
近三月《小乐数学科普》精选文章合集目录202512—202602
2026年01月《小乐数学科普》精选文章合集目录索引
2025年《小乐数学科普》精选文章合集目录索引
《小乐数学科普》2024年合集
· 开放 · 友好 · 多元 · 普适 · 守拙·
让数学
更加
易学易练
易教易研
易赏易玩
易见易得
易传易及
欢迎评论、点赞、在看、在听
收藏、分享、转载、投稿
点击左下角 阅读原文
查看原始文章出处
点击底部一起捐
助力腾讯公益
点击zzllrr小乐
公众号主页
右上角
置顶★加星
数学科普不迷路！
原标题：《北大AI4Math董彬、刘若川等多位学者合作：《数学的一种现代重构——韦伊猜想的形式化证明与阐述》2026-11-11》