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
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.
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 |
10 July 2017 to 14 July 2017
19 July 2017 to 19 July 2017
27 May 2019 to 31 May 2019
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 | |
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
© 2023 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.