Всем привет! На manytask вышла первая домашка по Lean. Во всех задачах нужно заменить sorry на валидные доказательства. Чекер проверяет что доказательство компилируется и не содержит запрещенных тактик. В решении вы можете менять импорты, вводить новые теоремы, и делать все что угодно, только не менять формулировки задач.

Кроме того, появилась запись первой лекции

Для поиска лемм в Mathlib можно использовать leansearch.net (семантический поиск) и
loogle.lean-lang.org (синтаксический)

Вопросы можете задавать под этим постом, постараюсь оперативно отвечать