Доказал на Lean 4 несколько теорем про факториал и алгоритм Евклида.

Это было довольно забавно! Правда, на индукции я немного забуксовал. Нужно разобраться с этим подробнее. Советую попробовать вам самим доказать какие-нибудь теоремы.

Для обучения Lean есть несколько игр. Там постепенно вводятся тактики, хотя мне больше пользы принесло доказательство теорем в обычном редакторе с подсказками от ИИ. Он правда иногда ошибается, но Lean подсветит ошибки.

Есть учебники по Lean, а попробовать его можно в песочнице.

Если вы захотите посмотреть мои доказательства, вам нужно будет скопировать код в песочницу, и смотреть прогресс доказательства, наводя курсор на какое-либо место в доказательстве. Там будут показаны те положения, которые на уже точно известны, и те, которые нужно доказать.

Особенно интересно может быть написать какую-нибудь программу (это ведь язык программирования!) и доказать некоторые её свойства (это же помощник для доказательств!)

Буду рад, если кто-нибудь присоединится ко мне в изучении этого языка!