Videos and presentation materials from other INI events are also available.
Event | When | Speaker | Title | Presentation Material |
---|---|---|---|---|
BPR |
26th June 2017 11:00 to 12:00 |
Natarajan Shankar |
The Big Proof Agenda for Mechanizing Mathematical Discourse
We are creating and using mathematical knowledge at a rapidly
increasing rate. This growth creates the
need for automation in
building and indexing formal mathematical
knowledge
bases. Automated proof technologies such
as theorem proving,
satisfiability solving, and model checking are increasingly
being used for formalizing the behavior of computer
hardware and
software systems, constructing large libraries of formalized
mathematics, and solving open problems.
We outline an agenda for
the Big Proof programme toward pragmatic foundations
and practical technologies that can assist pure and applied
mathematicians solve large problems individually and collaboratively.
|
![]() ![]() |
BPR |
27th June 2017 11:00 to 12:00 |
Thierry Coquand |
Univalent type theory and modular formalisation of mathematics
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. |
![]() ![]() |
BPR |
27th June 2017 13:30 to 14:30 |
Andrew Pitts |
Using Agda to Explore Path-Oriented Models of Type Theory
Homotopy Type Theory (HoTT) has re-invigorated research into the theory and applications of the intensional version of Martin-Löf typetheory. On the one hand, the language of type theory helps to express synthetic constructions and arguments in homotopy theory and higher-dimensional category theory. On the other hand, the geometric and algebraic insights of those highly developed branches of mathematics shed new light on logical and type-theoretic notions. In particular, HoTT takes a path-oriented view of intensional (i.e.proof-relevant) equality: proofs of equality of two elements of a type x,y : A, i.e. elements of a Martin-Löf identity type Id_A x y, behave analogously to paths between two points x, y in a space A. The complicated internal structure of intensional identity types relatesto the homotopy classes of path spaces. To make this analogy preciseand to exploit it, it helps to have a wide range of models ofintensional type theory that embody this path-oriented view ofequality in some way. In this talk I will describe some recent work on path-oriented modelsof type theory carried out with my student Ian Orton and making use of the Agda theorem-prover. I will try to avoid technicalities in favourof describing why Agda in "unsafe" mode is so useful to us while wecreate new mathematics, rather than verifying existing mathematical theorems; and also describe some limitations of Agda (to do with quotient types) in the hope that the audience will tell me about a prover without those limitations. I also want to make some comments about mathematical knowledge representation as it relates to my search, as a homotopical ignoramus, for knowledge that will help in the construction of models of HoTT. |
![]() ![]() |
BPR |
28th June 2017 11:00 to 12:00 |
Marie-Françoise Roy |
Effectivity and Complexity Results in Hilbert's 17th problem Marie-Françoise Roy Université de Rennes 1, France
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.
|
![]() ![]() |
BPR |
29th June 2017 11:00 to 12:00 |
Jeremy Avigad |
The Lean Theorem Prover
Lean is a new, open source, interactive theorem prover designed to
support mathematical reasoning as well as hardware and software
verification. Because its logical foundation, dependent
type theory, has a computational interpretation, we can use Lean
as a programming language and evaluate expressions with a fast
bytecode evaluator. We obtain a metaprogramming language --
that is, a language that we can use to construct expressions
and proofs in dependent type theory itself -- by exposing Lean
internals through a suitable API. This provides us with a means
of extending Lean's functionality and automation within Lean
itself. In this talk, I will describe this
metaprogramming framework and some of its mechanisms for manipulating
expressions efficiently.
|
![]() ![]() |
BPR |
29th June 2017 15:30 to 17:30 |
Andrew Pitts |
HoTT research seminar (Coquand & Rijke)
15:30-16:30: Thierry Coquand (Chalmers), "Cubical stacks" 16:30-17:30: Egbert Rijke (CMU), “Colimits, descent and equifibrant replacement” |
![]() |
BPR |
30th June 2017 10:00 to 11:00 |
Natarajan Shankar |
A tutorial introduction to the PVS proof assistant The Prototype Verification System (PVS) is an interactive proof assistant developed at SRI International. The PVS specification language extends higher-order logic with predicate subtypes, dependent types, inductive datatypes, and parametric theories. These features make typechecking undecidable, or more accurately, decidable modulo proof obligations. The interactive proof assistant includes automated support for contextual simplification, rewriting, and SAT/SMT solving. PVS has been used to formalize large libraries (see, for example, https://github.com/nasa/pvslib). The tutorial gives a brief overview of the language, logic, and proof infrastructure of PVS. |
![]() ![]() |
BPR |
30th June 2017 11:00 to 12:00 |
Andreas Abel | A tutorial introduction to Agda |
![]() |
BPR |
3rd July 2017 11:00 to 12:00 |
Bas Spitters |
Synthetic topology in Homotopy Type Theory for probabilistic programming
The ALEA Coq library formalizes discrete measure theory using a
variant of the Giry monad, as a submonad of the CPS monad: (A →
[0, 1]) → [0, 1]. This allows to use Moggi’s monadic meta- language
to give an interpretation of a language, Rml, into type theory.
Rml is a functional language with a primitive for probabilistic
choice. This formalization was the basis for the
Certicrypt
system for verifying security protocols. Easycrypt is still based on
the same idea. We improve on the formalization by using homotopy
type theory which provides e.g. quotients and functional
extensionality. Moreover, homotopy type theory allows us to use
synthetic topology to present a theory which also includes
continuous data types, like [0, 1]. Such data types are relevant, for
instance, in machine learning and differential privacy. We indicate how our axioms are justified by Kleene-Vesley
realizability, a standard model for computation with
continuous data types. (Joint work with Florian Faissole.)
|
![]() ![]() |
BPR |
3rd July 2017 15:30 to 16:30 |
Johannes Hölzl |
Proof Automation - Automation in Isabelle's Analysis
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.
|
![]() ![]() |
BPR |
3rd July 2017 16:30 to 17:30 |
Natarajan Shankar |
Inference Algorithms
Johannes Holzl will present a short talk on Automation in Isabelle's Analysis. Natarajan Shankar will present an overview of some basic inference algorithms used in SAT and SMT solving, and in theorem proving. |
![]() ![]() |
BPR |
4th July 2017 10:30 to 11:30 |
Kuen-Bang Hou (Favonia) | Computational Higher-Dimensional Type Theory |
![]() ![]() |
BPR |
4th July 2017 13:00 to 14:00 |
Johannes Hölzl | Classical Analysis in Lean & Isabelle |
![]() ![]() |
BPR |
4th July 2017 15:30 to 17:30 |
Big Proof and Education (coordinated by Jeremy Avigad) | ||
BPR |
5th July 2017 13:30 to 14:30 |
Manuel Eberl |
Semi-Automatic Asymptotics in Isabelle/HOL
Computer Algebra Systems can easily compute limits and
asymptotic expansions of complicated real functions; interactive theorem
provers, on the other hand, provide very little support for such problems and
proving asymptotic properties of a function often involves long and tedious
manual proofs.
In this talk, I will present my work about bringing
automation for real-valued asymptotics to Isabelle/HOL using multiseries
expansions.
This yields a procedure to automatically prove limits and
‘Big-O'
estimates of real-valued functions similarly to computer
algebra systems like Mathematica and Maple – but while proving every step of
the process correct.
|
![]() ![]() |
BPR |
5th July 2017 15:30 to 17:30 |
Social Proof Seminar (coordinated by Fenner Tanswell) | ||
BPR |
6th July 2017 11:00 to 12:00 |
J Strother Moore |
Industrial Use of a Mechanical Theorem Prover
Several mechanical theorem provers and many mechanized decision procedures are in routine
use in the computing industry. The complexity of computer chip designs allow design flaws to slip past
unaided human reasoning of even the most
talented designers.
Bugs in fabricated
chips can cost hundreds of millions of
dollars to fix. So microprocessor companies use
mechanized theorem proving to prove that critical parts of designs implement the specified
functionality. In this talk I will explain how one theorem
prover is used in several companies,
including Intel, AMD, Centaur, ARM,
Oracle, and Rockwell Collins.
|
![]() ![]() |
BPR |
6th July 2017 13:00 to 13:40 |
Chris Kapulkin |
Type theory and higher categories
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. |
![]() |
BPR |
6th July 2017 13:40 to 14:20 |
Fabian Immler |
A Verified ODE Solver and Smale's 14th Problem
Smale's 14th Problem is a conjecture about chaos in a
particular dynamical system, the Lorenz attractor. The problem was solved by
Warwick Tucker with a combination of regular analysis and a computer-assisted
part. The computer-assisted part yields numerical bounds on solutions of the
Lorenz ODE, which are required to certify chaos.
In this talk, I will present the current library of ODEs
and verified numerical methods in Isabelle/HOL, and how I use it for a formal
verification of the computer-assisted part of Tucker's proof.
|
![]() ![]() |
BPR |
6th July 2017 15:30 to 16:30 |
Ulrik Buchholtz | Nominal applications of the classifying space of the finitary permutation group |
![]() |
BPR |
6th July 2017 16:30 to 17:30 |
Martin Hofmann | Interpretation of the Calculus of Constructions in dictoses | |
BPR |
7th July 2017 10:00 to 11:00 |
Benedikt Ahrens, Catherine LELAY |
Overview of Unimath
We will give an overview of the UniMath language and library. |
![]() |
BPR |
7th July 2017 11:00 to 11:30 |
Bas Spitters |
The HoTT library in Coq
We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including univalence, higher inductive types, and significant amounts of synthetic homotopy theory, as well as category theory and modalities. The library has been used as a basis for several independent developments. We discuss the decisions that led to the design of the library, and we comment on the interaction of homotopy type theory with recently introduced features of Coq, such as universe polymorphism and private inductive types. Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Mike Shulman, Matthieu Sozeau, Bas Spitters, The HoTT Library: A formalization of homotopy type theory in Coq (CPP17) pp. 164-172, 2017 10.1145/3018610.3018615 https://arxiv.org/abs/1610.04591 |
![]() |
BPR |
7th July 2017 11:30 to 12:00 |
Floris van Doorn |
The Lean HoTT 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.
|
![]() ![]() |
BPR |
7th July 2017 12:00 to 12:30 |
Dan Licata, Kuen-Bang Hou (Favonia) | Homotopy Type Theory in Agda |
![]() |
BPR |
7th July 2017 13:30 to 14:30 |
J Strother Moore |
An Industrially Useful Prover
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.
|
![]() ![]() |
BPR |
9th July 2017 14:00 to 17:00 |
Stephen Watt, Patrick Ion | International Knowledge Management Trust | |
BPRW01 |
10th July 2017 10:00 to 11:00 |
Thomas Hales |
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?
|
![]() ![]() |
BPRW01 |
10th July 2017 11:30 to 12:30 |
Vladimir Voevodsky |
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. |
![]() ![]() |
BPRW01 |
10th July 2017 14:30 to 15:30 |
Larry Paulson |
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. |
![]() ![]() |
BPRW01 |
10th July 2017 16:00 to 17:00 |
Stephen Watt |
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.
|
![]() ![]() |
BPRW01 |
11th July 2017 09:00 to 10:00 |
Steve Awodey |
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.
|
![]() |
BPRW01 |
11th July 2017 10:00 to 11:00 |
Martin Escardo |
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.
|
![]() ![]() |
BPRW01 |
11th July 2017 11:30 to 12:30 |
Floris van Doorn |
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 ![]() ![]() ![]() ![]() ![]() ![]() Related Links
|
![]() ![]() |
BPRW01 |
11th July 2017 14:30 to 15:30 |
Dan Licata |
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.
|
![]() ![]() |
BPRW01 |
11th July 2017 16:00 to 17:00 |
Peter LeFanu Lumsdaine |
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:
|
![]() ![]() |
BPRW01 |
12th July 2017 09:00 to 10:00 |
Assia Mahboubi |
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. |
![]() |
BPRW01 |
12th July 2017 10:00 to 11:00 |
Leonardo de Moura |
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 Links
|
![]() |
BPRW01 |
12th July 2017 11:30 to 12:30 |
Jasmin Blanchette |
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 Links
|
![]() |
BPRW01 |
12th July 2017 14:30 to 15:30 |
Ursula Martin |
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
|
![]() |
BPRW01 |
12th July 2017 16:00 to 17:00 |
Marijn Heule |
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. |
![]() ![]() |
BPRW01 |
13th July 2017 09:00 to 10:00 |
Georges Gonthier |
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. |
![]() ![]() |
BPRW01 |
13th July 2017 10:00 to 11:00 |
Tobias Nipkow |
Mining the Archive of Formal Proofs
Co-authors: Jasmin Christian Blanchette (Vrije Universiteit Amsterdam), Maximilian Haslbeck (Technical University Munich), Daniel Matichuk (Data61) The Archive of Formal Proofs is a vast collection of computer-checked proofs developed using the proof assistant Isabelle. We perform an in-depth analysis of the archive, looking at various properties of the proof developments, including size, dependencies, and proof style. Related Links
|
![]() |
BPRW01 |
13th July 2017 11:30 to 12:30 |
Grant Passmore |
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 real-world examples. We'll sketch many open problems and future directions along the way.
|
![]() |
BPRW01 |
13th July 2017 14:30 to 15:30 |
Mateja Jamnik |
Accessible Reasoning with Diagrams: Ontology Debugging
Co-authors: 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 one-to-one 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
|
![]() |
BPRW01 |
13th July 2017 16:00 to 17:00 |
Katya Komendenskaya |
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 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. |
![]() ![]() |
BPRW01 |
14th July 2017 09:00 to 10:00 |
Alison Pease |
The role of explanation in mathematical research
Co-authors: 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. |
![]() |
BPRW01 |
14th July 2017 10:00 to 11:00 |
Michael Kohlhase |
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 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. |
![]() |
BPRW01 |
14th July 2017 11:30 to 12:30 |
Jacques Fleuriot |
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
|
![]() |
BPRW01 |
14th July 2017 13:30 to 14:30 |
Stephanie Dick |
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 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.
|
![]() |
BPRW01 |
14th July 2017 14:30 to 15:30 |
Natarajan Shankar, Patrick Ion, William Timothy Gowers |
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, 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” |
![]() |
BPRW01 |
14th July 2017 16:00 to 17:00 |
Natarajan Shankar, Patrick Ion, William Timothy Gowers |
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, 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” |
![]() |
BPR |
17th July 2017 11:00 to 12:00 |
Maria Paola Bonacina | CDSAT: conflict-driven theory combination |
![]() ![]() |
BPR |
17th July 2017 15:30 to 16:00 |
Cesare Tinelli |
SMTCoq, a plug-in for the trustworthy integration of SAT/SMT solvers into Coq
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. |
![]() ![]() |
BPR |
17th July 2017 16:00 to 16:30 |
Wenda Li |
Evaluating winding numbers through Cauchy indices in Isabelle/HOL
In this talk, I will describe a newly developed tactic that evaluates winding numbers through Cauchy indices. By combining with remainder sequences, this theory of Cauchy indices also leads to decision procedures to count the number of complex roots of a polynomial in some domain.
|
![]() ![]() |
BPR |
17th July 2017 16:30 to 17:00 |
Bohua Zhan | Auto2 prover in Isabelle |
![]() |
BPR |
17th July 2017 17:00 to 17:30 |
Edward Ayers | A simple prover in the browser |
![]() |
BPR |
18th July 2017 11:00 to 12:00 |
Paulo Oliva |
Mining Human Proofs from Machine Proofs
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 |
![]() ![]() |
BPR |
18th July 2017 13:30 to 14:30 |
Josef Urban |
Combining Machine Learning and Automated Reasoning: Some Training Examples
Co-Author: Cezary Kaliszyk (U. of Innsbruck) I am planning to show some samples of how machine learning and automated reasoning are usefully combined in various tasks related to interactive/automated proving, and automated formalization. My plan is to make the session a bit more interactive/improvised and show/discuss things in more detail, such as what features we use, what are the datasets and benchmarks/competitions, what are the training/evaluation tasks, and how the resulting systems are run and used. I encourage questions and discussion. |
![]() |
BPR |
18th July 2017 15:30 to 16:00 |
Fenner Tanswell |
Go forth and multiply! Imperatives in mathematical proofs
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. |
![]() |
BPR |
18th July 2017 16:00 to 16:30 |
Lorenzo Lane |
Socialising proof
The following presentation will explore the
social mechanisms involved in validating proofs within pure mathematics. I will
use the high profile example of Mochizuki’s Proof of the ABC conjecture to
demonstrate the challenges involved in validating proofs. The acceptance of
proofs depends upon their conformity to certain standards, on possessing
relationships to existing bodies of knowledge, as well as being certified by
reputable members of the community of practice. Proofs thus need to be
socialised before they can be fully accepted. I shall demonstrate the
socialisation processes Mochizuki’s proof underwent, and explore the continuing
challenges the proof encounters in its bid to gain legitimacy within the
mathematical community. |
![]() |
BPR |
18th July 2017 16:30 to 17:30 |
Ursula Martin | Social proof: social session on the POPL experience | |
BPR |
21st July 2017 11:00 to 12:00 |
James Davenport | Computer Algebra and Formal Proof |
![]() |
BPR |
21st July 2017 13:30 to 14:30 |
Chris Sangwin | Reasoning by equivalence: the start of proof in elementary education |
![]() |
BPR |
24th July 2017 11:00 to 12:00 |
Natarajan Shankar, Leonardo de Moura, Arnold Neumaier, Cesare Tinelli |
Language and automation in mathematics
Arnold Neumaier will give a short talk on "The communication of mathematics". This will be followed by a discussion of the interaction between language and automation in current proof assistants. The seminar will actually run from 11 to 12.30. Abstract for Neumaier's talk: We discuss - from a mathematician's point of view - the characteristic features that make mathematics communicable between people, between people and software systems, and between software systems with different semantic foundations. This talk has a strong philosophical component, complementing the views presented during the Big Proofs program so far. It exposes important issues that I believe are essential for bridging the gap between the mathematics community and the formal theorem proving community. One of the main points made and illustrated is that the natural mathematical language is a highly optimized language for the efficient communication of precise concepts and their relations, whose main features are completely lost in the current generation of formalizations of mathematics. The insights obtained are the basis of my vision for a joint future of mathematics and formal verification, and provide a background for the design choices discussed in the lecture on Wednesday. |
![]() |
BPR |
24th July 2017 15:30 to 17:30 |
Jeremy Avigad | Big Proof & Education |
![]() ![]() |
BPR |
25th July 2017 11:00 to 12:00 |
Yves Bertot |
Building blocks towards modeling the physical world: analysis, geometry, computer arithmetics
In the long run, we should be able to formalize most of the design of cyber-physical systems and robots, to help detecting flaws at early stages of design. Among the many questions that arise, there is the question of going from an abstract design to a concrete implementation. I wish to describe two experiments where this path is taken.
Part of this work was done in collaboration with Clément Sartori. |
![]() |
BPR |
25th July 2017 14:00 to 16:00 |
Josef Urban, Mario Carneiro, Bohua Zhan | Systems Based on Set Theory |
![]() |
BPR |
26th July 2017 11:00 to 12:00 |
Arnold Neumaier |
Concise - a synthesis of types, grammars, semantics
(joint work with Peter Schodl, Ferenc Domes, Kevin Kofler, Andreas Pichler, and David Langer, Vienna) This talk features the design and implementation of tools that my research group in Vienna has created to pave the way towards automatically or interactively extracting from standard mathematical literature (such as the latex source of mathematics textbooks) a formal version of all (correct and incorrect) mathematical claims contained in it, including all claims in the proofs and all implicit information needed for their understanding. We have very encouraging performance results for certain low level partial goals in this direction. Completing this program (which I believe to be feasible with Thus it would bridge the mathematicians' side of the current gap between mathematics and formal theorem proving. Central to everything are the working implementation of
|
![]() |
BPR |
26th July 2017 14:30 to 15:30 |
Thomas Hales | An overview of the Flyspeck project |
![]() |
BPR |
26th July 2017 15:30 to 16:30 |
Joseph Corneli | Modelling the way mathematics is actually done |
![]() |
BPR |
26th July 2017 16:30 to 17:30 |
Social Proof Seminar (coordinated by Fenner Tanswell) | ||
BPR |
27th July 2017 11:00 to 12:00 |
Deepak Kapur |
Parametric Groebner basis computations and elimination
Parametric Groebner basis and systems were proposed in 1990's independently by Weispfenning and Kapur to study solutions of parametric polynomials for various specializations of parameters. Kapur's motivation for studying them arose from the application of geometry theorem proving and model based image analysis. Recently there is interest in using these structures for developing heuristics that first consider equalities over the complex field in a formula expressed using ordering relation with an objective of developing an incomplete method for solving problems formulated in the theory of real closed field. It is hoped this incomplete approach can handle a larger class of problems in practice than the cylinderical algebraic decomposition method by Collins and his collaborators. We will give an overview of algorithms for computing parametric Groebner basis and system developed in collaboration with Profs. Sun and Wang of the Academy of Mathematics and System Science of the Chinese Academy of Sciences. An existence proof of a canonical comprehensive Groebner basis associated a parametric ideal will be presented. However, an algorithm to compute this object is still elusive. Some open problems in this topic will be discussed. |
![]() |
BPR |
27th July 2017 13:30 to 14:30 |
Konstantin Korovin | Automated theorem proving in first-order logic: from superposition to instantiation |
![]() |
BPR |
27th July 2017 15:30 to 16:30 |
Vladimir Voevodsky | Simplicial and cubical sets - how they relate to each other (joint work with Chris Kapulkin) |
![]() |
BPR |
27th July 2017 16:30 to 17:30 |
Benedikt Ahrens | Categorical structures for type theory in univalent foundations" |
![]() |
BPR |
28th July 2017 11:00 to 12:00 |
Georges Gonthier | A MathComp Library tour |
![]() |
BPR |
28th July 2017 13:30 to 14:30 |
William Timothy Gowers |
How do human mathematicians avoid big searches?
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.
|
![]() |
BPR |
3rd August 2017 15:30 to 16:30 |
Vladimir Voevodsky | Cubical and simplicial 2 - the coherent nerve of a cubical category (joint work with K Kapulkin) |
![]() |