Computeraided 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 oddorder theorem in group theory. Can formalization technology help us to understand the statements of complicated conjectures such as Millennium (milliondollar) 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 longterm 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 wellknown that encoding inductives
using higherorder 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 topostheoretic, 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 CurryHoward logic used in MartinLoef 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
Coauthors: 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 EilenbergMacLane 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 Links

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 badlyunderstood, including:

INI 1 
09:00 to 10:00 
Assia Mahboubi (INRIA Saclay  ÎledeFrance) Formally Verified Approximations of Definite Integrals
Coauthors: Guillaume Melquiond (Inria, Université ParisSaclay), Thomas SibutPinote (Inria, Université ParisSaclay; É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
Coauthors: 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 objectlevel 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 smallscale interactive tactics, but also more substantial kinds of automation. Related Links

INI 1  
11:00 to 11:30  Morning Coffee  
11:30 to 12:30 
Jasmin Blanchette (INRIA Nancy  Grand Est); (MaxPlanckInstitut 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 higherorder logic (Matryoshka); model finding for counterexample generation (Nunchaku); and formalization of number theory together with a mathematician. Related Links

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 Links

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''
Coauthors: 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 bruteforce 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 longstanding 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 
09:00 to 10:00 
Georges Gonthier (INRIA Saclay  ÎledeFrance) Scaffolds and frames: the MathComp algebra formal library
It is commonplace to assert that a formalization library provides aframework for formal proof development  the resusable pieces offormalized mathematics that can be reassembled to build largertheories. This role is sometimes over emphasized by the "prooflibrary" moniker, implying that the main use of the library is toavoid duplicating proof work. However, our own experience with the MathComp library refutes thislimited view. First, most proofs in the more useful theories are veryshort, which shows that the structural elements afforded by a theory,such as concepts, combinators, or notation, can be more important thanthe "proof savings". Second, some of the more useful things providedby our library don't even qualify as mathematical theories. They arebits of scaffolding, ranging from naming conventions and scriptingidioms to syntax metatheories, that help build new theories withoutproviding any identifuable parts thereof. 
INI 1  
10:00 to 11:00 
Tobias Nipkow (Technischen Universität München) Mining the Archive of Formal Proofs
Coauthors: Jasmin Christian Blanchette (Vrije Universiteit Amsterdam), Maximilian Haslbeck (Technical University Munich), Daniel Matichuk (Data61) The Archive of Formal Proofs is a vast collection of computerchecked proofs developed using the proof assistant Isabelle. We perform an indepth analysis of the archive, looking at various properties of the proof developments, including size, dependencies, and proof style. Related Links

INI 1  
11:00 to 11:30  Morning Coffee  
11:30 to 12:30 
Grant Passmore (University of Cambridge) Formal Verification of Financial Algorithms, Progress and Prospects
Many deep issues plaguing today's financial markets are symptoms of a fundamental problem: The complexity of algorithms underlying modern finance has significantly outpaced the power of traditional tools used to design and regulate them. At Aesthetic Integration, we've pioneered the use of formal verification for analysing the safety and fairness of financial algorithms. With a focus on financial infrastructure (e.g., the matching logics of exchanges and dark pools), we'll describe the landscape, and illustrate our Imandra formal verification system on a number of realworld examples. We'll sketch many open problems and future directions along the way.

INI 1  
12:30 to 13:30  Lunch @ Wolfson Court  
13:30 to 14:30  Discussion  INI 1  
14:30 to 15:30 
Mateja Jamnik (University of Cambridge) Accessible Reasoning with Diagrams: Ontology Debugging
Coauthors: Gem Stapleton (University of Brighton, UK), Zohreh Shams (University of Cambridge, UK), Yuri Sato (University of Brighton, UK) Ontologies are notoriously hard to define, express and reason about. Many tools have been developed to ease the ontology debugging and reasoning, however they often lack accessibility and formalisation. A visual representation language, concept diagrams, was developed for ex pressing ontologies, which has been empirically proven to be cognitively more accessible to ontology users. In this paper we answer the question of “How can concept diagrams be used to reason about inconsistencies and incoherence of ontologies?”. We do so by formalising a set of infer ence rules for concept diagrams that enables stepwise verification of the inconsistency and incoherence of a set of ontology axioms. The design of inference rules is driven by empirical evidence that concise (merged) diagrams are easier to comprehend for users than a set of lower level diagrams that are a onetoone translation from OWL ontology axioms. We prove that our inference rules are sound, and exemplify how they can be used to reason about inconsistencies and incoherence. Related Links

INI 1  
15:30 to 16:00  Afternoon Tea  
16:00 to 17:00 
Katya Komendenskaya (HeriotWatt University) Machine Learning for Interactive Theorem Proving: Revisit, Reuse and Recycle your Proofs
Interactive theorem proving has seen major development in the past decade, and is being widely adopted in formalisation of mathematics and in verification. Further growth and dissemination of interactive theorem proving require more intelligent tools that can make this technology more user friendly and convenient. As full automation of interactive provers is impossible, it is important to develop better heuristics that enable to data mine the existing libraries and reuse existing proof strategies when writing new proofs. In this talk, I will talk about several projects devoted to Machine Learning for Interactive Theorem Proving (in Coq and ACL2) that I participated in in the last 5 years. I will give a light survey of a variety of machine learning methods that have already been employed in these provers, and will discuss, with some help from the audience, which of those methods bear more promise for the future. In the technical part, I will also talk about ML4PG  the machine learning extension to Proof general, that I have developed in collaboration with my colleagues, its recent extension CoqPR3 and the plans to reincarnate these tools in the upcoming new version of Proof General currently developed by INRIA and at MIT. Based on the joint work with G.Grov, T.Gransden, J.Heras, M.Johansson, E.McLean, N.Walkinshaw. 
INI 1 
09:00 to 10:00 
Alison Pease (University of Dundee) The role of explanation in mathematical research
Coauthors: Andrew Aberdein (Florida Institute of Technology), Ursula Martin (University of Oxford) Mathematical practice is an emerging interdisciplinary field which draws on philosophy and social science to understand how mathematics is produced. Online mathematical activity provides a novel and rich source of data for empirical investigation of mathematical practice  for example the community question answering system MathOverflow contains nearly 70,000 mathematical conversations, and polymath collaborations provide transcripts of the process of discovering proofs. Our preliminary investigations have demonstrated the importance of "soft" aspects such as analogy and creativity, alongside deduction and proof, in the production of mathematics, and have given us new ways to think about the roles of people and machines in creating new mathematical knowledge. We discuss our investigations into these resources, focusing on ways in which explanation and argumentation are used by mathematicians in both proofs and other mathematical contexts. 
INI 1  
10:00 to 11:00 
Michael Kohlhase (Jacobs University Bremen) Lightweight and Heavyweight Methods for Integrating Mathematical Libraries
Arguably, the most crucial resource for scaling up
mathematical proof to the Internet age is the availability of machineactionable libraries of mathematical knowledge as well as information systems and semantic services based on these libraries. There are various mathematical knowledge collections and information systems available. They range from completely informal ones like Wikipedia or the Cornell arXiv, zbMath, and MathSciNet via mathematical object databases like the GAP group libraries, the Online Encyclopedia of Integer sequences (OEIS), and the Lfunctions and Modular Forms Database (LMFDB) to theorem prover libraires like those of Mizar, Coq, PVS, and the HOL systems. Unfortunately, while all of these individually constitute steps into the direction of research data, they attack the problem at different levels (object, vs. document level) and direction (description vs. classificationbased) and are mutually incompatible and notinterlinked/aligned systematically. I will survey methods and systems which can act as stepping stones towards unifying these seeds into a Global Digital Library of Mathematics. These methods and systems are inherently of flexible formality (flexiformal) and range from heavyweight methods like developing modular metalogical formats for corepresenting logics and libraries in a common global meaningspace via all kinds of library translations to lightweight methods for aligning and crosslinking such libraries. I will exemplify the methods on pragmatic examples (e.g. translating LaTeX to HTML5 for arXiv.org importing PVS to OMDoc/MMT, or parsing the OEIS) and discuss the infrastructures we need for managing a global, flexiformal digital mathematical mathematical library. 
INI 1  
11:00 to 11:30  Morning Coffee  
11:30 to 12:30 
Jacques Fleuriot (University of Edinburgh) Proof Archeology: Historical Mathematics from an Interactive Theorem Proving Standpoint
The active study of historical mathematics is often viewed as being of peripheral interest to the working mathematician. The original work is instead recast within modern notation and standards of rigour, with the new formulation becoming the authoritative approach, while the analysis of the source text is left to historians. Although this is not inherently bad, since mathematical descriptions and ideas can become obsolete, one may argue that in the case of mathematical expositions that have shaped the field there is still much to be gained by going back to original sources. In this talk, we argue that interactive theorem proving can be an effective tool for the systematic analysis of such historical mathematics. It not only provides a rigorous means of investigating the original texts but can also act as a framework for formally reconstructing the proofs in ways that often respect the original reasoning, while eliciting steps and lemmas that can shine new light on the results. Synergistically, such reconstructions also often push the boundaries of formalized mathematics, resulting in new libraries and in the improvement, or even reformulation, of existing ones. We support our claims by examining proofs from Euler’s Introductio in Analysin Infinitorum (the "Introductio") published in 1748. In this, using what he calls “ordinary algebra”, he (algorithmically) derives the series for the exponential and trigonometric functions, and proves Euler’s Formula among many other classic results. We describe how Euler’s deft algebraic manipulations of infinitesimals and infinite numbers can be formally restored in the Isabelle theorem prover and argue that Euler was not as heedless as some have claimed. Related Links

INI 1  
12:30 to 13:30  Lunch @ Wolfson Court  
13:30 to 14:30 
Stephanie Dick (Harvard University) After Math: Reasoning, Computing, and Proof in the Postwar United States (via Skype)
Computers ought to produce in the long run some
fundamental change in the nature of all mathematical activity.” These words,
penned in 1958, capture the motivation behind an early field of computing
research called Automated TheoremProving or Automated Reasoning. Practitioners
of this field sought to program computers to prove mathematical theorems or to
assist human users in doing so. Everyone working in the field agreed that
computers had the potential to make novel contributions to the production of
mathematical knowledge. They disagreed about almost everything else. Automated
theoremproving practitioners subscribed to complicated and conflicting visions
of what ought to count and not count as a mathematical proof. There was also
disagreement about the character of human mathematical faculties  like
intuition, understanding, and reasoning  and how much the computer could be
made to possess them, if at all. Different practitioners also subscribed to
quite different imaginations of the computer itself, its limitations and
possibilities. Some imagined computers as mere plodding “slaves” who would take
over tedious and mechanical elements of mathematical research. Others imagined
them more generously as “mentors” or “collaborators” that could offer novel
insight and direction to human mathematicians. Still others believed that
computers would eventually become autonomous agents of mathematical research.
Automated theoremproving practitioners took their visions of mathematicians,
minds, computers, and proof, and built them right in to their theoremproving
programs. Their efforts did indeed precipitate transformations in the character
of mathematical activity but in varied and often surprising ways. They crafted
new formal and material tools and practices for wielding them that reshaped the
work of proof. They also reimagined what “reasoning” itself might be and what
logics capture or prescribe it. With a focus on communities based in the United
States in the second half of the twentieth century, this talk will introduce
different visions the novel practices and materialities of mathematical
knowledgemaking that emerged in tandem.

INI 1  
14:30 to 15:30 
William Timothy Gowers (University of Cambridge); Natarajan Shankar ; Patrick Ion (University of Michigan) Panel on future directions for Big Proof
The ambitious goal of the Newton Institute Big Proof programme is to bring together mathematicians, logicians, and
computer scientists engaged in developing and applying proof technology. This
panel will draw together the thinking of the workshop participants as a contribution
to a key expected output of the programme: a concrete, longterm research
agenda for making computational inference a basic technology for formalising,
creating, curating, and disseminating mathematical knowledge in digital form. Chair: Natarajan Shankar, Lead organiser of the Newton Institute Big Proof programme, a staff scientist in the Computer Science Laboratory at SRI International and creator of the PVS verification system. Panellists to include Professor Sir Tim Gowers FRS, Fields medallist and widely read thinker on mathematical issues, and Dr Patrick Ion, formerly editor of Mathematical Reviews, and founding member of the IMU’s " International Mathematical Knowledge Trust” 
INI 1  
15:30 to 16:00  Afternoon Tea  
16:00 to 17:00 
William Timothy Gowers (University of Cambridge); Natarajan Shankar ; Patrick Ion (University of Michigan) Panel on future directions for Big Proof
The ambitious goal of the Newton Institute Big Proof programme is to bring together mathematicians, logicians, and
computer scientists engaged in developing and applying proof technology. This
panel will draw together the thinking of the workshop participants as a contribution
to a key expected output of the programme: a concrete, longterm research
agenda for making computational inference a basic technology for formalising,
creating, curating, and disseminating mathematical knowledge in digital form. Chair: Natarajan Shankar, Lead organiser of the Newton Institute Big Proof programme, a staff scientist in the Computer Science Laboratory at SRI International and creator of the PVS verification system. Panellists to include Professor Sir Tim Gowers FRS, Fields medallist and widely read thinker on mathematical issues, and Dr Patrick Ion, formerly editor of Mathematical Reviews, and founding member of the IMU’s " International Mathematical Knowledge Trust” 
INI 1 