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.
Participation in INI programmes is by invitation only. Anyone wishing to apply to participate in the associated workshop(s) should use the relevant workshop application form.
For more info, please see the INI Big Proof programme
Organisers: Jeremy Avigad (Carnegie Mellon), Georges Gonthier (Microsoft), Ursula Martin (Oxford), J Strother Moore (Texas at Austin), Larry Paulson (Cambridge), Andrew Pitts (Cambridge) and Natarajan Shankar (SRI International)