∞-type Café Summer School TuT

∞-type Café 暑期学校 2026

∞-type Café 暑期学校 2026 将于 2026 年 8 月 6 日正式开始。这是我们的第二届暑校(第一届)，也是一次围绕现代数学、形式化证明与 AI4Math 展开的线上交流活动。

今年的课程试图讨论一个更开放的问题：当类型论、范畴论、自动定理证明和人工智能逐渐在数学研究中相遇时，我们能够做什么，又会遇到哪些困难？

8 月 24 日至 30 日期间，我们还计划与上海交通大学 AI4Math + Lean 暑校开展线上—线下联动。

我们不要求每位听众已经掌握所有相关知识。无论你关心无穷范畴、类型论、HOL、Lean、AI4Math，还是正在思考数学研究的工具、方法与未来，都欢迎带着自己的问题来到这里。

希望这次暑校不仅是一系列课程，也能成为大家交换知识、提出问题、分享想法并结识同行的地方。

相关重要信息

面向怎样的听众

  • 对无穷范畴，以及它与类型论和现代数学的联系感兴趣的同学；
  • 希望了解 HOL、tactic 编写与形式化证明方法的同学；
  • 关注 AI4Math 面临的困境、可能的出路，以及人工智能如何参与数学研究的同学；
  • 对数学研究的日常实践与长远发展感兴趣，包括 SNL、文档管理，以及“还能做一辈子的数学研究吗?”这一问题的同学。

八月课程与联动安排

本次系列课程将于 2026 年 8 月 6 日开始，内容涵盖无穷范畴、AI4Math、HOL、tactic 编写与数学研究等主题。课程默认于北京时间 19:00–21:00 举行；如有调整将另行通知。所有课程均使用同一腾讯会议链接。

日期 时间 讲者 课程
8 月 6 日（周四） 19:00–21:00 Cha0sButterf1y 无穷范畴（一）
8 月 7 日（周五） 19:00–21:00 Cha0sButterf1y 无穷范畴（二）
8 月 8 日（周六） 19:00–21:00 Cha0sButterf1y 无穷范畴（三）
8 月 12 日（周三） 19:00–21:00 Gestellmensch 0=1−1=−1+1=0
8 月 13 日（周四） 19:00–21:00 天行狸🐱 SNL 与文档管理
8 月 15 日（周六） 19:00–21:00 kokic AI4M 的困境
8 月 16 日（周日） 19:00–21:00 kokic HOL 所选择的道路
8 月 19 日（周三） 19:00–21:00 子鱼 AI4M 的出路
8 月 20 日（周四） 19:00–21:00 子鱼 如何写 tactic（一）
8 月 22 日（周六） 19:00–21:00 子鱼 如何写 tactic（二）
8 月 24 日（周一） 19:00–21:00 子鱼 如何写 tactic（三）
8 月 30 日（周日） 09:00–11:00 Gestellmensch 还能做一辈子的数学研究吗?

上交 AI4Math + Lean 暑校联动

8 月 24 日至 30 日期间，我们计划与上海交通大学 AI4Math + Lean 主题暑校开展线上—线下联动。线下课程不会进行直播；我们拟选择部分日期，在晚间 19:00–21:00 的答疑时段，邀请线下学员以个人形式参与线上社区活动。活动内容包括社区成员分享，以及围绕 Type Theory、Lean 4、AI4Math、学员项目与研究想法的提问和交流。具体安排将在确认后公布。

目前听众希望的talks

相关问题

  1. 本次活动是线上还线下？

    线上。

  2. 这次活动是否有录像？

    B站会同步更新。

  3. 这次活动是否会提供课上内容的相关材料？

    ntype-cafe-summer-school-2026 会同步更新课上的讲义，幻灯片，代码和推荐课外内容。

  4. 人在国外有时差，如何参与这次活动？

    课程默认在中国时区的晚上 19:00–21:00 举行；如有调整将另行通知。请听众合理安排时间。如果时间上存在无法避免的冲突，可以参考 Q2 和 Q3。

  5. 课后是否可以留一些练习作业？

    这当然是可以的，我们会与讲师进行沟通。作业后续可能还有答疑环节，这部分活动目前暂定在QQ群进行。

  6. 是否可以对想要入门的同学多一点的照顾？

    这是工具人一直争取的事，初步设计暑校的时候是没有前置课程的，但是工具人觉得这样可能会把很大一部分人排除在外，因此给大家贴心准备了相关前置课程。事实证明确实是这样，因为从问卷的情况来看熟悉类型论的人只有仅仅的%10。

  7. 是否可以充分考虑不同领域方向的听众？

    目前，数学系和计算机系的同学几乎分别占了一大半，我们在尽力平衡talks的相关性，可以看到talks里面有各自领域的东西。

  8. Infinity Type Café是怎样一个组织？

    一个大部分成员都是学生的组织。特别感谢那些在意见中给于我们的支持和鼓励的朋友！

相关人员

讲师

除了课程和 talks 的在线答疑，听众也可以通过上述联系方式联系讲师答疑，或加入暑校群（QQ 群号 1015828456）询问问题。寻找讲师答疑即代表您同意我们在暑校相关内容中（包括但不限于录播视频和暑校网站）公开您的问题和答疑内容。

特别演讲人

  • 等一个

组织者

Thanks!