AML

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