Description

The conference "Formal Math Frontiers: From Implementation to AI Assistance" aims to provide a comprehensive overview of the cutting-edge developments and practical challenges in formal mathematics. The program begins by examining the foundational engineering principles behind interactive theorem prover implementation, including core architectural decisions. It then addresses the critical need for standardized evaluation through the introduction of a formal, multi-level benchmark series for advanced algebra. A key session introduces the ongoing process of formalizing deep theoretical results, exemplified by the mechanization of a major criterion in commutative algebra. The focus subsequently shifts to the transformative role of artificial intelligence, exploring human-machine collaborative workflows in theorem proving and culminating in a live demonstration of an AI-assisted proving tool. Collectively, this event bridges the gap between the theoretical, engineering, and AI-assistance dimensions of modern formal mathematics.

Conference Schedule