On December 10th, AI-HSS hosted the 20th "Humanities × Technology" Thinkers’ Forum. Centered on the theme "The Development and Application of Modern Type Theory," the forum invited Professor Luo Zhaohui from the Department of Computer Science at Royal Holloway, University of London—a leading scholar in modern type theory and its applications—as the keynote speaker. Professor Wan Xiaolong served as the host. Professor Wan warmly welcomed and sincerely thanked Professor Luo for his participation, briefly introducing his main research areas and cutting-edge achievements. Professor Luo has dedicated his career to the study of modern type theory and its applications, producing remarkable research outcomes. His original works include Computation and Reasoning on unified type theory, Formal Semantics Based on Modern Type Theory on natural language semantics, and the Chinese monograph The Development and Application of Modern Type Theory.

During the lecture, Professor Luo began by outlining the developmental trajectory and theoretical framework of modern type theory. He noted that the evolution of type theory has progressed from the proposal of Russell's paradox to the construction of ramified type theory, the refinement of simple type theory, and ultimately the establishment of a comprehensive system of modern type theory. Modern type theory encompasses complex type structures such as dependent types and inductive types, and can be categorized into predicative and impredicative types.

Subsequently, Professor Luo shifted the focus to the meta-theory and applications of modern type theory, particularly emphasizing its role in natural language semantics. He also highlighted its applications in formalizing mathematical reasoning and interactive theorem proving in computer science, while offering insights into the future development of modern type theory. Additionally, Professor Luo shared his perspectives on modern type theory and provided suggestions on how to apply it in practical research.

During the Q&A session, attendees engaged in in-depth discussions with Professor Luo on topics such as the philosophical puzzle "Is a white horse a horse?" Drawing from his research experience, Professor Luo addressed the questions one by one, emphasizing the flexible use of abstract objects rather than relying solely on reference, and explaining how proofs can be transformed into standard forms for logical judgment by computers.

Finally, Professor Wan summarized the lecture, once again expressing sincere gratitude to Professor Luo and encouraging students interested in research to actively participate and contribute their expertise. The lecture provided attendees with rich academic insights, systematically reviewing the core knowledge of modern type theory while offering valuable research guidance. It fully demonstrated the value of academic sharing and played a significant role in fostering the academic growth of students and faculty in related fields, as well as promoting interdisciplinary integration and development.