Я не могу поверить, что люди пишут код на Lean вручную. И что до LLM все это формализовывалось. Формализовать что-либо в Lean так же приятно, как снимать кожу с себя картофелечисткой, и так же интересно, как смотреть, как сохнет краска.

Не рассказывай мне о "радости игры" / "это так интерактивно" или что-то в этом роде. Есть игры, в которых есть на что посмотреть, так же как и везде есть ра*е, и я знаю разницу.

@notmoeezm "Мне вообще пофиг, если машины проверяют доказательства" источник: парень, который настраивает алгоритмы поиска в пространстве доказательств для удовольствия, используя Lean😞