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.

- AI and big-data methods in theorem proving and mathematics
- Collaboration between automated and interactive theorem proving
- Common-sense reasoning and reasoning in science
- Alignment and joint processing of formal, semi-formal, and informal libraries
- Methods for large-scale computer understanding of mathematics and science
- Combinations of linguistic/learning-based and semantic/reasoning methods

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.

Cameron Freer | Priors on propositions: towards probabilistic programming for theorem proving |

Georges Gonthier | Formalising mathematical conventions |

Thomas C. Hales | F-ABSTRACTS (formal abstracts) - project introduction and discussion |

John Harrison | What has Artificial Intelligence Ever Done For Us (Formalizers)? |

Andreas Holmstrom | Number-theoretic conjecturing via zeta types and Tannakian symbols |

Michael Kohlhase | Tapping Sources of Mathematical (Big) Data |

David McAllester | Models of Mentalese |

Tim Rocktäschel | Deep Prolog: End-to-end Differentiable Proving in Knowledge Bases |

Stephan Schulz | Deep Reasoning - A Vision for Automated Deduction |

Luciano Serafini | Logic Tensor Networks |

Martin Suda | Measuring progress to predict success: Can a good proof strategy be evolved? |

Sarah Loos | Can Deep Learning Help Formal Reasoning? |

Alexander Bentkamp, Jasmin Christian Blanchette and Dietrich Klakow: An Isabelle Formalization of the Expressiveness of Deep Learning |

Chad Brown: Problems from the Grundlagen |

Przemyslaw Chojecki: DeepAlgebra - an outline of a program |

Joe Corneli and Moritz Schubotz: math.wikipedia.org: A vision on a collaborative semi-formal, language independent math(s) encyclopedia |

Michael Färber, Cezary Kaliszyk and Josef Urban: Monte Carlo Connection Prover |

Jan Jakubuv, Josef Urban and Robert Veroff: Towards AI Methods for Prover9 |

Eugen Kuksa: Logic-Independent Premise Selection for Autormated Theorem Proving |

Ramana Kumar and Benya Fallenstein: Applying Formal Verification to Reflective Reasoning |

Yutaka Nagashima Towards Smart Proof Search for Isabelle |

Karol Pąk and Aleksy Schubert: Greedy Algorithms for Finding Maximum Number of Then Step in Reasoning |

Bruno Woltzenlogel Paleo and John Slaney: Proof Search in Conflict Resolution |

Marwin Segler and Mark Waller: Chemical Discovery as a Knowledge Graph Completion Problem |

Josef Urban and Jiri Vyskocil: Progress in Automating Formalization |

~~Submission deadline: December 1, 2016~~~~Author notification: December 23, 2016~~- Conference registration: January 20, 2017
- Camera-ready versions: February 1, 2017
- Conference: March 26-30, 2017

The (extended) abstracts of all the invited and contributed talks are now available online.

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).

Noriko Arai | National Institute of Informatics |

Jasmin Christian Blanchette | INRIA Nancy |

Ulrich Furbach | University of Koblenz |

Deyan Ginev | Jacobs University Bremen and Authorea |

Thomas C. Hales (co-chair) | University of Pittsburgh |

Sean Holden | University of Cambridge |

Geoffrey Irving | |

Cezary Kaliszyk (co-chair) | University of Innsbruck |

Jens Otten | University of Oslo |

Claudio Sacerdoti Coen | University of Bologna |

Stephan Schulz (co-chair) | DHBW Stuttgart |

Geoff Sutcliffe | University of Miami |

Josef Urban (co-chair) | Czech Technical University in Prague |

- A bus bringing the participants from Innsbruck to the conference center and back is provided.
- On Sunday the 26th the bus will depart from Innsbruck Central station at 10:45am, leave from the airport at 11:15 am and continue to Obergurgl.
**Please note the time change which happens in Europe on the night 25/26th March.**- If you want to join the bus at the train station look for the Info-Point. There, you will find the bus driver with the sign "University Center Obergurgl" as well as some of the University of Innsbruck organizers.
- If you want to join the bus at the airport, the bus will stop in front of the terminal, it will have the "Obergurgl" sign, and there will be organizers joining the bus as well.
- We expect to reach the conference center around 1pm, and after checking and lunch the first session will start at 3pm.
- On Thursday: check-out by 10am, bus leaves at 10:30, arrival in Innsbruck between 12:30 and 13:30 (depends on weather conditions and traffic). The bus will first stop at the airport and then in the city center (main railway station).

13:00-15:00 | lunch and check-in |

15:00-16:30 |
Welcome John Harrison What has Artificial Intelligence Ever Done For Us (Formalizers)?Stephan Schulz Deep Reasoning - A Vision for Automated Deduction |

16:30-17:00 | coffee break |

17:00-18:30 |
Sarah LoosCan Deep Learning Help Formal Reasoning?Tim Rocktäschel Deep Prolog: End-to-end Differentiable Proving in Knowledge Bases |

19:00 | dinner |

8:30-10:00 |
Georges GonthierFormalising mathematical conventionsThomas C. Hales F-ABSTRACTS (formal abstracts) - project introduction and discussion |

10:00-10:30 | coffee break |

10:30-11:45 |
Michael KohlhaseTapping Sources of Mathematical (Big) DataJosef Urban and Jiri Vyskocil Progress in Automating Formalization |

11:45-16:00 | free time |

16:00-16:30 | coffee break |

16:30-18:45 |
Andreas HolmstromNumber-theoretic conjecturing via zeta types and Tannakian symbolsPrzemyslaw Chojecki DeepAlgebra - an outline of a programshort break Marwin Segler and Mark Waller Chemical Discovery as a Knowledge Graph Completion ProblemJoe Corneli and Moritz Schubotz math.wikipedia.org: A vision on a collaborative semi-formal, language independent math(s) encyclopedia |

19:00 | dinner |

8:30-10:00 |
Luciano SerafiniLogic Tensor NetworksDavid McAllester Mathematics, Ontology and Reference |

10:00-10:30 | coffee break |

10:30-12:00 |
Ramana Kumar and Benya FallensteinApplying Formal Verification to Reflective ReasoningAlexander Bentkamp, Jasmin Christian Blanchette and Dietrich Klakow An Isabelle Formalization of the Expressiveness of Deep LearningYutaka Nagashima Towards Smart Proof Search for Isabelle |

12:00-17:20 | free time |

17:20-18:30 |
AITP Discussion or free time |

19:00 | dinner |

8:30-10:00 |
Cameron FreerPriors on propositions: towards probabilistic programming for theorem provingMartin Suda Measuring progress to predict success: Can a good proof strategy be evolved? |

10:00-10:30 | coffee break |

10:30-11:30 |
Jan Jakubuv and Robert VeroffTowards AI Methods for Prover9Michael Färber Monte Carlo Connection Prover |

11:30-16:00 | free time |

16:00-16:30 | coffee break |

16:30-18:40 |
Chad BrownProblems from the GrundlagenEugen Kuksa Logic-Independent Premise Selection for Autormated Theorem Provingshort break Karol Pąk and Aleksy Schubert Greedy Algorithms for Finding Maximum Number of Then Step in ReasoningBruno Woltzenlogel Paleo and John Slaney Proof Search in Conflict Resolution |

19:00 | dinner |

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