The Big Proof Agenda for Mechanizing Mathematical Discourse
1 hour 9 mins,
990.81 MB,
MPEG-4 Video
640x360,
29.97 fps,
44100 Hz,
1.91 Mbits/sec
Share this media item:
Embed this media item:
Embed this media item:
About this item
Description: |
Shankar, N
Monday 26th June 2017 - 11:00 to 12:00 |
---|
Created: | 2017-07-19 17:41 |
---|---|
Collection: | Big proof |
Publisher: | Isaac Newton Institute |
Copyright: | Shankar, N |
Language: | eng (English) |
Distribution: | World (downloadable) |
Explicit content: | No |
Aspect Ratio: | 16:9 |
Screencast: | No |
Bumper: | UCS Default |
Trailer: | UCS Default |
Abstract: | 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. |
---|
Available Formats
Format | Quality | Bitrate | Size | |||
---|---|---|---|---|---|---|
MPEG-4 Video * | 640x360 | 1.91 Mbits/sec | 990.81 MB | View | Download | |
WebM | 640x360 | 1.03 Mbits/sec | 536.19 MB | View | Download | |
iPod Video | 480x270 | 491.01 kbits/sec | 248.14 MB | View | Download | |
MP3 | 44100 Hz | 251.19 kbits/sec | 126.95 MB | Listen | Download | |
Auto | (Allows browser to choose a format it supports) |