成电讲堂

8月31日，北京大学文再文教授和北京航空航天大学韩德仁教授应邀做客“学者论坛”，开展运筹学的形式化与定理证明、随机优化理论前沿进展专题讲座。本次学者论坛由教师发展中心主办，数学科学学院、计算机科学与工程学院（网络空间安全学院）和航空航天学院联合承办，数学科学学院徐立伟教授主持。

文再文教授以“智能数学推理：形式化与定理证明”为题作了报告，以费马大定理的证明历史开场，指出了形式化的必要性及其广泛应用，并介绍了数学形式化的典型软件系统。随后，他介绍了团队开源项目optlib，包括其目标、网页、论文及当前进展。该库已在Lean4中完成凸函数、次梯度、邻近算子以及梯度法、Nesterov加速法等十余类算法的定义与收敛性证明，并现场演示表达式树构造，让听众直观感受数学优化形式化的魅力。

面向未来，他介绍了“智能数学推理引擎——ReasLab”蓝图，认为该平台将融合Lean、Coq、Isabelle等优势，通过基于树结构的前提选择、CoSProver及SITA框架，实现从自然语言问题到形式化抽象的自动桥接，目标是为教学、科研和工业提供人人可用的形式化工具。

韩德仁教授以“Enhanced randomized Douglas-Rachford method: Improved probabilities and adaptive momentum”为题作了报告，介绍了随机迭代方法在解决大规模线性系统的机器学习和信号处理中的应用。例如，利用随机道格拉斯-拉奇福德（RDR）方法，可通过两个随机选择的超平面反射迭代，并与当前点进行凸组合来更新迭代。此外，他还介绍可以通过引入改进的采样策略和自适应的重球动量来增强RDR方法。 

讲座结束后，两位主讲专家与参会师生进行了热烈交流。