Conference: School and Workshop on Univalent Mathematics

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

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.