cd ..

:~/Teaching Economics to my Computer (New)

In summer 2022, I launched a project to formalize some foundational microeconomics in the Lean proof assistant.

Lean is a programming language that implements dependent type theory. It is possible to formalize complex mathematical concepts in this language. More importantly, it is possible to have the computer exhaustively check proofs of results written in this language.

The more knowledge that is encoded in a Lean (or any formal system) the easier it is to check, and possibly in the future, automatically generate proofs.

What’s Done?

Mas-Colell, Whinston, Green Microeconomic Theory

- Proposition 1.B.1 - Proposition 1.B.2 Kreps’ Microeconomics Foundations

- Proposition 1.9: various relation properties.