Speaker: 魏陈锐，北京通用人工智能研究院

Inviter: 李伟

Title: Machine Learning for Automated Theorem Proving: Challenges and Advances

Language: Chinese

Time & Venue: 2024.07.03 15:00-16:00 思源楼 813

Abstract: In this talk, I will provide an overview of modern learning-based theorem provers, including interactive theorem provers based on formal verification systems and neural-symbolic theorem provers. I will discuss their architecture, applications in proof search, and their performance in various domains. The presentation will also cover the automated generation of synthetic theorems and the training of domain-specific neural provers using synthetic datasets. Additionally, I will highlight our recent work on the automated proving of Olympiad algebraic inequalities with highly human-readable proofs, as well as the discovery of novel and non-trivial theorems. Finally, I will explore the potential use of artificial intelligence in advancing modern mathematics.