Lean 4 — это интерактивный помощник по доказательствам, где математика пишется как код, а машина проверяет каждое определение и шаг

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