学术报告 | 1月9日 形式化方式系列讲座：Automated Theorem Proving

Automated Theorem Proving: a Technology Roadmap

Theorem provers are typically classified as automatic or interactive, which misrepresents what each is for. Automation is necessary because formal proofs even of trivial facts are long and difficult to construct; the role of interaction is not merely to guide automation but to construct and edit large hierarchies of specifications. The proof assistant Isabelle is an example of sophisticated interactive technologies (such as its representation of formal logics and its sophisticated prover IDE) that also relies heavily on automatic technologies (through its nitpick and sledgehammer subsystems). The talk will give an architectural overview of Isabelle and its technologies, both internal to Isabelle and external. The speaker will also speculate on how future technologies, especially machine learning, could assist (not replace) the user.

Lawrence Paulson FRS (http://www.cl.cam.ac.uk/~lp15/) is Director of Research at the University of Cambridge, where he has held established positions since 1983. He has written over 120 refereed conference and journal papers as well as four books. He introduced the popular [Isabelle](http://www.cl.cam.ac.uk/research/hvg/Isabelle/) theorem proving environment in 1986, and made contributions to the verification of cryptographic protocols, the formalisation of mathematics, automated theorem proving technology, and other fields. He achieved a formal analysis of the ubiquitous TLS protocol, which is used to secure online shopping, and the formal verification of advanced mathematical results such as Gödel's second incompleteness theorem. In 2008, he introduced MetiTarski (http://www.cl.cam.ac.uk/~lp15/papers/Arith/), an automatic theorem prover for real-valued functions such as logarithms and exponentials. He has supervised over 20 postgraduate students and numerous postdoctoral researchers. He has the honorary title of Distinguished Affiliated Professor from the Technical University of Munich and is an ACM Fellow and a Fellow of the Royal Society. He holds a PhD in Computer Science from Stanford University, and a BS in Mathematics from the California Institute of Technology.