题目：数学形式化与大模型

报告人：马家骏副教授 (厦门大学)

时间： 2025年6月17日, 上午10:00-11:00

地点： 精正楼103


报告摘要：

近年来，数学命题及其证明的形式化取得了突破性进展。其中最具代表性的成果之一，是由Kevin Buzzard等人于2017年发起并推动的数学定义与定理库——Mathlib。在Lean和Mathlib的基础上，各类数学形式化项目蓬勃涌现。与此同时，全球诸多科技公司和科研机构也在积极探索基于Lean的自动化证明与大模型结合的相关研究，推动了人工智能与数学形式化的深度融合。可以说，Lean所引领的数学形式化浪潮，正成为变革数学研究范式的重要力量。


本报告将结合本人近年来对Lean和Mathlib的应用与实践，围绕以下几个方面与大家交流：

1. 博弈论中若干基本结果的形式化尝试及本科毕业论文指导经验；

2. 抽象代数课程内容的形式化实践及借助Lean4Game进行辅助教学的初步探索；

3. Mathlib库的使用与优化方面的体会与建议；

4. Lean元编程及其与大模型集成应用的初步探索。


报告人简介：


马家骏，现为厦门大学成人直播 副教授。于2007年获苏州大学理学学士学位，2013年2月获新加坡国立大学博士学位，导师朱程波教授。曾经在新加坡国立大学、本古里安大学、香港中文大学、上海交通大学等进行科研工作。 2021年7月到厦门大学成人直播 工作至今。长期从事典型群表示论及相关Langlands纲领问题的研究。


邀请人：白占强