Formalizing Economics in Lean 4
Master Project

MSc Project: Formalising Economics in Lean 4

This document gives an overview of thesis work in this area: what the projects involve, what background they need, which results could be formalised, and where to start reading. No prior knowledge of economics, category theory, or Lean is required; these are covered during the thesis, with supervision.

Background

A proof assistant is a program that checks a mathematical proof step by step. Lean 4 is one such system. Its library, Mathlib, contains checked proofs ranging from first-year calculus to recent research results.

Economics does not generally work this way. Economic theorems are checked by other economists reading them. Those theorems are used in areas such as tax design, auction rules, market regulation, and the schemes that match students to schools or donors to patients.

These projects state economic theorems in Lean and prove them there, so that every step is machine-checked. In some cases this makes explicit an assumption that the informal proof left unstated.

Fields involved

• Economics. The source of the theorems: microeconomics, social choice and voting, mechanism design, game theory.
• Lean 4 and Mathlib. The system in which the proofs are written and checked. Much of the work is translating economic definitions into precise mathematical objects.
• Category theory. A general language for describing structure. Used in one group of topics.
• Haskell. Used in one group of topics, to derive program code from a checked proof so that the proof’s guarantees are enforced by the type system.

Background required and acquired

Requirements vary by topic. Real analysis at second-year undergraduate level and basic abstract algebra are generally useful, and familiarity with functional programming or formal logic helps. Prior experience with Lean is not required.

Over a thesis, students generally acquire: the ability to read and write economic theory at a rigorous level, working knowledge of a proof assistant, and — depending on the topic — category theory or type-level programming.

Topics

The areas below are ones this project has worked in, each with examples of results that could be formalised. They are starting points rather than a fixed menu: a thesis can take up a question from within one of them, combine several, or pursue a related result that is not mentioned here.

1. Markets: prices, monopoly, and welfare. These topics concern the conditions under which a market has a price at which supply equals demand, whether that price is unique, and the effects of monopoly on welfare. Results that could be formalised: existence and uniqueness of a competitive equilibrium price, where the main tool is the Intermediate Value Theorem; the Lerner index, which relates a monopolist’s markup to the price sensitivity of demand; the deadweight loss caused by monopoly; and the existence of equilibrium in markets where each firm’s best action increases with its rivals’ actions, which uses a fixed-point theorem for ordered sets. Reading: Competitive equilibrium, Arrow–Debreu model, Lerner index, Deadweight loss, Intermediate value theorem, Knaster–Tarski theorem.

2. Impossibility results. Several results in economics state that no set of rules can achieve a given combination of goals. Results that could be formalised: Myerson–Satterthwaite, that when a buyer and a seller each know only their own valuation, no mechanism guarantees they trade whenever trade would benefit both; Arrow’s theorem, that any method of combining individual rankings into a single group ranking which satisfies a short list of conditions is a dictatorship; and Gibbard–Satterthwaite, that any voting rule over three or more options under which no voter ever gains by misreporting preferences is also a dictatorship. Reading: Myerson–Satterthwaite theorem, Arrow’s impossibility theorem, Gibbard–Satterthwaite theorem, Social choice theory. Geanakoplos, Three brief proofs of Arrow’s impossibility theorem (2005), gives a short proof.

3. Bookkeeping and blockchain. Double-entry bookkeeping has an algebraic structure that can be stated in group-theoretic terms. A blockchain ledger records the same information in a different form. Results that could be formalised: the group structure underlying the requirement that debits equal credits; an isomorphism showing that a blockchain ledger and a double-entry journal carry the same information; and a Haskell implementation in which books that do not balance cannot be represented. The implementation is the largest part of this work. Reading: Double-entry bookkeeping, Blockchain, Group (mathematics), Isomorphism. Then Ellerman, The mathematics of double entry bookkeeping (1985), and Renes, Blockchains and non-financial performance (2023).

4. Mechanism design and category theory. Mechanism design concerns the design of rules: auctions, voting systems, and schemes that match students to schools. These topics restate parts of it in the language of category theory. Results that could be formalised: Arrow’s theorem restated as the emptiness of a particular collection of objects; and the question of whether an optimal mechanism can be characterised by a universal property. The second is difficult and remains open. Reading: Mechanism design, Category theory, Functor, Universal property. For related background, see the work of Hedges and others on “open games.”

5. Equilibrium in games. These topics concern whether players who each choose a best reply to the others reach a stable outcome. Results that could be formalised: existence of Nash equilibrium in finite games, proved using a fixed-point theorem; and correlated equilibrium, in which the players observe a common random signal before acting. The set of correlated equilibria has a simpler structure, so existence is easier to establish. Reading: Nash equilibrium, Correlated equilibrium, Brouwer fixed-point theorem, Kakutani fixed-point theorem.

Reading on the tools

Lean. The Natural Number Game is an introductory tutorial that runs in a browser; it is listed on the Lean community’s Learn page. Theorem Proving in Lean 4 is the standard reference, and the Mathlib documentation shows what has already been formalised. General overviews: Lean (proof assistant), Proof assistant.

Category theory. Needed only for the mechanism design topics. The Wikipedia articles listed under topic 4, then Riehl, Category Theory in Context, which is available free.

Economics. The Wikipedia articles above cover the individual results. Mas-Colell, Whinston & Green, Microeconomic Theory (1995), is the standard graduate reference.

Contact

This project is supervised by:

• Benedikt Ahrens, B.P.Ahrens@tudelft.nl
• Sander Renes, S.Renes-1@tudelft.nl