Типизированная математика

• Основы
  • Синтаксис
  • Функции
    • Лямбда-исчисление
    • Мир безымянных функций
    • Упражнения
  • Логика
    • Импликация
    • Квантор всеобщности
    • Конъюнкция и дизъюнкция
    • Отрицание
    • Квантор существования
    • Принцип исключённого третьего
    • Логика первого порядка
  • Исчисление построений
    • Свойства
    • Зависимые функции
    • Исчисление построений
    • Индуктивные типы
      • Двоичные деревья
      • Деревья бесконечной ширины
      • Парадоксальный индуктивный тип
      • Списки
    • Исчисление индуктивных построений
  • Lean
    • Установка
    • Основы Lean
    • Упражнения
    • Равенство
  • Натуральные числа
    • Сложение
    • Сравнения
    • Разрешимость
    • Вычитание
    • Умножение
    • Сильная индукция
    • Деление и остаток
    • Где найти леммы?
• Разное
• Сообщество