∞-type Café Summer School TuT

∞-type Café Summer School 2026

The ∞-type Café Summer School 2026 will officially begin on August 6, 2026. This is our second summer school (first edition) and an online event centered on modern mathematics, formal proof, and AI4Math.

This year’s program seeks to explore a broader question: as type theory, category theory, automated theorem proving, and artificial intelligence increasingly converge in mathematical research, what can we do, and what difficulties will we encounter?

From August 24 to 30, we also plan to organize online–offline collaborative activities with the Shanghai Jiao Tong University AI4Math + Lean Summer School.

We do not expect every participant to have already mastered all the relevant background. Whether you are interested in infinity categories, type theory, HOL, Lean, AI4Math, or are thinking about the tools, methods, and future of mathematical research, you are welcome to bring your questions.

We hope this summer school will be more than a series of courses: a place where participants can exchange knowledge, ask questions, share ideas, and meet peers.

Key Information

Intended Audience

  • Students interested in infinity categories and their connections with type theory and modern mathematics;
  • Students who would like to learn about HOL, tactic writing, and formal proof methods;
  • Students interested in the challenges and possible directions of AI4Math, and in how artificial intelligence may contribute to mathematical research;
  • Students interested in both the everyday practice and long-term future of mathematics, including SNL, documentation management, and the question “Can We Still Spend a Lifetime Doing Mathematical Research?”

August Courses and Collaborative Events

This series begins on August 6, 2026, and covers infinity categories, AI4Math, HOL, tactic writing, and the future of mathematical research. Classes are scheduled by default for 19:00–21:00 China Standard Time; any changes will be announced separately. Every class uses the same Tencent Meeting link.

Date Time Speaker Topic
August 6 (Thursday) 19:00–21:00 Cha0sButterf1y Infinity Categories I
August 7 (Friday) 19:00–21:00 Cha0sButterf1y Infinity Categories II
August 8 (Saturday) 19:00–21:00 Cha0sButterf1y Infinity Categories III
August 12 (Wednesday) 19:00–21:00 Gestellmensch 0=1−1=−1+1=0
August 13 (Thursday) 19:00–21:00 天行狸🐱 SNL and Documentation Management
August 15 (Saturday) 19:00–21:00 kokic Challenges Facing AI4Math
August 16 (Sunday) 19:00–21:00 kokic The Path Chosen by HOL
August 19 (Wednesday) 19:00–21:00 子鱼 A Way Forward for AI4Math
August 20 (Thursday) 19:00–21:00 子鱼 How to Write Tactics I
August 22 (Saturday) 19:00–21:00 子鱼 How to Write Tactics II
August 24 (Monday) 19:00–21:00 子鱼 How to Write Tactics III
August 30 (Sunday) 09:00–11:00 Gestellmensch Can We Still Spend a Lifetime Doing Mathematical Research?

Collaboration with the SJTU AI4Math + Lean Summer School

From August 24 to 30, we plan to organize online–offline collaborative events with the AI4Math + Lean Summer School at Shanghai Jiao Tong University. The in-person courses will not be livestreamed. Instead, on selected evenings from 19:00 to 21:00, participants at the in-person school will be invited to join the online community in an individual capacity. These sessions may include presentations by community members, questions and discussion on Type Theory, Lean 4, and AI4Math, as well as exchanges of projects and research ideas. Further details will be announced once confirmed.

Talks Currently Requested by Participants

Frequently Asked Questions

  1. Is this event online or in person?

    Online.

  2. Will this event be recorded?

    Recordings will be uploaded to Bilibili.

  3. Will materials related to the course content be provided?

    ntype-cafe-summer-school-2026 will be updated throughout the event with lecture notes, slides, code, and recommended supplementary materials.

  4. How can people outside China participate despite the time difference?

    Classes are scheduled by default from 19:00 to 21:00 China Standard Time; any changes will be announced separately. Participants should arrange their schedules accordingly. If an unavoidable scheduling conflict arises, please see Q2 and Q3.

  5. Can exercises or assignments be provided after class?

    Certainly. We will discuss this with the lecturers. Follow-up Q&A sessions may also be arranged; for now, we tentatively plan to hold these in the QQ group.

  6. Can additional support be provided for beginners?

    This is something the organizers have consistently advocated. The original summer-school plan did not include prerequisite courses, but the organizers felt that this might exclude a large proportion of interested participants, so we prepared these foundation courses with everyone in mind. The survey results confirmed that this was necessary: only %10 of respondents were familiar with type theory.

  7. Can the event adequately accommodate participants from different fields?

    At present, students in mathematics and computer science each account for nearly half of the audience. We are doing our best to balance the relevance of the talks, and the talk list includes material from both fields.

  8. What kind of organization is Infinity Type Café?

    It is an organization whose members are mostly students. We are especially grateful to everyone who has offered us support and encouragement in their feedback!

People

Lecturers

In addition to the online Q&A sessions for courses and talks, participants may contact the lecturers using the details above or join the summer-school group (QQ group number 1015828456) to ask questions. By seeking help from a lecturer, you consent to our making your questions and the corresponding answers public in summer-school-related materials, including but not limited to recorded videos and the summer-school website.

Special Guest Speaker

  • To be announced

Organizers

Thanks!