Hello.

Stream: new members

[Greg Leo]

Hello all, I am a professor of Economics in the US. I have been watching Kevin’s videos, and I would like to try a similar teaching experience with some of undergraduates and graduate students- to formalize some of our basic microeconomic theory results.

I am very new to Lean, and just working through some basics at the moment.

[Kevin Buzzard]

Hi! What are examples of these basic results?

[Greg Leo]

We tend to start with relations that represent “preferences”. We assume some basic axioms and build up from there. One early goal I can imagine is formalizing the “Debreu Theorems” which are various statements about the representation of these preference relations by real-valued functions

[Kevin Buzzard]

Just looking on the Wikipedia page it looks like this should be fine to do in Lean 3 if you use its maths library mathlib.

[Greg Leo]

Excellent. After reading a bit yesterday, what’s what I installed. I am going to work through the natural number game and some examples on relations in the documentation today.

[Greg Leo]

To be honest, as far as teaching goes, I think even proving some simple results about relations will be instructive for my students- especially my undergrads. I loved how you relate using Lean to playing levels of a game. I think this could help get some students interested in mathematics.

[Greg Leo]

I often use the same analogy when I solve models for my class using some live-coding style lectures I do with lyx (a latex frontend) and mathematica.

[Andrew Souther]

Hello! I have an ongoing project to formalize some basic ideas from Rational Choice Theory and Social Choice Theory in my repository lean-social-choice. The repo is a bit messy right now, but you may find some of the work helpful. Feel free to reach out with any questions or ideas. Notably, I have formalized Arrow's Impossibility Theorem. Now, I am working to formalize a current ongoing research project in Voting Theory.

Eventually, I hope to branch out and formalize some Game Theory or classic Micro Theory. I would love to hear how some of this work pans out for you!