数学家眼中“无聊”的 Bruck loop

hbghlyj

xenaproject 的文章A computer-generated proof that nobody understands

数学家眼中“无聊”的 Bruck loop

“Nobody in my department cares about Bruck loops. People care about objects which it takes an entire course to define, not a paragraph.” — xenaproject, July 6, 2019

虽然 Bruck loop的机算证明长达 30000 行，甚至有 J. D. Phillips 与 David Stanovský 在 2012 年于《Communications in Algebra》上发表的论文（已上传至 ResearchGate）加以阐述，但由于其定义只需 19 条公理、理论背景浅显，研究人员普遍认为其学术价值有限。

“They are working on results about objects which in some cases take hundreds of axioms to define, or are even more complicated: sometimes even the definitions of the objects we study can only be formalised once one has proved hard theorems.” — xenaproject, July 6, 2019

数学家更倾向于研究那些定义繁复、依赖多项前置定理的对象，而非短短一段文字就可定义的结构
Shimura variety需先构建 Hermitian 对称空间、约化代数群及其同余子群的框架，才能在此基础上定义；
CM 阿贝尔簇理论是理解 Shimura variety公理化的关键前提，涉及复乘理论中对端同态环的深刻研究；
全局类域论构成了 CM 阿贝尔簇定理的基础，描述了全局数域可换扩张与其本原子群之间的对应关系；
étale cohomology 作为代数簇的同调工具，需要引入 Grothendieck 的 étale 拓扑及其相应的同调群定义。

This is all to do with subtleties such as fashions in mathematics, and which areas are regarded as important (that is, worth funding). — xenaproject, July 6, 2019

研究热点往往受资助机构偏好影响。镜像对称、完美域空间、特征 p 下代数簇的规范环、Shimura 丽形的 étale 同调以及 Langlands 思想等领域因其深度更易获得项目支持。对于仅靠逻辑游戏式的结构和短小公理系统，数学界普遍不屑投入，认为其学术回报与资助可能性不足。

I once went to an entire 24 lecture course by John Coates which assumed local class field theory and deduced the theorems of global class field theory. I have read enough of the book by Shimura and Taniyama on CM abelian varieties to know what’s going on there. … And then there is still the small matter of the definition of etale cohomology. — xenaproject, July 6, 2019

作者回忆，为了真正理解 Shimura variety，他先后参加了约翰·科茨（John Coates）关于局部与全局类域论的 24 次专题讲座，阅读了 Shimura & Taniyama 关于 CM 阿贝尔簇的著作，并在历经约 100 小时研读后，才得以正式给出 Shimura variety在数域上的定义，随后还需掌握 étale 同调的构造与公理化流程。

hbghlyj

The goal of the Xena Project is to get mathematicians, especially undergraduates, using computer proof verification software.

项目旨在让数学本科生通过将课程习题转化为“Lean 游戏关卡”来学习并掌握形式化证明技术，从而培养他们使用 Lean 及其数学库 mathlib 的能力，以便将来能在更高深的数学领域中进行计算机辅助证明。
Mathlib 是一个由社区志愿者持续维护的开源库，涵盖了从集合论到代数、分析等多门本科纯数学课程的核心定理和工具包，Xena 项目正是在此基础上发展和扩展本科课程内容的形式化工作。
团队不仅定期（疫情前为帝国理工大校园内每周四晚；疫情后转至 Discord）召开研讨会，讨论如何将二年级代数、三年级课程等内容逐步录入 mathlib，还鼓励全球数学爱好者在 GitHub 上贡献和认领任务，迄今已有多位学生和研究人员参与其中。

The Xena Project aims to get mathematics undergraduates (at Imperial College and beyond) trained in the art of formalising mathematics on a computer. Why? Because I have this feeling that digitising mathematics will be really important one day.

hbghlyj

虽然 Xena 项目已在本科课程层面取得进展，但对更高深数学的形式化依然面临多重障碍。

One reason why computers are not proving theorems about the etale cohomology of Shimura varieties over number fields is that the human race have not yet taken the time to tell a proof verification system what the phrase ‘etale cohomology of a Shimura variety over a number field’ means.

即便是在定义上，像 Shimura 丽形的规范模型或 étale 同调这类概念，必须先手动将成百上千条定理和公理编码进系统中，人力成本极高，导致至今仍未有人完成此类概念的形式化。

I am currently finding it very hard to think of people who know the definition of the canonical model of a Shimura variety and also know how to use proof verification systems.

高级数学研究者往往熟悉复杂的理论背景，却不一定掌握 Lean 及其自动化策略；而精通 Lean 的计算机科学家通常缺乏阅读 Deligne、Shimura 等原始论文所需的深厚数论与几何学功底，两者交集甚少，形成了严重的“跨界”障碍。

Some of the gaps in mathlib that currently make this challenging.

例如，在形式化Geometric Algebra时，研究者发现 mathlib 中尚缺乏对 Clifford 代数商结构的支持，需要先行扩展库中对张量代数与商群的定义，才能进行后续证明工作。

In the course of formalizing Galois theory in Lean, we faced challenges such as representing finite dimensional vector spaces and handling quotient structures in mathlib.

在形式化伽罗瓦理论时，也遇到向量空间、域扩张等基础构造在 mathlib 中尚不完备的问题，必须先补齐这些关键组成部分，才能继续推进主定理的证明。

The natural framework to define objects like Shimura varieties is within some higher order logical structure; even for the definition of a topological space one has to quantify over subsets rather than just elements.

高阶逻辑的表达能力虽强，却也意味着在 Lean 中处理时需要引入依赖类型、Universe 层级管理等复杂机制，这些机制尚未在 mathlib 中完全成熟，给形式化带来额外难度。

To lower the barrier of entry for contributors and to lessen the burden of reviewing contributions, we have developed a number of tools for the library which check proof developments for subtle mistakes in the code and generate documentation suited for our varied audience.

尽管社区已开发出各种辅助工具来降低贡献者门槛，但审核和维护大量形式化证明仍需极高的人力投入，这在学术界尚缺乏持续资助和专职支持的环境下，难以长期维系。

Such a project will enable Lean to understand many of the basic definitions in modern number theory and arithmetic geometry, meaning that it will be possible to start stating modern mathematical conjectures and theorems in number theory and arithmetic geometry which use such machinery.

reddit.com/r/math/comments/176vtju/kevin_buzz … h_grant_to_begin_the