报告时间：2016年11月17日（星期四）15:30-16:30报告地点：北京大学理科二号楼2736报告厅

主办单位：机器感知与智能教育部重点实验室

北京大学信息科学技术学院

特邀报告人：Prof. Herman Geuvers

报告摘要：

Mathematical proofs get more and more difficult and complex. At the same time more and more computer systems (software and hardware) can be verified rigidly using mathematical proof, so there is an increasing request for completely verified mathematical proofs. The field of Computer Assisted Mathematical Proofs fills this gap by allowing users to create complete mathematical proofs, interactively with the computer, where the computer checks each small reasoning step.

In the talk, I will illustrate this with two examples where the computer has been used to completely verify a proof: (1) From pure mathematics: The proof of the Kepler conjecture (2) From computer science: The proof of the correctness of a C compiler. Then I will discuss the present day limitations of Computer Assisted Mathematical Proofs, which basically rest on the limitations of proof automation. It has recently become clear that Machine Learning provides methods that apply very well to speeding up proof automation. Machine Learning does not supersede standard techniques (from Automated Theorem Proving) but provide the ideal additional technique. I will show how Machine Learning techniques fit in and what successes have been obtained in proof automation.

报告人简介：

Herman Geuvers is professor of Theoretical Computer Science in the Institute for Computing and Information Science (ICIS) of Radboud University Nijmegen in the Netherlands. He is also the head of the research institute ICIS. His research interest are: Logic in Computer Science in general. Type theory, lambda calculus, logic, theorem provers (especially interactive ones, with a bias to those based on type theory), formalizing mathematics, computer mathematics (combining proving and computing in one integrated computer environment), software verification, automata and formal languages.