I have also copied over the awaiting-review label from the old PR.

Latest version of code is updated, Kindly please review the code. Feel free to leave feedback. ; )

Auction is too specific. There are many other kinds of games in this theory. GameTheory?

I'm sorry that you have to wait for a long time. The main issue with this PR is that none of the current Mathlib maintainers is an expert in this area. We're trying to resolve this issue one way or another.

Do you have plans to formalize more advanced facts? If yes, what facts are you aiming for?

What do you think about giving a general definition of a game (what name should we use to avoid confusion with set theory games?) instead of building parallel APIs in 2 namespaces? This way you can define utility, pure and mixed strategies etc, then define firstPriceAuction (α : Type*) [Fintype α] : SomePrefixGame (Option α). While this approach requires more work at the start, it will make generic definitions (e.g., IsNashEquilibrium or IsDominating) apply to auctions.

@vihdzp What do you think about names for set theory games vs game theory/economics/social choice games?

These are completely different sorts of games.

GameTheory seems fine. I've only ever heard the stuff in SetTheory being referred to as combinatorial game theory with the extra qualifier.

Would it be possible to add more pointers to the reference, linking the results that you prove in this file to what is to be found in the book you quote?

GameTheory seems fine. I've only ever heard the stuff in SetTheory being referred to as combinatorial game theory with the extra qualifier.

I agree. As combinatorialGameTheory is often used to describe game theory problems that involve clear rules and strategic analysis. These problems typically involve finite, deterministic games, such as board games or other strategy games.

On the other hand, gameTheory is more general that encompasses studies involving mechanic design and strategic interactions in fields like economics. As my current plan involves Myerson's Lemma and mechanism design, then using gameTheory might be more appropriate.

Auction is too specific. There are many other kinds of games in this theory. gameTheory?

Actually auctions are just one specific application within gameTheory. gameTheory encompasses many other types of games and strategic interactions, including but not limited to mechanism design, game equilibria, and cooperative games.

For instance, myersonsLemma is also an important result in gameTheory, particularly in the field of mechanism design, which we have almost finished and pending for modification to Mathlib standard. It provides a method for designing incentive compatible mechanisms that allow participants to maximize their individual interests while also achieving the overall objectives desired by the designer. In doing so, myersonsLemma helps address issues of information asymmetry and incentive compatibility, making mechanism design widely applicable in areas such as auctions, public goods provision, and contract design.

For more of our plan, we have tried to 'sell' the plan formalised economic-related theorems to economist. I think we should spend more effort to address their attention and interests.

Would it be possible to add more pointers to the reference, linking the results that you prove in this file to what is to be found in the book you quote?

Hi, Filippo. It's great see you view our PR. I have attached the main reference of mine to the description of this PR. Since we are a group of students contributing to formalising gameTheory. We might use different references. I will check with my group members and update others'.

I doubt we'll ever have both namespaces open at once, the theories are very distinct from what little I know. It should be fine having something like Auction.Game.

In my personal view, gameTheory/Auction/Basic.lean,gameTheory/Myerson/Basic.lean,gameTheory/Nash/Basic.lean might be fine? Note that almost all specific field have a file named Basic.lean.

I doubt we'll ever have both namespaces open at once, the theories are very distinct from what little I know. It should be fine having something like Auction.Game.

In my personal view, gameTheory/Auction/Basic.lean,gameTheory/Myerson/Basic.lean,gameTheory/Nash/Basic.lean might be fine? Note that almost all specific field have a file named Basic.lean.

We were discussing namespaces, not file paths.

I suggest that you start with defining a game as something like

namespace GameTheory

universe u -- or should we drop universe polymorphism in this theory?

structure Game (Player : Type u) where
  /-- The type of possible strategies of a player. -/
  Strategy : Player → Type u
  /-- If each player chooses a strategy, then player `p` wins `payout f p`. -/
  payout : ((p : Player) → Strategy p) → Player → ℝ

Then you can define auction as

/-- Scheme of an auction with a single prize.

This formalization assumes that only the winner pays a price,
i.e., there are no entrance fees etc. -/
structure AuctionScheme (Player : Type u) where
  /-- Who gets the prize. -/
  winner (bid : Player → ℝ) : Player
  /-- How much does the winner pay for the prize. -/
  price (bid : Player → ℝ) : ℝ

def AuctionScheme.toGame {Player : Type u} (scheme : AuctionScheme Player)
    (utility : Player → ℝ) : Game Player where
  Strategy _ := ℝ
  payout (bid : Player → ℝ) (p : Player) := Pi.single (scheme.winner bid) (utility p - scheme.price p)

The first price auction and the second price auction can be defined as specific AuctionSchemes. Some definitions (e.g., DominantStrategy) can be given for any game, then used in theorems for these auctions.

@urkud : although dominant strategy is a common concept, it's definitions vary depending on the ambient context. I think having a common namespace called GameTheory would be a mistake unless there are further namespaces, such as AuctionTheory in this case. Also it might help to put all this in a Mathlib namespace to make it easy for downstream users to use similar names for different contexts.

@urkud : although dominant strategy is a common concept, it's definitions vary depending on the ambient context.

Could you please provide more details? What example doesn't agree with this?

def Game.Strategy.IsDominant {Player : Type} (g : Game Player) (p : Player) (s : g.Strategy p) : Prop :=
  ∀ s' t, g.payout t p ≤ g.payout (Function.update t p s') p

@urkud : I think having a common namespace called GameTheory would be a mistake unless there are further namespaces, such as AuctionTheory in this case.

I claim that Auction should be a special case of a Game, with different auctions (first price, second price etc) being defs of type Auction. Then facts about auctions will naturally go to GameTheory.Auction, while general facts will go to GameTheory.Game.

@urkud : although dominant strategy is a common concept, it's definitions vary depending on the ambient context.

Could you please provide more details? What example doesn't agree with this?

def Game.Strategy.IsDominant {Player : Type} (g : Game Player) (p : Player) (s : g.Strategy p) : Prop :=
  ∀ s' t, g.payout t p ≤ g.payout (Function.update t p s') p

I think it is too deeply tied to a specific kind of normal form game. In an extensive form game or an iterated game, players could have perfect or imperfect information about the previous actions of the other players. This definition of domination is too tightly coupled with one form of games.

Generalising the definition of games too much might make it clunky to work. I would put your definitions under a namespace called Normal Form Games.

Any game with multiple states, imperfect information etc can be represented as a Game in the sense of above definition (i.e., you can have structures describing a specific type of a game, then have toGame function). I don't know whether it should be called Game or NormalFormGame. However, I'm sure that definitions that can be given in this generality, should be given in this generality.

I think it is too deeply tied to a specific kind of normal form game. In an extensive form game or an iterated game, players could have perfect or imperfect information about the previous actions of the other players. This definition of domination is too tightly coupled with one form of games.

Generalising the definition of games too much might make it clunky to work. I would put your definitions under a namespace called Normal Form Games.

But even in an iterated game or a game with imperfect information about previous actions, there is still the notion of a "strategy". Each player picks a strategy, and then you play out the game and see what valuations result. So I think this still fits into @urkud's framework.

Any game with multiple states, imperfect information etc can be represented as a Game in the sense of above definition (i.e., you can have structures describing a specific type of a game, then have toGame function). I don't know whether it should be called Game or NormalFormGame. However, I'm sure that definitions that can be given in this generality, should be given in this generality.

I am a bit short of time. @urkud I looked at your definitions and I can see that the definitions could be generalised like this. But it is hard to be certain that this generality is convenient and covers everything, since the field is vast and studied by different departments. Changing it later can be a headache because all theorems would have to be fixed. Therefore, I request that the PR include good instantiations of different kinds of games and auctions before it is accepted. In other words, I think the definitions need to be battle-tested first.

Since I don't have the time to do this, I recommend the following highly regarded books, one from Econ people and one from TCS people:

1. From the econ side, there is Ariel Rubinstein and Martin Osborne's book
2. From the CS side, the book by Noam Nisan et al on Algorithmic Game Theory

The AGT book (2) is more extensive and treats combinatorial auctions in Chapter 11

Given that other parts of the library will probably never depend on this, I suggest that we create a new repository instead of pushing it to Mathlib right away. I can create leanprover-community/GameTheory this weekend, then push some basic theory there. @hcWang942 What do you think about this? This will make it easier to experiment with API and add results without going through Mathlib review process.

Of course, "pure math" results that are useful for game theory/auction theory (e.g., Brouwer fixed-point theorem) should go to Mathlib.

Given that other parts of the library will probably never depend on this, I suggest that we create a new repository instead of pushing it to Mathlib right away. I can create leanprover-community/GameTheory this weekend, then push some basic theory there. @hcWang942 What do you think about this? This will make it easier to experiment with API and add results without going through Mathlib review process.

Of course, "pure math" results that are useful for game theory/auction theory (e.g., Brouwer fixed-point theorem) should go to Mathlib.

I like this idea. If @hcWang942 agrees, my fair division PR could also go to this new repository.

Given that other parts of the library will probably never depend on this, I suggest that we create a new repository instead of pushing it to Mathlib right away. I can create leanprover-community/GameTheory this weekend, then push some basic theory there. @hcWang942 What do you think about this? This will make it easier to experiment with API and add results without going through Mathlib review process.

Of course, "pure math" results that are useful for game theory/auction theory (e.g., Brouwer fixed-point theorem) should go to Mathlib.

I agree, creating a new repo to store the theorems is not a bad idea. As you mentioned, other parts of the Mathlib probably won't depend on this, at least in the near future. However, we still hope to create relevant dependencies within the repository. Our team recently recruited five new undergraduates to focus their Final Year Project on GameTheory, and we will continue to work on this in the near future.

I believe that many theories in GameTheory are very helpful for Mechanism Design, and as Pure Math continues to expand in the Mathlib library, I think further improving more Applied areas will be a good direction. I believe it will also have good application prospects, although this will only be effective after we have formalized enough content. The development of Lean has been notably neglected by economists. Our project aims to bridge this gap.

Given that other parts of the library will probably never depend on this, I suggest that we create a new repository instead of pushing it to Mathlib right away. I can create leanprover-community/GameTheory this weekend, then push some basic theory there. @hcWang942 What do you think about this? This will make it easier to experiment with API and add results without going through Mathlib review process.
Of course, "pure math" results that are useful for game theory/auction theory (e.g., Brouwer fixed-point theorem) should go to Mathlib.

I like this idea. If @hcWang942 agrees, my fair division PR could also go to this new repository.

Sure! It's great to see that we can make GameTheory more complete and better! @Shreyas4991

By the way, one more question is do I need to fix the entire structure before the maintainer adds it to the new repo?

Moreover, may I have the maintaining rights to the new GameTheory repo? This would make it easier for me and my team to contribute to the entire repo. I can also help reviewing the new PRs to the repo. Thx @urkud

Let's discuss the editorial policy of the new repo early next week. I'm busy at my day job right now.

Well I am actually agree that creating a separate repository for GameTheory in LeanCommunity is a good proposal.

One reason mentioned by Yael is that the content of Gametheory is not 'abstract' enough, also we need the flexibility for experimentation and iteration as we formalize different areas of game theory, we can avoids prematurely generalizing or abstracting concepts before we have a good understanding of how they will be used across different game theoretic models. Furthermore, it allows us to develop and refine these formalizations independently, while still enrich mathlib's core libraries.

We can always revisit incorporating parts into mathlib later if generally useful abstractions emerge. For now, a repo gives us the freedom to focus on formalizing game theory concepts. I appreciate the suggestions to improve integration with mathlib, but I think the separate repo approach strikes a good balance between mathlib and developing specialized game theory formalizations.

I think if @Shreyas4991 agree we may contribute the Gametheory repo together. And the standard might be slightly off a little bit. For instance, only pass the lint and CI? I am not so sure about this standard, maintainer might have a more expertise suggestion on it.

For the plan, we still exploring to do more things in mechanism design and auctions in game theory.

One key theorem we could focus on is the affiliated signal version of Myerson's revenue equivalence theorem, proven by Paul Klemperer and his collaborators in 1989. This theorem, which essentially shows how bidders' mutual influence can drive up prices, is a good example of monotone comparative analysis, an area of particular interest to many theoretical economists.

Regarding equilibrium refinement, Selten's trembling hand equilibrium is a widely used method for eliminating equilibria in complete information settings. This concept, which earned Selten a Nobel Prize, aims to remove less ‘plausible’ Nash equilibria by considering the stability of equilibria under small mistakes by players. In incomplete information settings, we might look at refining perfect Bayesian Nash equilibria using the incentive compatible condition proposed by Milgrom and Weber.

Using Lean for these proofs could be particularly valuable. It could ensure that we don't overlook any possibilities when solving for equilibria and performing equilibrium deletion. This rigorous proof process could also provide insights for designing experiments to validate how these mechanisms operate in practice.

The logic behind Myerson's equivalence theorem might follow a similar approach:

• Identify the equilibrium sets for mechanisms A and B
• Refine these equilibria
• Compare the allocations and revenues at the refined equilibrium points

Formalizing these processes with Lean could allow us to avoid relying on specific parameter values, potentially leading to more general and convincing results. The challenge lies in clearly describing these problems within Lean's framework.

This approach could be particularly powerful for comparing mechanisms. For instance, to show that mechanism A is at least as good as mechanism B, we could use Lean to systematically work through the steps of finding equilibria, refining them, and comparing outcomes. This could provide a more comprehensive and reliable analysis than traditional methods that often rely on specific numerical examples.

The main challenge will likely be in translating these game-theoretic concepts and processes into Lean's formal language. However, once accomplished, this could open up new possibilities for automated checking and verification of game-theoretic results.

To date, we have contacted two economists in Singapore to help us confirm the applicability and feasibility of our theoretical approach. We are also actively advancing our project with the aim of 'selling' our ideas to a broader group of economists once we have made further progress. This might presents a good opportunity to show to the economics of the potential of formalization methods in economic theory research.

It looks like this PR is not ready for merging and might soon to be made redundant by the creation of a new game theory repo. Tagging awaiting-author for now. Feel free to remove it if I misunderstood!