Registration is now open.


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, mathematics, physics, relations to general AI (AGI), Formal Abstracts, linguistic processing of mathematics/science, modern AI and big-data methods, and several sessions with contributed talks. The focused sessions will be based on invited talks and discussion oriented. Most of the sessions will be scheduled in the afternoons to allow US participants.

Confirmed (Virtual) Participants/Speakers (TBC)

Kevin BuzzardImperial College London
Miles CranmerPrinceton University
Michael R. DouglasStony Brook University
Vlad FiroiuDeepMind
Ben GoertzelSingularityNET
Georges GonthierINRIA
Thomas C. HalesUniversity of Pittsburgh
Sean HoldenUniversity of Cambridge
Mikoláš JanotaUniversity of Lisbon
Cezary KaliszykUniversity of Innsbruck
Peter KoepkeUniversity of Bonn
Michael KinyonUniversity of Denver
Ramana KumarDeepMind
David McAllesterToyota Technological Institute at Chicago
Tomáš MikolovCzech Technical University in Prague
Melanie MitchellSanta Fe Institute
Adam PeaseArticulate Software
Stanislas PoluOpenAI
Markus RabeGoogle Research
Fabian RuhleCERN
Stephan SchulzDHBW Stuttgart
David StanovskýCharles University
Martin SudaCzech Technical University in Prague
Josef UrbanCzech Technical University in Prague
Robert VeroffUniversity of New Mexico
Lucy Lu WangAllen Institute for AI
Yuhuai (Tony) WuUniversity of Toronto

Invited talks (to be completed)

Miles CranmerPrinceton University
Vlad FiroiuDeepMind
Ben GoertzelSingularityNET
Melanie MitchellSanta Fe Institute
Fabian RuhleCERN
Lucy Lu WangAllen Institute for AI

Dates (TBA)

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

Contributed talks

Boris Shminke and Wesley Fussner. Mining counterexamples for wide-signature algebras with an Isabelle server
Martin Suda. A Closer Look at Successful Clause Derivations Through the Lens of Recursive Neural Networks
Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi and Kyunghyun Cho. NaturalProofs: Mathematics meets Natural Language
Landon D. C. Elkind. Computer Verification for Historians of Philosophy
Jin Xing Lim, Barnabé Monnot, Georgios Piliouras and Shaowei Lin. (Auto)Complete this Proof: Decentralized Proof Generation via Smart Contracts
Jonathan Laurent and André Platzer. Designing a Theorem Prover for Reinforcement Learning and Neural Guidance
Yutaka Nagashima. Faster Smarter Proof by Induction in Isabelle/HOL with Definitional Quantifiers
Jakub Dakowski, Aleksandra Draszewska, Barbara Adamska, Dominika Juszczak, Łukasz Abramowicz and Robert Szymański. Creation of a modular proof assistant engine for a logic e-tutor
Adam Pease, Paulo Santos and Alexandre Rademaker. A Corpus of Spatial Reasoning Problems
Karel Chvalovský and Jan Jakubův. Characteristic Subsets of TPTP Benchmarks
Gergő Csaba Kertész, Péter Szeredi and Zsolt Zombori. Ordering Subgoals in a Backward Chaining Prover
David McAllester, Michael Douglas and Floris van Doorn. Handling Cryptomorphism in Proof Assistants and Automated Concept Formation
Albert Q. Jiang, Wenda Li, Jesse M. Han and Yuhuai Wu. LISA: Language models of ISAbelle proofs
Christian Szegedy, Markus Rabe and Henryk Michalewski. Retrieval-Augmented Proof Step Synthesis
Jelle Piepenbrock, Tom Heskes, Mikoláš Janota and Josef Urban. Learning Equational Theorem Proving
Jesse Han, Tao Xu, Stanislas Polu, Arvind Neelakantan and Alec Radford. Contrastive finetuning of generative language models for informal premise selection
Frederik Schmitt, Christopher Hahn, Jens U. Kreber, Markus N. Rabe and Bernd Finkbeiner. Deep Learning for Temporal Logics
Yuhuai Wu. Latent Action Space for Efficient Planning in Theorem Proving
Kristóf Szabó and Zsolt Zombori. Dreaming to Prove
Mikolas Janota, Antonio Morgado and Petr Vojtechovsky. Minimal Generating Sets in Magmas
Jan Hůla, David Mojžíšek and Mikolas Janota. Towards Graph Neural Networks for SMT Portfolios
Anton Lorenzen, Peter Koepke and Adrian De Lon. Dealing with Soft Types in Naproche’s Logical Backend
Mikoláš Janota, Jelle Piepenbrock and Bartosz Piotrowski. Learning SMT Enumeration
Thibault Gauthier. Synthesis of Recursive Functions from Sequences of Natural Numbers
Lasse Blaauwbroek and Herman Geuvers. ITP Automation in Practice: A User Study on Tactician
Karel Chvalovský, Jan Jakubuv, Miroslav Olšák and Josef Urban. Learning Reasoning Components
Zarathustra Goertzel, Jan Jakubuv and Josef Urban. Parental Guidance in E
Filip Bártek and Martin Suda. Project Proposal: Model-Based Optimization of Strategy Schedules
Edvard Holden and Konstantin Korovin. Representing First-order Problems for Heuristic Selection
Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Cezary Kaliszyk and Josef Urban. Decision Trees for Tactic Prediction in Coq


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 (TBC)

Jasmin Christian BlanchetteINRIA Nancy
Ulrich FurbachUniversity of Koblenz
Thibault GauthierCzech Technical University in Prague
Michael R. Douglas (co-chair)Stony Brook University
Thomas C. Hales (co-chair)University of Pittsburgh
Sean HoldenUniversity of Cambridge
Cezary Kaliszyk (co-chair)University of Innsbruck
Michael KinyonUniversity of Denver
Peter KoepkeUniversity of Bonn
Michael KohlhaseFAU Erlangen-Nürnberg
Konstantin KorovinThe University of Manchester
Ramana Kumar (co-chair)DeepMind
Adam PeaseArticulate Software
Stephan Schulz (co-chair)DHBW Stuttgart
Geoff SutcliffeUniversity of Miami
Christian SzegedyGoogle Research
Josef Urban (co-chair)Czech Technical University in Prague
Sarah WinklerUniversity of Innsbruck
Yuhuai (Tony) WuUniversity of Toronto
Zsolt ZomboriAlfréd Rényi Institute of Mathematics

Pictures from the previous conferences

Location, Prices and Further Local Information

The conference will take place from September 5 to September 10 2021 in the CNRS Paul-Langevin Conference Center located in the mountain village of Aussois in Savoy. Dominated by the "Dent Parrachée", one of the highest peaks of La Vanoise, Aussois is located on a sunny plateau at 1500 m altitude, offering a magnificent panorama of the surrounding mountains and a direct access to the downhill ski slopes or cross country slopes in winter. The total price for accommodation, food and registration for the five days will be around 600 EUR. Online participation will be most likely for free but may be limited to relevant participants.


Aussois is less than 2h from the airports of Lyon, Geneve, Chambery, Annecy, Grenoble and Turin. There are trains and buses to Modane from these airports. Aussois is 8km from the Modane TGV station with direct trains from/to Paris. We will organize a bus for the participants from there to Aussois. Further buses to these airports / station can be found here and it is easy to get a taxi from Modane to Aussois and back.

The first meal is dinner on September 5 and the last meal is lunch on Friday September 10 . There will be a full morning session on Friday. The planned departure of our bus from Modane to Aussois is at around 19:15 pm on Sunday, September 5 . The bus will wait for the TGV train from Paris arriving to Modane at 18:46. The train starts at 14:40 in Paris Gare de Lyon, and it also stops in Lyon-St Exupery at 16:38 and in Chambery-Challes-E at 17:44. The distance from Modane to Aussois is 8km and there are taxis and alternative buses.

We have not yet set the time for the departure of the bus after lunch on September 10 . This will be optimized based on your departure flights during the conference (but taking taxi back to Modane is easy). The center will close after our last session on Friday. If you want to stay for the weekend, the center recommends Hotel des Mottets which is 5 minutes from the center and their prices are very reasonable: . If you registered, please fill in this Google form to indicate if you plan to take our bus to Modane, your food preferences, whom you want to share a room with, if you plan to stay longer, etc.