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.
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, Floris van Doorn and Vladimir Voevodsky
Deadline for applications: 08 April 2017
Please note members of Cambridge University are welcome to turn up and sign in as a non-registered attendee on the day(s) during the workshop and attend the lecture(s). Please note that we cannot provide you with any support including name badge, meals or accommodation.
In addition to visiting the INI, there are multiple ways in which you can participate remotely.
- Registration Package: £227
- Student Registration Package: £177
The Registration Package includes admission to all seminars, lunches and refreshments on the days that lectures take place (Monday - Friday), wine reception and formal dinner, but does not include other meals or accommodation.
Registration and Accommodation
- Accommodation Package: £577
The Accommodation Package includes a registration fee, bed and breakfast accommodation at Churchill from the evening of Sunday 9th July 2017 to breakfast on Saturday 15th July 2017, together with lunches and refreshments during the days that lectures take place (Monday - Friday). The formal dinner is also included, but no other evening meals.
Formal Dinner Only
- Formal Dinner: £50
Participants on the Accommodation Package or Registration Package, including organisers and speakers, are automatically included in this event. For all remaining participants who would like to attend, such as programme participants, the above charge will apply.
Accommodation in single study bedrooms with shared facilities, breakfast and lunches are provided at Churchill College,
Lunch will be served at Wolfson Court in the Cafeteria from 12:30 to 13:30 on days that lectures take place.
- Accommodation Package and Registration Package participants should present their badge as payment for their meal
- Those issued with a blue Institute door entrance card can add money onto the card via the Porters' Lodge at Wolfson Court
- Other participants must purchase their meal using their dining card via the Porters' Lodge (forms can be found on the registration desk or at the Porters' Lodge)
Participants are free to make their own arrangements for dinner.
The Formal Dinner will take place on Wednesday 12th July at Emmanuel College. Participants on the Accommodation Package or Registration Package, including organisers and speakers, are automatically included in this event.