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

Sun, 06 Mar 2022 21:21:13 -0800 

本次招新有很多新的小伙伴加入，院系分布也更加多元，欢迎你们加入 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<https://en.wikipedia.org/wiki/List_of_unsolved_problems_in_mathematics>

[2] Agda - Universe 
Levels<https://agda.readthedocs.io/en/latest/language/universe-levels.html>

[3] Pusheen<http://pusheen.com/>


--
Yipeng Liu

-- 
您收到此邮件是因为您订阅了 Google 网上论坛的“TUNA 主邮件列表”群组。
要退订此群组并停止接收此群组的电子邮件，请发送电子邮件到tuna-general+unsubscr...@googlegroups.com。
要在网络上查看此讨论，请访问 
https://groups.google.com/d/msgid/tuna-general/TYWP286MB22026ABEEDAE4DBFCAEC2AC2EA089%40TYWP286MB2202.JPNP286.PROD.OUTLOOK.COM。

回复