skip to content

Big Conjectures

Presented by: 
Thomas Hales University of Pittsburgh
Monday 10th July 2017 - 10:00 to 11:00
INI Seminar Room 1
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? 
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons