题目：人工智能与定理证明

报告人：王善文，中国人民大学

时间：4月28日，16：00

地点：东区第五教学楼5407教室

摘要：在本报告中, 我们将从数学研究的主要逻辑范式来分析当前人工智能在定理证明方面的进展, 并介绍交互式定理证明助手Lean。