报告时间：2026年6月15日（周一）上午 09:30-11:30
报告地点：天博体育 天赐庄校区精正楼309教室
报告人：Hongwei Wang，西交利物浦大学 / 纽约大学阿布扎比跨学科数据科学与人工智能中心
报告摘要：
本报告以同伦论与无穷范畴为出发点，探讨现代数学基础与形式化证明之间的深刻联系，并展望人工智能辅助自动推理的未来方向。
报告分三个部分。第一部分介绍基本群胚与无穷群胚的核心概念：经典基本群 π₁(X) 如何自然升级为基本群胚 Π₁(X)，进而通向路径无穷群胚 Π∞(X)；后者在同伦类型论（HoTT）中作为基本对象的地位，以及从覆叠空间分类等价 Cov(X) ≃ Set^{Π₁(X)} 到参数化谱理论的概念路径。第二部分介绍同伦类型论与 Curry-Howard 对应如何为形式化数学提供语言基础：类型即命题，程序即证明，以及 Lean 4 与 Mathlib 如何将大规模数学定理的机器验证变为现实。第三部分聚焦于形式化数学的最新进展与前景。Meta FAIR 团队近期推出了 AutoformBot 系统与 ATLAS 形式化库，通过多智能体协作将 26 部开放教材自动形式化为超过 45,000 条 Lean 4 声明，标志着研究生级数学的大规模形式化在技术和经济层面已成为现实。与此同时，Kimina-Prover 等系统在 MiniF2F 基准测试上达到了 80% 以上的通过率，首次展示了神经定理证明器随模型规模提升的性能缩放规律。报告将探讨这些进展对未来数学研究范式的深远影响，以及稳定同伦论的形式化作为当前重要开放问题的前景。
Abstract: This talk traces a conceptual path from homotopy theory and infinity-categories to the formalisation of mathematics and AI-assisted automated reasoning. The talk is divided into three parts. The first part introduces the fundamental groupoid and the infinity-groupoid: how the classical fundamental group π₁(X) naturally upgrades to the fundamental groupoid Π₁(X), and further to the path infinity-groupoid Π∞(X); the role of the latter as the basic object in Homotopy Type Theory (HoTT); and the conceptual path from the covering space classification equivalence Cov(X) ≃ Set^{Π₁(X)} to parametrised spectra theory. The second part explains how HoTT and the Curry-Howard correspondence provide the linguistic foundation for formalised mathematics: types as propositions, programs as proofs, and how Lean 4 and Mathlib make machine-verified formalisation of large-scale mathematics a reality. The third part focuses on recent advances and future prospects in formalised mathematics. The Meta FAIR team recently introduced the AutoformBot system and the ATLAS library, autoformalisng 26 open-access textbooks into over 45,000 Lean 4 declarations through multi-agent collaboration, marking a milestone in the technical and economic feasibility of graduate-level mathematics formalisation at scale. Meanwhile, systems such as Kimina-Prover have achieved pass rates exceeding 80% on the MiniF2F benchmark, demonstrating for the first time clear performance scaling with model size in neural theorem provers. The talk will discuss the profound implications of these developments for the future paradigm of mathematical research, and the formalisation of stable homotopy theory as an important open problem on the current frontier.
报告人简介：
王鸿玮（Hongwei Wang），西交利物浦大学2026届本科毕业生，因其优异的学业成绩和在数学方面的突出表现，已获得纽约大学阿布扎比跨学科数据科学与人工智能中心全额奖学金，继续攻读硕/博士学位。
邀请人：马欣荣