From the Fundamental Lemma to Discrete Geometry, to Formal Verification

University Of Pittsburgh, Pittsburgh PA

Investigators

Abstract

During June 18-22, 2018, the University of Pittsburgh will host an international conference entitled "From the Fundamental Lemma, to Discrete Geometry, to Formal Verification". The conference website can be accessed at http://www.mathematics.pitt.edu/hales60/. The aim of the conference is to explore the interface between the subjects listed in the title, with the primary focus on emphasizing similarities between different fields and finding new applications of existing techniques and methods from different areas. Major experts in each individual field will lecture on the main developments and applications, with the goal of making the ideas accessible to a non-expert audience. By bringing together researchers from the areas of Automorphic Forms, Motivic Integration, Discrete Geometry, and Formal Verification, we hope to highlight and deepen the connections between these areas. Among other things, the conference will highlight the structural relationship between the classical geometric methods of partitioning space used to prove the Kepler conjecture and the new methods of harmonic analysis used to prove the sphere packing results in higher dimensions. In addition, the conference will attempt to bring together the Formal Verification community and the community of researchers working on the formal logic-based version of motivic integration. Both fields share similar techniques and the exchange of ideas between the two fields should be very fruitful. Formal verification of (broadly adopted) encryption standards is ultimately an issue pertaining to the foundation of society, and the involvement of the mathematical community in such efforts is absolutely crucial. The conference will feature a session on formal verification of encryption standards, including a public lecture on a recently verified NIST cryptographic standard. The Formal Abstracts project aims to provide a semantic representation of (ultimately all) mathematical knowledge accessible to the society, and many of participants of this conference are active members of the project. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.