| 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? |





