From the Fundamental Lemma to Discrete Geometry, to Formal Verification

2018年6月18-22日，匹兹堡大学将主办一场题为《从基本引理到离散几何，再到形式验证》的国际会议。会议网址为：http://www.mathematics.pitt.edu/hales60/.。会议的目的是探索标题所列主题之间的接口，主要重点是强调不同领域之间的相似之处，并从不同领域寻找现有技术和方法的新应用。每个领域的主要专家将就主要的发展和应用进行演讲，目的是让非专家受众能够理解这些想法。通过聚集来自自同构形式、基元积分、离散几何和形式验证等领域的研究人员，我们希望突出和深化这些领域之间的联系。在其他方面，会议将突出用于证明开普勒猜想的经典几何划分空间方法和用于证明高维球填充结果的调和分析新方法之间的结构关系。此外，会议将尝试将形式验证界和致力于基于形式逻辑的Motivic整合版本的研究人员社区聚集在一起。这两个领域拥有相似的技术，两个领域之间的思想交流应该是非常富有成效的。对(广泛采用的)加密标准的正式验证最终是一个与社会基础有关的问题，数学界的参与是绝对关键的。会议将举行一场关于加密标准正式验证的会议，包括一场关于最近验证的NIST加密标准的公开讲座。正式摘要项目旨在提供社会可获得的(最终所有)数学知识的语义表示，本次会议的许多参与者都是该项目的活跃成员。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

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.