Verified Computation and Proof

验证计算和证明

• 批准号: 1615444
• 负责人: Jeremy Avigad
• 金额: $ 14.98万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2016
• 资助国家: 美国
• 起止时间: 2016-09-01 至 2018-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1615444&HistoricalAwards=false
• 关键词: Verified; Computation; Proof

Mathematics is exceedingly complex, and avoiding mistakes is crucial to keeping our mathematics correct, meaningful, and reliable. This project involves the use of logic-based computational methods to support mathematical reasoning. The PI will contribute to the development of a theorem prover called Lean, which can be used to verify complex proofs and calculations. The system enables us to build mathematical libraries that are verified on the basis of a formal axiomatic system, with the computer checking each and every claim on the basis of a small set of axioms and rules. The system will support exploration and the discovery of new mathematics, and can also be used to verify properties of complex systems in computer science, engineering, and finance.The development of Lean is based at Microsoft Research, Redmond, but it is an open-source, community-based project that currently involves researchers at Carnegie Mellon University, Stanford, and the University of Washington as well. The PI will develop Lean's libraries and automation to support applications in fields such as engineering and mathematical finance. Specifically, the PI and his collaborators and students at Carnegie Mellon will extend the libraries for analysis and measure theory and measure-theoretic probability, as well as parts of algebra and homotopy type theory. They will also contribute to other types of automation currently under development in Lean, and develop decision procedures and algorithms for special domains. Finally, they will continue to develop interactive online course material, based on Lean, to provide better educational resources for logic and formal methods.

数学是极其复杂的，避免错误是保持我们的数学正确、有意义和可靠的关键。这个项目涉及使用基于逻辑的计算方法来支持数学推理。PI将有助于开发一个名为Lean的定理证明器，该定理证明器可用于验证复杂的证明和计算。这个系统使我们能够建立数学库，这些库是在一个正式的公理系统的基础上验证的，计算机根据一小组公理和规则来检查每一个断言。该系统将支持探索和发现新的数学，也可用于验证计算机科学、工程和金融领域复杂系统的特性。精益的开发基于微软雷德蒙德研究院，但它是一个开源的、基于社区的项目，目前包括卡内基梅隆大学、斯坦福大学和华盛顿大学的研究人员。PI将开发精益的库和自动化，以支持工程和数学金融等领域的应用。具体来说，PI和他的合作者以及卡内基梅隆大学的学生将扩展分析和测量理论和测量理论概率论的库，以及部分代数和同伦类型理论。他们还将为其他类型的自动化做出贡献，目前正在精益开发中，并为特殊领域开发决策程序和算法。最后，他们将继续开发基于精益的交互式在线课程材料，为逻辑和形式化方法提供更好的教育资源。