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? |
Presentation Files | 21474_0.pdf |