Есть подозрения

lex_kravetski — 26.08.2025 Дошёл всё-таки до доказательств при помощи Lean — благо мне подсказали материалы, основанные на примерах.

И обнаружил странное: в эту игру можно играть не приходя в сознание.

В том смысле, что я не совсем ещё понял что там чему соответствует и как работает. То есть как это соотносится с реальными суждениями, мне не совсем ясно. А временами неясно совсем. И точно так же мне не совсем ясно, как это на самом деле работает в Lean. А временами… ну… вы знаете.

Однако закономерности всё равно видны, поэтому я настрочил за очень короткий срок штук тридцать доказательств, которые в материалах даются в качестве упражнений.

Выглядит сие очень подозрительно: как будто настолько чистый формализм, что достаточно уметь, скажем так, переставлять строки, а остальное неважно — язык будет рапортовать, что «ура, у нас тут ещё одно строжайшее доказательство». А к таким штукам я отношусь с большим подозрением.

Оставить комментарий

Популярные посты:

• Ранее
• Архив