Почти 20 лет назад я написал учебник по анализу — «Анализ I» 📘. Его цель — дополнить существующие учебники, сделав акцент на основах: построении натуральных, целых, рациональных и действительных чисел 🔢, а также базовой теории множеств и логики для строгих доказательств 🧠.
И вот теперь я представляю Lean-версию книги 🚀 — «перевод» определений, теорем и задач из текста в код Lean. Это позволяет выполнять задания, заполняя пропущенные места в коде («sorries»). Официальных решений я не планирую публиковать — предлагаю создавать fork-репозитории с вашими решениями! 💡
Структура Lean-проекта:
- Глава 2.1: Натуральные числа 🌱
- Глава 2.2: Сложение ➕
- Глава 2.3: Умножение ✖️
- Эпилог главы 2: Изоморфизм с натуральными числами Mathlib 🔄
- Глава 3.1: Основы теории множеств 🌀
- Глава 4.1: Целые числа 🔢
Проект частично независим от стандартной библиотеки Lean Mathlib но использует её там, где это необходимо. Например:
- Сначала я вручную создаю «альтернативные» натуральные числа (`Chapter2.Nat`) 🌿, повторяя леммы из Mathlib (но оставляю доказательства как задания!).
- Затем в эпилоге устанавливается изоморфизм между ними и стандартными натуральными числами Mathlib 🌐.
- После этого `Chapter2.Nat` объявляются устаревшими, и работа продолжается с Mathlib. 📉
Такой подход постепенно погружает в мир Lean и Mathlib, сочетая изучение анализа с освоением инструментов формальной верификации — как в известной игре «Natural number game» 🎮 (которая тематически перекликается с главой 2 моего учебника).
P.S. Пока проект находится в одном репозитории с блогом, но в будущем может выделиться в отдельный 📂. Присоединяйтесь — исследуйте анализ через код! 👨💻👩💻