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

时间: 2022-03-12 19:00-21:00 地点: 新水 304 tunight welcome proof-assistant
资源链接:

本次招新有很多新的小伙伴加入,院系分布也更加多元,欢迎你们加入 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,开始后公布

以下为喵喵的附言:

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

[1] List of unsolved problems in mathematics

[2] Agda - Universe Levels

[3] Pusheen

清华大学 TUNA 协会原名清华大学学生网管会,注册名清华大学学生网络与开源软件协会,是由清华大学网络技术和开源软件爱好者、技术宅组成的团体。现阶段向校内外提供开源软件镜像等服务。

The best team on the planet.