Як вивчати Lean

Огляд того, як почати працювати з Lean з нуля

Lean - це і функціональна мова програмування загального призначення, і асистент доведення теорем. Існує чимало ресурсів для вивчення Lean: одні з них зосереджуються на аспектах програмування, інші на застосуванні Lean як доводжувача теорем.

Книга Functional Programming in Lean знайомить із парадигмою функціонального програмування на прикладі Lean. Вона адресована програмістам, які хочуть вивчити Lean, навіть якщо вони раніше не мали досвіду роботи з функціональними мовами програмування.

Для глибшого ознайомлення з доведенням теорем у Lean як офіційний ресурс указано книгу Theorem Proving in Lean 4.

The Lean Language Reference - це авторитетне джерело докладної інформації про мову.

Багато додаткових ресурсів для вивчення Lean пропонує Lean Community.