Летняя математическая школа "Алгебра и геометрия"

Как писать математику используя систему Кок

Владимир Воеводский (Institute for Advanced Studies, США)

Видеозаписи лекций

• Лекция 1
• Лекция 2

Резюме

Кок - это программа, которая предоставляет набор инструментов для эффективной работы с формальными рассуждениями в современной (зависимой, полиморфной) теории типов.

На основании таких теорий типов сформулированы унивалентные основания, в которых примитивными объектами являются не множества, а бесконечность-групойды или, эквивалентно, гомотопические типы.

Поэтому, используя Кок, можно "писать" унивалентную математику в такой форме, что правильность рассуждений проверяется компьютером.

Я покажу часть имеющейся у нас сейчас библиотеки конструкций, включая конструкцию локализации коммутативных колец, и мы попробуем в классе построить конструкцию спектров коммутативных колец.

Студентам будет полезно посмотреть статью Experimental library of univalent formalization of mathematics, а также скачать и установить программу Кок.

Кок файл, созданный на лекциях, можно найти здесь.