January 26, 2017

The talk will cover several AI methods used to learn proving of conjectures over large formal mathematical corpora. This includes (i) machine-learning methods that learn from previous proofs how to suggest the most relevant lemmas for proving the next conjectures, (ii) methods that guide low-level proof-search algorithms based on previous proof traces, and (iii) methods that automatically invent suitable theorem-proving strategies on classes of problems.

The talk will cover several AI methods used to learn proving of conjectures over large formal mathematical corpora. This includes (i) machine-learning methods that learn from previous proofs how to suggest the most relevant lemmas for proving the next conjectures, (ii) methods that guide low-level proof-search algorithms based on previous proof traces, and (iii) methods that automatically invent suitable theorem-proving strategies on classes of problems.

I will show examples of AI systems implementing positive feedback loops between induction and deduction, and show the performance of the current methods over large libraries of existing proof assistants such as Isabelle, Mizar, and HOL. Finally, I will mention emerging AI systems that combine statistical parsing of informal mathematics with such strong theorem proving methods.

Josef Urban is a senior researcher at the Czech Institute of Informatics, Robotics and Cybernetics (CIIRC) of the Czech Technical University in Prague where he is heading the ERC-funded project AI4REASON. His main interest is development of combined inductive and deductive AI methods over large formal (fully semantically specified) knowledge bases, such as large corpora of formally stated mathematical definitions, theorems and proofs. His systems have won several competitions in this field. He received his MSc in Mathematics and PhD in Computers Science from the Charles University in Prague, worked as an assistant professor in Prague, and as a researcher at the University of Miami and Radboud University Nijmegen.

Its **program** consists of a **one-hour lecture** followed by a **discussion**. The lecture is based on an (internationally) exceptional or remarkable achievement of the lecturer, presented in a way which is comprehensible and interesting to a broad computer science community. The lectures is in English.

**The seminar** is organized by the organizational committee consisting of Roman Barták (Charles University, Faculty of Mathematics and Physics), Michal Chytil (Czech Academy of Sciences, Computer Science Institute), Pavel Kordík (Czech Tech. Univ., Faculty of Information Technologies), Jan Kybic (Czech Tech. Univ., Faculty of Electrical Engineering), Michal Pěchouček (Czech Tech. Univ., Faculty of Electrical Engineering), Jiří Sgall (Charles University, Faculty of Mathematics and Physics), Vojtěch Svátek (University of Economics, Faculty of Informatics and Statistics), Michal Šorel (Czech Academy of Sciences, Institute of Information Theory and Automation), Tomáš Werner (Czech Tech. Univ., Faculty of Electrical Engineering), and Filip Železný (Czech Tech. Univ., Faculty of Electrical Engineering)

**The idea to organize this seminar** emerged in discussions of the representatives of several research institutes on how to avoid the undesired fragmentation of the Czech computer science community.