Voevodsky 在一篇关于泛等基础的动机的文章中回忆了促使他研究形式化数学的几次事件:
- 在 1999-2000 年, Voevodsky 发现他 1992-1993 年的一篇论文中的关键引理证明有误. 那几年之间, 许多数学家研究并讨论过这篇文章, 但无人指出错误.
- 1998 年, C. Simpson 的文章 Homotopy Types of Strict 3-groupoids 包含了一个例子, 说明 Voevodsky 与 Kapranov 1989 年的文章 ∞-Groupoids as a Model for a Homotopy Category 的主要结果不成立. 但当时没有人能指出 Voevodsky 与 Kapranov 论证中的具体错误. 这个错误直到 2013 年才被清晰地认识.
他总结道,
A technical argument by a trusted author, which is hard to check and looks similar to arguments known to be correct, is hardly ever checked in detail.
由可信的作者给出的技术论证, 如果难以检验, 但又长得像正确的证明, 那么几乎从不会有人仔细验证.
V. Voevodsky, The Origins and Motivations of Univalent Foundations
接着他认为
… the only long-term solution was somehow to make it possible for me to use computers to verify my abstract, logical, and mathematical constructions.
唯一的长期解决方案是让计算机能够验证我那些抽象的逻辑和数学构造.
V. Voevodsky, 上述引文
当时形式化数学的系统已经存在, 但没有适合于 Voevodsky 希望做的与高阶范畴有关的数学的系统. Voevodsky 指出问题的根源在于当时人们使用的数学的基础不适合于他想做的数学.