精益定理证明的回顾

当我开始寻找比HOL-Light更强大的基础系统时，我转向了Lean。HOL-Light是我多年来一直乐于使用的校对助手。 HOL-Light擅长于其工作（例如真实和复杂的分析），但在处理大型对象（例如所有集合的类别）方面却不足。

Coq和Lean均基于CiC（归纳结构演算）的逻辑基础。与HOL不同，CiC可以轻松地对在数学中广泛使用的大多数结构进行编码。

1.精益听起来很棒：开源，小的可信任内核，强大的精心制作引擎，包括类似于Prolog的用于类分类解析的算法，多核支持，增量编译，对构造和经典数学的支持，同构的成功项目类型理论，出色的文档和Web浏览器界面。精益源文件可以在Emacs，Visual Studio Code或CoCalc中进行编辑。

精益似乎是从过去十年对Coq系统的研究中学到的。

2.更详细地讲，“极简和高性能内核”是精益的明确目标。已经给出了内核的独立实现（Selsam在2000行中，等等），从而减轻了对Lean C ++实现中的错误的担忧。

3.现在，已经完全阐明了“精益”的语义（这要感谢基于Werner的Mario Carneiro）。特别是，卡内罗（Carneiro）在ZFC集合论中建立了精益逻辑模型（具有非累积性Universe的CiC）（通过数量众多的难以接近的基数来增强）。

4.精益语法干净。例如，要在一个阿贝尔群中添加两个元素，一个元素可以简单地写x + y，而精益正确地推断出要在其中进行相加的组。稍后，我还有更多要讲的精益语法。

5.精益使您可以轻松地从构造逻辑转换为经典逻辑（只需打开经典逻辑模块）。精益使商类型变得容易（与Coq不同，后者倾向于使用笨拙的setoid）。

6.精益是它自己的元语言。我觉得这很吸引人。与此形成对比的是HOL-Light，后者将OCaml作为元语言，而Coq则具有针对战术的领域专用语言Ltac。

7.最后，有个人原因。卡内基-梅隆大学是精益图书馆发展的中心。我住在匹兹堡，并且经常参加CMU的精益小组会议。

1.内核is肿。具体而言，据我所知，出于性能原因，互归类型将很快移入内核。这破坏了极简内核的先前主张。

2.精益不向后兼容。精益3打破了精益2的库，并且旧库仍未移植到精益3。在将近两年之后，这种情况似乎永远不会发生。取而代之的是，新图书馆的建造成本很高。精益4保证在精益3库到达时就打破它。简而言之，精益是实验性的，不断发展的且不稳定的。

3.学习曲线陡峭。学会熟练使用精益是非常困难的。您是斯坦福大学，CMU或Pitt的研究生吗？您是凯文·巴扎德（Imperial Buzzard）指导下的Imperial大学学生吗？如果没有，精益可能不适合您。

4.精益是自己的语言。精益是新的，语言库几乎不存在。几乎没有任何主要程序是用精益编写的。 Java程序员比精益程序员大一百万。首先，在Lean中不可能进行任何认真的编程。

我想念HOL-Light，他的语言是一种成熟的编程语言（OCaml），带有大型支持库。每当我需要战术时，我就坐下来用OCaml编写。我在精益开发中无法做到这一点，并且在无法进行认真编程的环境中工作非常令人沮丧。

实际上，如果我可以用精益编写自己的代码来解决我不喜欢的问题，那么我几乎可以接受所有其他批评。我已经与专家讨论了精益编程问题，这些工具根本不可用。

5.精益打字是名义上的，而非结构性的。作为数学家和OCaml程序员，我会偏向于倾向于结构化方法的设计决策。数学家习惯于使用集合论，并且应该做出决策，通过使类型更可互操作来推动类型论变得更像集合。

6.存在性能问题。 （对我，甚至对任何人）尚不清楚为什么性能如此大的问题，因为Lean是为实现性能而用C ++实现的。但是实际上，数学库的编译当前非常缓慢。这里不对劲。

7.需要丑陋的投影链。考虑半群的定义（具有关联二进制运算的数学结构）

宇宙u类半群（α：类型u）扩展has_mulα：=（mul_assoc：∀a b c：α，a * b * c = a *（b * c））

这看起来很简单，并且具有吸引人的语法，因为该类扩展了has_mul，因此允许将符号*用于乘法。但是，细化者将其扩展为丑陋的东西

@ [类，优先级100]结构semigroup：类型u→类型u字段：semigroup.mul：{{α：类型u} [c：半组α]，α→α→αsemigroup.mul_assoc：∀{α：类型u } [c：半群α]（ab c_1：α），@ eqα（@ has_mul.mulα（@ has_mul.mkα（@ semigroup.mulαc）））（@ has_mul.mulα（@ has_mul.mkα （@ semigroup.mulαc））ab）c_1）（@ has_mul.mulα（@ has_mul.mkα（@ semigroup.mulαc））a（@ has_mul.mulα（@ has_mul.mkα（@semigroup .mulαc））b c_1））

每次使用乘法符号时，半群都将显式转换为另一个结构has_mul，该结构负责处理乘法。

我特意选择了一个非常简单的示例。当您看一看更复杂的数学结构（例如有序环）的丑陋扩展时，情况会变得更加糟糕。

8.结构取决于符号。精益有一个关于乘法组的结果库和一个独立的关于加性组的结果库。唯一的区别是，一个使用符号*进行分组操作，另一个使用符号+进行分组操作。数学家发现使群论中的定理依赖于用于合成的符号是荒谬的。

在依赖群体的结构中，问题变得更加严重。例如，有两种类型的两组乘积，因为第一个因子可以是+-组或*-组，第二个因子也可以是两者中的任一个。

这个设计缺陷背后有一段有趣的历史。最初，类型类被引入功能语言中，以减少即席多态性。最初是清除操作员超载符号的一种方法，最后是将焊接符号焊接到不受欢迎的结构上。

9.禁止携带钻石。从编程语言的角度来看，我了解与钻石有关的问题。但是，对于数学家来说，钻石是极其天然的，并且以很多名称（回弹，纤维产品，笛卡尔方等）大量出现。在我看来，设计用于数学的系统所要做的不只是宣布它们为非法。

阅读导致钻石禁令的完整讨论，在辩论中（毫无说服力地）指出，即使代数图书馆在许多地方都使用钻石，但该禁令只会``成为一个小麻烦''。实际上，我认为这是一个主要障碍。有人告诉我，我只能给出自己的带有菱形的类的实现，但是请参见上面的第4项-实际上，我没有计算机语言可用于此目的。

10.从数学的角度来看，结构是毫无意义的参数化。为了简要介绍参数和捆绑的主题，用户选择数据是否作为外部参数出现。这是参数和捆绑形式的岩浆示例

结构magma_with_parameter（α：Type *）：=（op：α→α→α）结构magma_bundled：=（α：Type *）（op：α→α→α）

我认为参数化或捆绑式变体类似于或不类似于柯里化；函数的参数是连续显示还是作为单个有序元组显示？但是，currying函数和currying结构之间存在很大差异。在咖喱函数和非咖喱函数之间切换很便宜，但是精益几乎不可能咖喱一个结构。即，捆绑的内容以后无法作为参数打开。 （使用sigma类型可以很容易地朝着增加结构捆绑的方向发展。）这意味着库设计师被迫采取保守的方法，并公开任何用户可能希望公开的任何内容作为参数，因为一旦捆绑，它不会回来。

根据与给定上下文相关的任何信息，数学家倾向于灵活地选择公开哪些信息。他们不希望将硬捆绑到库中的预定捆绑决策。

精益结构如何无意义地参数化？作为说明，该组的基础载波的类型α：Type *作为参数传递（如上述magma_with_parameter示例中所示）。对于数学家来说，这完全是毫无意义的信息，它作为参数传递。谁在乎该基础组的特殊性？重要的是小组的结构。数学家说，令G为群，但绝不让α为集合，而令G为在载体α上构造的群。精益要求用户在每该死的时间都给α和G。其他语言设计师则代表用户奋斗，以节省他们的按键和样板。我希望精益也一样。

随着代数结构的复杂性增加，情况变得更糟。您不能只是说，让M为拓扑环R的拓扑模块。我计算7种不同的结构，每次在Lean中引入拓扑模块时都必须首先明确声明。这是无法忍受的。我还没有计算拓扑双模的张量积，但您明白了。如果您想知道，是的，数学家会采用拓扑双模的张量积。

（精益之所以这样做是有原因的：它使用暴露的参数α作为类型分类解析的索引，作为避免钻石的廉价方法，等等。但是为什么要强迫数学家进入精益内部？

11.精益舍弃了有价值的信息，这些信息随后将由其类型类解析引擎重建（以成本为代价）。

例如，我们在Lean中写G：groupα表示G是一个带有载波α的组。然后，当我们写关联定律x（xyz：α），x * y * z = x *（y * z）时，有价值的信息会丢失，因为所有类型信息都指向载体α而不是组G，所以精益必须寻找与原始类型α相关的G组。

如果同一基础载体上有两个组（例如发生在半直接产品上），那么精益将给出不可预测的结果。这里有一种设置优先级的方法，但是不建议这样做，因为这些设置具有全局范围。

∀（x y z：G），x * y * z = x *（y * z）。

与精益的区别可能很小，但现在该语句尚未丢弃G组，我们也不必寻找它。由于G不是类型，因此z：G强制转换为z：G.carrier，或更详细地说，z：group.carrier G，并且该组仍然可见。