Univalent Foundations of Mathematics

统一数学基础

• 批准号: 1100938
• 负责人: Vladimir Voevodsky
• 金额: $ 10万
• 依托单位: Institute For Advanced Study
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2011
• 资助国家: 美国
• 起止时间: 2011-08-01 至 2015-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1100938&HistoricalAwards=false
• 关键词: Univalent; Foundations; Mathematics

The correspondence between homotopy types and higher categorical analogs of groupoids, first conjectured by Alexander Grothendieck, naturally leads to a view of mathematics where sets are used to parametrize collections of objects without "internal structure", while collections of objects with "internal structure" are parametrized by more general homotopy types. Univalent foundations are based on the combination of this view with the discovery that it is possible to directly formalize reasoning about homotopy types using Matin-Lof type theories. We expect that this new approach to the foundations will finally make it practical for mathematicians to use proof development software in their everyday work. The sophistication and user friendliness of such software ("proof assistants") have been growing steadily for decades and its use in computer science is becoming standard. Enabling its use in pure mathematics will be of great benefit to the new generations of mathematicians and to the mathematical community as a whole.

同伦类型和群胚的更高范畴类似物之间的对应关系，首先由亚历山大格罗滕迪克提出，自然导致了一种数学观点，其中集合用于参数化没有“内部结构”的对象集合，而具有“内部结构”的对象集合则由更一般的同伦类型参数化。单价基础是基于这一观点与发现的结合，即可以使用Matin-Lof型理论直接形式化同伦类型的推理。我们希望这种新的基础方法最终能够使数学家在日常工作中使用证明开发软件变得实用。几十年来，这种软件（“证明助手”）的复杂性和用户友好性一直在稳步增长，它在计算机科学中的使用正在成为标准。使其在纯数学中的使用将对新一代的数学家和整个数学界都有很大的好处。