Big Conjectures

Duration: 58 mins 13 secs

Share this media item:

Embed this media item:

<iframe width="_width_" height="_height_" src="https://sms.cam.ac.uk/media/2524216/embed" frameborder="0" scrolling="no" allowfullscreen></iframe>

Choose size:

About this item

Available Formats

About this item

Description:	Hales, T Monday 10th July 2017 - 10:00 to 11:00


Created:	2017-07-24 17:43
Collection:	Big proof
Publisher:	Isaac Newton Institute
Copyright:	Hales, T
Language:	eng (English)


Abstract:	Proof assistants have been used to verify complicated proofs such as the Kepler conjecture in discrete geometry and the odd-order theorem in group theory. Can formalization technology help us to understand the statements of complicated conjectures such as Millennium (million-dollar) problems of the Clay Institute, the geometric Langlands conjecture, or the Kelvin problem for optimal partitions of space?

Abstract:

Proof assistants have been used to verify complicated proofs such as the Kepler conjecture in discrete geometry and the odd-order theorem in group theory. Can formalization technology help us to understand the statements of complicated conjectures such as Millennium (million-dollar) problems of the Clay Institute, the geometric Langlands conjecture, or the Kelvin problem for optimal partitions of space?

Available Formats

Format	Quality	Bitrate	Size
MPEG-4 Video	640x360	1.93 Mbits/sec	846.70 MB	View	Download
WebM	640x360	688.21 kbits/sec	293.45 MB	View	Download
iPod Video	480x270	522.17 kbits/sec	222.65 MB	View	Download
MP3	44100 Hz	249.78 kbits/sec	106.60 MB	Listen	Download
Auto *	(Allows browser to choose a format it supports)