From the Fundamental Lemma to Discrete Geometry, to Formal Verification

从基本引理到离散几何，再到形式验证

• 批准号: 1761653
• 负责人: Bogdan Ion
• 金额: $ 3.5万
• 依托单位: University of Pittsburgh
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-05-01 至 2019-04-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1761653&HistoricalAwards=false
• 关键词: Fundamental; Lemma; Discrete; Geometry; Formal

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.

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