No results found

GameTheory

GameTheory Project

Welcome to the Game Theory project! This repository contains implementations and analyses related to game theory based on Mathlib. Our group is working on more contributions on the formalization of gamtheory perfix. Below is a brief overview of the contents and setup instructions.

Contents

  • GameTheory/Secondprice.lean: Formalise some core concepts and results in auction theory. This includes definitions for first-price and second-price auctions, as well as several fundamental results and helping lemmas.
  • GameTheory/Zerosum.lean: The complete proof of von Neumann's minimax theorem about zero-sum games.

Current plan for formalization of Game Theory

The current plan for the formalizing of Game Theory include:

1. Auction Theory. 🎉 (200+ lines, PR) link
  • Essential definitions of Sealed-bid auction, First-price auction and Second-price auction.
  • First-price auction has no dominant strategy.
  • Second-price auction has dominant strategy. (Second-price auction is DSIC)
  • Will depend on #14163 once that PR is merged. The Fintype lemmas introduced by this PR have been added in that PR and will be removed from here once that PR gets merged
2. Mechanism design & Myerson's Lemma. 🎉 (400+ lines, pending for modification to Mathlib Standard)
  • Mechanism design An allocation rule is implementable if there exists - Dominant Strategy Incentive Compatible (DSIC) payment rule - An allocation rule is monotone if for every bidder’s gain is nondecreasing w.r.t. her/his bid
  • Myerson's Lemma Implementable ⇔ Monotone In the above case, the DSIC payment rule is unique.
3. von Neumann‘s Minimax Theorem. 🎉 (800+ lines, pending for modification to Mathlib Standard)
  • Equilibrium in zero sum game
  • Formalization strategy: via Loomis’s theorem.
4. Nash Equilibrium. 🎉 (pending for modification to Mathlib Standard)
5. Brouwer fixed-point theorem. (Work in Progress)
6. More Mechanism design.(Planning)

Reference

Roughgarden, Tim. Twenty Lectures on Algorithmic Game Theory. Cambridge University Press, 2020. Link

Contributors

Current contributors to this project are:

Authored-by:

Running on Gitpod

This project is configured to run on Gitpod. Simply open the repository in Gitpod to get a ready-to-use development environment in your browser.

Contributions

Contributions are welcome! Please fork the repository and create a pull request with your changes. Ensure to follow the coding standards and include tests for any new features.

License

This project is licensed under the MIT License.