Lean 4 — это интерактивный помощник по доказательствам, где математика пишется как код, а машина проверяет каждое определение и шаг рассуждения
Учебник Mathematics in Lean учит формализовывать задачи на понятном «языке доказательств»: от элементарной теории чисел до анализа и меры
За спиной — большая библиотека Mathlib и активное сообщество в чате Lean Zulip, так что вы не останетесь одни
Книга задумана как «живой» учебник внутри VS Code
Открываете Lean, печатаете определения и леммы, а в правой панели сразу видите цели и подсказки от системы
Практика — в центре: каждый раздел сопровождается файлом с примерами и упражнениями, их удобно править прямо в редакторе и тут же смотреть реакцию Lean (вплоть до простых экспериментов вроде #eval "Привет, мир!")
Старт простой: ставите Lean 4 и VS Code, клонируете репозиторий mathematics_in_lean, открываете папку MIL и работаете в своей копии, чтобы безболезненно подтягивать обновления
Внутри — аккуратная структура по главам, текстовые подсказки и готовые решения в отдельной папке для самопроверки
Документацию удобно вызывать прямо из редактора через команду «Lean 4: Docs»
Если не хочется настраивать среду локально, всё запускается в облаке через Gitpod: открыли проект — и можно учиться с телефона или любого ноутбука
Учебник ещё развивается, поэтому время от времени стоит обновлять репозиторий — материалы пополняются
https://leanprover-community.github.io/mathematics_in_lean/C01_Introduction.html
Учебник Mathematics in Lean учит формализовывать задачи на понятном «языке доказательств»: от элементарной теории чисел до анализа и меры
За спиной — большая библиотека Mathlib и активное сообщество в чате Lean Zulip, так что вы не останетесь одни
Книга задумана как «живой» учебник внутри VS Code
Открываете Lean, печатаете определения и леммы, а в правой панели сразу видите цели и подсказки от системы
Практика — в центре: каждый раздел сопровождается файлом с примерами и упражнениями, их удобно править прямо в редакторе и тут же смотреть реакцию Lean (вплоть до простых экспериментов вроде #eval "Привет, мир!")
Старт простой: ставите Lean 4 и VS Code, клонируете репозиторий mathematics_in_lean, открываете папку MIL и работаете в своей копии, чтобы безболезненно подтягивать обновления
Внутри — аккуратная структура по главам, текстовые подсказки и готовые решения в отдельной папке для самопроверки
Документацию удобно вызывать прямо из редактора через команду «Lean 4: Docs»
Если не хочется настраивать среду локально, всё запускается в облаке через Gitpod: открыли проект — и можно учиться с телефона или любого ноутбука
Учебник ещё развивается, поэтому время от времени стоит обновлять репозиторий — материалы пополняются
https://leanprover-community.github.io/mathematics_in_lean/C01_Introduction.html