Красивое: GlimpseOfLean : an introduction to theorem proving in Lean for the impatient.

Вот секретная ссылочка на код, в самом низу которой есть ссылочка на онлайн-версию. Просто симпатичная обучалка тактикам лина, а если ставите курсор на строчку, то видно как меняются значения переменных.

Евросообщество Lean4 доступ к своему сервису для России уже давно закрыло (как и к Racket кстати), поэтому можно в этот онлайн зайти только через впн, ну а так как скоро и эти три буквы у нас будут тотально ликвидированы и потеряется доступ к тысячам важнейших мировых математических и компьютерных ресурсов

(как например Калифорнийский университет Беркли, который на днях (следом за Йелем) признали нежелательной экстремистской организацией, и даже просто за ссылки на его научные труды - или за использование FreeBSD :) - можно легко получить штраф, если не что похуже -- от низовых исполнителей для лёгкой статистики, разбираться никто не будет),

рекомендую скачать себе локально весь GlimpseOfLean кому интересно, пока ещё не поздно. Ну и вообще готовимся к самому худшему. На моей жизни я уже ничего позитивного не жду.

p.s. Забыл, в их последнем деплое закомментите
import Mathlib.Data.Complex.Trigonometric