BPRW01
10 July 2017 to 14 July 2017
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 workshop is the synthesis of major themes in our INI programme, Big Proof, and 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.
The workshop 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. It will explore 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.
Speakers
Jeremy Avigad, Steve Awodey, Jasmin Blanchette, Leo De Moura, Stephanie Dick, Martin Escardo, Jacques Fleuriot, Georges Gonthier, Tom Hales, Marjin Heule, Patrick Ion, Mateja Jamnik, Michael Kohlhase, Ekaterina Komendantskaya, Dan Licata, Peter Lumsdaine, Assia Mahboubi, Ursula Martin, Tobias Nipkow, Grant Passmore, Larry Paulson, Alison Pease, Stephen Watt, Floris van Doorn and Vladimir Voevodsky.
The Institute kindly requests that any papers published as a result of this programme’s activities are credited as such. Please acknowledge the support of the Institute in your paper using the following text:
The author(s) would like to thank the Isaac Newton Institute for Mathematical Sciences, Cambridge, for support and hospitality during the programme Computer-aided mathematical proof, where work on this paper was undertaken. This work was supported by EPSRC grant EP/K032208/1.
Monday 10th July 2017 | |||
---|---|---|---|
09:00 to 09:50 | No Room Required | ||
09:50 to 10:00 | No Room Required | ||
10:00 to 11:00 |
Thomas Hales University of Pittsburgh |
Room 1 | |
11:00 to 11:30 | No Room Required | ||
11:30 to 12:30 |
Vladimir Voevodsky Institute for Advanced Study, Princeton |
Room 1 | |
12:30 to 13:30 | No Room Required | ||
13:30 to 14:30 | Room 1 | ||
14:30 to 15:30 |
Larry Paulson University of Cambridge |
Room 1 | |
15:30 to 16:00 | No Room Required | ||
16:00 to 17:00 |
Stephen Watt University of Waterloo |
Room 1 | |
17:00 to 18:00 | No Room Required |
Tuesday 11th July 2017 | |||
---|---|---|---|
09:00 to 10:00 |
Steve Awodey Carnegie Mellon University |
Room 1 | |
10:00 to 11:00 |
Martin Escardo University of Birmingham |
Room 1 | |
11:00 to 11:30 | No Room Required | ||
11:30 to 12:30 |
Floris van Doorn Carnegie Mellon University |
Room 1 | |
12:30 to 13:30 | No Room Required | ||
13:30 to 14:30 | Room 1 | ||
14:30 to 15:30 |
Dan Licata Wesleyan University |
Room 1 | |
15:30 to 16:00 | No Room Required | ||
16:00 to 17:00 |
Peter LeFanu Lumsdaine Stockholm University |
Room 1 |
Wednesday 12th July 2017 | |||
---|---|---|---|
09:00 to 10:00 |
Assia Mahboubi INRIA Saclay - Île-de-France |
Room 1 | |
10:00 to 11:00 |
Leonardo de Moura Microsoft (UK) |
Room 1 | |
11:00 to 11:30 | No Room Required | ||
11:30 to 12:30 |
Jasmin Blanchette INRIA Nancy - Grand Est; Max-Planck-Institut für Informatik, Saarbrücken |
Room 1 | |
12:30 to 13:30 | No Room Required | ||
13:30 to 14:30 | Room 1 | ||
14:30 to 15:30 |
Ursula Martin University of Oxford |
Room 1 | |
15:30 to 16:00 | No Room Required | ||
16:00 to 17:00 |
Marijn Heule University of Texas at Austin |
Room 1 | |
19:30 to 22:00 | No Room Required |
Thursday 13th July 2017 | |||
---|---|---|---|
09:00 to 10:00 |
Georges Gonthier INRIA Saclay - Île-de-France |
Room 1 | |
10:00 to 11:00 |
Tobias Nipkow Technischen Universität München |
Room 1 | |
11:00 to 11:30 | No Room Required | ||
11:30 to 12:30 |
Grant Passmore University of Cambridge |
Room 1 | |
12:30 to 13:30 | No Room Required | ||
13:30 to 14:30 | Room 1 | ||
14:30 to 15:30 |
Mateja Jamnik University of Cambridge |
Room 1 | |
15:30 to 16:00 | No Room Required | ||
16:00 to 17:00 |
Katya Komendenskaya Heriot-Watt University |
Room 1 |
Friday 14th July 2017 | |||
---|---|---|---|
09:00 to 10:00 |
Alison Pease University of Dundee |
Room 1 | |
10:00 to 11:00 |
Michael Kohlhase Jacobs University Bremen |
Room 1 | |
11:00 to 11:30 | No Room Required | ||
11:30 to 12:30 |
Jacques Fleuriot University of Edinburgh |
Room 1 | |
12:30 to 13:30 | No Room Required | ||
13:30 to 14:30 |
Stephanie Dick Harvard University |
Room 1 | |
14:30 to 15:30 |
Natarajan Shankar ; Patrick Ion ; William Timothy Gowers University of Cambridge |
Room 1 | |
15:30 to 16:00 | No Room Required | ||
16:00 to 17:00 |
Natarajan Shankar ; Patrick Ion ; William Timothy Gowers University of Cambridge |
Room 1 |
Subscribe for the latest updates on events and news
Isaac Newton Institute for Mathematical Sciences, 20 Clarkson Road, Cambridge CB3 0EH United Kingdom
Tel: +44 1223 335999 Email: reception@newton.ac.uk
© 2024 Isaac Newton Institute for Mathematical Sciences. All Rights Reserved. Privacy Policy
INI is a creative collaborative space which is occupied by up to fifty-five mathematical scientists at any one time (and many more when there is a workshop). Some of them may not have met before and others may not realise the relevance of other research to their own work.
INI is especially important as a forum where early-career researchers meet senior colleagues and form networks that last a lifetime.
Here you can learn about all activities past, present and future, watch live seminars and submit your own proposals for research programmes.
Within this section of the website you should find all the information required to arrange and plan your visit to the Institute. If you have any further questions, or are unable to find the information you require, please get in touch with the relevant staff member or our Reception team via our contact pages.
INI and its programme participants produce a range of publications to communicate information about activities and events, publish research outcomes, and document case studies which are written for a non-technical audience. You will find access to them all in this section.
The Isaac Newton Institute aims to maximise the benefit of its scientific programmes to the UK mathematical science community in a variety of ways.
Whether spreading research opportunities through its network of correspondents, offering summer schools to early career researchers, or hosting public-facing lectures through events such as the Cambridge Festival, there is always a great deal of activity to catch up on.
Find out about all of these endeavours in this section of the site.
There are various ways to keep up-to-date with current events and happenings at the Isaac Newton Institute. As detailed via the menu links within this section, our output covers social media streams, news articles, a regular podcast series, an online newsletter, and more detailed documents produced throughout the year.
“A world famous place for research in the mathematical sciences with a reputation for efficient management and a warm welcome for visitors”
The Isaac Newton Institute is a national and international visitor research institute. It runs research programmes on selected themes in mathematics and the mathematical sciences with applications over a wide range of science and technology. It attracts leading mathematical scientists from the UK and overseas to interact in research over an extended period.
INI has a vital national role, building on many strengths that already exist in UK universities, aiming to generate a new vitality through stimulating and nurturing research throughout the country.During each scientific programme new collaborations are made and ideas and expertise are exchanged and catalysed through lectures, seminars and informal interaction, which the INI building has been designed specifically to encourage.
For INI’s knowledge exchange arm, please see the Newton Gateway to Mathematics.
The Institute depends upon donations, as well as research grants, to support the world class research undertaken by participants in its programmes.
Fundraising activities are supported by a Development Board comprising leading figures in academia, industry and commerce.
Visit this section to learn more about how you could play a part in supporting INI’s groundbreaking research.
In this section you can find contact information, staff lists, maps and details of how to find INI’s main building in Cambridge.
Our administrative staff can help you with any queries regarding a prospective or planned visit. If you would like to discuss a proposed a research programme or other event, our senior management team will be happy to help.
Use this for pages on our website, including: visitor information, details about INI, fellowships, history, outreach, news, podcasts and more.
Use this for information about INI programmes, workshops, seminars, pre-prints, and participants.