Programme theme
Proofs as constructive demonstrations of mathematical validity have been at the heart of mathematics since antiquity. Formal proof systems capture the definitions, statements, and proofs of mathematical discourse using precisely defined formal languages and rules of inference. Formal proofs have enabled mathematicians to rigorously explore foundational issues of expressiveness, consistency, independence, completeness, computability, and decidability. The formalisation of proof facilitates the representation and manipulation of mathematical knowledge with modern digital computers. During the last sixty years, the digitisation of formal mathematics has yielded satisfiability solvers, rewriting engines, computer algebra systems, automated theorem provers, and interactive proof assistants. Proof technology can be used to perform large calculations reliably, solve systems of constraints, discover and visualise examples and counterexamples, simplify expressions, explore hypotheses, navigate large libraries of mathematical knowledge, capture abstractions and patterns of reasoning, and interactively construct proofs. The scale and sophistication of proof technology is approaching a point where it can effectively aid human mathematical creativity at all levels of expertise. Modern satisfiability solvers can efficiently solve problems with millions of Boolean constraints in hundreds of thousands of variables. Automated theorem provers have discovered proofs of open problems. Interactive proof assistants have been used to check complicated mathematical proofs such as those for the Kepler’s conjecture and the Feit-Thompson odd order theorem. Such systems have also been applied to the verification of practical artifacts such as central processing units (CPUs), compilers, operating system kernels, file systems, and air traffic control systems. Several high-level programming languages employ logical inference as a basic computation step.
This programme is directed at the challenges of bringing proof technology into mainstream mathematical practice. The specific challenges addressed include
- Novel pragmatic foundations for representing mathematical knowledge and vernacular inspired by set theory, category theory, and type theory.
- Large-scale formal mathematical libraries that capture background knowledge spanning a range of domains.
- Algorithmic and engineering issues in building and integrating large-scale inference engines.
- The social exploration and curation of formalised mathematical and scientific knowledge.
- Educational proof technology in support of collaborative learning.
This programme brings together mathematicians interested in employing proof technology in their research, logicians exploring pragmatic and foundational issues in the formalisation of mathematics, and computer scientists engaged in developing and applying proof technology. The programme includes a week-long workshop exploring foundational, theoretical, and practical challenges in exploiting proof technology to transform mathematical practice across a range of scientific and engineering disciplines. A key expected output is a concrete, long-term research agenda for making computational inference a basic technology for formalising, creating, curating, and disseminating mathematical knowledge in digital form.
BPR programme: Georges Gonthier explains "Four colour theorem"
Preprints
| Title | Year | Programme | |
|---|---|---|---|
Modelling the Way Mathematics Is Actually DoneAuthors: Raymond Puzio, Dave Murray-Rust, Gabriela Rino Nesin, Ursula Martin, Joseph Corneli, Alison Pease |
2017 | BPR | 6 October 2017 |
Workshops
Computer-aided mathematical proof
10 July 2017 to 14 July 2017
Big Proof - Challenges in Industry and Research
19 July 2017 to 19 July 2017
Big Proof Follow on
27 May 2019 to 31 May 2019
Seminars
| Monday 26th June 2017 | |||
|---|---|---|---|
| 11:00 to 12:00 |
Natarajan Shankar |
Room 2 | 
|
| Tuesday 27th June 2017 | |||
|---|---|---|---|
| 11:00 to 12:00 |
Thierry Coquand Göteborgs Universitet |
Room 2 |
|
| 13:30 to 14:30 |
Andrew Pitts University of Cambridge |
Room 2 |
|
| Wednesday 28th June 2017 | |||
|---|---|---|---|
| 11:00 to 12:00 |
Marie-Françoise Roy Université de Rennes 1 |
Room 2 |
|
| Thursday 29th June 2017 | |||
|---|---|---|---|
| 11:00 to 12:00 |
Jeremy Avigad Carnegie Mellon University |
Room 2 |
|
| 15:30 to 17:30 |
Andrew Pitts University of Cambridge |
Room 2 |
|
| Friday 30th June 2017 | |||
|---|---|---|---|
| 10:00 to 11:00 |
Natarajan Shankar |
Room 2 |
|
| 11:00 to 12:00 |
Andreas Abel Göteborgs Universitet |
Room 2 |
|
| Monday 3rd July 2017 | |||
|---|---|---|---|
| 11:00 to 12:00 |
Bas Spitters Aarhus Universitet |
Room 2 |
|
| 15:30 to 16:30 |
Johannes Hölzl Technische Universität München |
Room 2 |
|
| 16:30 to 17:30 |
Natarajan Shankar |
Room 2 |
|
| Tuesday 4th July 2017 | |||
|---|---|---|---|
| 10:30 to 11:30 |
Kuen-Bang Hou (Favonia) Carnegie Mellon University |
Room 2 |
|
| 13:00 to 14:00 |
Johannes Hölzl Technische Universität München |
Room 2 |
|
| 15:30 to 17:30 | Room 2 | ||
| Wednesday 5th July 2017 | |||
|---|---|---|---|
| 13:30 to 14:30 |
Manuel Eberl Technische Universität München |
Room 2 |
|
| 15:30 to 17:30 | Room 2 | ||
| Thursday 6th July 2017 | |||
|---|---|---|---|
| 11:00 to 12:00 |
J Strother Moore University of Texas at Austin; University of Edinburgh |
Room 2 |
|
| 13:00 to 13:40 |
Chris Kapulkin University of Western Ontario |
Room 2 |
|
| 13:40 to 14:20 |
Fabian Immler Technische Universität München |
Room 2 |
|
| 15:30 to 16:30 |
Ulrik Buchholtz Technische Universität Darmstadt |
Room 2 |
|
| 16:30 to 17:30 |
Martin Hofmann Ludwig-Maximilians-Universität München |
Room 2 | |
| Friday 7th July 2017 | |||
|---|---|---|---|
| 10:00 to 11:00 |
Benedikt Ahrens INRIA Rennes - Bretagne Atlantique ; Jean-Pierre LELAY Institute for Advanced Study, Princeton |
Room 2 |
|
| 11:00 to 11:30 |
Bas Spitters Aarhus Universitet |
Room 2 |
|
| 11:30 to 12:00 |
Floris van Doorn Carnegie Mellon University |
Room 2 |
|
| 12:00 to 12:30 |
Dan Licata Wesleyan University ; Kuen-Bang Hou (Favonia) Carnegie Mellon University |
Room 2 |
|
| 13:30 to 14:30 |
J Strother Moore University of Texas at Austin; University of Edinburgh |
Room 2 |
|
| Sunday 9th July 2017 | |||
|---|---|---|---|
| 14:00 to 17:00 |
Patrick Ion University of Michigan ; Stephen Watt University of Waterloo |
Room 1 | |
| Monday 17th July 2017 | |||
|---|---|---|---|
| 11:00 to 12:00 |
Maria Paola Bonacina Università degli Studi di Verona |
Room 2 |
|
| 13:00 to 14:00 |
Cesare Tinelli University of Iowa |
No Room Required | |
| 15:30 to 16:00 |
Cesare Tinelli University of Iowa |
Room 2 |
|
| 16:00 to 16:30 |
Wenda Li Cambridge Research Institute |
Room 2 |
|
| 16:30 to 17:00 |
Bohua Zhan Massachusetts Institute of Technology |
Room 2 |
|
| 17:00 to 17:30 |
Edward Ayers University of Cambridge |
Room 2 |
|
| Tuesday 18th July 2017 | |||
|---|---|---|---|
| 11:00 to 12:00 |
Paulo Oliva Queen Mary University of London |
Room 2 |
|
| 13:30 to 14:30 |
Josef Urban Czech Technical University |
Room 2 |
|
| 15:30 to 16:00 |
Fenner Tanswell University of Oxford |
Room 2 |
|
| 16:00 to 16:30 |
Lorenzo Lane University of Edinburgh; University of Oxford |
Room 2 |
|
| 16:30 to 17:30 |
Ursula Martin University of Oxford |
Room 2 | |
| Friday 21st July 2017 | |||
|---|---|---|---|
| 11:00 to 12:00 |
James Davenport University of Bath |
Room 2 |
|
| 13:30 to 14:30 |
Chris Sangwin University of Edinburgh |
Room 2 |
|
| Monday 24th July 2017 | |||
|---|---|---|---|
| 11:00 to 12:00 |
Arnold Neumaier Universität Wien ; Cesare Tinelli University of Iowa ; Leonardo de Moura Microsoft (USA) ; Natarajan Shankar SRI International |
Room 2 |
|
| 15:30 to 17:30 |
Jeremy Avigad Carnegie Mellon University |
Room 2 |
|
| Tuesday 25th July 2017 | |||
|---|---|---|---|
| 11:00 to 12:00 |
Yves Bertot INRIA Sophia Antipolis |
Room 2 |
|
| 14:00 to 16:00 |
Bohua Zhan Massachusetts Institute of Technology ; Josef Urban Czech Technical University ; Mario Carneiro Carnegie Mellon University; Ohio State University |
Room 2 |
|
| Wednesday 26th July 2017 | |||
|---|---|---|---|
| 11:00 to 12:00 |
Arnold Neumaier Universität Wien |
Room 2 |
|
| 14:30 to 15:30 |
Thomas Hales University of Pittsburgh |
Room 2 |
|
| 15:30 to 16:30 |
Joseph Corneli University of Edinburgh; University of London |
Room 2 |
|
| 16:30 to 17:30 | Room 2 | ||
| Thursday 27th July 2017 | |||
|---|---|---|---|
| 11:00 to 12:00 |
Deepak Kapur University of New Mexico |
Room 2 |
|
| 13:30 to 14:30 |
Konstantin Korovin University of Manchester |
Room 2 |
|
| 15:30 to 16:30 |
Vladimir Voevodsky Institute for Advanced Study, Princeton |
Room 2 |
|
| 16:30 to 17:30 |
Benedikt Ahrens INRIA Rennes - Bretagne Atlantique |
Room 2 |
|
| Friday 28th July 2017 | |||
|---|---|---|---|
| 11:00 to 12:00 |
Georges Gonthier INRIA Saclay - Île-de-France |
Room 2 |
|
| 13:30 to 14:30 |
William Timothy Gowers University of Cambridge |
Room 1 |
|
| Thursday 3rd August 2017 | |||
|---|---|---|---|
| 15:30 to 16:30 |
Vladimir Voevodsky Institute for Advanced Study, Princeton |
Room 2 |
|
Organisers
- Jeremy Avigad Carnegie Mellon University
- Leonardo de Moura Microsoft (UK)
- Georges Gonthier INRIA Saclay - Île-de-France
- Ursula Martin University of Oxford
- J Strother Moore University of Texas at Austin; University of Edinburgh
- Lawrence Paulson University of Cambridge
- Andrew Pitts University of Cambridge
- Natarajan Shankar
Speakers
- Andreas Abel Göteborgs Universitet
- Benedikt Ahrens INRIA Rennes - Bretagne Atlantique
- Jeremy Avigad Carnegie Mellon University
- Edward Ayers University of Cambridge
- Yves Bertot INRIA Sophia Antipolis
- Maria Paola Bonacina Università degli Studi di Verona
- Ulrik Buchholtz Technische Universität Darmstadt
- Mario Carneiro Carnegie Mellon University; Ohio State University
- Thierry Coquand Göteborgs Universitet
- Joseph Corneli University of Edinburgh; University of London
- James Davenport University of Bath
- Leonardo de Moura Microsoft (USA)
- Manuel Eberl Technische Universität München
- Georges Gonthier INRIA Saclay - Île-de-France
- William Timothy Gowers University of Cambridge
- Thomas Hales University of Pittsburgh
- Martin Hofmann Ludwig-Maximilians-Universität München
- Kuen-Bang Hou (Favonia) Carnegie Mellon University
- Johannes Hölzl Technische Universität München
- Fabian Immler Technische Universität München
- Patrick Ion
- Chris Kapulkin University of Western Ontario
- Deepak Kapur University of New Mexico
- Konstantin Korovin University of Manchester
- Lorenzo Lane University of Edinburgh; University of Oxford
- Catherine LELAY Institute for Advanced Study, Princeton
- Wenda Li University of Cambridge
- Dan Licata Wesleyan University
- Ursula Martin University of Oxford
- J Strother Moore University of Texas at Austin; University of Edinburgh
- Arnold Neumaier Universität Wien
- Paulo Oliva Queen Mary University of London
- Andrew Pitts University of Cambridge
- Marie-Françoise Roy Université de Rennes 1
- Chris Sangwin University of Edinburgh
- Natarajan Shankar SRI International
- Bas Spitters Aarhus Universitet
- Fenner Tanswell University of Oxford
- Cesare Tinelli University of Iowa
- Josef Urban Czech Technical University
- Floris van Doorn Carnegie Mellon University
- Vladimir Voevodsky Institute for Advanced Study, Princeton
- Stephen Watt University of Waterloo
- Bohua Zhan Massachusetts Institute of Technology
Participants
- Andreas Abel Göteborgs Universitet
- Peter Aczel University of Manchester
- Benedikt Ahrens INRIA Rennes - Bretagne Atlantique
- David Aspinall University of Edinburgh; The Alan Turing Institute
- Jeremy Avigad Carnegie Mellon University
- Steve Awodey Carnegie Mellon University
- Andrej Bauer University of Ljubljana
- Yves Bertot INRIA Sophia Antipolis
- Jasmin Blanchette Vrije Universiteit Amsterdam; Max-Planck-Institut für Informatik, Saarbrücken
- Maria Paola Bonacina Università degli Studi di Verona
- Simon Boulier INRIA Rennes - Bretagne Atlantique
- Ulrik Buchholtz Technische Universität Darmstadt
- Mario Carneiro Carnegie Mellon University; Ohio State University
- Thierry Coquand Göteborgs Universitet
- Joseph Corneli University of Edinburgh; University of London
- James Davenport University of Bath
- Leonardo de Moura Microsoft (USA)
- Manuel Eberl Technische Universität München
- Gabriel Ebner Vienna University of Technology
- Martin Escardo University of Birmingham
- Marcelo Fiore University of Cambridge
- Jacques Fleuriot University of Edinburgh
- Cameron Freer None / Other
- Georges Gonthier INRIA Saclay - Île-de-France
- Timothy Griffin University of Cambridge
- Thomas Hales University of Pittsburgh
- Yacin Hamami Vrije Universiteit Brussel
- Hugo Herbelin INRIA Paris - Rocquencourt; Université Paris 7 - Denis-Diderot
- Tony Hoare
- Martin Hofmann Ludwig-Maximilians-Universität München
- Kuen-Bang Hou (Favonia) Carnegie Mellon University
- Martin Hyland University of Cambridge
- Johannes Hölzl Technische Universität München
- Fabian Immler Technische Universität München
- Mateja Jamnik University of Cambridge
- Chris Kapulkin University of Western Ontario
- Deepak Kapur University of New Mexico
- Michael Kohlhase Jacobs University Bremen
- Katya Komendenskaya Heriot-Watt University
- Konstantin Korovin University of Manchester
- Oliver Kullmann Swansea University
- Lorenzo Lane University of Edinburgh; University of Oxford
- Catherine LELAY Institute for Advanced Study, Princeton
- Robert Lewis Carnegie Mellon University
- Wenda Li University of Cambridge
- Dan Licata Wesleyan University
- Peter LeFanu Lumsdaine Stockholm University
- Benedikt Löwe Universiteit van Amsterdam; Universität Hamburg
- Assia Mahboubi INRIA Saclay - Île-de-France
- Ursula Martin University of Oxford
- Norman Megill None / Other
- Arnold Neumaier Universität Wien
- Tristan Nguyen Air Force Office of Scientific Research
- Tobias Nipkow Technischen Universität München
- Paige North University of Cambridge
- Steven Obua University of Edinburgh
- Paulo Oliva Queen Mary University of London
- Ian Orton University of Cambridge
- Grant Passmore Aesthetic Integration Ltd
- Lawrence Paulson University of Cambridge
- Alison Pease University of Dundee
- Andrew Pitts University of Cambridge
- Egbert Rijke Carnegie Mellon University
- Marie-Françoise Roy Université de Rennes 1
- Chris Sangwin University of Edinburgh
- Peter Sewell University of Cambridge
- Natarajan Shankar SRI International
- Bas Spitters Aarhus Universitet
- Fenner Tanswell University of Oxford
- Laurent Théry INRIA Sophia Antipolis
- Cesare Tinelli University of Iowa
- Sebastian Ullrich Karlsruhe Institute of Technology (KIT)
- Josef Urban Czech Technical University
- Christian Urban King's College London
- Floris van Doorn Carnegie Mellon University
- Vladimir Voevodsky Institute for Advanced Study, Princeton
- Tamara von Glehn University of Cambridge
- Stephen Watt University of Waterloo
- Makarius Wenzel None / Other
- Freek Wiedijk Radboud Universiteit Nijmegen
- Christoph Wintersteiger Microsoft (UK)
- Bohua Zhan Massachusetts Institute of Technology
Supported By
