Registration is now closed.


Large-scale semantic processing and strong computer assistance of mathematics and science is our inevitable future. New combinations of AI and reasoning methods and tools deployed over large mathematical and scientific corpora will be instrumental to this task. The AITP conference is the forum for discussing how to get there as soon as possible, and the force driving the progress towards that.



There will be several focused sessions on AI for ATP, ITP and mathematics, modern AI and big-data methods, and several sessions with contributed talks. The focused sessions will be based on invited talks and discussion oriented.

Confirmed participants/speakers (TBC)

Wolfgang BibelDarmstadt University of Technology
Kevin BuzzardImperial College London
Ben GoertzelSingularityNET
Georges GonthierINRIA
Thomas C. HalesUniversity of Pittsburgh
Sean HoldenUniversity of Cambridge
Mikoláš JanotaUniversity of Lisbon
Chris KapulkinUniversity of Western Ontario
Michael KinyonUniversity of Denver
Angeliki Koutsoukou-ArgyrakiUniversity of Cambridge
Ramana KumarDeepMind
Sarah LoosGoogle Research
David McAllesterToyota Technological Institute at Chicago
Tomáš MikolovFacebook AI Research
Scott MorrisonAustralian National University
Arnold NeumaierUniversity of Vienna
Adam PeaseInfosys
Joao Marques SilvaUniversity of Lisbon
Martin SudaCzech Technical University in Prague
Ilya SutskeverOpenAI
Christian SzegedyGoogle Research

Contributed talks

Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine and Hans-Jörg Schurr: Better SMT Proofs for Easier Reconstruction
Luis Berlioz: Project Proposal: Creating a Database of Definitions From Large Mathematical Corpora
Lasse Blaauwbroek: Tactic Learning for Coq
Chad Brown, Thibault Gauthier and Josef Urban: Translating from Higher-Order to Higher-Order
David Cerna: Towards A New Type of Prover: On the Benefits of Discovering Sequences of ``Related'' Proofs
Jasmin Christian Blanchette, Daniel El Ouraoui, Pascal Fontaine and Cezary Kaliszyk: Machine learning for instance selection in SMT solving
Karel Chvalovský, Thibault Gauthier and Josef Urban: First Experiments with Data Driven Conjecturing
Yassmeen Elderhalli, Osman Hasan and Sofiene Tahar: Using Machine Learning to Minimize User Intervention in Theorem Proving based Dynamic Fault Tree Analysis
Steffen Frerix and Peter Koepke: Making Set Theory Great Again: The Naproche-SAD Project
Thibault Gauthier and Josef Urban: Arithmetical Mini-Games
Edvard Holden and Konstantin Korovin: SMAC and XGBoost your Theorem Prover
Jan Jakubuv and Josef Urban: Clause Features for Theorem Prover Guidance
Robert Kahlert, Bettina Berendt and Benjamin Rode: Beyond Surface Event Representation
Alexei Lisitsa: Automated Reasoning for the Andrews-Curtis Conjecture
Dennis Müller, Florian Rabe and Michael Kohlhase: How to Leverage a Large Dataset of Formalized Mathematics with Machine Learning?
Yutaka Nagashima: Towards Machine Learning Induction
Julian Parsert, Stephanie Autherith and Cezary Kaliszyk: Teaching the Structure of First-order Formulas to Neural Networks
Adam Pease: Arithmetic and Inference in a Large Theory
Bartosz Piotrowski, Chad Brown, Josef Urban and Cezary Kaliszyk: Can Neural Networks Learn Symbolic Rewriting?
Michael Rawson and Giles Reger: Towards an Efficient Architecture for Intelligent Theorem Provers
Giles Reger and Martin Suda: Can a Failed Strategy be Useful?
Aleksandra Samonek: Focusing proofs and logics for models of computation
Martin Smolík and Josef Urban: Project Proposal: Neural Modelling of Mathematical Structures
Robert Veroff, Josef Urban and Michael Kinyon: Hint Selection and Prioritization
Qingxiang Wang, Cezary Kaliszyk and Josef Urban: Exploration of Machine Translation Techniques in Auto-formalization of Mathematics: Experiment Proposal
Sarah Winkler: Maedmax at School: Learning Selection in Equational Reasoning
Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk and Josef Urban: Curriculum Learning and Theorem Proving


AITP solicits contributed talks. Selection of those will be based on extended abstracts/short papers of 2 pages formatted with easychair.cls. Submission is via EasyChair ( Accepted contributions will be published in an informal book of abstracts for distribution at the conference.


We will consider an open call for post-proceedings in an established series of conference proceedings (LIPIcs, EPiC, JMLR) or a journal (AICom, JAR, JAIR).

Program Committee

Jasmin Christian BlanchetteINRIA Nancy
Ulrich FurbachUniversity of Koblenz
Thomas C. Hales (co-chair)University of Pittsburgh
Sean HoldenUniversity of Cambridge
Mikoláš JanotaUniversity of Lisbon
Moa JohanssonChalmers University
Cezary Kaliszyk (co-chair)University of Innsbruck
Michael KohlhaseFAU Erlangen-Nürnberg
Konstantin KorovinThe University of Manchester
Ramana Kumar (co-chair)DeepMind
Claudio Sacerdoti CoenUniversity of Bologna
David McAllesterToyota Technological Institute at Chicago
Adam PeaseInfosys
Stephan Schulz (co-chair)DHBW Stuttgart
Geoff SutcliffeUniversity of Miami
Christian SzegedyGoogle Research
Josef Urban (co-chair)Czech Technical University in Prague

Arrival and departure

Location, Prices and Further Local Information

The conference will take place from April 7 to April 12 in the stunning scenery of the Tyrolean Alps in the Obergurgl Conference Center of the University of Innsbruck. The pictures of the rooms are here. Obergurgl is a picturesque village located at an altitude of 2000m, a 1-hour drive from Innsbruck. It offers a variety of winter-sport activities such as skiing, snowshoeing and hiking at this time of the year. The total price for accommodation in a twin room (based on 2-person occupancy), food (half-board) and registration for the five days will be around 670 EUR. There are also several hotels in Obergurgl - booking early is recommended.

Hotels in Innsbruck

If you stay in Innsbruck before/after the conference, we recommend the following hotels, we have good experience with

Skiing equipment and passes

You can rent skis/snowboards/boots/helmets in Obergurgl or already in Innsbruck. It might be hard to rent clothing in Obergurgl, but it is possible in Innsbruck (e.g., here).
Ski+Boots rental per day: 30-50Euros per day (depending on the quality).
Obergurgl daily ski passes: From noon: 40Euros. From 11am: 45Euros. 3 days: 143Euros

Here are two photos from 2016 showing the skiing conditions and the village (with the conference center hidden on the right side of the photo) taken in April.

Acknowledgements and Sponsorship

We thank the University of Innsbruck for their support of the Obergurgl conference center.