在2012-13年，该研究所的学院数学举办了一个特别的年度，专门讨论"单价的基础，由史蒂夫Awodey，卡内基梅隆大学教授，蒂埃里Coquand他是哥德堡大学的教授弗拉基米尔•Voevodsky他是数学学院的教授。这个研究项目的中心是发展新的数学基础，非常适合使用计算机证明助手作为数学形式化的辅助。这样的证明系统可以用来验证单个数学证明的正确性，也可以允许数学家社区建立共享的、可搜索的形式化定义、定理和证明库，促进大规模的数学形式化。
这种计算工具的可能性最终是基于数学逻辑基础的思想，这是一种哲学上迷人的发展，但自19世纪开始以来，对日常数学几乎没有实际影响。但是，在过去十年中，计算机形式化的进步已经增加了数学逻辑基础的实际效用。单价基础是这一发展的下一步:一种基于被称为类型理论的逻辑系统的新基础，它非常适合人类数学实践和计算机形式化。此外，它还借鉴了同伦理论的新见解，这是数学中致力于研究空间中连续变形的分支。这是一个特别令人惊讶的来源，因为该领域通常被视为远离基金会。
在这特殊的一年里，来自世界各地的32位计算机科学、逻辑学和数学领域的顶尖研究人员聚集在IAS开发这一新的数学基础。每周的研讨会、讲座、工作组、教程和其他活动的雄心勃勃的计划导致了活跃的互动和思想、技能和观点的激烈交流，从而导致参与者之间的大量合作。该计划的目标实现超出预期，产生了一个强大而灵活的新的基础系统称为同伦类型理论基于早期的类型理论系统，这些系统最初用于构造数学和计算机编程，并由同伦理论激发的新原则加以扩充。除了一系列与基础相关的理论成果之外，在这个新体系中还发展了大量的数学成果，包括同伦理论、高级范畴理论、集合理论和实分析的开端。与此同时，努力集中于开发新的和现有的计算机证明辅助工具，以便将这些和今后的结果正式化。建立了一个广泛的代码库，在此基础上可以建立未来的工作，并给出了同伦理论中重要结果的形式化证明，例如计算许多球的同伦群。在一项非凡的合作努力下，特别学年的参与者还编写了一本教科书，在新的逻辑系统中发展了数学的基础和各个专业领域。这本书不仅记录了特殊年份的成果，而且对未来进入该领域的研究人员也是有用的介绍。
_____________________
数学逻辑基础的思想至少可以追溯到戈特洛布·弗雷格Begriffsschrift1879年，他开始证明算术可以完全从逻辑中推导出来，这种方式是“无间隙”的，因此不需要直觉的跳跃。弗雷格的逻辑演绎系统——看起来有点像复杂的接线图——很快就被伯特兰·罗素发现包含了一个矛盾:一个灾难性的逻辑不一致，这使得原本不关心逻辑的数学家开始更加关注逻辑的精确性。罗素自己提出了一种基于类型理论的解决方案，恩斯特·泽梅洛提出了另一种基于康托尔集合理论公理的解决方案。在二十世纪二三十年代，杰出的数学家大卫希尔伯特，赫尔曼·韦尔(教授，1933-51)，以及约翰·冯·诺依曼(教授，1933 - 57)从事数学基础工作，在库尔特的著名发现中达到顶峰Gödel(成员，开始于1933年;教授，1953-76)关于逻辑形式化的限制。Gödel表明，一个完整和一致的逻辑形式的偶数算术在数学上是不可能的;而且，这个结果与许多数学家的实践经验是一致的，即使是最基本的数学理论的形式化也是不切实际的复杂和无关紧要的精细。Russell的系统只经过了362页费力的形式推导，就得出了1 + 1 = 2的结果!
到了20世纪50年代，数学学界已经达成了一种共识，即逻辑基础的程序，虽然在原则上或作为数学的一个分支可能很有趣，但对整个数学的一般实践用处不大。Gödel和Paul Cohen (Member, 1959 - 61,67)关于著名连续统假设的形式不可定性的结果进一步强化了这一观点。逻辑理论的许多后续研究都与计算这一新领域有关;的确，正是早期的逻辑学工作导致了现代计算机的发展，随后理论和实际计算的进步与逻辑研究密切相关。
但是，随着现代计算机在速度和容量上的进步以及其编程方面的理论进步，出现了一种引人注目而又有点讽刺意味的可能性:使用计算机来帮助几乎被遗忘的数学形式化程序。因为曾经人类无法完成的复杂或乏味的工作现在可以由计算机来完成。随着这一进步，计算机形式化形式的逻辑基础最终可能成为数学家日常工作的实际帮助，通过验证定义和证明的正确性，组织大规模的理论，利用形式化结果库，并促进合作发展统一的形式化数学系统。Gödel可能已经表明数学在原则上不能完全形式化，但在实践中，当复杂的计算机系统能够发挥作用时，形式化仍然有很大的好处。
数学基础的这个新概念，与计算机的使用紧密联系在一起，以提供形式严谨性的保证，并帮助处理复杂性的爆炸，这似乎是如此自然，以至于未来的数学历史学家很可能会想，弗雷格和罗素是如何在没有计算机运行它们之前发明了形式基础系统的想法的。基金会与计算机结合起来工作得这么好也不是巧合;如前所述，现代计算机基本上是从早期的逻辑研究中诞生的，它的现代程序和操作系统仍然与它们进化而来的逻辑系统密切相关。从某种意义上说，现代计算机可以说是“靠逻辑运行”的。
这就是“一元基础”项目的出发点:基于新的数学基础开发计算机证明助手的时机已经成熟。但是，不仅是技术的进步使这个计划在今天可行;逻辑理论的最新突破也发挥了重要作用。其中一个进步是发现了一些现代证明系统所使用的类型理论系统与同伦理论的数学领域之间的联系，这通常需要高度的数学抽象才能开始。这种联系允许对一些重要的概念进行直接的、逻辑的形式化，这些概念在数学的各个领域都有广泛的应用。一个重要的例子是集合的基本概念，它在单价基础中可以从更原始的概念中定义，正如最近由Voevodsky发现的那样。一个相关的发现，也是由于Voevodsky，是单价公理，这说明，大致，同构的数学对象可以被识别。这种强大的推理新原理，与日常数学实践相一致，但不是传统集合论基础的一部分，与同型论观点完全相容，而且确实加强了同型论观点，同时极大地简化了类型论作为基础系统的使用。最后，发现了一些基本数学空间的直接、逻辑描述，如n-维球n，以及其他各种基本结构，导致了一个既全面又强大的系统，同时仍然与计算机上的实现密切相关。
参考文献
Steve Awodey, Alvaro Pelayo和Michael A. Warren，“同伦类型理论中的Voevodsky的一价公理”，美国数学学会公告(即将出版)。
乔治·戴森，《朱利安·毕格罗:抽象逻辑与实用机器的桥梁》学会信(2013年春季):14-15。
Thomas C. Hales，《形式证明》美国数学学会公告55岁,没有。11(2008): 1370-80。
高等研究院的单价基础项目，Bob的游戏同伦型论:数学的单价基础(2013)。http://homotopytypetheory.org/book/．
____________________
同伦类型理论允许“同伦类型逻辑”
以下文本摘自《同伦类型理论:数学的一元基础》一书的引言，该书是由该特殊年份的参与者共同撰写的关于一元基础的文章，可在http://homotopytypetheory.org/book/．
同伦类型理论是数学的一个新分支，它以一种令人惊讶的方式结合了几个不同领域的方面。它是基于最近发现的一种联系同伦论而且类型理论．同伦理论是代数拓扑和同调代数的产物，与更高的范畴理论有关系，而类型理论是数学逻辑和理论计算机科学的一个分支。尽管这两者之间的联系目前是密集调查的重点，但越来越明显的是，它们只是一个课题的开始，需要更多的时间和更艰苦的工作才能完全理解。它涉及到球体的同伦群、类型检查的算法和弱∞群胚的定义等看似遥远的主题。
同伦型理论也为数学的基础带来了新的思想。一方面，有沃厄夫斯基的微妙和美丽单价公理．单价公理特别暗示同构结构可以被识别，这是数学家们在工作日愉快地使用的原则，尽管它与传统基础的“官方”学说不相容。另一方面，我们有更高的归纳类型，这些类型为同伦理论的一些基本空间和结构提供了直接的、逻辑的描述:球体、圆柱体、截断、局部化等。当结合到同伦类型理论中时，这些创新允许了一种全新的“同伦类型逻辑”。
这提出了一种具有内在同型内容的数学基础的新概念，一种数学对象的“不变”概念，以及方便的机器实现，可以为工作的数学家提供实际的帮助。这是单价基础项目。本书旨在首次系统地阐述一元基础的基础知识，并收集这种新型推理方式的实例——但不要求读者了解或学习任何形式逻辑，也不要求读者使用任何计算机证明辅助工具。
我们强调同伦型理论是一个年轻的领域，而单价基础则是一项正在进行中的工作。这本书应该被看作是写作时该领域状态的“快照”，而不是对一个已建立的大厦的精雕细琢的阐述。正如我们稍后将简要讨论的那样，同伦类型理论的许多方面还没有被完全理解——但在撰写本文时，它的大致轮廓似乎足够清晰。最终的理论可能不会完全像这本书中描述的那样，但它肯定至少同样有能力和强大;鉴于这里给出的结果，我们因此相信，单价基础最终可以取代集合论，成为大多数数学家所做的非形式化数学的“隐含基础”。
单价公理的基本思想可以解释如下。在类型理论中，一个人可以有一个宇宙U，它的项本身就是类型，a: u等。这些类型的项U通常称为小字体。和其他类型一样，U身份类型为IdU，表示恒等关系a = b在小字体之间。把类型看作空间，U是一个空间，它的点都是空间;为了理解它的身份类型，我们必须问，空间之间的路径是什么U？单价公理说这样的路径对应于同伦等价b。．冒着过于简单化的危险，我们可以简单地说明如下:
单价公理:(a = b)多通道通道(a多通道通道)．
换句话说，恒等等价。特别是，有人可能会说“等效类型是相同的”。
从同伦的观点来看，单价意味着相同同伦类型的空间在宇宙中由一条路径连接U，符合对(小)空间进行分类的直观。然而，从逻辑的角度来看，这是一个全新的想法:它说同构的事物可以被识别!数学家们当然习惯于在实践中识别同构结构，但他们通常是通过“滥用符号”或其他一些非正式的方法来这样做的，因为他们知道所涉及的对象并不是“真正”相同的。但在这个新的基础方案中，这些结构可以被正式地识别，在逻辑意义上，涉及其中一个的每一个属性或结构也适用于另一个。事实上，现在的标识是明确的，财产和建筑可以系统地沿着它运输。此外，不同的方式，这些身份可能形成一个结构，一个人可以(而且应该!)考虑。
通过在同伦类型论中使用具有恒等的路径的识别，这些类型的“归纳定义的空间”可以在类型论中通过“归纳原理”来描述，完全类似于经典的例子，如自然数和不相交并。由此产生的高级归纳类型提供了一种直接的“逻辑”方式来推理熟悉的空间，例如球体，它(结合一元性)可以用于执行同伦理论中熟悉的论点，例如以纯形式的方式计算球体的同伦群。由此产生的证明是经典同伦论思想与经典类型论思想的结合，对这两个学科都产生了新的见解。
此外，这只是冰山一角:许多来自同伦理论的抽象结构，如同伦直连、悬架、波斯特尼科夫塔、局部化、完成和光谱化，也可以表示为更高的归纳类型……因此，一价和高级归纳类型的结合暗示了同伦理论实践中某种革命的可能性。
古典数学家在学习类型论时经常遇到的一个困难是，类型论通常表现为完全或部分形式化的演绎系统。这种风格在证明研究中非常有用，但在应用的非正式推理中使用并不特别方便。对大多数数学家来说，甚至对那些可能对数学基础感兴趣的人来说，它都不熟悉。目前工作的一个目标是发展一种在一元基础上做数学的非正式风格，它既严谨又精确，但也更接近于日常数学的表达语言和风格。
在现代数学中，人们通常以一种原则上可以在初等集合论系统中形式化的方式来构造和推理数学对象，例如ZFC(泽梅洛-弗朗克尔公理加上选择公理)——至少要有足够的创造力和耐心。在大多数情况下，人们甚至不需要意识到这种可能性，因为它在很大程度上符合证明必须“完全严密”的条件(在这个意义上，所有数学家都是通过教育和经验直观地理解的)。但人们确实需要学会小心“非正式集合论”的一些方面:使用太大或不成熟的集合;选择公理及其等价物;甚至(本科生)反证法;等等。采用一种新的基本系统，如同伦类型理论，作为非正式推理的隐含形式基础，将需要调整一些人的本能和实践。本文旨在作为这种“新型数学”的一个例子，它仍然是非正式的，但现在原则上可以在同伦类型理论中形式化，而不是ZFC，再次给予足够的独创性和耐心。
值得强调的是，在这个新制度中，这种形式化可以带来真正的实际好处。类型论的形式化系统适合于计算机系统，并已在现有的证明辅助工具中得到实现。证明助手是一种计算机程序，它指导用户构造完全形式化的证明，只允许有效的推理步骤。它还提供了一定程度的自动化，可以搜索现有定理的库，甚至可以从结果(构造性)证明中提取数值算法。
我们相信，一元基础程序的这方面区别于其他基础方法，可能为工作的数学家提供了一种新的实用工具。事实上，基于旧类型理论的证明助手已经被用于形式化大量的数学证明，例如四色定理和费特-汤普森定理。一元基础的计算机实现目前正在进行中(就像理论本身一样)。然而，即使是它目前可用的实现(主要是对现有证明助手(如Coq)的小修改)也已经证明了它们的价值，不仅在已知证明的形式化方面，而且在发现新证明方面。事实上，这本书中描述的许多证明实际上是第一次在证明助手中以完全形式化的形式完成的，直到现在才第一次被“非形式化”——这是正式数学和非正式数学之间通常关系的逆转。
人们可以想象，在不久的将来，数学家可以通过在一个证明助手中形式化的单价基础系统中工作来验证他们自己论文的正确性，这样做将变得像用TeX排版他们自己的论文一样自然。(这究竟是出版商的梦想，还是他们的噩梦，还有待观察。)原则上，这可能同样适用于任何其他基础系统，但我们认为使用单价基础更实际，正如目前的工作和它的正式对应工作所见证的那样。