Speaker(s) Thomas Hales University of Pittsburgh
Date 10 July 2017 – 10:00 to 11:00
Venue INI Seminar Room 1
Session Title Big Conjectures
Event [BPRW01] Computer-aided mathematical proof
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? 

Supported By