Кроме эссе о вычислительном подходе, в сосденем чате мне посоветовали следующие две статьи, мимо которых было очень сложно пройти:
1. Formal Microeconomic Foundations and the First Welfare Theorem
2. Social Choice Theory in Isabelle/HOL

Первая формализует в Isabelle/HOL 2 экономические модели и доказывает First Theorem of Welfare Economics (рациональные эгоистичные агенты со временем достигают эффективной аллокации -- далее FWT). Вторая доказывает Arrow's Impossibility theorem (далее AIT)-- теорему, которая утверждает, что с некоторыми минимальными условиями невмешательства выборная система приводит к диктатуре.

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

With that out of the way, я бы вернулся к FWT.
Статья вводит краткую историю интереса к формальной верификации подобных теорем, и описывает как они влияют на мир -- в первую очередь, через уже привычное нам влияние на policy decisions. С развитием доказательного софта, пишут авторы, можно более четко и формально определять экономическую теорию, понимать ее предпосылки и ограничения.

Для доказательства FWT авторы строят небольшой фреймворк из формализации нескольких определений и двух экономических моделей:
1. pure consumer market
2. means of production private ownership model

После небольшой справки о доказательств в экономике, в т.ч. через Теорию Игр и формализацию эквилибриума с помощью языка Coq, нам помогают сориентироваться в языке Isabelle/HOL и переходят к микроэкономическим определениям -- в первую очередь, кто есть producer, а кто consumer. Особенно важно, что авторы рассматривают модель с perfect competition и только в определенных видах рынков, где каждый актор совершает только предельно малый процент транзакций.

Сам процесс я в деталях описывать пока не буду для экономии места и времени (к чему прошу отнестись с пониманием), поэтому предлагаю принять доказательства авторов на веру.

К каким выводам можно прийти рассмотрев подобные доказательства?

Во-первых, что уже существует некоторый фреймворк, в рамках которого можно было бы обращаться к более конкретным и вычислимым вещам, и, соответственно, более прозрачным и предсказуемым policy decisions.

Во-вторых, что в рамках теории еще существует непаханное поле, которое требует подробного вмешательства и конкретизации -- мы не можем принимать экономические решения, исходя только из крайне абстрактных примеров и подходов, которые на реальный мир сейчас не распространяются: мне сложно придумать рынки, которые соответствовали предпосылкам. Однако, это не в коем случае не инвалидирует теоремы теоретически (в конце концов, сложно инвалидировать формальную логику), но дает возможность понимать, в какую сторону теорию можно развивать, чтобы получать предсказуемые результаты.

К статье о AIT я подробно подберусь несколько позже, но пока могу отметить два предварительных соображения:
1) авторы статьи о доказательстве FWT неоднократно ее упоминали и ссылались в контексте Game Theory, что делает Social Choice особенно интересным в контектсе описания систем открытыми играми и, через это, компьютеризации многих непрозрачных и эксплуатируемых механизмов в обществе
2) Доказательство AIT также открывает дорогу конкретизации в формальной верификации социального выбора, что может, как и формализация экономики, положительно повлиять (и обязательно повлияет!) на правовые//избирательные policy decisions, не говоря уже о взаимосвязи собственно экономики с правовой сферой.