Conference: School and Workshop on Univalent Mathematics

该奖项支持明尼苏达大学2024/7/28-8/2期间第四届单价数学学校和研讨会的参与者。由菲尔兹奖牌获得者弗拉基米尔·沃沃茨基设计的“单价基础”是数学的另一种基础，特别适合于正式的计算机验证。因此，在单价基础中形成的数学证明可以由计算机自动检查。这次研讨会将是美国系列研讨会的第一次，旨在培训参与者在单价基金会的理论和实践方面的培训，并促进相关领域的研究活动。单价基金会有一些新的特点：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.