1984年1月，亚历山大Grothendieck他向法国国家科学研究中心提交了他的提案“Esquisse d 'un Programme”。不久，这本书的副本开始在数学家中流传。几个月后，在莫斯科大学读本科一年级时，我的第一位科学顾问乔治·沙巴特(George Shabat)给了我一本这本书。在学习了一些法语后，我的唯一目的是能够阅读这篇文章，我开始研究其中列出的一些想法。
1988年或1989年，我遇到了迈克尔Kapranov谁对发展的观点同样着迷数学新的“高维”对象的灵感来自范畴理论和二范畴理论。
我们共同发表的第一篇论文叫做“∞-群poids作为a的模型”同伦类别。”在这篇文章中，我们声称提供了一个严格的数学公式，并证明了Grothendieck的思想，连接了两类数学对象:∞-群胚和同伦类型。
后来，我们决定将类似的想法应用于当时的另一个顶级数学问题:构造动机的上同调，亚历山大·贝林森在1987年的一篇论文中推测存在，罗伯特·麦克弗森(现任数学学院教授)，以及瓦迪姆·谢赫特曼。
1990年夏天，卡帕拉诺夫安排我不用申请就被哈佛大学研究生院录取。几个月后，他在康奈尔大学，我在哈佛大学，我们的数学道路出现了分歧。我把精力集中在动力上上同调之后还有动机同伦理论。我1991年3月29日的笔记，开头的问题是“代数变种或方案的同伦理论是什么?”
动机上同调在当时被认为是高度推测性的，缺乏坚实的基础。1986年开创性的论文“代数循环和更高”k理论”斯宾塞布洛赫出版后不久被发现安德烈Suslin在引理1.1的证明中包含一个错误。证据无法确定，论文中几乎所有的主张都没有得到证实。
一份新的证明直到1993年才公布于众，它用30页复杂的论证取代了原来论文中的一段，而且过了许多年才被认为是正确的。有趣的是，这个新的证明是基于马克·斯皮瓦可夫斯基(Mark Spivakovsky)的一个老结果，他几乎在同一时间宣布了奇点猜想解析度的证明。斯皮瓦可夫斯基关于奇点分辨率的证明被认为是正确的，好几年后才发现其中有一个错误。这个猜想仍然没有定论。
动机上同调的方法是我和Andrei Suslin一起提出的埃里克·弗里德兰德我绕过了Bloch的引理，而是依靠我的论文“带转移的前束的上同调理论”，这是我在1992-93年还是研究所成员时写的。1999-2000年，我再次在国际会计学会做了一系列讲座皮埃尔Deligne(数学学院的教授)正在做笔记，检查我论证的每一步。直到那时，我才发现我论文中一个关键引理的证明有一个错误，而这个引理，正如所陈述的那样，是无法挽救的。幸运的是，我能够证明一个更弱、更复杂的引理，它对所有应用都是充分的。修正后的论证序列于2006年发表。
这个故事让我很害怕。从1993年开始，多组数学家在研讨会上研究了我的论文，并在他们的工作中使用了它，但没有人注意到这个错误。这显然不是意外。一个可信的作者的技术论证，很难核查，看起来与已知正确的论证相似，几乎从来没有被详细核查过。
但这并不是数学文本中错误持续存在的唯一问题。1998年10月，卡洛斯·辛普森向arXiv预印本服务器提交了一篇题为“严格3-群胚的同伦类型”的论文。它声称提供了一个论证，暗示我和卡普拉诺夫在1989年发表的“∞-群波群”论文的主要结果不可能是真的。然而，我和卡普拉诺夫自己也曾考虑过类似的批评，并互相说服对方，认为它并不适用。在2013年秋天之前，我一直认为我们是对的(!!)
我可以看到导致这种令人发指的情况的两个因素:辛普森声称已经构建了一个反例，但他无法说明我们论文中的错误在哪里。因此，不清楚是我们在论文中某个地方犯了错误，还是他在反例中某个地方犯了错误。目前的数学研究依赖于一个基于声誉的相互信任的复杂系统。辛普森的论文发表时，我和卡普拉诺夫都有了很高的声誉。辛普森的论文对我们的结果产生了怀疑，导致其他研究人员没有使用它，但没有人站出来质疑我们的结果。
在我发现我的动机论文中的错误的时候，我正在研究一个新的发展，我称之为2理论。当我致力于这些想法时，我越来越不确定如何继续下去。二元理论的数学正是我和卡普拉诺夫在1989年梦想的高维数学的一个例子。我真的很喜欢发现新的结构，这些结构不是低维结构的直接延伸。
但是，要达到我认为必要的严谨和精确的工作水平，需要付出巨大的努力，而且会产生非常难以阅读的文本。谁能保证我没有忘记什么，没有犯错误，即使是更简单的论点中的错误也需要数年才能发现?我想就是在这一刻，我基本上停止了所谓的“好奇心驱动的研究”，开始认真思考未来。我没有工具去探索那些好奇心引导我的领域，那些我认为有价值、有趣和美丽的领域。
所以我开始研究我能做些什么来创造这样的工具。我很快就明白了，唯一的长期解决办法就是让我能够用电脑来验证我抽象的、逻辑的和数学的结构。这种软件从六十年代就开始开发了。当时，当我在2000年左右开始寻找实用的证明助手时，我找不到一个。有几个小组在开发这样的系统，但没有一个适合我所需要的那种数学系统。
当我第一次开始探索这种可能性时，计算机证明验证在数学家中几乎是一个禁忌的话题。关于计算机证明助手的需求的对话总是会转移到Gödel的不完备性定理(它与实际问题无关)，或者转移到一两个已经存在的证明的验证案例，这些例子只是用来证明整个想法是多么不切实际。
在这段时间里，有汤姆·黑尔斯和卡洛斯·辛普森等为数不多的数学家坚持不懈地推动数学计算机验证领域的发展。今天，仅仅几年后，计算机验证的证明和数学推理一般看起来完全可行的许多人的工作单价的基础同伦类型理论。
需要解决的主要挑战是，数学基础还没有为这项任务的要求做好准备。用一种精确到计算机都能理解的语言来表述数学推理，意味着使用一种基本的数学系统，而不是作为建立一些基本定理的一致性标准，而是一种可以用于日常数学工作的工具。现有的基本制度存在两个主要问题，使之不完善。首先，现有的数学基础是建立在谓词逻辑语言上的，这类语言的局限性太大。其次，现有的基础不能用来直接表达对这样的对象的陈述，例如，我在2理论的工作。
然而，要接受数学需要一个全新的基础是极其困难的。甚至许多与同伦类型理论有直接联系的人也在与这个观点作斗争。有一个很好的理由:现有的数学基础——ZFC而且范畴论——非常成功。对我个人来说，克服范畴论作为数学新基础的候选人的吸引力是最具挑战性的。
故事从ZFC开始:TheZermelo-Fraenkel理论用选择公理。自20世纪上半叶以来，数学被作为一门基于ZFC的科学，ZFC作为谓词逻辑的一种特殊理论被引入。因此，想要深谙数学之道的人有一条简单的路可走——学习谓词逻辑是什么，然后学习一种叫做ZFC的特定理论，然后学习如何将关于几个基本数学概念的命题转化为ZFC的公式，然后通过例子，学会相信数学的其余部分可以简化为这几个基本概念。
这种状态对数学极为有益，它被理所当然地认为是20世纪抽象数学取得巨大成功的原因。从历史上看，ZFC的第一个问题可以在早期布尔巴基的伟大事业的衰落中看到，这是因为二十世纪下半叶数学的主要组织思想是基于范畴理论的，而范畴理论无法用ZFC来很好地呈现。范畴论的成功启发了这样一种观点，即范畴是“下一个维度的集合”，数学的基础应该建立在范畴论或其高维类似物的基础上。
对我来说，最大的障碍是类别是“下一个维度的集合”。我清楚地记得，当我明白这个想法是错误的时候，我所经历的那种突破的感觉。类别不是“下一个维度的集合”。它们是“下一维的部分有序集”和“下一维的部分有序集”广群．
这种关于“群胚”和“范畴”的新观点对我来说需要一些调整，因为我记得我学数学的那些人都强调，格罗滕迪克研究代数几何的方法之所以如此成功，原因之一是他打破了老派学者的传统，坚持考虑所有的态射，而不仅仅是同构。(群胚通常由集合级对象及其同构组成，而类别通常由集合级对象和所有的态射组成。)
单价基金会与基于ZFC的基金会一样，是一个完整的基金会体系，但与基于ZFC的基金会有很大不同。为了提供一种比较形式，让我假设任何既适合人类推理又适合计算机验证的数学基础都应该具有以下三个组成部分。
第一个组成部分是形式演绎系统:一种语言和用这种语言操作句子的规则，这些规则是纯形式的，这样计算机程序就可以验证这种操作的记录。第二个组成部分是一种结构，它以人类直观可理解的心理对象的形式为这种语言的句子提供意义。第三个组成部分是一个结构，它使人们能够根据与语言直接相关的对象来编码数学思想。
在基于zfc的地基中，第一个组件有两个“层”。第一层是构建演绎系统的一般机制，称为谓词逻辑;第二层是一个特殊的演绎系统，称为ZFC，通过将该机制应用于一组操作和公理而得到。ZFC中的第二个组件基于人类直观理解层次结构的能力。事实上，ZFC的公理可以被视为所有层次结构都满足的属性的集合，再加上假定存在无限层次结构的无穷公理。第三个组成部分是一种按照层次结构来编码数学概念的方法，这种方法从编码集合的数学属性的规则开始。这就是为什么ZFC通常被称为集合论。
一元基础的原始形式演绎系统被称为归纳结构的演算，或中投公司．它是由蒂埃里Coquand而且克里斯汀•波林大约在1988年，它是基于计算机语言理论和实践的思想与构造数学思想的结合。与这些思想相关的关键名称是尼古拉·德·布吕因政府，每Martin-Lof而且让吉拉德．证明助理的正式演绎制度公鸡是中投公司的直系后裔。
单价基础的第二个组成部分，即为CIC的句子提供直接意义的结构，是基于单价模型的。通过这些模型与句子直接相关的对象称为同伦类型。同伦类型的世界被我们称为h-level的东西分层，h-level 1的类型对应于逻辑命题，h-level 2的类型对应于集合。我们对更高层次类型的直觉主要来自它们与多维形状的联系，基于zfc的数学研究了几十年。
单价基的第三个组成部分，是一种用同伦类型来编码一般数学概念的方法，它是基于我们在“∞-群胚”论文中考虑的70年代末Grothendieck思想的逆转。无论是在数学上还是在哲学上，这都是这个故事中最深刻也是最难以理解的部分。
自2005年以来，我一直在研究导致发现单价模型的想法，并于2009年11月在Ludwig-Maximilians-Universität München上就这一主题进行了首次公开演讲。虽然我独立地构建了我的模型，但这个方向的进展早在1995年就开始出现，并与马丁•霍夫曼，托马斯streich，史蒂夫Awodey,迈克尔•沃伦．
2010年春天，我向数学学院建议，我将在2012-13学年组织一个关于数学新基础的特别项目，尽管当时还不清楚该领域是否已经为这样的项目做好了准备。
现在我用一个证明助手来做数学运算。我有很多愿望想让这个证明助手更好地工作，但至少我不用回家担心在工作中犯了错误。我知道如果我做了某件事，我就做了，我不需要回到它，也不需要担心我的论点太复杂，也不需要担心如何让别人相信我的论点是正确的。我可以相信电脑。在计算机科学领域有很多人在为我们的项目做出贡献，但大多数数学家仍然不相信这是一个好主意。我认为这是非常错误的。
我要感谢所有努力理解单价基金会理念的人，感谢所有发展这些理念的人，感谢所有努力将这些理念传播给他人的人。
建议查看:关于单价基础的特别方案弗拉基米尔•Voevodsky该研究所在2012 - 2013年组织的一项研究结果是，二十多位数学家在不到六个月的时间里写出了一本600页的书。这本书在http://homotopytypetheory.org/book/．本文改编自Voevodsky在3月份的一次演讲;该视频可在//www.pdxgs.com/video/voevodsky14/．
