Big Proof

ICMS, Bayes Centre, 47 Potterrow, Edinburgh EH8 9BT

27 - 31 May 2019

Organisers

Ursula Martin, University of Edinburgh and University of Oxford
Natarajan Shankar, SRI International

The Isaac Newton Institute programme on Big Proof during the summer of 2017 drew a great deal of interest from mathematicians, philosophers, and computer scientists.  In May 2019 a week-long follow-up workshop funded by the Isaac Newton Institute will take place at the International Centre for Mathematical Sciences in Edinburgh. This workshop will take forward a number of the key initiatives from Big Proof:

• Pragmatic foundations for the formalization of mathematical proofs.
• Social processes that support research, exposition, and learning in mathematics.
• Interchange formats and repositories for formal mathematical knowledge
• Scalable proof automation
• Applications of Big Proof technology

Arrangements
This workshop will commence at 13:00 on Monday 27 May and finish on Friday 31 May at 12 noon.

On Monday 27 May, you should aim to arrive at ICMS, for registration at 13:00 -13:50. Tea/coffee will be served. The workshop will begin with a welcome talk at 13:50 followed by the first talk art 14:00.

All speakers and invitees should now have received an invitaiton to attend. Further details of the programme will be issued in April.


Travel
Please note that it is your responsibility to have adequate travel insurance to cover medical and other emergencies that may occur on your trip.
Please see the Visiting ICMS page for details of our location.
A taxi directly from the airport will cost approximately 20.00 to 25.00 GBP to the city centre for a one-way journey.
There is also a bus service direct from the airport to the city centre which will cost 4.50 GBP single or 7.50 GBP return - the Airlink 100. This is a frequent service (every 10 minutes during peak times) and will bring you close to Waverley Railway Station, only a short walk to the workshop venue.
Lothian buses charge £1.70 for a single, £4.00 for a day ticket. Please note that the exact fare is required and no change is given.
If travelling by train, please note that Edinburgh has several railway stations - Waverley Railway Station being the main station and closest to the workshop venue. If you alight at Edinburgh Waverley, the workshop venue is an easy 15 minute walk away

 

ICMS does NOT use third parties to arrange accommodation.  If you are approached by a third party (e.g. Business Travel Management) asking for booking details, please ignore.  If you have any concerns please contact ICMS.


Accommodation
If you are booking your own accommodation for this workshop, here are a few suggestions below which are close to ICMS and reasonably priced.

    • Masson House Pollock Halls of Residence, The University of Edinburgh, 18 Holyrood Park Road, Edinburgh EH16 5AY 0800 028 7118 (UK only) - +44 (0)131 651 2189 - University of Edinburgh accommodation. Pollock Halls is about a 20-25 minute walk
    • Ibis Hotel on South Bridge (not Hunter Square) A 2 minute walk from ICMS.
    • Motel One Edinburgh (Please note that Motel One has two hotels in the city centre - Motel One Royal or Motel One Princes.  Both are within 5 to 10 minutes walk from ICMS)
    • Jurys Inn Edinburgh, 43 Jeffrey Street, Edinburgh EH1 1DH +44 (0)131 200 3300 - A 5 minute walk from ICMS.
    • Edinburgh City Hotel, 79 Lauriston Place, Edinburgh, EH3 9HZ  +44 (0)131 622 7979 - Also around a 5 minute walk from ICMS
    • St Christophers Hostel, 9-13 Market Street, Edinburgh EH1 1DE  (approx 25.00 or less depending on offers available)+44 (0)20 7407 1856 - bookings

Programme

The programme is shown below. Abstracts are available here.

Monday 27 May 2019


13:00-14:00

Registration with Tea/Coffee

14:00-15:00

Tom Hales (University of Pittsburgh)
Mathematical Definitions, Formally Speaking

pdf of the talk is available here

15:00-15:30

Tea/Coffee

15:30-16.15

Lawrence Paulson (University of Cambridge)
Formalising Mathematics In Simple Type Theory

pdf of the talk is available here

16:15-17:00

Natarajan Shankar (SRI International)
Proofs and Things

pdf of the talk is available here

17:00- 18:00

Informal wine reception

Tuesday 28 May 2019


09:00-10:00

Jeremy Avigad (Carnegie Mellon University)
The Mechanization of Mathematics

pdf of this talk is available here

10:00-10:30

Tea/Coffee

10:30-11:15

Peter Koepke (University of Bonn)
Modeling human proof checking in the Naproche-SAD system

pdf of the talk is available here

11:15-12:00

Chris Sangwin (University of Edinburgh)
Online proof and elementary mathematics from an educational perspective

pdf of the talk is available here

12:00-12.45

Michael Douglas (Stony Brook University)
String theory, mathematical databases and formal methods

pdf of the talk is available here

12.45

Group Photo in Lecture Theatre

12.45-14.00

Lunch provided in 5.03

14:00-15:00

Ian Ford (Wolfram Research)
Mathematical Knowledge Representation and Reasoning in the Wolfram Language

pdf of the talk is available here

15:00-15:30

Tea/Coffee

15.30-16.15

Michael Barany (University of Edinburgh)
Janus in the mathematics library: foundations, communities, meaning, and scale in the mathematics literature

pdf of the talk is available here

16:15-17:00

Katya Komendentskaya (Heriot-Watt University)
Verification of Neural Networks for the masses: are our programming languages ready?

pdf of the talk is available here

17:40
18:00-19:00

Doors Open to the public
Public lecture
Donald MacKenzie (University of Edinburgh)
How to be a High Frequency Trader

Room G.03, Ground Floor, Bayes Centre

19:00-19:45

Informal wine reception in Atrium, Ground Floor Bayes Centre

Wednesday 29 May 2019


09:00-10:00

Kevin Buzzard (Imperial College London)
Mathematical objects in dependent type theory

pdf of the talk is available here

10:00-10:30

Tea/Coffee

10:30-11:15

Silvia De Toffoli (Princeton University)
Diagrammatic Notations in Mathematical Proofs

pdf of the talk is available here

11:15-12:00

Angeliki Koutsoukou-Argyraki (University of Cambridge)
Formalising Mathematics-In Praxis: First Experiences with Isabelle/HOL

12:00-12.45

David Saxton (DeepMind)
Teaching machines to do mathematics like humans

12.45-14.00

Lunch provided in 5.03

14:00-15:00

John Harrison (Amazon Web Services)
The HOL Light Mathematical Libraries

15:00-15:30

Tea/Coffee

15.30-16.15

Fenner Tanswell (Loughborough University)
The Social Epistemology of Mathematical Collaboration

pdf of the talk is available here

16.15-17.00

Alison Pease (University of Dundee)
Automating "human-like" example-use in mathematics

pdf of the talk is available here

Thursday 30 May 2019

09:00-10:00

Michael Kohlhase (FAU Erlangen-Nürnberg)
FAIRMath: Making mathematical Data FAIR (Findable, Accessible, Interoperable, and Reusable)

pdf of the talk is available here

10:00-10:30

Tea/Coffee

10:30-11:15

Josef Urban (Czech Technical University in Prague)
Learning and Reasoning over Big Proof Corpora

pdf of the talk is available here

11:15-12:00

Marie Kerjean (Inria)
A formal, classical proof of the Hahn-Banach theorem

pdf of the talk is available here

12:00-12.45

Benedikt Löwe (Universitaet Hamburg)
Why did mathematicians not embrace the vision of the QED manifesto?

pdf of the talk is available here

12.45-14.00

Lunch provided in 5.03

14:00-15:00

George Gonthier (Inria Saclay)
On the Impact of Big Proofs on Provers

pdf of the talk is available here

15:00-15:30

Tea/Coffee

15.30-16.15

Gilles Dowek (Inria)
Logipedia: a system-independent encyclopedia of formal proofs

pdf of the talk is available here

16.15-17.00

Ursula Martin (University of Oxford/Edinburgh)
The craft and culture of proof

pdf of the talk is available here

19:00

Workshop dinner at Blonde Restaurant, 75 St. Leonard’s Street, Edinburgh

Friday 31 May 2019


09:00-10:00

Stephen Watt (University of Waterloo)
The NASA Effect of a Global Digital Math Library

pdf of the talk is available here

10:30-11:00

Tea/Coffee

10:30-12:00

Panel chaired by Natarajan Shankar (SRI International)  to discuss next steps:

Members to include Alan Bundy (Edinburgh), Ian Ford (Wolfram Research), John Harrison (Amazon Web Services), Alison Pease (Dundee) Stephen Watt (Waterloo)

12:00

Close of workshop

 

List of Delegates

Last Name First Name Institution
Abdulaziz Mohammad Technical University of Munich
Arthan Rob Lemma 1 Ltd
Aspinall David  University of Edinburgh
Avigad Jeremy Carnegie Mellon University
Ayers Edward University of Cambridge
Barany Michael University of Edinburgh
Barton Reid  
Benzmüller Christoph Freie Universität Berlin & University of Luxembourg
Bordg Anthony University of Cambridge
Bundy Alan  University of Edinburgh
Butler David  University of Edinburgh
Buzzard Kevin Imperial College London
Campbell Brian University of Edinburgh
Chevallier Mark  University of Edinburgh
Corneli Joseph University of Edinburgh
Dahmen Sander VU Amsterdam
Davenport James University of Bath
Di Toffoli Silvia Princeton University
Douglas Michael Stony Brook University
Dowek Gilles Inria
Eberl Manuel Technical University of Munich
Fleuriot Jacques University of Edinburgh
Ford Ian  Wolfram Research
Gonthier Georges Inria Saclay
Hales Tom University of Pittsburgh
Harrison John Amazon Web Services
Ion Patrick IMKT & University of Michigan
Jackson Paul  University of Edinburgh
Kammar Ohad Oxford University
Kerjean Marie Inria
Kientiz Daniel Heriot-Watt University
Koepke Peter   University of Bonn
Kohlhase Michael FAU Erlangen-Nürnberg
Kokke Wen University of Edinburgh
Komendantskaya  Ekaterina  Heriot-Watt University
Koutsoukou-Argyraki Angeliki University of Cambridge
Kulesza Kamil  Polish Academy of Sciences
Kuzmickas Paulius University of Dundee
Lewis Robert Vrije Universiteit Amsterdam
Li Wenda University of Cambridge
Lindley Sam University of Edinburgh
Löwe Benedikt Universitaet Hamburg
MacKenzie Donald University of Edinburgh
Martin Ursula University of Edinburgh/University of Oxford
Massot Patrick Université Paris Sud
McKinna James University of Edinburgh
Morris  Imogen  University of Edinburgh
Morrison Scott Australian National University
Nawrocki     Wojciech    University of Edinburgh
Nummelin Visa  Vrije Universiteit Amsterdam
Palmer Jake  University of Edinburgh
Paulson Lawrence University of Cambridge
Pease Alison University of Dundee
Pollack Randy University of Edinburgh/LFCS
Rabe Florian Universities Erlangen-Nuremberg and Paris-Sud
Ramamoorthy Subramanian University of Edinburgh
Rozplokhas Dmitry JetBrains
Sangwin Chris University of Edinburgh
Saxton David DeepMind
Shankar Natarajan SRI International
Sogokon Andrew The University of Edinburgh
Stark Ian The University of Edinburgh
Stewart Robert Heriot-Watt University
Strickland Neil University of Sheffield
Tanswell Fenner Loughborough University
Urban Josef Czech Technical University in Prague
Watt Stephen M University of Waterloo
Wiedijk Freek Radboud University Nijmegen
Winterstein Daniel  Good-Loop