Seminars (BPR)

 In the first part of the talk, I will try to compare the way mathematical collectionsare represented in set theory, simple type theory, dependent type theory and finallyunivalent type theory. The main message is that the univalence axiom is a strongform of extensionality, and that extensionality axiom is important for modularisationof concepts and proofs. The goal of this part is to explain to people familiar to simpletype theory why it might be interesting to extend this formalism with dependent types and the univalence axiom. 
The second part will try to explain in what way we can see models of univalent typetheory as generalisations of R. Gandy’s relative consistency proof of the extensionalityaxioms for simple type theory.

Hilbert 17th problem asks whether a polynomial taking   only non-negative values is a sum of squares (in the field of   rational functions).  Its positive solution around 1925 by Artin   does not make it possible to construct the sum of squares. Since   then, some progress made it possible to give such contructions and   to bound the degrees of the polynomials appearing in the sum of   squares. An explicit recent proof gives elementary recursive degree   bounds. The method of construction illustrates the current renewal   of constructive algebra.

15:30-16:30: Thierry Coquand (Chalmers), "Cubical stacks"

16:30-17:30: Egbert Rijke (CMU), “Colimits, descent and equifibrant replacement”

It is essential in Isabelle's analysis library has special support to handle continuity, measurability, and differentiability, etc. This is quite different to *big* automation like SMT or what Sledgehammer does.

Type theory is often referred to as the internal language of higher categories. This covers a range of ideas: results from HoTT can be interpreted in a variety of higher-categorical settings, and conversely, many higher-categorical notions can be expressed and studied in type theory. In this talk, I will report on the progress towards a single master theorem subsuming many of these informal statements.

We will give an overview of the UniMath language and library.

An overview of the homotopy type theory library in Lean, in comparison towards the other proof assistants available for HoTT. This talk is more aimed towards the HoTT community. A second talk will be given during the workshop which is more aimed towards the formal verification community.

The ACL2 theorem prover is an interactive  automatic prover for the programming language Common  Lisp.  It provides a convenient language for building  prototypes of hardware and software designs,  algorithms, and other computing systems.  In fact, the  language is executed efficiently enough to permit some  practical systems to be built in it.  But ACL2 also  provides an environment for proving theorems about  those prototypes.  In this talk I will demonstrate how  ACL2 presents itself to the user, show a small example  proof project about low-level code, and discuss the  aspects of ACL2 that have made it attractive as a tool  for industry.

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? 

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. 

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.

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 Links

• https://github.com/leanprover/lean2/blob/master/hott/hott.md  - The Lean HoTT library
• https://github.com/cmu-phil/Spectral  - The Spectral Sequences project

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.

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 Links

• https://leanprover.github.io/ - Lean website

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

• https://www.cs.ox.ac.uk/people/ursula.martin/- Ursula Martin, University of Oxford

  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.

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 real-world examples. We'll sketch many open problems and future directions along the way.

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 Coq-PR3 and the plans to re-incarnate 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.

Arguably, the most crucial resource for scaling up mathematical proof to
the Internet age is the availability of machine-actionable 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 L-functions 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.
classification-based) and are mutually incompatible and
not-interlinked/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 meta-logical formats for co-representing logics and
libraries in a common global meaning-space via all kinds of library
translations to lightweight methods for aligning and cross-linking 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.

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 Theorem-Proving 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 theorem-proving 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 theorem-proving practitioners took their visions of mathematicians, minds, computers, and proof, and built them right in to their theorem-proving 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 knowledge-making that emerged in tandem.

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, long-term 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”

This talk will give an overview of SMTCoq, a plug-in for the integration of external solvers into the Coq proof assistant. Based on a checker for general first-order proof certificates fully implemented and proved correct in Coq, SMTCoq has two main functionalities: (i) act as a trustworthy checker for proof certificates produced by SAT or SMT solvers, (ii) increase the level of automation in Coq by dispatching selected Coq subgoals to such solvers and incorporating their proof, all in a safe way. The current version of SMTCoq supports proof certificates produced by the SAT solver ZChaff, for propositional logic, and the SMT solvers veriT and CVC4, for the quantifier-free fragment of the combined theory of fixed-size bit vectors, functional arrays with extensionality, linear integer arithmetic, and uninterpreted function symbols.
The talk will discuss SMTCoq's philosophy and architecture, and will provide some technical details on the integration of CVC4 as well as examples of automated goal discharging based on combined calls to CVC4 and veriT.

The talk is based on joint work with Burak Ekici, Alain Mebsout, Chantal Keller, Guy Katz, Andrew Reynolds, and Clark Barrett.

When recently investigating an intuitionistic fragment of Lukasiewicz logic [1-4], we were able to discover several interesting theorems of this logic by searching for valid equations in the algebra of hoops. Our search for valid equations or counter-models was done using prover9 and mace4 (https://www.cs.unm.edu/~mccune/mace4/). In this talk I will describe some of the results obtained, mainly around double negation translations of the classical logic into the intuitionistic counter-part, but also the process by which we managed to translate prover9 equational proofs into human readable (and hopefully understandable) proofs.

Joint work with Rob Arthan.

[1] R Arthan and P Oliva, Negative translations for affine and Lukasiewicz logic, under review (http://www.eecs.qmul.ac.uk/~pbo/papers/paper045.pdf)
[2] R Arthan and P Oliva, On pocrims and hoops, Arxiv (https://arxiv.org/abs/1404.0816)
[3] R Arthan and P Oliva, On affine logic and Lukasiewicz logic, Arxiv (https://arxiv.org/abs/1404.0570)
[4] R Arthan and P Oliva, Dual hoops have unique halving, McCune Festschrift, LNAI 7788, pp. 165-180, 2013

In this talk I will emphasise the activity of proving in securing mathematical knowledge. I will be drawing on observations of the language used in mathematical proofs to argue that the proofs themselves can contain a mix of propositional and imperatival content, very much in the style of a recipe or set of instructions for other mathematicians to carry out the same proving activity. This also applies to diagrams in proofs, which I shall compare to instructions for LEGO models and Ikea furniture. The idea is that this will then provide a natural picture of informal proofs and their epistemic significance, fitting in with modern approaches in epistemology, especially on knowledge-how and virtue epistemology.

I shall try to explain why I believe that computers will probably surpass humans at finding proofs within a small number of decades. The main content of the talk will be a close analysis of a few example problems of varying difficulty for humans, focusing on what humans do in order to reduce the size of the search space. Thus, it will be in the spirit of Polya, but with the ultimate goal of educating computers rather than humans.