Formalizing the Solow Model in \(\mathbb {N}\) aproche
摘要
In 1956, Robert M. Solow published a mathematical theory which describes capital accumulation, technological advancements, and population growth. The Solow model is widely used in economics. In this paper we describe a formalization of the model in the \(\mathbb {N}\) aproche proof assistant. The formalization also encompasses mathematical foundations from real analysis. This is the first formalization of an economic model which is also readable like an ordinary mathematical text.