Dr. Bohua Zhan, Technical University of Munich

2018.06.28 15:15-16:15,

2018.06.29 15:15-16:15

【Abstract】Interactive theorem proving studies the construction of formal proofs on the computer with human guidance. It can be applied to formally verify results in both mathematics and computer science. Formalizations in mathematics can serve one of several purposes: verify potentially controversial results in mathematical research, support verification of computer programs and systems, and as an aid to teaching proofs in mathematics.

In this series of two talks, I will give an introduction to the field of interactive theorem proving, with a focus on formalizations in mathematics. The talks will be self-contained, and no background in logic is assumed.

In the first talk, I will begin by reviewing the basic concepts of the field, then describe some major recent results in formalization of mathematics. In the second talk, I will discuss the important concept of proof automation, and my own work in this area. Finally, I will suggest some ideas for future work.