一段时间以来，我一直在考虑举办一系列名为“万能证明助手”的研讨会，专门针对所有不同的证据助手。除了现有的助手(Isabelle/HOL，CoQ，AGDA，Lean)之外，还有其他有趣的实验验证助手，还有一些还在开发中，或者只是概念的证明。我想更多地了解他们，我想我不是唯一的一个。
让证明助理的作者前往卢布尔雅那，并在我们的数学和理论计算机科学基础研讨会上发表演讲，在很大程度上已经成为不可能的事情。但幸运的是，世界范围内的研究研讨会正在迅速转移到网上，我们的基金会研讨会也是如此。因此，我很高兴地宣布，首届“每一位校对助理”研讨会：
时间：2020年4月30日(星期四)18：00至19：00(中欧夏季时间，UTC+2)地点：在线Zoom ID 965 4439 5816发言人：Valery Isaev(JetBrains Research)。
摘要：我将讨论JetBrainsResearch开发的验证助手Arend。AREND的目的是为同伦型理论和普通数学中的结果形式化提供一个强大的系统。为了实现后者的目标，我们证明了一个灵活的类系统，它具有子类型、泛多态和强大的层次推理机制，商集具有方便的模式匹配原则。我们最近还实现了一个战术框架，可以用来自动化……。
我还有几个正在筹备中，所以关注这个博客，基金会研讨会的公告，或者关注我的Twitter账户@andrejbauer。
PVS和ACL2是否包括在内。两人都是博耶-摩尔家族的成员。ACL2在硬件验证方面拥有重要的用户。PVS在CPS社区中使用。
我不确定我们将涵盖哪些内容。我们将从更接近类型理论社区的证明助手开始，因为我更了解那里的风景。
PVS和ACL2肯定与CoQ、AGDA、Lean、Isabelle等一起属于成立的集团。我们最终会达到这些目标的。
这些谈话内容会被录下来放在什么地方吗？它们看起来非常有趣，错过它们也一样。
我的证明编辑器(DC证明)是一个非常简单的系统，它基于我自己的自然演绎和集合论版本，您可能会发现它们本身很有趣。DC证明旨在向数学本科生介绍证明的基本方法。
我是一个业余软件开发人员。我与任何学术机构没有联系，也没有研究生学位。
我把时区搞乱了，错过了第一次演讲。有可能有录音吗？期待系列！
研讨会将被录制，视频将在网上发布。有关第一个视频，请参阅上面的链接。我还将提供到校对助手的链接。
如果您想推荐一名打样助理，请通过电子邮件与我联系。我注意到了评论中的建议。
使用Markdown写下您的评论。使用$⋯$表示内联，使用$$⋯$$表示显示LaTeX公式，使用<；PRE>；⋯<；/PRE>；表示显示代码。您的电子邮件地址仅用于计算您的重力头像，不会存储在任何地方。评论通过拉取请求进行审核。