Verified Computation and Proof

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

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.