Email Gateway (Aug 22 2022 at 16:01): Email Gateway (Aug 22 2022 at 16:01):From: Lawrence Paulson <lp15@cam.ac.uk>
I am happy to announce this new entry, from Julian Parsert and Cezary Kaliszyk:
https://www.isa-afp.org/entries/First_Welfare_Theorem.html
"Economic activity has always been a fundamental part of society. Due to modern day politics, economic theory has gained even more influence on our lives. Thus we want models and theories to be as precise as possible. This can be achieved using certification with the help of formal proof technology. Hence we will use Isabelle/HOL to construct two economic models, that of the the pure exchange economy and a version of the Arrow-Debreu Model. We will prove that the First Theorem of Welfare Economics holds within both. The theorem is the mathematical formulation of Adam Smith's famous invisible hand and states that a group of self-interested and rational actors will eventually achieve an efficient allocation of goods and services."
I look forward to seeing more work on economics and finance!
Larry Paulson
Email Gateway (Aug 22 2022 at 16:01):From: Corey Richardson <corey@octayn.net>
I'm really looking forward to seeing more economics too! But I'd love to
see this one ;)
https://www.isa-afp.org/browser_info/current/AFP/First_Welfare_Theorem/document.pdf
is a 404. Guess I just wait for Jenkins to catch up
Email Gateway (Aug 22 2022 at 16:01):From: Lars Hupel <hupel@in.tum.de>
Those aren't being generated by Jenkins though, only for the devel AFP :-)
Cheers
Lars
Email Gateway (Aug 22 2022 at 16:02):From: Lawrence Paulson <lp15@cam.ac.uk>
Working now. Sorry about that.
Larry
Last updated: Apr 26 2024 at 12:28 UTC