# Timetable (BPRW01)

## Computer-aided mathematical proof

Monday 10th July 2017 to Friday 14th July 2017

 09:00 to 09:50 Registration 09:50 to 10:00 Welcome from Christie Marr (INI Deputy Director) 10:00 to 11:00 Thomas Hales (University of Pittsburgh)Big Conjectures Proof assistants have been used to verify complicated proofs such as the Kepler conjecture in discrete geometry and the odd-order theorem in group theory. Can formalization technology help us to understand the statements of complicated conjectures such as Millennium (million-dollar) problems of the Clay Institute, the geometric Langlands conjecture, or the Kelvin problem for optimal partitions of space? INI 1 11:00 to 11:30 Morning Coffee 11:30 to 12:30 Vladimir Voevodsky (Institute for Advanced Study, Princeton)UniMath - its present and its future. UniMath refers to several things. It is a univalent foundation of mathematics. It is the subset of Coq in which this foundation is currently implemented and it is a library of formalized mathematics written using this implementation. My talk will be mostly about the library. I will give examples of problems whose constructions have been recently formalized in the UniMath as study problems by graduate students. I will give an example of a more complex problem whose construction has been recently formalized as a part of a paper accepted to a conference proceedings. Finally, I will outline a direction for the future development of the UniMath that requires constructions to considerably more complex problems that can only be stated in the univalent type theory and, as far as I know, have never been solved either formally or informally. INI 1 12:30 to 13:30 Lunch @ Wolfson Court 13:30 to 14:30 Discussion INI 1 14:30 to 15:30 Larry Paulson (University of Cambridge)Proof Assistants: From Symbolic Logic To Real Mathematics? Mathematicians have always been prone to error. As proofs get longer and more complicated, the question of correctness looms ever larger. Meanwhile, proof assistants — formal tools originally developed in order to verify hardware and software — are growing in sophistication and are being applied more and more to mathematics itself. When will proof assistants finally become useful to working mathematicians? Mathematicians have used computers in the past, for example in the 1976 proof of the four colour theorem, and through computer algebra systems such as Mathematica. However, many mathematicians regard such proofs as suspect. Proof assistants (e.g. Coq, HOL and Isabelle/HOL) are implementations of symbolic logic and were originally primitive, covering only tiny fragments of mathematical knowledge. But over the decades, they have grown in capability, and in 2005, Gonthier used Coq to create a completely formal proof of the four colour theorem. More recently, substantial bodies of mathematics have been formalised. But there are few signs of mathematicians adopting this technology in their research. Today's proof assistants offer expressive formalisms and impressive automation, with growing libraries of mathematical knowledge. More however must be done to make them useful to mathematicians. Formal proofs need to be legible with a clear connection to the underlying mathematical ideas. INI 1 15:30 to 16:00 Afternoon Tea 16:00 to 17:00 Stephen Watt (University of Waterloo)Mathematical Knowledge at Scale The world's largest organism is a clonal colony of quaking aspen in Utah, with some 40,000 trunks spanning 43 hectares and massing an estimated 6,000 metric tons.  This is not a forest of individuals, but a single, living organism.  We may think of mathematical knowledge in the same way.   It is the goal of the International Mathematical Knowledge Trust (IMKT) to develop a global digital mathematics library, not as a comprehensive collection of individual articles, but as an integrated knowledge base, both for human readers and machine services.   This talk presents the goals of the IMKT, the direction of its first steps, challenges to be overcome, and a long-term picture of scalable mathematical knowledge integration. INI 1 17:00 to 18:00 Welcome Wine Reception at INI
 09:00 to 10:00 Steve Awodey (Carnegie Mellon University)Impredicative encodings in HoTT We investigate the prospects for impredicative encodings of inductive types (including higher inductive types) in HoTT.  It is well-known that encoding inductives using higher-order quantification provides a potential theoretical and practical simplification of the system.  Using the further resources available in HoTT allows for a sharpening of the familiar System F style impredicative encodings of inductive types, but this begs the question of whether impredicativity is formally compatible with univalence.  We give a realizability model using a combination of topos-theoretic, homotopical, and recent cubical methods.  Joint work with Jonas Frey and Pieter Hofstra. INI 1 10:00 to 11:00 Martin Escardo (University of Birmingham)Logic in univalent type theory We explain and illustrate the logic used in univalent type theory, and we compare it to the usual Curry-Howard logic used in Martin-Loef type theory. INI 1 11:00 to 11:30 Morning Coffee 11:30 to 12:30 Floris van Doorn (Carnegie Mellon University)Homotopy Type Theory in Lean Co-authors: Ulrik Buchholtz (TU Darmstadt), Jakob von Raumer (University of Nottingham) We discuss the homotopy type theory library in the Lean proof assistant. The library is especially geared toward synthetic homotopy theory, and contains many results in that area, among which are the computation of , a formalization of Eilenberg-MacLane spaces and the adjunction of pointed maps and the smash product. We have a novel method of implementing higher inductive types (HITs), where we only take two HITs as primitives and add their computation rules to the kernel of Lean. We define all other HITs in terms of these two primitive ones. Other features include the use of cubical methods, a large algebraic hierarchy and category theory library. Related Linkshttps://github.com/leanprover/lean2/blob/master/hott/hott.md  - The Lean HoTT libraryhttps://github.com/cmu-phil/Spectral  - The Spectral Sequences project INI 1 12:30 to 13:30 Lunch @ Wolfson Court 13:30 to 14:30 Discussion INI 1 14:30 to 15:30 Dan Licata (Wesleyan University)Small Proofs There is an old idea in programming languages that the right way to solve a problem is to (1) design and implement a programming language in which solving the problem is easy, and then (2) write the program in that language. Some applications of homotopy type theory to the formalization of mathematics have this flavor: First, we design a type theory and study its semantics. Then, we use that type theory, including features such as the univalence axiom, higher inductives types, interval objects, and modalities, as a language where it is easy to talk about certain mathematical structures, which enables short formalizations of some theorems. In this talk, I will give a flavor for what this looks like, using examples drawn from homotopy, cubical, and cohesive type theories. I hope to stimulate a discussion about the pros and cons of factoring the formalization of mathematics through the design of new programming languages/logical systems. INI 1 15:30 to 16:00 Afternoon Tea 16:00 to 17:00 Peter LeFanu Lumsdaine (Stockholm University)Schemas and semantics for Higher Inductive Types Higher inductive types are now an established tool of homotopy type theory, but many important questions about them are still badly-understood, including:can we set out a scheme defining “general HITs”, analogously to how CIC defines “general inductive types”?can we find a small specific collection of HITs from which one can construct “all HITs”, analogously to how the type-formers of MLTT suffice for inductive types?how can we model HITs (specific or general) in interesting homotopical settings?I will survey these questions and present what I know of progress on them (in particular, the cell monads semantics of Lumsdaine/Shulman https://arxiv.org/abs/1705.07088); I will also open the floor for interested audience members to briefly present other current work on these topics. INI 1
 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