*时间：2023年6月12日 10:00-11:00
*地点：河口大楼B101
*主讲人：张继平 院士（北京大学）
*主持人：吕长虹 教授

*讲座内容简介：

计算机辅助研究在最近几十年的数学发展中发挥着愈来愈大的作用，COQ 和 LEAN（proof assistants）等证明助手是数学形式化的结果， 帮助数学家完成了不少重要的证明验证工作，如基于COQ Feit-Thompson 奇阶群可解的著名定理曾得到机器的证明验证。而机器学习模型是一个巨大进步，不仅帮助数学家做计算和证明验证， 甚至启发了代数学家的数学直觉， 在表示论研究中取得重要突破。 数学形式化使机器可以“学习” 和“懂” 更多的数学，将促进数学研究方式和发展方式的巨大变革。

*主讲人简介：

北京大学博雅讲席教授、中国科学院院士、中俄数学中心主任。深圳国际数学中心执行主任。曾获国家杰出青年基金、教育部长江特聘教授、全国五一劳动奖章、全国先进工作者、全国优秀科技工作者、国家自然科学奖、陈省身数学奖等。曾任 Algebra Colloq 主编，现为 Asia-European J. Math和《数学学报》副主编。曾任中国数学会副理事长，国际数学家联盟发展与交流委员会委员，教育部科技委数理学部常务副主任，中国青年科技协会副会长。他在有限群表示论研究中取得的杰出成就，奠定了高维Galois表示自守提升理论的重要基础。他在任北京大学数学科学学院院长期间，为数学学科发展做出重要贡献，他制定和实施的创新人才计划培养出包括数学黄金一代在内的世界一流人才。 他应邀主持深圳市诺奖实验室—深圳国际数学中心的建设和发展，进而全职引进国际数学大师、菲尔兹奖获得者杰曼诺夫等一批国际一流数学家。