09:00 to 10:00 Assia Mahboubi (INRIA Saclay - Île-de-France)Formally Verified Approximations of Definite Integrals Co-authors: Guillaume Melquiond (Inria, Université Paris-Saclay), Thomas Sibut-Pinote (Inria, Université Paris-Saclay; École polytechnique) Finding an elementary form for an antiderivative is often a difficult task, thus numerical integration is a common tool when it comes to making sense of a definite integral. Some of the numerical integration methods can even be made rigorous: not only do they compute an approximation of the integral value but they also bound its inaccuracy. Yet numerical integration is still missing from the toolbox when performing formal proofs in analysis, but also in other areas of mathematics that shall involve the evaluation of some integrals like number theory, dynamical systems... In this talk, we describe and discuss an efficient method for automatically computing and proving bounds on some definite integrals inside the Coq proof assistant. INI 1 10:00 to 11:00 Leonardo de Moura (Microsoft (UK))Metaprogramming with Dependent Type Theory Co-authors: Gabriel Ebner (Vienna University of Technology), Sebastian Ullrich (Karlsruhe Institute of Technology), Jared Roesch (University of Washington), Jeremy Avigad (Carnegie Mellon University) Dependent type theory is a powerful framework for interactive theorem proving and automated reasoning, allowing us to encode mathematical objects, data type specifications, assertions, proofs, and programs, all in the same language. Here we show that dependent type theory can also serve as its own metaprogramming language, that is, a language in which one can write programs that assist in the construction and manipulation of terms in dependent type theory itself. Specifically, we describe the metaprogramming language currently in use in the Lean theorem prover, which extends Lean's object language with an API for accessing internal procedures and provides ways of reflecting object-level expressions into the metalanguage. We provide evidence to show that our language is performant, and that it provides a convenient and flexible way of writing not only small-scale interactive tactics, but also more substantial kinds of automation. Related Linkshttps://leanprover.github.io/ - Lean website INI 1 11:00 to 11:30 Morning Coffee 11:30 to 12:30 Jasmin Blanchette (INRIA Nancy - Grand Est); (Max-Planck-Institut für Informatik, Saarbrücken)Hammers and Model Finders, and Beyond Integrations of automatic theorem provers in proof assistants -- in the form of "hammers" -- are useful to formalize arbitrary mathematics. I will briefly talk about the experience we have with Sledgehammer and then focus on two ongoing project in which I am involved and a future one (modulo funding): automation of higher-order logic (Matryoshka); model finding for counterexample generation (Nunchaku); and formalization of number theory together with a mathematician. Related Linkshttp://matryoshka.gforge.inria.fr - Matryoshka project INI 1 12:30 to 13:30 Lunch @ Wolfson Court 13:30 to 14:30 Discussion INI 1 14:30 to 15:30 Ursula Martin (University of Oxford)The social machine of mathematics How does mathematics come about? Formal proof is only part of the story, and in this paper I present the results of highly interdisciplinary work, using philosophy, social scence and history alongside computer science research in artificial intelligence, argumentation theory and verification, to show the scope for new techniques to support concept formation and argument finding, while highlighting the roles that risk, doubt, error, explanation and group knowledge play in the human production and use of mathematics. Related Linkshttps://www.cs.ox.ac.uk/people/ursula.martin/- Ursula Martin, University of Oxford INI 1 15:30 to 16:00 Afternoon Tea 16:00 to 17:00 Marijn Heule (University of Texas at Austin)Everything's Bigger in Texas: The Largest Math Proof Ever'' Co-authors: Oliver Kullmann (Swansea University) and Victor Marek (University of Kentucky)Many search problems, from artificial intelligence to combinatorics, explore large search spaces to determine the presence or absence of a certain object. These problems are hard due to combinatorial explosion, and have traditionally been called infeasible. The brute-force method, which at least implicitly explores all possibilities, is a general approach to search systematically through such spaces. Brute force has long been regarded as suitable only for simple problems. This has changed in the last two decades, due to the progress in satisfiability (SAT) solving, which renders brute force into a powerful approach to deal with many problems easily and automatically.We illustrate the strength of SAT via the Boolean Pythagorean Triples problem, which has been a long-standing open problem in Ramsey Theory. Our parallel SAT solver allowed us to solve the problem on a cluster in about two days using 800cores, demonstrating its linear time speedup on many hard problems. Due to the general interest in this mathematical problem, our result requires a formal proof. Exploiting recent progress in unsatisfiability proof checking, we produced and verified a clausal proof of the smallest counterexample, which is almost 200 terabytes in size. These techniques show great promise for attacking a variety of challenging problems arising in mathematics and computer science. INI 1 19:30 to 22:00 Formal dinner at Emmanuel College