Speaker: Josef Urban, Czech Technical University

Title: AI and Theorem Proving

Abstract: The talk will discuss the main approaches that combine machine learning with automated theorem proving and automated formalization. This includes learning to choose relevant facts for “hammer” systems, guiding the proof search of tableaux and superposition automated provers by interleaving learning and proving (reinforcement learning) over large ITP libraries, guiding the application of tactics in interactive tactical systems, and various forms of lemmatization and conjecturing. I will also show some demos of the systems, and discuss autoformalization approaches such as learning probabilistic grammars from aligned informal/formal corpora, combining them with semantic pruning, and using neural methods to learn direct translation from Latex to formal mathematics.