金枪鱼之夜：2022 年春季学期迎新会 & 定理证明辅助工具

本次招新有很多新的小伙伴加入，院系分布也更加多元，欢迎你们加入 TUNA！本周六将举办迎新会，按照惯例首先会有 TUNA 的简介、互相认识的环节和建设 TUNA 的 n+1 种方式，在此之外还会由喵喵介绍定理证明辅助工具的友好入门方式。

自动化定理证明是一种形式化验证方法，目的是通过计算机程序进行数学定理的证明。对于不同的公理系统，定理证明辅助工具（Proof Assistant）能够推论出一个定理在此系统下是正确的或者错误的，还是不可证明的。本次 Tunight 由喵喵为大家带来一种友好的 Proof Assistant 入门方式：基于常见工程编程语言的类型系统，类比逻辑系统，在不加严格证明的情况下直觉引导下，尝试逐渐扩展出具有更强表达能力的一个定理证明辅助语言，从而解释 Proof Assistant 中各种设计的目的和逻辑基础。

• 主讲人：刘一芃、刘晓义
• 时间：2022/03/12（周六） 19:00 UTC +08:00
• 活动形式：线下 + 线上会议 + 直播
  • 地点：新水 304
  • 线上会议：Zoom 922 1245 8772 密码 20220312
  • 直播链接：YouTube，开始后公布

---

以下为喵喵的附言：

数学复杂¹，定理证明工具为了理解数学至少同等复杂²，但猫咪大脑简单³。因此可以证明，喵喵使用人类方式尝试学习定理证明工具会发生大困难。为了解决这个问题，喵喵尝试展示一种 猫咪-friendly 的 Proof Assistant 的入门方式。本方法受限于喵喵的刚刚入门的水平有限，极具实验性，欢迎各位 PL / TT 人前来教教，爱护喵喵！

[1] List of unsolved problems in mathematics

[2] Agda - Universe Levels

[3] Pusheen