内容介绍：

Interactive theorem proving involves using proof assistants to construct and verify formal proofs of mathematical theorems. It can be applied to verify results in both mathematics and computer science. Proof automation is an important tool in interactive theorem proving, as it can significantly reduce the amount of guidance that the user needs to provide to formalize a proof.

Auto2 is a new proof automation tool written for Isabelle, designed to combine the advantages of existing approaches to automation: tactics and external automatic theorem provers. In this talk, I will describe the ideas behind auto2, and its application to formalization of mathematics, in particular building a library of mathematics from the axioms of set theory to the definition of the fundamental group in algebraic topology.