Conference: School and Workshop on Univalent Mathematics

本奖项支持于20124/7/28 -8/2在明尼苏达大学举办的第四届单价数学研讨班的参与者。由菲尔兹奖得主弗拉基米尔·沃沃茨基（Vladimir Voevodsky）设计的“一元基础”是数学的另一种基础，特别适合于正式的计算机验证。因此，用单值基础表述的数学证明可以由计算机自动检查。这个讲习班将是在美国举办的系列讲习班中的第一个，目的是对参加者进行单价基金会理论和实践方面的培训，并促进有关领域的研究活动。单价基础提供了一些新的特点：1。它建立在类型理论的基础上，而类型理论是一种形式语言，可以证明它更符合日常数学，并支持有效的计算机检查。集合论中的传统集合仍然可以表示为特定类型。元素之间的等式可以有更丰富的结构，适合于表示，例如，两个同构集合之间的不同同构。同构原则是内置的，它正式断言同构结构必须被视为平等的，因此，所有的定义都自动尊重同构。参与者将学习如何在一个可以提供即时反馈的计算机系统（证明助手）中使用单价基础来表达数学思想。有关该活动的更多信息可在https://unimath.github.io/minneapolis2024/.This上获得，该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

This award supports participants of the Fourth School and Workshop on Univalent Mathematics during 2024/7/28-8/2 at the University of Minnesota. The "Univalent Foundations," devised by Fields Medalist Vladimir Voevodsky, is an alternative foundation for mathematics that is particularly amenable to formal computer verification. Mathematical proofs formulated in the Univalent Foundations can thus be checked by computers automatically. This workshop will be the first one in the series in the United States, and aims to train the participants in the theory and practice of the Univalent Foundations and foster research activities in related areas.The Univalent Foundations offers certain novel features:1. It is based on type theory, a formal language that arguably matches everyday mathematics better and supports effective computer checking.2. Traditional sets from set theory can still be represented as particular types.3. Equalities between elements can have richer structures suitable for representing, for example, different isomorphisms between two isomorphic sets.4. The univalence principle is built-in, which formally asserts that isomorphic structures must be treated as equal, and thus, all definitions automatically respect isomorphisms.Participants will learn how to express mathematical ideas using the Univalent Foundations in a computer system (proof assistant) that can offer immediate feedback. More information about the event is available at https://unimath.github.io/minneapolis2024/.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.