I might try this as a fun hobby project
Has anybody tried formalizing economics in Coq/Lean?
-
Sort of there has been some work done in Mathematica, see the Theorema project. also there has been some work done with Idris and I think also Agda. Lean is sort of new, I've been planning on looking into it further. I've not seen anything specific for Coq but the above languages are competitors so they cover basically what you are asking for. I've posted on this on EJMR before, so a search could turn up something I've missed. There are a very small number of economists interested in this stuff but they do exist.
-
Sort of there has been some work done in Mathematica, see the Theorema project. also there has been some work done with Idris and I think also Agda. Lean is sort of new, I've been planning on looking into it further. I've not seen anything specific for Coq but the above languages are competitors so they cover basically what you are asking for. I've posted on this on EJMR before, so a search could turn up something I've missed. There are a very small number of economists interested in this stuff but they do exist.
thanks for the tip
-
I might try this as a fun hobby project
Are you actually an economist?
Economics isn't in principle derivable from axioms using logic, and hence not possible to formalize.
WTF are you babbling about?shoo reg monkey, this is a theorist thread
I don't think he is even an economist. Probably a sociologist pretending to be a reg monkey because he thinks its a status upgrade.
-
I might try this as a fun hobby project
Are you actually an economist?
Economics isn't in principle derivable from axioms using logic, and hence not possible to formalize.
WTF are you babbling about?shoo reg monkey, this is a theorist thread
There is no possible way that a PhD economics theorist would be so utterly stoopid and cIuless to think economics could be formalized with a therem-prove like Coq.
-
I might try this as a fun hobby project
Are you actually an economist?
Economics isn't in principle derivable from axioms using logic, and hence not possible to formalize.
WTF are you babbling about?shoo reg monkey, this is a theorist thread
There is no possible way that a PhD economics theorist would be so utterly stoopid and cIuless to think economics could be formalized with a therem-prove like Coq.
Paper no. 8 http://www.socscistaff.bham.ac.uk/rowat/
-
I might try this as a fun hobby project
Are you actually an economist?
Economics isn't in principle derivable from axioms using logic, and hence not possible to formalize.
WTF are you babbling about?Tell that to Arrow and Debreu
Neither tried to formalize economics with a Theorem-prover, you imbeciIe.
Neither would. It is laughable that anyone but an utterly naive and cIueless undergrad would think it made sense to consider.
-
I might try this as a fun hobby project
Are you actually an economist?
Economics isn't in principle derivable from axioms using logic, and hence not possible to formalize.
WTF are you babbling about?Tell that to Arrow and Debreu
Neither tried to formalize economics with a Theorem-prover, you imbeciIe.
Neither would. It is laughable that anyone but an utterly naive and cIueless undergrad would think it made sense to consider.The claim was that it is not possible to formalize economics, both of them attempted to formalize parts of economics. If one can formalize it by using axiomatic approaches, then one can certainly use proof assistants to assist in this process. This is precisely what CR has been doing for a number of years and he has received reasonably large grants to do so. He is not the only one. There are other people using proof assistants in economics as well. That you do not know this speaks to your ignorance of what research is being conducted in this area.
-
The claim was that it is not possible to formalize economics, both of them attempted to formalize parts of economics. If one can formalize it by using axiomatic approaches, then one can certainly use proof assistants to assist in this process. This is precisely what CR has been doing for a number of years and he has received reasonably large grants to do so. He is not the only one. There are other people using proof assistants in economics as well. That you do not know this speaks to your ignorance of what research is being conducted in this area.
Using mathematics to formalizing specific mathematical problems that arise in economics, is NOT even remotely the same as "formalizing economics with a theorem-prover".
Either you are being purposely obtuse, or you're really not very smart.
-
I might try this as a fun hobby project
Are you actually an economist?
Economics isn't in principle derivable from axioms using logic, and hence not possible to formalize.
WTF are you babbling about?Tell that to Arrow and Debreu
Neither tried to formalize economics with a Theorem-prover, you imbeciIe.
Neither would. It is laughable that anyone but an utterly naive and cIueless undergrad would think it made sense to consider.I don’t think anyone has ever been as upset over proof assistants are you are right now