skip to content

The Big Proof Agenda for Mechanizing Mathematical Discourse

Presented by: 
Natarajan Shankar
Monday 26th June 2017 - 11:00 to 12:00
INI Seminar Room 2
We are creating and using mathematical knowledge at a rapidly
increasing rate.  This growth creates the
need for automation in
building and indexing formal mathematical 

bases.  Automated proof technologies such
as theorem proving,
satisfiability solving, and model checking are increasingly
being used for formalizing the behavior of computer 

hardware and
software systems, constructing large libraries  of formalized
mathematics, and solving open problems. 
We outline  an agenda for
the Big Proof programme toward pragmatic foundations
and practical technologies that can assist pure and applied
mathematicians solve large problems individually and collaboratively.
Presentation Material: 
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons