Проект формально проверяет экономические теории и модели с помощью математического доказательства в Lean 4, чтобы исключить ошибки в расчётах.
LeanEconomics переносит экономическую теорию и алгоритмы решения экономических моделей на язык формальной верификации Lean 4 с использованием библиотеки Mathlib. Каждая теорема в проекте проверяется программой-ядром с нуля, без допущений на веру, что исключает ошибки, которые могут накапливаться при обычном цитировании старых доказательств. Первый результат проекта — строгое доказательство единственности стационарного равновесия в экономической модели Айягари 1994 года, вопрос, остававшийся открытым много лет.
Описание автора:Economic theory and the algorithms that solve economic models, formalised in Lean 4 against Mathlib
