skip to content

The Big Proof Agenda for Mechanizing Mathematical Discourse

Presented by: 
Natarajan Shankar SRI International
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  knowledge 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.

The video for this talk should appear here if JavaScript is enabled.
If it doesn't, something may have gone wrong with our embedded player.
We'll get it fixed as soon as possible.
Presentation Material: 
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons